Algorithmic Verification and Synthesis of Hybrid Control Systems

University Of Notre Dame, Notre Dame IN

Investigators

Abstract

A supervisory hybrid system is a system generating a mixture of discrete-valued and continuous-valued signals. Such systems arise when computers supervise or control complex dynamical plants. In recent years, there has been significant interest in the use of algorithmic methods for the verification and synthesis of hybrid control systems. Algorithmic methods use algorithms whose successful execution provide necessary and sufficient conditions on the system's ability to satisfy a desired behavior. Symbolic model checking for hybrid automata represent a well-known algorithmic approach to hybrid system verification. Hybrid system model checking, unfortunately, has been shown to be undecidable for many classes of hybrid systems and this negative result has greatly limited the practical potential of algorithmic methods in analyzing and synthesizing hybrid control systems. This project proposes a paradigm shift in which we use algorithmic methods to verify the existence of 'controlled' hybrid systems satisfying desired behaviors. This approach to verification is decidable for a large class of practical systems and therefore provides a breakthrough making possible the development of algorithmic methods that provide a practical means for the verification and synthesis of hybrid control systems.