Speaker |
B. Srivathsan (Labri Bordeaux, F) |
Title | Zone-based verification of timed automata revisited |
When | 29.02.2012, 10:00 |
Where | Room 5056 (!) |
Abstract | We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are approximations of so-called zones. For effectiveness, the approximations are parametrized by the maximal lower and upper bounds (LU-bounds) occuring in the guards of the automaton. For reasons of efficiency, only convex approximations have been implemented in tools.
We provide an efficient technique to incorporate a non-convex approximation that subsumes existing convex ones. Moreover, we show that this approximation is the biggest approximation with respect to LU-bounds that is sound and complete for reachability. The structure of our new algorithm also permits to calculate LU-bounds on-the-fly during exploration, yielding further improvement. In the second part of the talk, we consider the Büchi emptiness problem: does the automaton have an infinite non-Zeno run satisfying he Büchi accepting condition? The standard solution to this problem involves adding an auxiliary clock to take care of non-Zenoness. We show that this simple transformation may sometimes result in an exponential blowup. We propose a method avoiding this blowup for a wide class of approximations. For the other approximations, we show that this blowup is unavoidable. Joint work with Frédéric Herbreteau, Dileep Kini and Igor Walukiewicz |
Slides | download |
Event calendar
- Subscribe to the ics feed.
Upcoming Events
- No Events