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

- Relatore
- Alberto Casagrande - Dipartimento di Matematica e Informatica (Università di Udine)
- Data e ora
- martedì 7 novembre 2006 alle ore 17.30 - caffè, tè & C. ore 17.00
- Luogo
- Ca' Vignal 3 - Piramide, Piano 0, Sala Verde
- Referente
- Tiziano Villa
- Referente esterno
- Data pubblicazione
- 20 ottobre 2006
- Dipartimento

## Riassunto

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.

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.