
Evènement pour le groupe Modélisation et Verification
Date  20130110 11:3012:30 
Titre  Timebounded reachability for monotonic hybrid automata 
Résumé 
Hybrid automata (HA) form a very popular class of model for describing hybrid systems, i.e. systems that exhibit both discrete and continuous behaviors. An HA is roughly speaking a finite automaton augmented with a finite set of realvalued variables, whose values evolve continuously with time elapsing. The rate of growth of those variables can change along time and depends on the current location of the automaton. Unfortunately, HA are notoriously hard to analyse: even the reachability problem is undecidable on the very restricted subclass of stopwatch automata (where variables can have rates 0 or 1 only).
However, most of the undecidability results on HA rely on the unboundedness of time to encode runs of undecidable models such as twocounter machines. A natural question is thus to study the timebounded variant of the verification problems on HA, hoping that this additional requirement will allow to recover decidability. A further incentive is the recent line of research by Ouaknine, Worrell, et al., who have shown the benefits of considering timebounded variants of classical problems in the case of (alternating) timed automata.
In this talk, we study the timebounded reachability problem for monotonic rectangular hybrid automata (MRHA). An MRHA is a rectangular hybrid automata where the rate of each clock is either alway nonnegative, or always nonpositive. We show that this problem is decidable (even though the unbounded reachability problem for even very simple classes of hybrid automata is wellknown to be undecidable), and give a precise characterisation of its complexity: it is NExpTimec. We also show that extending this class by either allowing a clock to have positive and negative rates in the same HA, or by allowing diagonal guards, leads to undecidability, even in bounded time. Finally, we present a more practical extension of our positive result, by showing that we can effectively compute fixpoints characterising the sets of states that are reachable (resp. coreachable) within T time units from a given state.
This is joint work with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, JeanFrançois Raskin and James Worrell. 
Lieu  076 
Orateur  Gilles Geeraerts 
Email  gilles.geeraerts@ulb.ac.be 
Url  ULB, Belgium 
Aucun document lié à cet événement. RetourRetour à l'index
 