Zone-based verification of timed automata revisited


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