Reversible Regular Languages : Logical and Algebraic Characterisations

• Autorzy: Gastin Paul , Manuel Amaldev , Govind R.

Identyfikatory

DOI

10.3233/FI-2021-2045

• Języki publikacji: EN

Abstrakty

EN

We present first-order (FO) and monadic second-order (MSO) logics with predicates ‘between’ and ‘neighbour’ that characterise the class of regular languages that are closed under the reverse operation and its subclasses. The ternary between predicate bet(x, y, z) is true if the position y is strictly between the positions x and z. The binary neighbour predicate N(x, y) is true when the the positions x and y are adjacent. It is shown that the class of reversible regular languages is precisely the class definable in the logics MSO(bet) and MSO(N). Moreover the class is definable by their existential fragments EMSO(bet) and EMSO(N), yielding a normal form for MSO formulas. In the first-order case, the logic FO(bet) corresponds precisely to the class of reversible languages definable in FO(<). Every formula in FO(bet) is equivalent to one that uses at most 3 variables. However the logic FO(N) defines only a strict subset of reversible languages definable in FO(+1). A language-theoretic characterisation of the class of languages definable in FO(N), called locally-reversible threshold-testable (LRTT), is given. In the second part of the paper we show that the standard connections that exist between MSO and FO logics with order and successor predicates and varieties of finite semigroups extend to the new setting with the semigroups extended with an involution operation on its elements. The case is different for FO(N) where we show that one needs an additional equation that uses the involution operator to characterise the class. While the general problem of characterising FO(N) is open, an equational characterisation is shown for the case of neutral letter languages.

Słowa kluczowe

EN

regular languages; reversible languages; first-order logic; automata; semigroups

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 180, nr 4
• Strony: 333--350
• Opis fizyczny: Bibliogr. 18 poz., rys.

Twórcy

autor

Gastin Paul

• Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, France

autor

Manuel Amaldev

• Indian Institute of Technology Goa, India

autor

Govind R.

• Chennai Mathematical Institute, Chennai, India
• LaBRI, University of Bordeaux, France

Bibliografia

• [1] Thomas W. Classifying Regular Events in Symbolic Logic. J. Comput. Syst. Sci., 1982. 25(3):360-376. doi:10.1016/0022-0000(82)90016-2.
• [2] Schützenberger MP. On Finite Monoids Having Only Trivial Subgroups. Information and Control, 1965. 8(2):190-194. doi:10.1016/S0019-9958(65)90108-7.
• [3] McNaughton R, Papert SA. Counter-Free Automata (M.I.T. Research Monograph No. 65). The MIT Press, 1971. ISBN: 0262130769.
• [4] Straubing H. Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser Verlag, Basel, Switzerland, 1994. ISBN: 3-7643-3719-2.
• [5] Krebs A, Lodaya K, Pandya PK, Straubing H. Two-variable Logic with a Between Relation. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. 2016 pp. 106-115. doi:10.1145/2933575.2935308.
• [6] Krebs A, Lodaya K, Pandya PK, Straubing H. An Algebraic Decision Procedure for Two-Variable Logic with a Between Relation. In: 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK. 2018 pp. 28:1-28:17. doi:10.4230/LIPIcs.CSL.2018.28.
• [7] Krebs A, Lodaya K, Pandya PK, Straubing H. Two-variable logics with some betweenness relations: Expressiveness, satisfiability and membership. arXiv preprint arXiv:1902.05905, 2019.
• [8] Tesson P, Therien D. Diamonds Are Forever: The Variety DA. In: Semigroups, Algorithms, Automata and Languages, Coimbra (Portugal) 2001. World Scientific, 2002 pp. 475-500.
• [9] Crvenković S, Dolinka I. Varieties of involution semigroups and involution semirings: a survey. In: Proceedings of the International Conference “Contemporary Developments in Mathematics” (Banja Luka, 2000), Bulletin of Society of Mathematicians of Banja Luka. 2000 pp. 7-47.
• [10] Gastin P, Manuel A, Govind R. Logics for Reversible Regular Languages and Semigroups with Involution. In: Hofman P, Skrzypczak M (eds.), Proceedings of the 23th International Conference on Developments in Language Theory (DLT’19), volume 11647 of Lecture Notes in Computer Science. Springer, Warsaw, Poland, 2019 pp. 182-191. doi:10.1007/978-3-030-24886-4_13.
• [11] Kamp JAW. Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California, 1968.
• [12] Beauquier D, Pin JÉ. Languages and Scanners. Theor. Comput. Sci., 1991. 84(1):3-21. doi:10.1016/0304-3975(91)90258-4.
• [13] Ebbinghaus HD, Flum J. Finite Model Theory: Second Edition. Springer Monographs in Mathematics. Springer Berlin Heidelberg, 2005. ISBN: 9783540287889.
• [14] Pin JÉ. Mathematical Foundations of Automata Theory. URL https://www.irif.fr/~jep/PDF/MPRI/MPRI.pdf.
• [15] Brzozowski JA, Simon I. Characterizations of Locally Testable Events. In: 12th Annual Symposium on Switching and Automata Theory, East Lansing, Michigan, USA, October 13-15, 1971. 1971 pp. 166-176. doi:10.1109/SWAT.1971.6.
• [16] Paperman C. Semigroup Online. URL https://www.paperman.name/semigroup/.
• [17] Tilson B. Categories as algebra: An essential ingredient in the theory of monoids. Journal of Pure and Applied Algebra, 1987. 48(1-2):83-198. doi:10.1016/0022-4049(87)90108-3.
• [18] Straubing H. Finite semigroup varieties of the form V ٭ D. Journal of Pure and Applied Algebra, 1985. 36:53-94.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).