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.