A Decidable Extension of Data Automata
Zhilin Wu (State Key Laboratory of Computer Science, Institute of, Software, Chinese Academy of Sciences)

TL;DR
This paper introduces a new decidable extension of data automata called class automata with priority class condition, linking it to priority multicounter automata and extending analysis capabilities for array programs.
Contribution
It proposes a novel decidable class automata model with priority class condition, expanding the theoretical framework and practical applications in data automata.
Findings
Decidability of the new model established via correspondence with priority multicounter automata.
Completes the theoretical link between class automata conditions and counter machine models.
Extended decidability results for array-accessing program analysis.
Abstract
Data automata on data words is a decidable model proposed by Boja\'nczyk et al. in 2006. Class automata, introduced recently by Boja\'nczyk and Lasota, is an extension of data automata which unifies different automata models on data words. The nonemptiness of class automata is undecidable, since class automata can simulate two-counter machines. In this paper, a decidable model called class automata with priority class condition, which restricts class automata but strictly extends data automata, is proposed. The decidability of this model is obtained by establishing a correspondence with priority multicounter automata. This correspondence also completes the picture of the links between various class conditions of class automata and various models of counter machines. Moreover, this model is applied to extend a decidability result of Alur, Cern\'y and Weinstein on the algorithmic analysis…
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.
