Abstract
The Büchi non-emptiness problem for timed automata concerns deciding if a given automaton has 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 the non-Zenoness. In this paper, we show that this simple transformation may sometimes result in an exponential blowup. We propose a method avoiding this blowup. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Herbreteau, F., Srivathsan, B., & Walukiewicz, I. (2010). Efficient emptiness check for timed Büchi automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6174 LNCS, pp. 148–161). https://doi.org/10.1007/978-3-642-14295-6_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
