Algebraic synthesis and verification of discrete supervisory controllers for forbidden path specifications

The method for formal synthesis of discrete supervisory controllers presented here is based on an automaton model of the plant which describes its uncontrolled behavior and a specification of states or state sequences (paths) of the plant which must be prevented by the controller. The model of the plant and the description of the specification are combined in one homogeneous Boolean equation, the so-called Lagrangean equation. Forbidden path problems can be solved by expanding the Lagrangean equation. A nondeterministic sequential state feedback controller can be synthesized by means of a standard structure and by studying the solution sets of the expanded Lagrangean equation