Skip to Main content Skip to Navigation
Conference papers

Efficient On-The-Fly Emptiness Check for Timed Büchi Automata

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 solution to this problem amounts to searching for a cycle in the so-called zone graph of the automaton. Since non-Zenoness cannot be verified directly from the zone graph, additional constructions are required. In this paper, it is shown that in many cases, non-Zenoness can be ascertained without extra constructions. An on-the-fly algorithm for the non-emptiness problem, using an efficient non-Zenoness construction only when required, is proposed. Experiments carried out with a prototype implementation of the algorithm are reported and the results are seen to be promising.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Frédéric Herbreteau Connect in order to contact the contributor
Submitted on : Wednesday, June 30, 2010 - 2:22:10 PM
Last modification on : Saturday, June 25, 2022 - 10:32:02 AM
Long-term archiving on: : Tuesday, October 23, 2012 - 9:40:37 AM


Files produced by the author(s)




Frédéric Herbreteau, B. Srivathsan. Efficient On-The-Fly Emptiness Check for Timed Büchi Automata. ATVA - 8th International Symposium on Automated Technology for Verification and Analysis - 2010, Sep 2010, Singapore, Singapore. pp.218-232, ⟨10.1007/978-3-642-15643-4_17⟩. ⟨inria-00496366⟩



Record views


Files downloads