The synthesis of controllers for discrete event systems, as introduced by Ramadge and Wonham, amounts to computing winning strategies in parity games. We show that in this framework it is possible to extend the speciÿcations of the supervised systems as well as the constraints on the controllers by expressing them in the modal -calculus.
In order to express unobservability constraints, we propose an extension of the modalcalculus in which one can specify whether an edge of a graph is a loop. This extended -calculus still has the interesting properties of the classical one. In particular it is equivalent to automata with loop testing. The problems such as emptiness testing and elimination of alternation are solvable for such automata.
The method proposed in this paper to solve a control problem consists in transforming this problem into a problem of satisÿability of a -calculus formula so that the set of models of this formula is exactly the set of controllers that solve the problem. This transformation relies on a simple construction of the quotient of automata with loop testing by a deterministic transition system. This is enough to deal with centralized control problems. The solution of decentralized control problems uses a more involved construction of the quotient of two automata.
This work extends the framework of Ramadge and Wonham in two directions. We consider inÿnite behaviours and arbitrary regular speciÿcations, while the standard framework deals only with speciÿcations on the set of ÿnite paths of processes. We also allow dynamic changes of the sets of observable and controllable events.