Extending B\"uchi Automata with Constraints on Data Values
Ahmet Kara, Tony Tan

TL;DR
This paper extends B"uchi automata to handle data values in omega-words, proving decidability of the emptiness problem and applying it to certain logical fragments for data words.
Contribution
It introduces a new automata model for data omega-words and establishes decidability results for related logical formalisms.
Findings
Decidability of emptiness for extended B"uchi automata with data.
Decidability of two-variable first-order logic for data omega-words.
Decidability of certain linear temporal logic extensions for data omega-words.
Abstract
Recently data trees and data words have received considerable amount of attention in connection with XML reasoning and system verification. These are trees or words that, in addition to labels from a finite alphabet, carry data values from an infinite alphabet (data). In general it is rather hard to obtain logics for data words and trees that are sufficiently expressive, but still have reasonable complexity for the satisfiability problem. In this paper we extend and study the notion of B\"uchi automata for omega-words with data. We prove that the emptiness problem for such extension is decidable in elementary complexity. We then apply our result to show the decidability of two kinds of logics for omega-words with data: the two-variable fragment of first-order logic and some extensions of classical linear temporal logic for omega-words with data.
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 · Logic, programming, and type systems · semigroups and automata theory
