×

zbMATH — the first resource for mathematics

Event clock automata: from theory to practice. (English) Zbl 1348.68102
Fahrenberg, Uli (ed.) et al., Formal modeling and analysis of timed systems. 9th international conference, FORMATS 2011, Aalborg, Denmark, September 21–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24309-7/pbk). Lecture Notes in Computer Science 6919, 209-224 (2011).
Summary: Event clock automata (ECA ) are a model for timed languages that has been introduced by R. Alur et al. [Theor. Comput. Sci. 211, No. 1–2, 253–273 (1999; Zbl 0912.68132)] as an alternative to timed automata, with better theoretical properties (for instance, ECA are determinizable while timed automata are not). In this paper, we revisit and extend the theory of ECA. We first prove that no finite time abstract language equivalence exists for ECA, thereby disproving a claim in the original work on 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 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 ECA.
For the entire collection see [Zbl 1223.68006].

MSC:
68Q45 Formal languages and automata
Software:
Kronos; Tempo
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 8–22. Springer, Heidelberg (1999) · Zbl 1046.68574 · doi:10.1007/3-540-48683-6_3
[2] Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–236 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[3] Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theoretical Computer Science 211(1-2), 253–273 (1999) · Zbl 0912.68132 · doi:10.1016/S0304-3975(97)00173-4
[4] Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: Proceedings of QEST 2006, pp. 125–126. IEEE Computer Society, Los Alamitos (2006)
[5] Bellman, R.: Dynamic Programming. Princeton university press, Princeton (1957) · Zbl 0077.13605
[6] Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24(3), 281–320 (2004) · Zbl 1073.68041 · doi:10.1023/B:FORM.0000026093.21513.31
[7] 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) · doi:10.1007/BFb0028779
[8] Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998) · doi:10.1007/BFb0054180
[9] Di Giampaolo, B., Geeraerts, G., Raskin, J., Sznajder, N.: Safraless procedures for timed specifications. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 2–22. Springer, Heidelberg (2010) · Zbl 1290.68070 · doi:10.1007/978-3-642-15297-9_2
[10] Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990) · doi:10.1007/3-540-52148-8_17
[11] Dima, C.: Kleene theorems for event-clock automata. In: Ciobanu, G., Păun, G. (eds.) FCT 1999. LNCS, vol. 1684, pp. 215–225. Springer, Heidelberg (1999) · Zbl 0948.68106 · doi:10.1007/3-540-48321-7_17
[12] D’Souza, D., Tabareau, N.: On timed automata with input-determined guards. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 68–83. Springer, Heidelberg (2004) · Zbl 1109.68503 · doi:10.1007/978-3-540-30206-3_7
[13] Geeraerts, G., Raskin, J.-F., Sznajder, N.: Event-Clock Automata: from Theory to Practice. Technical report., http://arxiv.org/abs/1107.4138 · Zbl 1348.68102
[14] Raskin, J.-F., Schobbens, P.-Y.: The logic of event clocks: decidability, complexity and expressiveness. Automatica 34(3), 247–282 (1998) · Zbl 0978.03015
[15] Sorea, M.: Tempo: A model-checker for event-recording automata. In: Proceedings of RT-TOOLS 2001, Aalborg, Denmark (August 2001)
[16] Tang, N., Ogawa, M.: Event-clock visibly pushdown automata. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tuma, P., Valencia, F. (eds.) SOFSEM 2009. LNCS, vol. 5404, pp. 558–569. Springer, Heidelberg (2009) · Zbl 1206.68183 · doi:10.1007/978-3-540-95891-8_50
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.