Quotient-based Control Synthesis for Non-Deterministic Plants with Mu-Calculus Specifications

We study the control of a nondeterministic discrete event system (DES) subject to a control specification expressed in the propositional mu-calculus, under complete observation of events. Given a plant automaton model and a mu-calculus specification we provide a set of rules that computes the "quotient" of the specification against the plant, which is another mu-calculus formula such that a supervisor exists if and only if the quotiented formula is satisfiable. Thus the control problem is reduced to one of mu-calculus satisfiability. We also present a tableau-based satisfiability solving algorithm that identifies a model for the quotiented formula. The resulting model serves as a supervisor. The complexity of supervisor existence verification as well as model synthesis is single exponential in the size of the plant as well as the size of the specification formula