×

A perfect class of context-sensitive timed languages. (English) Zbl 1436.68161

Brlek, Srečko (ed.) et al., Developments in language theory. 20th international conference, DLT 2016, Montréal, Canada, July 25–28, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9840, 38-50 (2016).
Summary: Perfect languages – a term coined by J. Esparza et al. [in: Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS’12. Los Alamitos, CA: IEEE Computer Society. 285–294 (2012; Zbl 1362.68168)] – are the classes of languages that are closed under Boolean operations and enjoy decidable emptiness problem. Perfect languages form the basis for decidable automata-theoretic model-checking for the respective class of models. Regular languages and visibly pushdown languages are paradigmatic examples of perfect languages. R. Alur and D. L. Dill [Theor. Comput. Sci. 126, No. 2, 183–235 (1994; Zbl 0803.68071)] initiated the language-theoretic study of timed languages and introduced timed automata capturing a timed analog of regular languages. However, unlike their untimed counterparts, timed regular languages are not perfect. R. Alur et al. [Theor. Comput. Sci. 211, No. 1–2, 253–273 (1999; Zbl 0912.68132)] later discovered a perfect subclass of timed languages recognized by event-clock automata. Since then, a number of perfect subclasses of timed context-free languages, such as event-clock visibly pushdown languages, have been proposed. There exist examples of perfect languages even beyond context-free languages: – S. La Torre et al. [“A robust class of context-sensitive languages”, in: Proceedings of the 22nd annual IEEE symposium on logic in computer science, LICS’07. Los Alamitos, CA: IEEE Computer Society. 161–170 (2007; doi:10.1109/LICS.2007.9)] characterized first perfect class of context-sensitive languages via multistack visibly pushdown automata with an explicit bound on number of stages where in each stage at most one stack is used. In this paper we extend their work for timed languages by characterizing a perfect subclass of timed context-sensitive languages called dense-time multistack visibly pushdown languages and provide a logical characterization for this class of timed languages.
For the entire collection see [Zbl 1342.68008].

MSC:

68Q45 Formal languages and automata
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abdulla, P., Atig, M., Stenman, J.: Dense-timed pushdown automata. In: LICS, pp. 35–44 (2012) · Zbl 1360.68535 · doi:10.1109/LICS.2012.15
[2] Alur, R., Dill, D.: A theory of timed automata. TCS 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. TCS 211(1–2), 253–273 (1999) · Zbl 0912.68132 · doi:10.1016/S0304-3975(97)00173-4
[4] Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Symposium on Theory of Computing, pp. 202–211 (2004) · Zbl 1192.68396 · doi:10.1145/1007352.1007390
[5] Atig, M.F.: Model-checking of ordered multi-pushdown automata. Log. Methods Comput. Sci. 8(3), 1–31 (2012) · Zbl 1279.68206
[6] Bar-Hillel, Y., Perles, M., Shamir, E.: On formal properties of simple phrase structure grammars. Zeitschrift für Phonetik, Sprachwissenschaft und Kommunikationsforschung 14, 143–172 (1961) · Zbl 0106.34501
[7] Bhave, D., Dave, V., Krishna, S.N., Phawade, R., Trivedi, A.: A logical characterization for dense-time visibly pushdown automata. In: Dediu, A.-H., Janoušek, J., Martín-Vide, C., Truthe, B. (eds.) LATA 2016. LNCS, vol. 9618, pp. 89–101. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-30000-9_7 · Zbl 1435.68144 · doi:10.1007/978-3-319-30000-9_7
[8] Bhave, D., Dave, V., Krishna, S.N., Phawade, R., Trivedi, A.: A perfect class of context-sensitive timed languages. Technical report, IIT Bombay (2016). www.cse.iitb.ac.in/internal/techreports/reports/TR-CSE-2016-80.pdf · Zbl 1435.68144
[9] Czerwiński, W., Hofman, P., Lasota, S.: Reachability problem for weak multi-pushdown automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 53–68. Springer, Heidelberg (2012) · Zbl 1364.68247 · doi:10.1007/978-3-642-32940-1_6
[10] Esparza, J., Ganty, P., Majumdar, R.: A perfect model for bounded verification. In: LICS, pp. 285–294. IEEE Computer Society (2012) · Zbl 1362.68168 · doi:10.1109/LICS.2012.39
[11] La Torre, S., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS, pp. 161–170 (2007) · doi:10.1109/LICS.2007.9
[12] La Torre, S., Napoli, M., Parlato, G.: Scope-bounded pushdown languages. In: Shur, A.M., Volkov, M.V. (eds.) DLT 2014. LNCS, vol. 8633, pp. 116–128. Springer, Heidelberg (2014) · Zbl 1345.68211 · doi:10.1007/978-3-319-09698-8_11
[13] La Torre, S., Napoli, M., Parlato, G.: A unifying approach for multistack pushdown automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 377–389. Springer, Heidelberg (2014) · Zbl 1425.68215 · doi:10.1007/978-3-662-44522-8_32
[14] La Torre, S., Madhusudan, P., Parlato, G.: The language theory of bounded context-switching. In: López-Ortiz, A. (ed.) LATIN 2010. LNCS, vol. 6034, pp. 96–107. Springer, Heidelberg (2010) · Zbl 1283.68197 · doi:10.1007/978-3-642-12200-2_10
[15] Trivedi, A., Wojtczak, D.: Recursive timed automata. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 306–324. Springer, Heidelberg (2010) · Zbl 1305.68115 · doi:10.1007/978-3-642-15643-4_23
[16] Van 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.