Modulo Counting on Words and Trees
Logic in Computer Science
2017-10-17 v1
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.
Cite
@article{arxiv.1710.05582,
title = {Modulo Counting on Words and Trees},
author = {Bartosz Bednarczyk and Witold Charatonik},
journal= {arXiv preprint arXiv:1710.05582},
year = {2017}
}
Comments
Full version of a paper published in proceedings of FSTTCS 2017 conference