Document Open Access Logo

Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order

Authors Dominik Peteler, Karin Quaas

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.76.pdf
  • Filesize: 0.61 MB
  • 15 pages

Document Identifiers

Author Details

Dominik Peteler
  • Universität Leipzig, Germany
Karin Quaas
  • Universität Leipzig, Germany

Funding

  • Quaas, Karin: Funded by the Deutsche Forschungsgemeinschaft (DFG), project 406907430.

Acknowledgements

We would like to thank the anonymous reviewers for their very careful reading and many insightful comments that led to the improvement of this article.

Cite As Get BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 76:1-76:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.MFCS.2022.76

Abstract

We study constraint automata that accept data languages on finite string values. Each transition of the automaton is labelled with a constraint restricting the string value at the current and the next position of the data word in terms of the prefix and the suffix order. We prove that the emptiness problem for such constraint automata with Büchi acceptance condition is NL-complete. We remark that since the constraints are formed by two partial orders, prefix and suffix, we cannot exploit existing techniques for similar formalisms. Our decision procedure relies on a decidable characterization for those infinite paths in the graph underlying the automaton that can be completed with string values to yield a Büchi-accepting run. Our result is - to the best of our knowledge - the first work in this context that considers both prefix and suffix, and it is a first step into answering an open question posed by Demri and Deters.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Data Languages
  • Strings
  • Constraints
  • Prefix
  • Suffix
  • Automata
  • Linear Temporal Logic

Metrics

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

References

  1. Roberto Amadini, Graeme Gange, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. String constraint solving: Past, present and future. In ECAI 2020 - 24th European Conference on Artificial Intelligence, volume 325, pages 2875-2876. IOS Press, 2020. URL: https://doi.org/10.3233/FAIA200431.
  2. Philippe Balbiani and Jean-François Condotta. Computational complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning. In Frontiers of Combining Systems, pages 162-176, 2002. Google Scholar
  3. Mikolaj Bojanczyk. Atom Book. https://www.mimuw.edu.pl/ bojan/paper/atom-book, 2019. URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  4. Mikolaj Bojanczyk, Bartek Klin, and Joshua Moerman. Orbit-finite-dimensional vector spaces and weighted register automata. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-13. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470634.
  5. 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.
  6. Claudia Carapelle, Alexander Kartzow, and Markus Lohrey. Satisfiability of ECTL^* with constraints. J. Comput. Syst. Sci., 82(5):826-855, 2016. URL: https://doi.org/10.1016/j.jcss.2016.02.002.
  7. Karlis Cerans. Deciding properties of integral relational automata. In Automata, Languages and Programming, 21st International Colloquium, ICALP94, pages 35-46, 1994. URL: https://doi.org/10.1007/3-540-58201-0_56.
  8. Wojciech Czerwinski, Antoine Mottet, and Karin Quaas. New techniques for universality in unambiguous register automata. In 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, volume 198 of LIPIcs, pages 129:1-129:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.129.
  9. 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.
  10. 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.
  11. Stéphane Demri and Régis Gascon. Verification of qualitative Z constraints. Theor. Comput. Sci., 409(1):24-40, 2008. URL: https://doi.org/10.1016/j.tcs.2008.07.023.
  12. Stéphane Demri and Régis Gascon. The effects of bounding syntactic resources on presburger LTL. J. Log. Comput., 19(6):1541-1575, 2009. URL: https://doi.org/10.1093/logcom/exp037.
  13. 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.
  14. 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.
  15. Régis Gascon. An automata-based approach for CTL^* with constraints. Electr. Notes Theor. Comput. Sci., 239:193-211, 2009. URL: https://doi.org/10.1016/j.entcs.2009.05.040.
  16. 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 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005141.
  17. 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.
  18. 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. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.84.
  19. Alexander Kartzow and Thomas Weidner. Model checking constraint LTL over trees. CoRR, abs/1504.06105, 2015. URL: http://arxiv.org/abs/1504.06105.
  20. 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.
  21. Dietrich Kuske and Georg Zetzsche. Languages ordered by the subword order. In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, volume 11425 of LNCS, pages 348-364. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_20.
  22. Gennady S. Makanin. The problem of solvability of equations in a free semi-group. Math. USSR Sbornik, 32(2):129-198, 1977. Google Scholar
  23. Marvin Minsky. Computation, Finite and Infinite Machines. Prentice Hall, 1967. Google Scholar
  24. 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.
  25. Joël Ouaknine and James Worrell. On the language inclusion problem for timed automata: Closing a decidability gap. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 54-63. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319600.
  26. 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.
  27. Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the AMS, 141:1-23, 1969. Google Scholar
  28. Luc Segoufin and Szymon Torunczyk. 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. A technical report containing proofs that we refer here to can be found under URL: https://www.mimuw.edu.pl/~szymtor//papers/regdata.pdf.
  29. Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the Symposium on Logic in Computer Science (LICS '86), pages 332-344, 1986. Google Scholar
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