In earlier work (LICS 2016), the authors introduced two-variable first-order logic supplemented by a binary relation that allows one to say that a letter appears between two positions. We found an effective algebraic criterion that is a necessary condition for definability in this logic, and conjectured that the criterion is also sufficient, although we proved this only in the case of two-letter alphabets. Here we prove the general conjecture. The proof is quite different from the arguments in the earlier work, and required the development of novel techniques concerning factorizations of words. We extend the results to binary relations specifying that a factor appears between two positions.

It is an open problem whether definability in Propositional Dynamic Logic (PDL) on forests is decidable. Based on an algebraic characterization by Bojańczyk, et. al., (2012) in terms of forest algebras, Straubing (2013) described an approach to PDL based on a k-fold iterated distributive law. A proof that all languages satisfying such a k-fold iterated distributive law are in PDL would settle decidability of PDL. We solve this problem in the case k = 2: All languages recognized by forest algebras satisfying a 2-fold iterated distributive law are in PDL. Furthermore, we show that this class is decidable. This provides a novel nontrivial decidable subclass of PDL, and demonstrates the viability of the proposed approach to deciding PDL in general.

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.

We study an extension of FO2[<], first-order logic interpreted in finite words, in which formulas are restricted to use only two variables. We adjoin to this language two-variable atomic formulas that say, 'the letter a appears between positions x and y'. This is, in a sense, the simplest property that is not expressible using only two variables.

We use the recently developed theory of forest algebras to find algebraic characterizations of the languages of unranked trees and forests definable in various logics. These include the temporal logics CTL and EF, and first-order logic over the ancestor relation. While the characterizations are in general non-effective, we are able to use them to formulate necessary conditions for definability and provide new proofs that a number of languages are not definable in these logics.

This paper presents a decidable characterization of tree languages that can be defined by a boolean combination of Sigma1formulas. This is a tree extension of the Simon theorem, which says that a string language can be defined by a boolean combination of Sigma1formulas if and only if its syntactic monoid is J-trivial.

We consider an extension of first-order logic by modular quantifiers of a fixed modulus q. Drawing on collapse results from finite model theory and techniques of finite semigroup theory, we show that if the only available numerical predicate is addition, then sentences in this logic cannot define the set of bit strings in which the number of 1's is divisible by a prime p that does not divide q. More generally, we completely characterize the regular languages definable in this logic. The corresponding statement, with addition replaced by arbitrary numerical predicates, is equivalent to the conjectured separation of the circuit complexity class $ACC$ from $NC^1$. Thus our theorem can be viewed as proving a highly uniform version of the conjecture.

Two results by Schutzenberger (1965) and by Mc- Naughton and Papert (1971) lead to a precise description of the expressive power of first order logic on words interpreted as ordered colored structures. In this paper, we study the expressive power of existential formulas and of Boolean combinations of existential formulas in a logic enriched by modular numerical predicates. We first give a combinatorial description of the corresponding regular languages, and then give an algebraic characterization in terms of their syntactic morphisms. It follows that one can effectively decide whether a given regular language is captured by one of these two fragments of first order logic. The proofs rely on nontrivial techniques of semigroup theory: stamps, derived categories and wreath products.