Seminar 28 Feb, 2012
Zone-based verification of timed automata revisited
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 the 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
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 the 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
