Document Open Access Logo

A Note on C² Interpreted over Finite Data-Words

Authors Bartosz Bednarczyk , Piotr Witkowski

PDF
Thumbnail PDF

File

LIPIcs.TIME.2020.17.pdf
  • Filesize: 0.54 MB
  • 14 pages

Document Identifiers

Author Details

Bartosz Bednarczyk
  • Computational Logic Group, TU Dresden, Germany
  • Institute of Computer Science, University of Wrocław, Poland
Piotr Witkowski
  • Institute of Computer Science, University of Wrocław, Poland

Funding

  • Bednarczyk, Bartosz: supported by "Diamentowy Grant" no. DI2017 006447.
  • Witkowski, Piotr: supported by NCN grant no. 2016/21/B/ST6/01444.

Cite AsGet BibTex

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)
https://doi.org/10.4230/LIPIcs.TIME.2020.17

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Two-variable logic
  • data-words
  • VASS
  • decidability
  • undecidability
  • counting

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Rajeev Alur, Pavol Cerný, and Scott Weinstein. Algorithmic analysis of array-accessing programs. ACM Trans. Comput. Log. 2012, 2012. URL: https://doi.org/10.1145/2287718.2287727.
  2. Henrik Björklund and Mikolaj Bojańczyk. Shuffle Expressions and Words with Nested Data. In MFCS 2007, 2007. A version with an appendix available at https://www.mimuw.edu.pl/~bojan/upload/confmfcsBjorklundB07.pdf. URL: https://doi.org/10.1007/978-3-540-74456-6_66.
  3. Henrik Björklund and Thomas Schwentick. Class-Memory Automata Revisited, pages 201-215. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-48317-7_12.
  4. Mikolaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log. 2011, 2011. URL: https://doi.org/10.1145/1970398.1970403.
  5. Mikolaj Bojańczyk and Slawomir Lasota. An extension of data automata that captures XPath. LMCS 2012, 2012. URL: https://doi.org/10.2168/LMCS-8(1:5)2012.
  6. Benedikt Bollig. An Automaton over Data Words That Captures EMSO Logic. In CONCUR 2011, 2011. URL: https://doi.org/10.1007/978-3-642-23217-6_12.
  7. Benedikt Bollig, Peter Habermehl, Martin Leucker, and Benjamin Monmege. A robust class of data languages and an application to learning. LMCS 2014, 2014. URL: https://doi.org/10.2168/LMCS-10(4:19)2014.
  8. Patricia Bouyer. A logical characterization of data languages. Inf. Process. Lett. 2002, 2002. URL: https://doi.org/10.1016/S0020-0190(02)00229-6.
  9. Patricia Bouyer, Antoine Petit, and Denis Thérien. An algebraic approach to data languages and timed languages. Inf. Comput. 2003, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00038-5.
  10. Witold Charatonik, Yegor Guskov, Ian Pratt-Hartmann, and Piotr Witkowski. Two-variable First-Order Logic with Counting in Forests. In LPAR 2018, 2018. Google Scholar
  11. Witold Charatonik, Ian Pratt-Hartmann, and Piotr Witkowski. Two-Variable Logic with Counting and Data-Trees. Submitted. Available at URL: http://www.cs.man.ac.uk/~ipratt/papers/logic/c21d1e.pdf.
  12. Witold Charatonik and Piotr Witkowski. Two-variable Logic with Counting and a Linear Order. LMCS 2016, 2016. URL: https://doi.org/10.2168/LMCS-12(2:8)2016.
  13. Taolue Chen, Fu Song, and Zhilin Wu. Formal Reasoning on Infinite Data Values: An Ongoing Quest. In SETSS 2016, Chongqing, China, March 28 - April 2, 2016, 2016. URL: https://doi.org/10.1007/978-3-319-56841-6_6.
  14. Conrad Cotton-Barratt. Using Class Memory Automata in Algorithmic Game Semantics. PhD thesis, University of Oxford, UK, 2016. Google Scholar
  15. Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong. Weak and Nested Class Memory Automata. In LATA 2015, 2015. URL: https://doi.org/10.1007/978-3-319-15579-1_14.
  16. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for Petri nets is not elementary. In STOC 2019, 2019. URL: https://doi.org/10.1145/3313276.3316369.
  17. Loris D'Antoni. In the maze of data languages. CoRR, 2012. URL: http://arxiv.org/abs/1208.5980.
  18. Stéphane Demri, Diego Figueira, and M. Praveen. Reasoning about Data Repetitions with Counter Systems. LMCS 2016, 2016. URL: https://doi.org/10.2168/LMCS-12(3:1)2016.
  19. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 2009, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  20. Kousha Etessami, Moshe Y. Vardi, and Thomas Wilke. First-Order Logic with Two Variables and Unary Temporal Logic. Inf. Comput. 2002, 2002. URL: https://doi.org/10.1006/inco.2001.2953.
  21. Diego Figueira. A Decidable Two-Way Logic on Data Words. In LICS 2011, 2011. URL: https://doi.org/10.1109/LICS.2011.18.
  22. Daniel Genkin, Michael Kaminski, and Liat Peterfreund. A note on the emptiness problem for alternating finite-memory automata. Theor. Comput. Sci. 2014, 2014. URL: https://doi.org/10.1016/j.tcs.2014.01.020.
  23. Erich Grädel and Martin Otto. On Logics with Two Variables. Theor. Comput. Sci. 1999, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00308-9.
  24. Ahmet Kara. Logics on data words: Expressivity, satisfiability, model checking. PhD thesis, Technical University of Dortmund, Germany, 2016. URL: http://hdl.handle.net/2003/35216.
  25. Jérôme Leroux and Sylvain Schmitz. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In LICS 2019, 2019. URL: https://doi.org/10.1109/LICS.2019.8785796.
  26. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1967. Google Scholar
  27. Angelo Montanari, Marco Pazzaglia, and Pietro Sala. Metric propositional neighborhood logic with an equivalence relation. Acta Inf. 2016, 2016. URL: https://doi.org/10.1007/s00236-016-0256-3.
  28. Matthias Niewerth. Data definition languages for XML repository management systems. PhD thesis, Technical University of Dortmund, Germany, 2016. Google Scholar
  29. Ian Pratt-Hartmann. The Two-Variable Fragment with Counting Revisited. In WoLLIC 2010, 2010. URL: https://doi.org/10.1007/978-3-642-13824-9_4.
  30. Ian Pratt-Hartmann. The two-variable fragment with counting and equivalence. Math. Log. Q. 2015, 2015. URL: https://doi.org/10.1002/malq.201400102.
  31. Sebastian Rudolph. Presburger Concept Cardinality Constraints in Very Expressive Description Logics - Allegro sexagenarioso ma non ritardando. In Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 2019. URL: https://doi.org/10.1007/978-3-030-22102-7_25.
  32. Fu Song and Zhilin Wu. On temporal logics with data variable quantifications: Decidability and complexity. Inf. Comput. 2016, 2016. URL: https://doi.org/10.1016/j.ic.2016.08.002.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact