eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-08-22
76:1
76:15
10.4230/LIPIcs.MFCS.2022.76
article
Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order
Peteler, Dominik
1
Quaas, Karin
1
Universität Leipzig, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol241-mfcs2022/LIPIcs.MFCS.2022.76/LIPIcs.MFCS.2022.76.pdf
Data Languages
Strings
Constraints
Prefix
Suffix
Automata
Linear Temporal Logic