Abstraction refinement for emptiness checking of alternating data automata. (English) Zbl 1423.68255

Iosif, Radu; Xu, Xiao

Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 10806, 93-111 (2018).

Summary: Alternating automata have been widely used to model and verify systems that handle data from finite domains, such as communication protocols or hardware. The main advantage of the alternating model of computation is that complementation is possible in linear time, thus allowing to concisely encode trace inclusion problems that occur often in verification. In this paper we consider alternating automata over infinite alphabets, whose transition rules are formulae in a combined theory of Booleans and some infinite data domain, that relate past and current values of the data variables. The data theory is not fixed, but rather it is a parameter of the class. We show that union, intersection and complementation are possible in linear time in this model and, though the emptiness problem is undecidable, we provide two efficient semi-algorithms, inspired by two state-of-the-art abstraction refinement model checking methods: lazy predicate abstraction [T. A. Henzinger et al., in: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2002. New York, NY: Association for Computing Machinery (ACM). 58–70 (2002; Zbl 1323.68374)] and the Impact semi-algorithm [K. L. McMillan, Lect. Notes Comput. Sci. 4144, 123–136 (2006; Zbl 1188.68196)]. We have implemented both methods and report the results of an experimental comparison.
For the entire collection see [Zbl 1408.68007].

MSC:

68Q45	Formal languages and automata
68Q60	Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 1323.68374; Zbl 1188.68196