Evènement pour le groupe Modélisation et Verification
|Date|| 2013-01-10 11:30-12:30|
|Titre||Time-bounded reachability for monotonic hybrid automata |
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 real-valued 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 two-counter machines. A natural question is thus to study the time-bounded 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 time-bounded variants of classical problems in the case of (alternating) timed automata.
In this talk, we study the time-bounded reachability problem for monotonic rectangular hybrid automata (MRHA). An MRHA is a rectangular hybrid automata where the rate of each clock is either alway non-negative, or always non-positive. We show that this problem is decidable (even though the unbounded reachability problem for even very simple classes of hybrid automata is well-known to be undecidable), and give a precise characterisation of its complexity: it is NExpTime-c. 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. co-reachable) within T time units from a given state.
This is joint work with Thomas Brihaye, Laurent Doyen, Joël Ouaknine, Jean-François Raskin and James Worrell. |
|Orateur||Gilles Geeraerts |
|Url||ULB, Belgium |
Aucun document lié à cet événement.RetourRetour à l'index