Modulo Counting on Words and Trees.

From International Center for Computational Logic

Toggle side column

Modulo Counting on Words and Trees.

Bartosz BednarczykBartosz Bednarczyk,  Witold CharatonikWitold Charatonik
Modulo Counting on Words and Trees.


Bartosz Bednarczyk, Witold Charatonik
Modulo Counting on Words and Trees.
FSTTCS 2017, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, December 2017
  • KurzfassungAbstract
    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.
  • Forschungsgruppe:Research Group: Computational Logic
@InProceedings{bednarczyk_et_al:LIPIcs:2018:8408,
  author =	{Bartosz Bednarczyk and Witold Charatonik},
  title =	[[:Vorlage:Modulo Counting on Words and Trees]],
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Satya Lokam and R. Ramanujam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/8408},
  URN =		{urn:nbn:de:0030-drops-84083},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.12},
  annote =	{Keywords: satisfiability, trees, words, two-variable logic, modulo quantifiers}
}