B. Srivathsan (Labri Bordeaux, F)
|Title||Zone-based verification of timed automata revisited|
|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
- Subscribe to the ics feed.
- No Events