Efficient Emptiness Check for Timed Büchi Automata (Extended version)

Abstract : The Büchi non-emptiness problem for timed automata refers to 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, it is shown that this simple transformation may sometimes result in an exponential blowup. A construction avoiding this blowup is proposed. It is also shown that in many cases, non-Zenoness can be ascertained without extra construction. An on-the-fly algorithm for the non-emptiness problem, using non-Zenoness construction only when required, is proposed. Experiments carried out with a prototype implementation of the algorithm are reported.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2012, Special issue on Computer Aided Verification (CAV'10), 40 (2), pp.122-146. 〈10.1007/s10703-011-0133-1〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00584849
Contributeur : Frédéric Herbreteau <>
Soumis le : lundi 11 avril 2011 - 09:26:09
Dernière modification le : jeudi 11 janvier 2018 - 06:20:17

Identifiants

Collections

Citation

Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz. Efficient Emptiness Check for Timed Büchi Automata (Extended version). Formal Methods in System Design, Springer Verlag, 2012, Special issue on Computer Aided Verification (CAV'10), 40 (2), pp.122-146. 〈10.1007/s10703-011-0133-1〉. 〈inria-00584849〉

Partager

Métriques

Consultations de la notice

44