One quantifier alternation in first-order logic with modular predicates

Kufleitner, Manfred; Walter, Tobias

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 49 (2015) no. 1, pp. 1-22.

Adding modular predicates yields a generalization of first-order logic $FO$ over words. The expressive power of $FO[<,MOD]$ with order comparison $x<y$ and predicates for $x\equiv imodn$ has been investigated by Barrington et al. The study of $FO[<,MOD]$-fragments was initiated by Chaubard et al. More recently, Dartois and Paperman showed that definability in the two-variable fragment $F{O}^2[<,MOD]$ is decidable. In this paper we continue this line of work. We give an effective algebraic characterization of the word languages in $\Sigma {}_2[<,MOD]$. The fragment $\Sigma {}_2$ consists of first-order formulas in prenex normal form with two blocks of quantifiers starting with an existential block. In addition we show that $\Delta {}_2[<,MOD]$, the largest subclass of $\Sigma {}_2[<,MOD]$ which is closed under negation, has the same expressive power as two-variable logic $F{O}^2[<,MOD]$. This generalizes the result $F{O}^2[<]=\Delta {}_2[<]$ of Thérien and Wilke to modular predicates. As a byproduct, we obtain another decidable characterization of $F{O}^2[<,MOD]$.

M. Arfi, Opérations polynomiales et hiérarchies de concaténation. Theor. Comput. Sci. 91 (1991) 71–84. | DOI | MR | Zbl

D.A.M. Barrington, K.J. Compton, H. Straubing and D. Thérien, Regular languages in NC${}^1$. J. Comput. Syst. Sci. 44 (1992) 478–499. | DOI | MR | Zbl

L. Chaubard, J.-É. Pin and H. Straubing, Actions, wreath products of $𝒞$-varieties and concatenation product. Theor. Comput. Sci. 356 (2006) 73–89. | DOI | MR | Zbl

L. Chaubard, J.-É. Pin and H. Straubing, First order formulas with modular predicates. In Proc. of LICS 2006. IEEE Computer Society (2006) 211–220.

L. Dartois and C. Paperman, Personal communication (2013).

L. Dartois and C. Paperman, Two-variable first order logic with modular predicates over words, in Proc. of STACS 2013, vol. 20 of LIPIcs. Dagstuhl Publishing (2013) 329–340. | MR

V. Diekert, P. Gastin and M. Kufleitner, A survey on small fragments of first-order logic over finite words. Int. J. Found. Comput. Sci. 19 (2008) 513–548. | DOI | MR | Zbl

Z. Ésik and M. Ito, Temporal logic with counting and the degree of aperiodicity of finite automata. Acta Cybernetica 16 (2003) 1–28. | MR | Zbl

Z. Ésik and K.G. Larsen, Regular languages definable by Lindström quantifiers. RAIRO: ITA 37 (2003) 179–241. | Numdam | MR | Zbl

J.A.W. Kamp, Tense Logic and the Theory of Linear Order. Ph.D. thesis, University of California (1968).

K. Krohn, J.L. Rhodes and B. Tilson, Homomorphisms and semilocal theory. In Chapter 8 of Algebraic Theory of Machines, Languages, and Semigroups. Academic Press (1968) 191–231.

M. Kufleitner and A. Lauser, The join levels of the Trotter-Weil hierarchy are decidable. In Proc. of MFCS 2012, vol. 7464. Lect. Notes Comput. Sci. Springer (2012) 603–614. | MR

M. Kufleitner and A. Lauser, Lattices of logical fragments over words. In Proc. of ICALP 2012, vol. 7392. Lect. Notes Comput. Sci. Springer (2012) 275–286.

M. Kufleitner and P. Weil, On logical hierarchies within $F{O}^2$-definable languages. Logical Methods Comput. Sci. 8 (2012). | MR | Zbl

R. McNaughton and S. Papert, Counter-Free Automata. The MIT Press, Cambridge, Mass. (1971). | MR | Zbl

J.-É. Pin, Varieties of Formal Languages. North Oxford Academic, London (1986). | MR | Zbl

J.-É. Pin, A variety theorem without complementation, in Russian Math. (Iz. VUZ) 39 (1995) 80–90.

J.-É. Pin and P. Weil. Polynomial closure and unambiguous product. Theory Comput. Syst. 30 (1997) 383–422. | DOI | MR | Zbl

J.-É. Pin and P. Weil, Semidirect products of ordered semigroups. Commun. Algebra 30 (2002) 149–169. | DOI | MR | Zbl

M. P. Schützenberger, On finite monoids having only trivial subgroups. Inf. Control 8 (1965) 190–194. | DOI | MR | Zbl

I. Simon, Piecewise testable events, in 2nd GI Conf. of Autom. Theor. Form. Lang., vol. 33. Lect. Notes Comput. Sci. Springer (1975) 214–222. | MR | Zbl

L.J. Stockmeyer, The complexity of decision problems in automata theory and logic. Ph.D. thesis, TR 133, M.I.T., Cambridge (1974).

H. Straubing, A generalization of the Schützenberger product of finite monoids. Theor. Comput. Sci. 13 (1981) 137–150. | DOI | MR | Zbl

H. Straubing, Finite semigroup varieties of the form $𝐕*𝐃$. J. Pure Appl. Algebra 36 (1985) 53–94. | DOI | MR | Zbl

H. Straubing, Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser, Boston, Basel and Berlin (1994). | MR | Zbl

H. Straubing, On logical descriptions of regular languages, in Proc. of LATIN 2002, vol. 2286. Lect. Notes Comput. Sci. Springer (2002) 528–538. | MR | Zbl

H. Straubing and D. Thérien, Regular languages defined by generalized first-order formulas with a bounded number of bound variables. Theory Comput. Syst. 36 (2003) 29–69. | DOI | MR | Zbl

H. Straubing, D. Thérien and W. Thomas, Regular languages defined with generalized quantifiers. Inf. Comput. 118 (1995) 289–301. | DOI | MR | Zbl

P. Tesson and D. Thérien, Diamonds are forever: The variety $DA$. In Proc. of Semigroups, Algorithms, Automata and Languages 2001. World Scientific (2002) 475–500. | MR | Zbl

D. Thérien, Classification of finite monoids: The language approach. Theor. Comput. Sci. 14 (1981) 195–208. | DOI | MR | Zbl

D. Thérien and Th. Wilke, Over words, two variables are as powerful as one quantifier alternation. In Proc. of STOC 1998. ACM Press (1998) 234–240. | MR | Zbl

W. Thomas, Classifying regular events in symbolic logic. J. Comput. Syst. Sci. 25 (1982) 360–376. | DOI | MR | Zbl

Ph. Weis, Expressiveness and succinctness of first-order logic on finite words. Ph.D. thesis, University of Massachusetts Amherst (2011).