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.
Type de document :
Communication dans un congrès
Ahmed Bouajjani and Wei-Ngan Chin. ATVA - 8th International Symposium on Automated Technology for Verification and Analysis - 2010, Sep 2010, Singapore, Singapore. Springer, 6252, pp.218-232, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-15643-4_17〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00496366
Contributeur : Frédéric Herbreteau <>
Soumis le : mercredi 30 juin 2010 - 14:22:10
Dernière modification le : jeudi 11 janvier 2018 - 06:20:17
Document(s) archivé(s) le : mardi 23 octobre 2012 - 09:40:37

Fichier

atva2010-full.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Frédéric Herbreteau, B. Srivathsan. Efficient On-The-Fly Emptiness Check for Timed Büchi Automata. Ahmed Bouajjani and Wei-Ngan Chin. ATVA - 8th International Symposium on Automated Technology for Verification and Analysis - 2010, Sep 2010, Singapore, Singapore. Springer, 6252, pp.218-232, 2010, Lecture Notes in Computer Science. 〈10.1007/978-3-642-15643-4_17〉. 〈inria-00496366〉

Partager

Métriques

Consultations de la notice

192

Téléchargements de fichiers

136