Supervisory control using satisfiability solvers

This paper discusses how satisfiability solvers may be used to verify and synthesize discrete event supervisors as defined in the supervisory control theory. By using the supervisory control theory it is possible to generate control functions that are correct by construction. However, the computations for verification and synthesis of the supervisors are NP-complete and in order to make the method applicable for industrial use it is necessary to use algorithms and tools that could solve problems of industrial size. Within the model checking community satisfiability solvers have become an important tool for verification of large hardware circuits. In this paper it is shown how to formulate some problems in the supervisory control theory as Boolean satisfiability problems. Formulations of satisfiability problems for synthesizing a path to a marked state, verification of controllability and verification of deadlock presence are presented. The method is evaluated on some examples of high complexity.