Solving two supervisory control benchmark problems using Supremica

Two supervisory control benchmark problems for WODESpsila08 are solved using the tool Supremica. Supremica is a tool for formal synthesis of discrete-event control functions based on discrete event models of the uncontrolled plant and specifications of the desired closed-loop behavior. By using formal synthesis of control functions the need for formal verification is reduced since the control functions are computed to automatically fulfill the given specifications, that is, they are ldquocorrect by constructionrdquo. The modeling framework in Supremica is based on finite automata. Supremica implements several techniques for being able to solve large scale problems. In this paper it is evaluated how the algorithms implemented in Supremica that are based on binary decision diagrams performs on the two benchmark problems. The two benchmark problems are generalization of two classical problems; cat and mouse, and the dining philosopherspsila problem. The benchmark problems are parameterized such that it is possible to create problem instances with huge state-spaces. The benchmark shows that supremica can efficiently solve rather large problem instances.