Document Open Access Logo

Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and Infix

Authors Jakub Michaliszyn , Jan Otop , Piotr Wieczorek

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.3.pdf
  • Filesize: 0.71 MB
  • 16 pages

Document Identifiers

Author Details

Jakub Michaliszyn
  • University of Wrocław, Poland
Jan Otop
  • University of Wrocław, Poland
Piotr Wieczorek
  • University of Wrocław, Poland

Funding

This work was supported by the National Science Centre (NCN), Poland under grant 2020/39/B/ST6/00521.

Cite As Get BibTex

Jakub Michaliszyn, Jan Otop, and Piotr Wieczorek. Reachability and Bounded Emptiness Problems of Constraint Automata with Prefix, Suffix and Infix. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 3:1-3:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.3

Abstract

We study constraint automata, which are finite-state automata over infinite alphabets consisting of tuples of words. A constraint automaton can compare the words of the consecutive tuples using Boolean combinations of the relations prefix, suffix, infix and equality.
First, we show that the reachability problem of such automata is PSpace-complete. Second, we study automata over infinite sequences with Büchi conditions. We show that the problem: given a constraint automaton, is there a bound B and a sequence of tuples of words of length bounded by B, which is accepted by the automaton, is also PSpace-complete. These results contribute towards solving the long-standing open problem of the decidability of the emptiness problem for constraint automata, in which the words can have arbitrary lengths.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • constraint automata
  • emptiness problem

Metrics

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

References

  1. Mikołaj Bojańczyk. Atom book, September 2019. URL: https://www.mimuw.edu.pl/~bojan/upload/main-10.pdf.
  2. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011. URL: https://doi.org/10.1145/1970398.1970403.
  3. Claudia Carapelle, Shiguang Feng, Alexander Kartzow, and Markus Lohrey. Satisfiability of ECTL_∗ with local tree constraints. Theory Comput. Syst., 61(2):689-720, 2017. URL: https://doi.org/10.1007/s00224-016-9724-y.
  4. Claudia Carapelle, Alexander Kartzow, and Markus Lohrey. Satisfiability of ECTL_∗ with constraints. J.omput. Syst. Sci., 82(5):826-855, 2016. URL: https://doi.org/10.1016/j.jcss.2016.02.002.
  5. Karlis Cerans. Deciding properties of integral relational automata. In Automata, Languages and Programming, 21st International Colloquium, ICALP94, Jerusalem, Israel, July 11-14, 1994, Proceedings, volume 820, pages 35-46. Springer, 1994. URL: https://doi.org/10.1007/3-540-58201-0_56.
  6. Stéphane Demri and Morgan Deters. Temporal logics on strings with prefix relation. J. Log. Comput., 26(3):989-1017, 2016. URL: https://doi.org/10.1093/logcom/exv028.
  7. Stéphane Demri and Deepak D'Souza. An automata-theoretic approach to constraint LTL. Inf. Comput., 205(3):380-415, 2007. URL: https://doi.org/10.1016/j.ic.2006.09.006.
  8. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  9. Stéphane Demri and Karin Quaas. Concrete domains in logics: a survey. ACM SIGLOG News, 8(3):6-29, 2021. URL: https://doi.org/10.1145/3477986.3477988.
  10. Stéphane Demri and Karin Quaas. Constraint automata on infinite data trees: From CTL(Z)/CTL*(Z) to decision procedures, 2023. URL: https://arxiv.org/abs/2302.05327.
  11. Régis Gascon. An automata-based approach for CTL∗ with constraints. In Joint Proceedings of the 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems, INFINITY 2006 / 2007 / 2008, volume 239 of Electronic Notes in Theoretical Computer Science, pages 193-211. Elsevier, 2009. URL: https://doi.org/10.1016/j.entcs.2009.05.040.
  12. Simon Halfon, Philippe Schnoebelen, and Georg Zetzsche. Decidability, complexity, and expressiveness of first-order logic over the subword ordering. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005141.
  13. Artur Jeż. Recompression: A simple and powerful technique for word equations. J. ACM, 63(1):4:1-4:51, 2016. URL: https://doi.org/10.1145/2743014.
  14. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  15. Prateek Karandikar and Philippe Schnoebelen. Decidability in the logic of subsequences and supersequences. In 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, volume 45 of LIPIcs, pages 84-97, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.84.
  16. Alexander Kartzow and Thomas Weidner. Model checking constraint LTL over trees, 2015. URL: https://arxiv.org/abs/1504.06105.
  17. Dietrich Kuske. Theories of orders on the set of words. RAIRO Theor. Informatics Appl., 40(1):53-74, 2006. URL: https://doi.org/10.1051/ita:2005039.
  18. Dietrich Kuske and Georg Zetzsche. Languages ordered by the subword order. In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of ETAPS 2019, Proceedings, volume 11425 of Lecture Notes in Computer Science, pages 348-364. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_20.
  19. Leonid Libkin, Wim Martens, and Domagoj Vrgoc. Querying graphs with data. J. ACM, 63(2):14:1-14:53, 2016. URL: https://doi.org/10.1145/2850413.
  20. Antonio Lozano and José L Balcázar. The complexity of graph problems for succinctly represented graphs. In International Workshop on Graph-Theoretic Concepts in Computer Science, pages 277-286. Springer, 1989. Google Scholar
  21. G. S. Makanin. The problem of solvability of equations in a free semigroup. Mathematics of The Ussr-sbornik, 32:129-198, 1977. Google Scholar
  22. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Log., 5(3):403-435, 2004. URL: https://doi.org/10.1145/1013560.1013562.
  23. Dominik Peteler and Karin Quaas. Deciding emptiness for constraint automata on strings with the prefix and suffix order. In 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, volume 241 of LIPIcs, pages 76:1-76:15, 2022. URL: https://doi.org/10.4230/LIPIcs.MFCS.2022.76.
  24. Wojciech Plandowski. Satisfiability of word equations with constants is in PSPACE. J. ACM, 51(3):483-496, 2004. URL: https://doi.org/10.1145/990308.990312.
  25. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1-35, 1969. Google Scholar
  26. Luc Segoufin and Szymon Toruńczyk. Automata based verification over linearly ordered data domains. In 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, volume 9 of LIPIcs, pages 81-92. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.STACS.2011.81.
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 About DROPS Imprint Privacy Contact