Modulo Counting on Words and Trees

2017/10/16 by Bartosz Bednarczyk, Bednarczyk, Bartosz, Witold Charatonik +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.1710.05582

Full version of a paper published in proceedings of FSTTCS 2017 conference

arxiv created 2017/10/16 · arxiv updated 2017/10/17

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.

Related

• Extending Two-Variable Logic on Trees
• Decidable fragments of first-order modal logics with counting quantifiers over varying domains
• Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees
• Modulo-Counting First-Order Logic on Bounded Expansion Classes
• One-Variable Logic Meets Presburger Arithmetic