Defining Temporal Hierarchies and How We Proved That Corresponding Hierarchies Are Always Strict

Table of Links

Abstract and 1 Introduction

2 Preliminaries

3 Temporal Hierarchies

4 Rating Maps

5 Optimal Imprints for TL(AT)

6 Conclusion and References

Appendix A. Appendix to Section 2 & Appendix B. Appendix to Section 3

Appendix C. Appendix to Section 4

Appendix D. Appendix to Section 5

6. Conclusion

We defined temporal hierarchies using the unary temporal logic operator C 7→ TL(C). We looked at the bases G and G + when G is a group prevariety. In this case, we proved that the corresponding hierarchies are always strict and we compared them with the corresponding concatenation hierarchies. Moreover, we proved that if G has decidable separation, then membership is decidable for levels one and two in both hierarchies. Our main theorem yields a stronger result for the particular bases ST and DD = ST+. Indeed, it implies that level two in both hierarchies has decidable covering. In turn, this implies that level three has decidable membership.

References

[1] Mustapha Arfi. Polynomial operations on rational languages. In Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, STACS’87, volume 247 of Lect. Notes Comp. Sci., pages 198–206. Springer, 1987.

[2] Mustapha Arfi. Operations polynomiales et hierarchies de concatenation. Theoretical Computer Science, 91(1):71–84, 1991.

[3] Christopher J. Ash. Inevitable graphs: a proof of the type II conjecture and some related decision procedures. International Journal of Algebra and Computation, 1(1):127–146, 1991.

[4] Janusz A. Brzozowski and Rina S. Cohen. Dot-depth of star-free events. Journal of Computer and System Sciences, 5(1):1–16, 1971.

[5] Janusz A. Brzozowski and Robert Knast. The dot-depth hierarchy of star-free languages is infinite. Journal of Computer and System Sciences, 16(1):37–55, 1978.

[6] Janusz A. Brzozowski and Imre Simon. Characterizations of locally testable events. Discrete Mathematics, 4(3):243–271, 1973.

[7] Laura Chaubard, Jean Eric Pin, and Howard Straubing. First order formulas with modular predicates. In ´ Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS’06), pages 211–220, 2006.

[8] Luc Dartois and Charles Paperman. Two-variable first order logic with modular predicates over words. In Proceedings of the 30th International Symposium on Theoretical Aspects of Computer Science, STACS’13, volume 20 of Leibniz International Proceedings in Informatics (LIPIcs), pages 329–340. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2013.

[9] Manuel Delgado. Abelian poinlikes of a monoid. Semigroup Forum, 56(3):339–361, 1998.

[10] Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-order logic with two variables and unary temporal logic. Information and Computation, 179(2):279–295, 2002.

[11] Hans W. Kamp. Tense Logic and the Theory of Linear Order. Phd thesis, Computer Science Department, University of California at Los Angeles, USA, 1968.

[12] Robert Knast. A semigroup characterization of dot-depth one languages. RAIRO - Theoretical Informatics and Applications, 17(4):321–330, 1983.

[13] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. Two-variable logic with a between relation. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’16, pages 106–115, 2016.

[14] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. An algebraic decision procedure for two-variable logic with a between relation. In 27th EACSL Annual Conference on Computer Science Logic, CSL’18, Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018.

[15] Andreas Krebs, Kamal Lodaya, Paritosh K. Pandya, and Howard Straubing. Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership. Logical Methods in Computer Science, 16(3), 2020.

[16] Manfred Kufleitner and Tobias Walter. One quantifier alternation in first-order logic with modular predicates. RAIRO Theorerical Informatics and Applications, 49(1):1–22, 2015.

[17] Alexis Maciel, Pierre P´eladeau, and Denis Th´erien. Programs over semigroups of dot-depth one. Theoretical Computer Science, 245(1):135–148, 2000.

[18] Stuart W. Margolis and Jean-Eric Pin. Products of group languages. In ´ FCT’85. Springer, 1985. [19] Robert McNaughton and Seymour A. Papert. Counter-Free Automata. MIT Press, 1971.

[20] Jean-Eric Pin. An explicit formula for the intersection of two polynomials of regular languages. In Proceedings of the 17th International Conference on Developments in Language Theory, DLT’13, volume 7907 of Lect. Notes Comp. Sci., pages 31–45. Springer, 2013.

[21] Jean-Eric Pin and Pascal Weil. Polynomial closure and unambiguous product. Theory of Computing Systems, 30(4):383–422, 1997.

[22] Jean-Eric Pin and Howard Straubing. Monoids of upper triangular boolean matrices. In ´ Semigroups. Structure and Universal Algebraic Problems, volume 39, pages 259–272. North-Holland, 1985.

[23] Thomas Place. The amazing mixed polynomial closure and its applications to two-variable first-order logic. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’22, 2022.

[24] Thomas Place and Marc Zeitoun. Separation and the successor relation. In 32nd International Symposium on Theoretical Aspects of Computer Science, STACS’15, Leibniz International Proceedings in Informatics (LIPIcs), pages 662–675. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015.

[25] Thomas Place and Marc Zeitoun. The covering problem. Logical Methods in Computer Science, 14(3), 2018.

[26] Thomas Place and Marc Zeitoun. Generic results for concatenation hierarchies. Theory of Computing Systems (ToCS), 63(4):849–901, 2019. Selected papers from CSR’17.

[27] Thomas Place and Marc Zeitoun. Going higher in first-order quantifier alternation hierarchies on words. Journal of the ACM, 66(2):12:1–12:65, 2019.

[28] Thomas Place and Marc Zeitoun. Separation and covering for group based concatenation hierarchies. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’19, pages 1–13. IEEE Computer Society, 2019.

[29] Thomas Place and Marc Zeitoun. Adding successor: A transfer theorem for separation and covering. ACM Transactions on Computational Logic, 21(2):9:1–9:45, 2020.

[30] Thomas Place and Marc Zeitoun. A generic polynomial time approach to separation by first-order logic without quantifier alternation. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, December 18-20, 2022, IIT Madras, Chennai, India, volume 250 of LIPIcs, pages 43:1–43:22. Schloss Dagstuhl - Leibniz-Zentrum f¨ur Informatik, 2022.

[31] Thomas Place and Marc Zeitoun. All about unambiguous polynomial closure. TheoretiCS, 2(11):1–74, 2023.

[32] Thomas Place and Marc Zeitoun. Group separation strikes back. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’23, pages 1–13. IEEE Computer Society, 2023.

[33] Thomas Place and Marc Zeitoun. On all things star-free. Journal, to appear, 2023.

[34] Thomas Place and Marc Zeitoun. A generic characterization of generalized unary temporal logic and two-variable first-order logic. In Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, CSL’24, 2024.

[35] Marcel Paul Sch¨utzenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190– 194, 1965.

[36] Marcel Paul Sch¨utzenberger. Sur le produit de concat´enation non ambigu. Semigroup Forum, 13:47–75, 1976.

[37] Imre Simon. Piecewise testable events. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pages 214–222. Springer, 1975.

[38] Howard Straubing. A generalization of the sch¨utzenberger product of finite monoids. Theoretical Computer Science, 13(2):137–150, 1981.

[39] Howard Straubing. Finite semigroup varieties of the form V ∗ D. Journal of Pure and Applied Algebra, 36:53–94, 1985.

[40] Denis Th´erien. Classification of finite monoids: The language approach. Theoretical Computer Science, 14(2):195– 208, 1981.

[41] Gabriel Thierrin. Permutation automata. Theory of Computing Systems, 2(1):83–90, 1968.

[42] Wolfgang Thomas. Classifying regular events in symbolic logic. Journal of Computer and System Sciences, 25(3):360–376, 1982.

[43] Denis Therien and Thomas Wilke. Over words, two variables are as powerful as one quantifier alternation. In Proceedings of the 30th Annual ACM Symposium on Theory of Computing, STOC’98, pages 234–240, New York, NY, USA, 1998. ACM.

[44] Yechezkel Zalcstein. Locally testable languages. Journal of Computer and System Sciences, 6(2):151–167, 1972.