Herbreteau, Frédéric and Srivathsan, B - Coarse abstractions make Zeno behaviours difficult to detect

lmcs:882 - Logical Methods in Computer Science, February 27, 2013, Volume 9, Issue 1
Coarse abstractions make Zeno behaviours difficult to detect

Authors: Herbreteau, Frédéric and Srivathsan, B

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.


Source : oai:arXiv.org:1106.1850
DOI : 10.2168/LMCS-9(1:6)2013
Volume: Volume 9, Issue 1
Published on: February 27, 2013
Submitted on: March 31, 2012
Keywords: Computer Science - Logic in Computer Science,D.2.4,F.1.3,F.1.1


Share

Consultation statistics

This page has been seen 56 times.
This article's PDF has been downloaded 16 times.