research-article

An Effective Characterization of the Alternation Hierarchy in Two-Variable Logic

Authors:

Howard StraubingAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 18, Issue 4

Article No.: 30, Pages 1 - 22

https://doi.org/10.1145/3149822

Published: 28 November 2017 Publication History

Abstract

We give an algebraic characterization, based on the bilateral semidirect product of finite monoids, of the quantifier alternation hierarchy in two-variable first-order logic on finite words. As a consequence, we obtain a new proof that this hierarchy is strict. Moreover, by application of the theory of finite categories, we are able to make our characterization effective: that is, there is an algorithm for determining the exact quantifier alternation depth for a given language definable in two-variable logic.

References

[1]

Jorge Almeida. 1994. Finite Semigroups and Universal Algebra. World Scientific.

[2]

Jorge Almeida and Pascal Weil. 1998. Profinite categories and semidirect products. Journal of Pure and Applied Algebra 123, 1--3 (1998), 1--50.

[3]

Janusz A. Brzozowski and Faith E. Fich. 1980. Languages of R-trivial monoids. J. Comput. Syst. Sci. 20, 1 (1980), 32--49.

[4]

Samuel Eilenberg. 1976. Automata, Languages, and Machines Vol. 2. Academic Press.

Digital Library

[5]

Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. 1997. First-order logic with two variables and unary temporal logic. In LICS. 228--235.

Digital Library

[6]

Neil Immerman and Dexter Kozen. 1989. Definability with bounded number of bound variables. Inf. Comput. 83, 2 (1989), 121--139.

Digital Library

[7]

Johan A. W. Kamp. 1968. Tense Logic and the Theory of Linear Order. Ph.D. Dissertation. University of California, Los Angeles.

[8]

Andreas Krebs and Howard Straubing. 2012. An effective characterization of the alternation hierarchy in two-variable logic. In Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’12). 86--98.

[9]

Kenneth Krohn, Richard Mateosian, and John Rhodes. 1967. Methods of the algebraic theory of machines. I: Decomposition theorem for generalized machines; properties preserved under series and parallel compositions of machines. J. Comput. Syst. Sci. 1, 1 (1967), 55--85.

Digital Library

[10]

Manfred Kufleitner and Alexander Lauser. 2013. Quantifier alternation in two-variable first-order logic with successor is decidable. In Proceedings of the 30th International Symposium on Theoretical Aspects of Computer Science (STACS’13). 305--316.

[11]

Manfred Kufleitner and Pascal Weil. 2009. On FO² quantifier alternation over words. In Mathematical Foundations of Computer Science. 513--524.

Digital Library

[12]

Manfred Kufleitner and Pascal Weil. 2012. The FO² alternation hierarchy is decidable. In Computer Science Logic. 426--439.

[13]

Jean-Éric Pin. 1986. Varieties of Formal Languages. North Oxford Academic.

[14]

John L. Rhodes and Bret Tilson. 1989. The kernel of monoid morphisms. Journal of Pure and Applied Algebra 62 (1989), 227--268.

[15]

Marcel Paul Schützenberger. 1961. A remark on finite transducers. Information and Control 4, 2--3 (1961), 185--196.

[16]

Marcel Paul Schützenberger. 1976. Sur le produit de concatenation non ambigu. Semigroup Forum 13, 1 (1976), 47--75.

[17]

Thomas Schwentick, Denis Thérien, and Heribert Vollmer. 2001. Partially-ordered two-way automata: A new characterization of DA. In Proceedings of the 5th International Conference on Developments in Language Theory (DLT’01), Revised Papers. 239--250.

Digital Library

[18]

Imre Simon. 1975. Piecewise testable events. In Automata Theory and Formal Languages. 214--222.

Digital Library

[19]

Benjamin Steinberg. 1998. Decidability and Hyperdecidability of Joins of Pseudovarieties. Ph.D. Dissertation. University of California at Berkeley. Retrieved from http://people.math.carleton.ca/&sim;bsteinbg/pubs/thesis.pdf

Digital Library

[20]

Howard Straubing. 1992. Circuit complexity and the expressive power of generalized first-order formulas. In ICALP. 16--27.

Digital Library

[21]

Howard Straubing. 2011. Algebraic characterization of the alternation hierarchy in FO²{<} on finite words. In Computer Science Logic. 525--537.

[22]

Howard Straubing and Denis Thérien. 2002. Weakly iterated block products of finite monoids. In LATIN. 91--104.

Digital Library

[23]

Pascal Tesson and Denis Thérien. 2002. Diamonds are forever: The variety DA. In Semigroups, Algorithms, Automata and Languages, Coimbra (Portugal) 2001. World Scientific, 475--500.

[24]

Denis Thérien. 1991. Two-sided wreath product of categories. Journal of Pure and Applied Algebra 74, 3 (1991), 307--315.

[25]

Denis Thérien and Thomas Wilke. 1998. Over words, two variables are as powerful as one quantifier alternation. In STOC. 234--240.

Digital Library

[26]

Bret Tilson. 1987. Categories as algebra: An essential ingredient in the theory of monoids. Journal of Pure and Applied Algebra 48, 1--2 (1987), 83--198.

[27]

Peter Trotter and Pascal Weil. 1997. The lattice of pseudovarieties of idempotent semigroups and a non-regular analogue. Algebra Universalis 37 (1997), 491--526.

[28]

Pascal Weil. 2000. Profinite methods in semigroup theory. International Journal of Algebra and Computation 12 (2000), 137--178.

[29]

Philipp Weis and Neil Immerman. 2009. Structure theorem and strict alternation hierarchy for FO² on words. Logical Methods in Computer Science 5, 3 (2009).

Cited By

Henriksson VKufleitner M(2023) Forbidden Patterns for FO 2 Alternation Over Finite and Infinite Words International Journal of Foundations of Computer Science10.1142/S012905412344002134:02n03(183-224)Online publication date: 22-Feb-2023
https://doi.org/10.1142/S0129054123440021
Henriksson VKufleitner M(2022)Conelikes and Ranker ComparisonsLATIN 2022: Theoretical Informatics10.1007/978-3-031-20624-5_22(359-375)Online publication date: 29-Oct-2022
https://doi.org/10.1007/978-3-031-20624-5_22
Henriksson VKufleitner M(2021)Deciding FO2 Alternation for Automata over Finite and Infinite WordsDevelopments in Language Theory10.1007/978-3-030-81508-0_15(180-191)Online publication date: 6-Aug-2021
https://doi.org/10.1007/978-3-030-81508-0_15

Recommendations

Arity and alternation: a proper hierarchy in higher order logics

We study the effect of simultaneously bounding the maximal-arity of the higher-order variables and the alternation of quantifiers in higher-order logics, as to their expressive power on finite structures (or relational databases). Let $\mathit{AA}^i(r,m)$ be the class of ( ...
Going Higher in First-Order Quantifier Alternation Hierarchies on Words

We investigate quantifier alternation hierarchies in first-order logic on finite words. Levels in these hierarchies are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language ...
Level Two of the Quantifier Alternation Hierarchy Over Infinite Words

The study of various decision problems for logic fragments has a long history in computer science. This paper is on the membership problem for a fragment of first-order logic over infinite words; the membership problem asks for a given language whether ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 18, Issue 4

October 2017

251 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3143777

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 28 November 2017

Accepted: 01 September 2017

Revised: 01 May 2017

Received: 01 October 2016

Published in TOCL Volume 18, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

DFG Emmy-Noether program KR

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
88
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Henriksson VKufleitner M(2023) Forbidden Patterns for FO 2 Alternation Over Finite and Infinite Words International Journal of Foundations of Computer Science10.1142/S012905412344002134:02n03(183-224)Online publication date: 22-Feb-2023
https://doi.org/10.1142/S0129054123440021
Henriksson VKufleitner M(2022)Conelikes and Ranker ComparisonsLATIN 2022: Theoretical Informatics10.1007/978-3-031-20624-5_22(359-375)Online publication date: 29-Oct-2022
https://doi.org/10.1007/978-3-031-20624-5_22
Henriksson VKufleitner M(2021)Deciding FO2 Alternation for Automata over Finite and Infinite WordsDevelopments in Language Theory10.1007/978-3-030-81508-0_15(180-191)Online publication date: 6-Aug-2021
https://doi.org/10.1007/978-3-030-81508-0_15

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents