@article {Tomlin2003Computational-t,
title = {Computational techniques for the verification of hybrid systems},
journal = {Proceedings of the IEEE},
volume = {91},
number = {7},
year = {2003},
month = {jul.},
pages = {986 - 1001},
abstract = {Hybrid system theory lies at the intersection of the fields of engineering control theory and computer science verification. It is defined as the modeling, analysis, and control of systems that involve the interaction of both discrete state systems, represented by finite automata, and continuous state dynamics, represented by differential equations. The embedded autopilot of a modern commercial jet is a prime example of a hybrid system: the autopilot modes correspond to the application of different control laws, and the logic of mode switching is determined by the continuous state dynamics of the aircraft, as well as through interaction with the pilot. To understand the behavior of hybrid systems, to simulate, and to control these systems, theoretical advances, analyses, and numerical tools are needed. In this paper, we first present a general model for a hybrid system along with an overview of methods for verifying continuous and hybrid systems. We describe a particular verification technique for hybrid systems, based on two-person zero-sum game theory for automata and continuous dynamical systems. We then outline a numerical implementation of this technique using level set methods, and we demonstrate its use in the design and analysis of aircraft collision avoidance protocols and in verification of autopilot logic.},
keywords = {aircraft collision avoidance protocols, aircraft control, automata, automata theory, autopilot logic, collision avoidance, computer science verification, continuous dynamical systems, control theory, discrete state systems, formal verification, game theory, hybrid system theory, hybrid systems, reachability, reachability analysis, system theory, two-person zero-sum game, verification},
issn = {0018-9219},
doi = {10.1109/JPROC.2003.814621},
url = {http://dx.doi.org/10.1109/JPROC.2003.814621},
author = {Tomlin, C.J. and Mitchell, I. and Bayen, A.M. and Oishi, M.}
}