On tractable instances of modular supervisory control

An instance of a modular supervisory control problem involves a plant automaton, described either as a monolithic, finite-state automaton (SUP1M), or as the synchronous product of several finite-state automata (SUPMM), along with a set of finite state, specification automata on a common alphabet. The marked language of the synchronous product of these automata represents the desired specification. A supervisory policy that solves the instance selectively disables certain events, based on the past history of event-occurrences, such that the marked behavior of the supervised system is a non-empty subset of the desired specification. Testing the existence of a supervisory policy for a variety of instances of modular supervisory control is PSPACE-complete [1]. This problem remains intractable even when the plant is a monolithic finite state automaton and the specification automata are restricted to have only two states with a specific structure [2]. We refer to this intractable class as SUP1Ω in this paper. After introducing complement sets for events in a plant automaton, we identify a subclass of SUP1Ω that can be solved in polynomial time. Using this class as the base, inspired by a family of subclasses of SAT(cf. section 4.2, [3]) that can be solved in polynomial time [4], we develop a family of subclasses of SUP1Ω that can be solved in polynomial time. The results of this paper are also used to identify a polynomial time hierarchy for certain intractable subclasses of SUPMM identified in this paper.