Modulo Counting on Words and Trees.

Bartosz BednarczykBartosz Bednarczyk, Witold CharatonikWitold Charatonik

Bartosz Bednarczyk, Witold Charatonik
Modulo Counting on Words and Trees.
In Satya V. Lokam, R. Ramanujam, eds., FSTTCS 2017, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, volume 93 of Leibniz International Proceedings in Informatics, 12:1--12:16, December 2017. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Details
Bibtex

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.
Weitere Informationen unter:Further Information: Link
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@InProceedings{bednarczyk_et_al:LIPIcs:2018:8408,
  author =	{Bartosz Bednarczyk and Witold Charatonik},
  title =	{{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}
}