Logics for Hybrid Systems

Abstract

Hybrid systems air he/erogenous dynamical systems cliaracterized by interacting continuous and discrete dynamics. Such mathematical mode's have proved fruitful in a great d:ersiry of engineering applications. Including air-traffic control, automated manufacturing, and cliemical process control. The high-profile and safely-critical nature of the application areas /'.as fostered a large and growing body of work on formal methods for hybrid systems: mathematical logics, computational models and methods, and computer-aided reasoning tools supporting the formal specification and verification of performance requirements for hybrid systems, and the design and synthesis of control programs for hybrid systems that are provably correct with respect to formal specifications. This paper offers a synthetic overview of, am! original contributions to, the use of logics and formal methods in the analysis of hybrid systems. Keywords-Automata, computer-aided analysis, computer-aided software engineering, design automation, formal languages, hybrid control systems, logic, software verification, temporal logic.