Games for synthesis of controllers with partial observation

The synthesis of controllers for discrete event systems, as intro-duced by Ramadge and Wonham, amounts to computing winning strate-gies in parity games. We show that in this framework it is possible to extend the specifications of the supervised systems as well as the con-straints on the controllers by expressing them in the modal µ-calculus. In order to express unobservability constraints, we propose an ex-tension of the modal µ-calculus in which one can specify whether an edge of a graph is a loop. This extended µ-calculus still has the inter-esting 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 con-sists in transforming this problem into a problem of satisfiability 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 re-lies 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 con-trol 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 infinite behaviours and arbitrary regular spec-ifications, while the standard framework deals only with specifications on the set of finite paths of processes. We also allow dynamic changes of the set of observable and controllable events