Hybrid Automata: Introduction, First-Order Approach, and Approximation Techniques

Systems having a mixed discrete-continuous evolution are called hybrid systems. Since hybrid systems cannot be studied by either dynamical system techniques or finite state system approaches only, specific formal tools, hybrid automata, were introduced to model them.
Intuitively, a hybrid automaton is a ``finite-state'' automaton with continuous variables which evolve according to a set of continuous laws. Such automata have been widely used to demonstrate the validity of hybrid system properties and, even if it is proved that many simple verification problems,
such as reachability, are not in general decidable over them, various model checking techniques have been proposed in the literature.
After a brief introduction, this talk will present both theoretical and computational approaches to model checking of hybrid automata.
For the theoretical based approach, we relate first-order theories and analytical results on multi-valued maps and we reduce the bounded reachability problem for hybrid
automata whose continuous laws are expressed by inclusions to a decidability problem for first-order
formulae over the reals. Then, we present two classes of hybrid automata for which the reachability problem can be decided.
For the approximation based approach, we introduce a new software package, called Ariadne, for the verification of hybrid automaton properties and we show that, since it relies on a rigorous computable
analysis framework to represent geometric objects, it is capable to achieve provable approximation bounds along the computation.