Safety alternating automata on data words
Ranko Lazic

TL;DR
This paper studies safety alternating automata on data words, establishing their computational complexity and exploring the decidability boundaries when extending the automata or logic features.
Contribution
It provides complexity results for safety automata with one register on data words and analyzes the impact of various extensions on decidability.
Findings
Nonemptiness is EXPSPACE-complete.
Inclusion is decidable but not primitive recursive.
Adding features like past operators or extra registers leads to undecidability.
Abstract
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. Safety one-way alternating automata with one register on infinite data words are considered, their nonemptiness is shown EXPSPACE-complete, and their inclusion decidable but not primitive recursive. The same complexity bounds are obtained for satisfiability and refinement, respectively, for the safety fragment of linear temporal logic with freeze quantification. Dropping the safety restriction, adding past temporal operators, or adding one more register, each causes undecidability.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · semigroups and automata theory · Logic, programming, and type systems
