Abstraction Refinement for Trace Inclusion of Data Automata

Abstract. A data automaton is a finite automaton equipped with vari-ables (counters) ranging over a multi-sorted data domain. The transitions of the automaton are controlled by first-order formulae, encoding guards and updates. We observe, in addition to the finite alphabet of actions, the values taken by the counters along a run of the automaton, and consider the data languages recognized by these automata. The problem addressed in this paper is the inclusion between the data languages recognized by such automata. Since the problem is undecid-able, we give an abstraction-refinement semi-algorithm, proved to be sound and complete, but whose termination is not guaranteed. The novel feature of our technique is checking for inclusion, without at-tempting to complement one of the automata, i.e. working in the spirit of antichain-based non-deterministic inclusion checking for finite automata [1]. The method described here has various applications, ranging from logics of unbounded data structures, such as arrays or heaps, to the ver-ification of real-time systems.