Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2017.12
URN: urn:nbn:de:0030-drops-84083
URL: https://drops.dagstuhl.de/opus/volltexte/2018/8408/
Bednarczyk, Bartosz ; Charatonik, Witold
Modulo Counting on Words and Trees
| pdf-format: |
|
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.
BibTeX - Entry
@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}
}
| Keywords: | satisfiability, trees, words, two-variable logic, modulo quantifiers | |
| Seminar: | 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017) | |
| Issue date: | 2018 | |
| Date of publication: | 12.02.2018 |
