×

zbMATH — the first resource for mathematics

Event-clock visibly pushdown automata. (English) Zbl 1206.68183
Nielsen, Mogens (ed.) et al., SOFSEM 2009: Theory and practice of computer science. 35th conference on current trends in theory and practice of computer science, Špindlerův Mlýn, Czech Republic, January 24–30, 2009. Proceedings. Berlin: Springer (ISBN 978-3-540-95890-1/pbk). Lecture Notes in Computer Science 5404, 558-569 (2009).
Summary: We introduce the class of event-clock visibly pushdown automata (ECVPAs) as an extension of event-clock automata. The class of ECVPAs, on one hand, can model simple real-time pushdown systems and, on the other hand, is determinizable and closed under Boolean operations. We also show that for a timed visibly pushdown automaton \(A\) and an ECVPA \(B\), the inclusion problem \(L(A) \subseteq L(B)\) is decidable.
For the entire collection see [Zbl 1154.68020].

MSC:
68Q45 Formal languages and automata
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005) · Zbl 1085.68078 · doi:10.1007/11523468_88
[2] Alur, A., Dill, D.: A theory of timed automata. Theor. Comp. Sci. 126, 183–235 (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. Theor. Comp. Sci 211, 253–273 (1999); A preliminary version appeared In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 1–13. Springer, Heidelberg (1994) · Zbl 0912.68132
[4] Alur, R., Madhusudan, P.: Visibly pushdown languages. In: STOC 2004, June 13-15, 2004, pp. 202–211. ACM Press, New York (2004) · Zbl 1192.68396
[5] Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 64–85. Springer, Heidelberg (1995) · doi:10.1007/3-540-60472-3_4
[6] Bouyer, P., Laroussinie, F.: Model Checking Timed Automata. In: Modeling and Verification of Real-Time Systems, pp. 111–140. ISTE Ltd. - John Wiley & Sons, Ltd. (2008) · doi:10.1002/9780470611012.ch4
[7] Bouyer, P., Larsen, K.G., Markey, N.: Model Checking One-clock Priced Timed Automata. Logical Methods in Computer Science 4(2:9) (2008) · Zbl 1149.68401
[8] Emmi, M., Majumdar, R.: Decision Problems for the Verification of Real-time Software. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 200–211. Springer, Heidelberg (2006) · Zbl 1178.68340 · doi:10.1007/11730637_17
[9] Finkel, A., Schnoebelen, P.: Well-Structured Transition Systems Everywhere! Theor. Comp. Sci. 256(1-2), 63–92 (2001) · Zbl 0973.68170 · doi:10.1016/S0304-3975(00)00102-X
[10] Henzinger, T.A., Raskin, J., Schobbens, P.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–598. Springer, Heidelberg (1998) · doi:10.1007/BFb0055086
[11] Ouaknine, J., Worrell, J.: On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap. In: LICS 2004, pp. 54–63. IEEE Press, Los Alamitos (2004)
[12] D’Souza, D.: A Logical Characterisation of Event Clock Automata. International Journal of Foundation for Computer Science 14(4), 625–640 (2003) · Zbl 1101.68647 · doi:10.1142/S0129054103001923
[13] 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
[14] Tang, N.V., Hung, D.V., Ogawa, M.: Modeling Urgency in Component-Based Real-time Systems. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 248–255. Springer, Heidelberg (2008) · Zbl 05252978 · doi:10.1007/978-3-540-77505-8_20
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.