DROPS

Document

DOI: 10.4230/LIPIcs.TIME.2020.17

A Note on C² Interpreted over Finite Data-Words

Authors: Bartosz Bednarczyk and Piotr Witkowski

Published in: LIPIcs, Volume 178, 27th International Symposium on Temporal Representation and Reasoning (TIME 2020)

Abstract

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.

Cite as

Bartosz Bednarczyk and Piotr Witkowski. A Note on C² Interpreted over Finite Data-Words. In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bednarczyk_et_al:LIPIcs.TIME.2020.17,
  author =	{Bednarczyk, Bartosz and Witkowski, Piotr},
  title =	{{A Note on C² Interpreted over Finite Data-Words}},
  booktitle =	{27th International Symposium on Temporal Representation and Reasoning (TIME 2020)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-167-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{178},
  editor =	{Mu\~{n}oz-Velasco, Emilio and Ozaki, Ana and Theobald, Martin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2020.17},
  URN =		{urn:nbn:de:0030-drops-129850},
  doi =		{10.4230/LIPIcs.TIME.2020.17},
  annote =	{Keywords: Two-variable logic, data-words, VASS, decidability, undecidability, counting}
}

Document

DOI: 10.4230/LIPIcs.CSL.2015.631

Two-variable Logic with Counting and a Linear Order

Authors: Witold Charatonik and Piotr Witkowski

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract

We study the finite satisfiability problem for the two-variable fragment of the first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of two linear orders (in presence of two other binary symbols). In the case of one linear order it is NEXPTIME-complete, even in presence of the successor relation. Surprisingly, the complexity of the problem explodes when we add one binary symbol more: C2 with one linear order and its successor, in presence of other binary predicate symbols, is decidable, but it is as expressive (and as complex) as Vector Addition Systems.

Cite as

Witold Charatonik and Piotr Witkowski. Two-variable Logic with Counting and a Linear Order. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 631-647, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{charatonik_et_al:LIPIcs.CSL.2015.631,
  author =	{Charatonik, Witold and Witkowski, Piotr},
  title =	{{Two-variable Logic with Counting and a Linear Order}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{631--647},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.631},
  URN =		{urn:nbn:de:0030-drops-54436},
  doi =		{10.4230/LIPIcs.CSL.2015.631},
  annote =	{Keywords: Two-variable logic, counting quantifiers, linear order, satisfiability, complexity}
}

Search Results

Documents authored by Witkowski, Piotr

A Note on C² Interpreted over Finite Data-Words

Abstract

Cite as

Two-variable Logic with Counting and a Linear Order

Abstract

Cite as

Thanks for your feedback!

Could not send message