Modulo Counting on Words and Trees

TL;DR

This paper investigates the satisfiability problem for a two-variable first-order logic with modulo counting over words and trees, providing complexity bounds and a new decision procedure.

Contribution

It introduces a small-model property for this logic, leading to a new proof of EXPSPACE upper bound for words and a 2EXPTIME algorithm for trees, with matching lower bounds.

Findings

Decidability of the logic over words and trees.

EXPSPACE upper bound for words.

2EXPTIME algorithm for trees.

Abstract

We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.