An Introduction to Hybrid Automata

Hybrid systems are digital real-time systems embedded in analog environments. A paradigmatic example of a hybrid system is a digital embedded control program for an analog plant environment, like a furnace or an airplane: the controller state moves discretely between control modes, and in each control mode, the plant state evolves continuously according to physical laws. Those systems combine discrete and continuous dynamics. Those aspects have been studied in computer science and in control theory. Computer scientists have introduced

hybrid automata

[28], a formal model that combines discrete control graphs, usually called

finite state automata

, with continuously evolving variables. A hybrid automaton exhibits two kinds of state changes:

discrete jump transitions

occur instantaneously, and

continuous flow transitions

occur when time elapses.

This chapter is organized as follows. First, we introduce the

syntax

and

semantics

of hybrid automata, and show how complex hybrid systems can be modeled

compositionally

as

products of

hybrid automata. Then, we define

safety properties

of hybrid automata and show how to model them using

monitors

. We show that the

verification

of those properties reduces naturally to reachability problems, that is, to decide if there exists a trajectory of the hybrid system that reaches a given set of states. As hybrid automata can be very complex mathematical objects, restricted subclasses for which we have

automatic analysis methods

have been introduced. In this introduction, we focus on

rectangular hybrid automata

and show how they can be used to

overapproximate

the behavior of more complex hybrid automata. We close the chapter by referencing the literature to allow the reader into go deeper into this flourishing research subject.