logo Région Lorraine

Meeting detail

Second meeting -- 12-13 June 2014 -- Loria, Nancy


Haniel Barbosa, Martin Bromberger, David Déharbe, Federico Dobal, Pascal Fontaine, Marek Košta, Stephan Merz, Thomas Sturm.

Invited: Erika Abraham, Florian Corzilius, Gereon Kremer


Tuesday, May 6

09:30-10:30 : introducing participants
10:30-12:00 : models for Virtual Substitution
14:00-15:00 : open seminar: Reachability Analysis of Hybrid Systems, Erika Abraham
15:00-17:00 : technical discussions (linear techniques)

Dinner in Nancy

Wednesday, May 7

09:00-11:00 : technical discussions (non-linear techniques)
11:00-12:00 : Prospective discussion
14:00-17:00 : technical discussions (improving simplex)

Reachability Analysis of Hybrid Systems (abstract)

Hybrid systems exhibit both dynamic and discrete behavior. Typically, the dynamic behavior stems from the continuous evolution of physical systems, whereas the discrete behavior stems from the execution steps of discrete controllers. As a modeling language we consider hybrid automata, extending discrete automata with continuous dynamics. Given a hybrid automaton model of a hybrid system, the perhaps most basic question one could be interested in is whether certain model states can be reached from a given initial state. Though this reachability problem sounds simple, it is undecidable for all but some very simple subclasses of hybrid automata. Nevertheless, there are different techniques to solve it in an incomplete manner. We discuss methods that use different geometric objects like polytopes, zonotopes, ellipsoids etc. to represent state sets, and apply a forward fixedpoint-based search to over-approximate the set of reachable states. Such methods need to determine successor sets under both discrete jumps and continuous evolution. The latter is often done by flowpipe construction, paving the whole flow by a set of geometric objects of the chosen type.