Quotient-based control synthesis for partially observed non-deterministic plants with mu-calculus specifications

We study the control of a nondeterministic plant subject to a specification expressed in the prepositional
mu
- calculus under a partial observability of events. We define a function to quotient the specification against the plant resulting in a "quotiented formula" with the property that a supervisor enforcing the desired specification exists if and only if the quotiented formula is satisfiable, and a model witnessing the satisfiability can be used as a supervisor. The quotiented formula belongs to an extended
mu
-calculus, which we call
O
-
mu
-calculus, where the extension is needed to express the observability constraint that cannot be expressed in the logic of
mu
-calculus. We present the syntax and semantics of
O
-
mu
-calculus and present a tableau-based satisfiability solving algorithm that also discovers a model for the quotiented formula when one exists.