×

zbMATH — the first resource for mathematics

Coarse abstractions make Zeno behaviours difficult to detect. (English) Zbl 1343.68139
Katoen, Joost-Pieter (ed.) et al., CONCUR 2011 – concurrency theory. 22nd international conference, CONCUR 2011, Aachen, Germany, September 6–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-23216-9/pbk). Lecture Notes in Computer Science 6901, 92-107 (2011).
Summary: 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.
For the entire collection see [Zbl 1221.68022].

MSC:
68Q45 Formal languages and automata
Software:
Kronos; REDLIB
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994) · Zbl 0803.68071
[2] Behrmann, G., Bouyer, P., Larsen, K.G., Pelanek, R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. Journal on Software Tools for Technology Transfer 8(3), 204–215 (2006) · Zbl 05075086
[3] Behrmann, G., David, A., Larsen, K.G., Haakansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST, pp. 125–126. IEEE Computer Society, Los Alamitos (2006)
[4] Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24(3), 281–320 (2004) · Zbl 1073.68041
[5] Bowman, H., Gómez, R.: How to stop time stopping. Formal Aspects of Computing 18(4), 459–493 (2006) · Zbl 1105.68059
[6] Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
[7] Dill, D.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) AVMFSS 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990)
[8] Gómez, R., Bowman, H.: Efficient detection of zeno runs in timed automata. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 195–210. Springer, Heidelberg (2007) · Zbl 1141.68435
[9] Herbreteau, F., Srivathsan, B.: Coarse abstractions make zeno behaviours difficult to detect. CoRR abs/1106.1850 (2011); Extended version with proofs · Zbl 1260.68205
[10] Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient Emptiness Check for Timed Büchi Automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 148–161. Springer, Heidelberg (2010) · Zbl 05772628
[11] Li, G.: Checking timed Büchi automata emptiness using LU-abstractions. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 228–242. Springer, Heidelberg (2009) · Zbl 1262.68093
[12] Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999)
[13] Tripakis, S.: Checking timed Büchi emptiness on simulation graphs. ACM Trans. on Computational Logic 10(3) (2009) · Zbl 1352.68165
[14] Tripakis, S., Yovine, S., Bouajjani, A.: Checking timed Büchi automata emptiness efficiently. Formal Methods in System Design 26(3), 267–292 (2005) · Zbl 1085.68083
[15] Wang, F.: Redlib for the formal verification of embedded systems. In: ISoLA, pp. 341–346. IEEE, Los Alamitos (2006)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.