Coarse abstractions make Zeno behaviours difficult to detect

Abstract : An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find runs that are non-Zeno. Over the years important improvements have been obtained in checking reachability properties for timed automata. We show that some of these very efficient optimizations make testing for Zeno runs costly. In particular we show NP-completeness for the LU-extrapolation of Behrmann et al. We analyze the source of this complexity in detail and give general conditions on extrapolation operators that guarantee a (low) polynomial complexity of Zenoness checking. We propose a slight weakening of the LU-extrapolation that satisfies these conditions.
Type de document :
Communication dans un congrès
Joost-Pieter Katoen and Barbara König. CONCUR - 22nd International Conference on Concurrency Theory - 2011, Sep 2011, Aachen, Germany. Springer, 6901, pp.92-107, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-23217-6_7〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00599553
Contributeur : Frédéric Herbreteau <>
Soumis le : vendredi 10 juin 2011 - 09:45:30
Dernière modification le : jeudi 11 janvier 2018 - 06:20:17

Lien texte intégral

Identifiants

Collections

Citation

Frédéric Herbreteau, B. Srivathsan. Coarse abstractions make Zeno behaviours difficult to detect. Joost-Pieter Katoen and Barbara König. CONCUR - 22nd International Conference on Concurrency Theory - 2011, Sep 2011, Aachen, Germany. Springer, 6901, pp.92-107, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-23217-6_7〉. 〈inria-00599553〉

Partager

Métriques

Consultations de la notice

30