Symbolic reachability computation using the disjunctive partitioning technique in Supervisory Control Theory

Supervisory Control Theory (SCT) is a model based framework for automatically synthesizing a supervisor that minimally restricts the behavior of a plant such that a given specification is fulfilled. A problem, which prevents SCT from having a major breakthrough industrially, is that the supervisory synthesis often suffers from the state-space explosion problem. To alleviate this problem, a well-known strategy is to represent and explore the state-space symbolically by using Binary Decision Diagrams. Based on this principle, an efficient symbolic state-space traversal approach, depending on the disjunctive partitioning technique, is presented and the correctness of it is proved. Finally, the efficiency of the presented approach is demonstrated on a set of benchmark examples.