Oded Maler,
Algorithmic Verification of Continuous and Hybrid Systems: Past, Present, Future
Hybrid systems combine the qualitative discrete dynamics of transition systems with continuous dynamics as expressed by ordinary differential equations. They can be viewed either as continuous systems augmented with mode switching and if-then-else rules or as automata where in addition to the transition dynamics, there are real-valued variables that evolve while the automaton is idling inside a state. Analyzing the behavior of such systems is notoriously difficult. From the discrete verification standpoint we go out of the finite-state setting and have to deal with infinite-valued variables (and dense time). On the other hand, discontinuous mode switching often breaks down the analytical toolbox available for continuous systems, especially for linear systems.
In the first part of the talk I will talk about early work of the verification community on hybrid systems. This work can be characterized by:
- The systems under study had a very simple (almost trivial) continuous dynamics in every state. Their simulation and analysis did not really require solving differential equations;
- The question posed consisted of exact verification/reachability decision problems and a precise yes/no answers were sought.
I will present my own work on the topic that have shown that for a certain variant of these systems reachability can be decided in dimension 2 (two state variables) but not in higher dimensions.
In the second part of the talk I will illustrate contemporary algorithms which:
- Can be applied to piecewise-affine dynamical systems, that is, hybrid automata such that the dynamics in each mode defined by a real linear differential equation;
- Compute an over-approximation of the set of reachable states whose over-approximation error can be controlled.
These algorithms are implemented in the SpaceEx tool and can verify quite large systems.
I will conclude with ongoing work on handling nonlinear systems and on moving closer to the only method currently used in practice, namely simulation. I will speculate about what is still missing in order to make this technology usable in practice.