2026-08-10T23:44:14Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12985 2024-03-06T10:51:30Z ddc:004 open_access

A Note on C² Interpreted over Finite Data-Words Bednarczyk, Bartosz Witkowski, Piotr Two-variable logic data-words VASS decidability undecidability counting We consider the satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers, interpreted over finite words with data, denoted here with C²[≤ , succ, ∼, π_bin]. In our scenario, we allow for using arbitrary many uninterpreted binary predicates from π_bin, two navigational predicates ≤ and succ over word positions as well as a data-equality predicate ∼. We prove that the obtained logic is undecidable, which contrasts with the decidability of the logic without counting by Montanari, Pazzaglia and Sala [Angelo Montanari et al., 2016]. We supplement our results with decidability for several sub-fragments of C²[≤ , succ, ∼, π_bin], e.g. without binary predicates, without successor succ, or under the assumption that the total number of positions carrying the same data value in a data-word is bounded by an a priori given constant. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bartosz Bednarczyk and Piotr Witkowski 2020 Is Part Of LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TIME.2020.17 urn:nbn:de:0030-drops-129850 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.17 eng https://creativecommons.org/licenses/by/3.0/legalcode