Symbolic Synthesis and Verification of Hierarchical Interface-based Supervisory Control

Abstract

<p>Hierarchical Interface-based Supervisory Control (HISC) is a method to alleviate the state-explosion problem when verifying the controllable and nonblocking properties of a large discrete event system. By decomposing a system as a number of subsystems according to the HISC method, we can verify the subsystems separately and the global system controllability and nonblocking property are guaranteed, so that potentially great computation effort is saved.</p> <p>In this thesis, we first present a predicate-based synthesis algorithm for each type of subsystem and then prove the correctness of the algorithms. Then a predicatebased verification algorithm for each type of subsystem is provided. Based on the predicate-based algorithms, a symbolic implementation is proposed by using Binary Decision Diagrams (BDD) and the fact that a subsystem is usually composed of a number of components. With the symbolic implementation, we can handle a much larger subsystem of each type.</p> <p>Two large and complicated examples (with estimated worst-case state space on the order of 1030) extended from the AlP example are provided for demonstrating the capabilities of the algorithms and the implementation. A software tool for the synthesis and verification using our approach is also developed.</p>