2011/06/04 by Zhilin Wu
Computer Science · #Formal Methods in Verification #Machine Learning and Algorithms #cs.FL #semigroups and automata theory
paper · pdf · doi:10.4204/eptcs.54.9
published as EPTCS 54, 2011, pp. 116-130 · In Proceedings GandALF 2011, arXiv:1106.0814
openalex publication_date 2011/06/04 · arxiv created 2011/06/07 · arxiv updated 2011/06/08 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/01
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 of array-accessing programs.