Title: Expressiveness and Succinctness of First-Order Logic on Finite Words

Speaker: Philipp Weis, UMass Amherst

Abstract:

Expressiveness, and more recently, succinctness, are two central concerns of finite model theory and descriptive complexity theory. Succinctness is
particularly interesting because it is closely related to the
complexity-theoretic trade-off between parallel time and the amount of
hardware. We develop new bounds on the expressiveness and succinctness of
first-order logic with two variables on finite words, present a related
result about the complexity of the satisfiability problem for this logic,
and explore a new approach to the generalized star-height problem from the
perspective of logical expressiveness.

We give a complete characterization of the expressive power of first-order
logic with two variables on finite words. Our main tool for this
investigation is the classical Ehrenfeucht-Fra•ssˇ game. Using our new
characterization, we prove that the quantifier alternation hierarchy for
this logic is strict, settling the main remaining open question about the
expressiveness of this logic.

A second important question about first-order logic with two variables on
finite words is about the complexity of the satisfiability problem for this
logic. Previously it was only known that this problem is NP-hard and in
NEXP. We prove a polynomial-size small-model property for this logic,
leading to an NP algorithm and thus proving that the satisfiability problem
for this logic is NP-complete.

Finally, we investigate one of the most baffling open problems in formal
language theory: the generalized star-height problem. As of today, we don't
even know whether there exists a regular language that has generalized
star-height larger than 1. This problem can be phrased as an expressiveness
question for first-order logic with a restricted transitive closure
operator, and thus allows us to use established tools from finite model
theory to attack the generalized star-height problem. Besides our
contribution to formalize this problem in a purely logical form, we have
developed several example languages as candidates for languages of
generalized star-height at least 2. While some of them still stand as
promising candidates, for others we present new results that prove that they
only have generalized star-height 1.