Quotient-based control synthesis for partially observed non-deterministic plants with mu-calculus specifications
Samik Basu, Ratnesh Kumar · 2007
We study the control of a nondeterministic plant subject to a specification expressed in the prepositionalmu- 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 extendedmu-calculus, which we callO-mu-calculus, where the extension is needed to express the observability constraint that cannot be expressed in the logic ofmu-calculus. We present the syntax and semantics ofO-mu-calculus and present a tableau-based satisfiability solving algorithm that also discovers a model for the quotiented formula when one exists.