18.1.   INTRODUCTION

For about the past 10 years, researchers in the traditionally distinct fields of
control theory and computer science verification have proposed models,
along with verification and controller synthesis techniques for complex, safety
critical systems. The area of hybrid systems theory studies systems that involve
the interaction of discrete event and continuous-time dynamics, and it provides
an effective modeling framework for complex continuous systems with
large numbers of operating modes. Examples include continuous systems
controlled by a discrete logic such as the autopilot modes for controlling an
aircraft, systems of many interacting processes such as air or ground transportation
systems in which discrete dynamics are used to model the coordination
protocols among processes, or continuous systems that have a phased
operation, such as biological cell growth and division.

The current and potential impact of hybrid systems lies in the confluence
of computational methods from control theory and from formal methods in
computer science verification. In the examples mentioned above, the system
dynamics are complex enough that traditional analysis and control methods
based solely on differential equations are not computationally feasible; analysis
based solely on discrete event dynamics ignores critical system behavior.
Our interest lies in developing computational tools for analyzing and controlling
the behavior of hybrid systems; our eventual goal is to develop a realtime
tool to provide online verification that a hybrid system satisfies its
specified behavior. This goal addresses one of the central themes of software-
enabled control, in which we seek a systematic methodology for the design,
validation, and implementation of control software.

In our work to date, the system specification that we are most interested
in is that of system safety, which asks the question, Is a potentially unsafe
configuration of the system reachable from an initial configuration? More
important for control theory, given a set of desired configurations, it is crucial
to be able to design the hybrid system control inputs to achieve these
configurations. Previous work in this area had focused on hybrid systems with
very simple continuous dynamic equations (such as clocks, or linear decou-
pled systems). Our research has three components: the problem formulation
for computing exact reachablesets of hybrid systems and the design of a
software tool to perform such calculations; the development of an algorithm
for computing overapproximations of reachable sets which works efficiently
in high dimensions; and the design of a real-time aircraft testbed for these
algorithms. We will focus on the first component in this chapter and briefly
outline our work on the second.