Beyond ω-regular languages: ωT-regular expressions and their automata and logic counterparts

Thumbnail Image
Full text at PDC
Publication Date
Advisors (or tutors)
Journal Title
Journal ISSN
Volume Title
Google Scholar
Research Projects
Organizational Units
Journal Issue
In the last years, some extensions of ω-regular languages, namely, ωB-regular (ω-regular languages extended with boundedness), ωS-regular (ω-regular languages extended with strong unboundedness), and ωBS-regular languages (the combination of ωB- and ωS-regular ones), have been proposed in the literature. While the first two classes satisfy a generalized closure property, which states that the complement of an ωB-regular (resp., ωS-regular) language is an ωS-regular (resp., ωB-regular) one, the last class is not closed under complementation. The existence of non-ωBS-regular languages that are the complements of some ωBS-regular ones and express fairly natural asymptotic behaviors motivates the search for other significant classes of extended ω-regular languages. In this paper, we present the class of ωT-regular languages, which includes meaningful languages that are not ωBS-regular. We define this new class of languages in terms of ωT-regular expressions. Then, we introduce a new class of automata (counter-check automata) and we prove that (i) their emptiness problem is decidable in PTIME, and (ii) they are expressive enough to capture ωT-regular languages. We also provide an encoding of ωT-regular expressions into S1S+U. Finally, we investigate a stronger variant of ωT-regular languages (-regular languages). We characterize the resulting class of languages in terms of -regular expressions, and we show how to map it into a suitable class of automata, called counter-queue automata. We conclude the paper with a comparison of the expressiveness of ωT- and -regular languages and of the corresponding automata.
"This is a pre-print of an article published in Theoretical Computer Science. The final authenticated version is available online at:”.
[1] D. Della Monica, A. Montanari, P. Sala, Beyond ωBS-regular languages: ωT-regular expressions and counter-check automata, in: P. Bouyer, A. Orlandini, P. San Pietro (Eds.), Proc. of the 8th International Symposium on Games, Automata, Logics and Formal Verification, GandALF, Roma, Italy, in: EPTCS, vol. 256, 2017, pp. 223–237. [2] D. Barozzini, D. Della Monica, A. Montanari, P. Sala, Counter-queue automata with an application to a meaningful extension of omega-regular languages, in: Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science (ICTCS) and the 32nd Italian Conference on Computational Logic (CILC), in: CEUR Workshop Proceedings,, vol. 1949, 2017, pp. 27–38. [3] J.R. Büchi, On a decision method in restricted second order arithmetic, in: Proc. of the 1960 Int. Congress on Logic, Methodology and Philosophy of Science, 1962, pp. 1–11. [4] R. McNaughton, Testing and generating infinite sequences by a finite automaton, Inf. Control 9(5) (1966) 521–530, https://doi .org /10 .1016 /S0019 -9958(66 )80013 -X. [5] C.C. Elgot, M.O. Rabin, Decidability and undecidability of extensions of second (first) order theory of (generalized) successor, J. Symb. Log. 31 (2) (1966) 169–181, https://doi .org /10 .1002 /malq .19600060105. [6] W. Thomas, Automata on infinite objects, in: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), MIT Press, 1990, pp. 133–192. [7] M. Bojanczyk, Weak MSO with the unbounding quantifier, Theory Comput. Syst. 48 (3) (2011) 554–576, https://doi .org /10 .1007 /s00224 -010 -9279 -2. [8] M. Bojanczyk, T. Colcombet, Bounds in ω-regularity, in: LICS, 2006, pp. 285–296. [9] M. Bojanczyk, T. Colcombet, Boundedness in languages of infinite words, Log. Methods Comput. Sci. 13 (4:3) (2017) 1–54. [10]M. Bojanczyk, S. Torunczyk, Deterministic automata and extensions of weak MSO, in: R. Kannan, K.N. Kumar (Eds.), Proc. of the 29th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS, in: LIPIcs, vol. 4, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2009, pp. 73–84. [11] R. Alur, T.A. Henzinger, Finitary fairness, ACM Trans. Program. Lang. Syst. 20 (6) (1998) 1171–1194, https://doi .org /10 .1145 /295656 .295659. [12] O. Kupferman, N. Piterman, M.Y. Vardi, From liveness to promptness, Form. Methods Syst. Des. 34 (2) (2009) 83–103, [13]D. Della Monica, A. Montanari, A. Murano, P. Sala, Prompt interval temporal logic, in: JELIA, in: LNCS, vol. 10021, Springer, 2016, pp. 207–222.[14]M. Bojanczyk, A bounding quantifier, in: CSL, in: LNCS, vol. 3210, Springer, 2004, pp. 41–55. [15]M. Bojanczyk, P. Parys, S. Torunczyk, The MSO+U theory of (N, <) is undecidable, in: STACS, in: LIPIcs, vol. 47, 2016, pp. 21:1–21:8. [16] D. Della Monica, A. Montanari, P. Sala, Beyond ωBS-regular languages: the class of ωT-regular languages, research Report 2017/01, Dept. of Mathematics, Computer Science, and Physics, University of Udine, Italy, 2017, /~angelo .montanari /res _rep2017 _1.pdf. [17]L. Breveglieri, A. Cherubini, C. Citrini, S. Crespi-Reghizzi, Multi-push-down languages and grammars, Int. J. Found. Comput. Sci. 7(03) (1996) 253–291. [18]M.F. Atig, B. Bollig, P. Habermehl, Emptiness of multi-pushdown automata is 2ETIME-complete, in: Developments in Language Theory, Springer, 2008, pp. 121–133. [19] S. Hummel, M. Skrzypczak, The topological complexity of MSO+U and related automata models, Fundam. Inform. 119 (1) (2012) 87–111,[20] M. Skrzypczak, Separation property for ωB-and ωS-regular languages, Log. Methods Comput. Sci. 10 (1) (2014), https://doi .org /10 .2168 /LMCS -10(1 :8 )2014.[21]A. Montanari, P. Sala, Adding an equivalence relation to the interval logic ABB: complexity and expressiveness, in: LICS, IEEE Computer Society, 2013, pp. 193–202. [22]A. Montanari, P. Sala, Interval logics and ωB-regular languages, in: LATA, in: LNCS, vol. 7810, Springer, 2013, pp. 431–443.