Using Modal Logics for the Formal Analysis and Synthesis of Hybrid Control Systems
Jennifer M. Davoren · 2000
: The purpose of this paper is two-fold. We first give an overview of recent work on the formal analysis and verification of hybrid systems, which are dynamical systems with both discrete and continuous changes of state. We then present new work on the use of poly-modal logics in the systematic synthesis of hybrid control systems direct from formal specifications. 1 1 Introduction The multi-disciplinary research field of hybrid systems has emerged over the last decade and lies at the interface of computer science, control engineering and applied mathematics. A hybrid dynamical system is one whose state may either evolve continuously for some duration of time according to one set of di#erential equations, or it may be abruptly reset to a new value from which evolution is governed by another set of di#erential equations, with the switches typically triggered by the occurrence of some discrete event. The hybrid phenomena captured by such mathematical models is manifested in a great div...