Coarse abstractions make Zeno behaviours difficult to detect (Extended abstract) - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Logical Methods in Computer Science Année : 2013

Coarse abstractions make Zeno behaviours difficult to detect (Extended abstract)

Résumé

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.

Dates et versions

hal-00829829 , version 1 (03-06-2013)

Identifiants

Citer

Frédéric Herbreteau, B. Srivathsan. Coarse abstractions make Zeno behaviours difficult to detect (Extended abstract). Logical Methods in Computer Science, 2013, Selected Papers of the "22nd International Conference on Concurrency Theory" CONCUR 2011, 9 (1). ⟨hal-00829829⟩

Collections

CNRS ANR
57 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More