A Note on C² Interpreted over Finite Data-Words

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.

Authors

• Bartosz Bednarczyk
• Piotr Witkowski 0001

Keywords

• Two-variable logic
• data-words
• VASS
• decidability
• undecidability
• counting