×

zbMATH — the first resource for mathematics

On regions and zones for event-clock automata. (English) Zbl 1314.68176
Summary: Event clock automata (\(\mathsf{ECA}\)) are a model for timed languages that has been introduced by Alur, Fix and Henzinger as an alternative to timed automata, with better theoretical properties (for instance, \(\mathsf{ECA}\) are determinizable while timed automata are not). In this paper, we revisit and extend the theory of \(\mathsf{ECA}\). We first prove that no finite time abstract language equivalence exists for \(\mathsf{ECA}\), thereby disproving a claim in the original work on \(\mathsf{ECA}\). This means in particular that regions do not form a time abstract bisimulation. Nevertheless, we show that regions can still be used to build a finite automaton recognizing the untimed language of an \(\mathsf{ECA}\). Then, we extend the classical notions of zones and DBMs to let them handle event clocks instead of plain clocks (as in timed automata) by introducing event zones and Event DBMs (EDBMs). We discuss algorithms to handle event zones represented as EDBMs, as well as (semi-) algorithms based on EDBMs to decide language emptiness of \(\mathsf{ECA}\).
MSC:
68Q45 Formal languages and automata
Software:
Kronos; Tempo
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur R (1999) Timed automata. In: Proceedings of CAV’99, vol 1633. Lecture notes in computer science. Springer, Berlin, pp 8-22 · Zbl 1046.68574
[2] Alur, R; Courcoubetis, C; Dill, D, Model-checking in dense real-time, Inf Comput, 104, 2-34, (1993) · Zbl 0783.68076
[3] Alur, R; Dill, D, A theory of timed automata, Theor Comput Sci, 126, 183-236, (1994) · Zbl 0803.68071
[4] Alur, R; Fix, L; Henzinger, TA, Event-clock automata: a determinizable class of timed automata, Theor Comput Sci, 211, 253-273, (1999) · Zbl 0912.68132
[5] Behrmann G, David A, Larsen KG, Håkansson J, Pettersson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: Proceedings of QEST’06. IEEE Computer Society, New York, pp 125-126 · Zbl 0978.03015
[6] Bellman R (1957) Dynamic programming. Princeton university press, Princeton · Zbl 0077.13605
[7] Bengtsson J, Griffioen WOD, Kristoffersen KJ, Larsen KG, Larsson F, Pettersson P, Yi W (2002) Automated verification of an audio-control protocol using Uppaal. J Log Algebr Program 52-53:163-181 · Zbl 1008.68009
[8] Bouyer P (2002) Modèles et algorithmes pour la vérification des systèmes temporisés. Thèse de doctorat, Laboratoire Spécification et Vérification. ENS Cachan, France · Zbl 0783.68076
[9] Bouyer P (2002) Timed automata may cause some troubles. In Research Report LSV-02-9, LSV, ENS DE CACHAN. http://www.lsv.enscachan.fr/Publis/RAPPORTS_LSV/PS/rrlsv-2002-9.rr.ps
[10] Bouyer, P, Forward analysis of updatable timed automata, Formal Methods Syst Des, 24, 281-320, (2004) · Zbl 1073.68041
[11] Bouyer P, Laroussinie F, Reynier P-A (2005) Diagonal constraints in timed automata: Forward analysis of timed systems. In: Pettersson P, Yi W (eds) Formal modeling and analysis of timed systems, vol 3829. Lecture notes in computer science. Springer, Berlin, pp 112-126 · Zbl 1175.68256
[12] Bozga M, Daws C, Maler O, Olivero A, Tripakis S, Yovine S (1998) Kronos: A model-checking tool for real-time systems. In: Proceedings of CAV’98, vol 1427. Lecture notes in computer science. Springer, Berlin, pp 546-550
[13] Cerans K (1993) Decidability of bisimulation equivalences for parallel timer processes. In: Proceedings of the fourth international workshop on computer aided verification, CAV ’92, London. Springer, Berlin, pp 302-315
[14] Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In Steffen B (ed) Proceedings of TACAS’98, vol 1384. Lecture notes in computer science. Springer, Berlin, pp 313-329
[15] Daws C, Tripakis S (1998) Model checking of real-time reachability properties using abstractions. In: TACAS. Springer, Berlin, pp 313-329
[16] Di Giampaolo B, Geeraerts G, Raskin J, Sznajder N (2010) Safraless procedures for timed specifications. In: Proceedings of FORMATS’10, vol 6246. Lecture notes in computer science. Springer, Berlin, pp 2-22 · Zbl 1290.68070
[17] Diekert V, Gastin P, Petit A (1997) Removing epsilon-transitions in timed automata. In: STACS 97, 14th Annual Symposium on theoretical aspects of computer science, vol 1200. Lecture notes in computer science. Springer, Berlin, pp 583-594
[18] Dill DL (1989) Timing assumptions and verification of finite-state concurrent systems. In: Proceedings of automatic verification methods for finite state systems, vol 407. Lecture notes in computer science. Springer, Berlin, pp 197-212
[19] Dima C (1999) Kleene theorems for event-clock automata. In: Proceedings of FCT’99, volume 1684 of Lecture Notes in computer science. Springer, Berlin, pp 215-225
[20] D’Souza D, Tabareau N (2004) On timed automata with input-determined guards. In Proccedings of FORMATS/FTRTFT’04, vol 3253. Lecture notes in computer science. Springer, Berlin, pp 68-83 · Zbl 1109.68503
[21] Geeraerts G, Raskin J-F, Sznajder N (2011) Event-clock automata : from theory to practice. In: Fahrenberg U, Tripakis S (eds) Proceedings of the 9th international conference on formal modelling and analysis of timed systems (FORMATS’11), vol 6919. Lecture notes in computer science. Springer, Berlin, pp 209-224 · Zbl 1348.68102
[22] Lindahl M, Pettersson P, Yi W (1998) Formal design and analysis of a gear-box controller. In: Proceedings of the 4th workshop on tools and algorithms for the construction and analysis of systems. vol 1384 .Lecture notes in computer science. Springer, Berlin, pp 281-297
[23] Miné A (2006) The octagon abstract domain. Higher-Order Symbol Comput 19(1):31-100, 2006. http://www.di.ens.fr/ mine/publi/article-mine-HOSC06.pdf · Zbl 1105.68069
[24] Pettersson, P, Yi W editors. Formal Modeling and Analysis of Timed Systems. In: Proceedings of the third international conference, FORMATS 2005, Uppsala, September 26-28, 2005, vol 3829. Lecture notes in computer science. Springer, Berlin
[25] Raskin, J-F; Schobbens, P-Y, The logic of event clocks: decidability, complexity and expressiveness, Automatica, 34, 247-282, (1998) · Zbl 0978.03015
[26] Sorea M (2001) Tempo: a model-checker for event-recording automata. In: Proceedings of RT-TOOLS’01, Aalborg
[27] Tang N, Ogawa M (2009) Event-clock visibly pushdown automata. In: Proceedings of SOFSEM’09, vol 5404. Lecture notes in computer science. Springer, Berlin, pp 558-569 · Zbl 1206.68183
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.