# The Impact of Alternation

## TL;DR

This paper extends alternating automata to infinite data domains, demonstrating linear-time Boolean operations and proposing semi-algorithms for the undecidable emptiness problem, with practical implementation and experimental evaluation.

## Contribution

It introduces a new class of alternating automata over infinite alphabets with efficient Boolean operations and semi-algorithms for emptiness, supported by implementation and experiments.

## Key findings

- Linear-time union, intersection, and complementation for the new automata.
- Two semi-algorithms inspired by abstraction refinement methods.
- Experimental comparison of the proposed semi-algorithms.

## Abstract

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 \cite{HJMS02} and the \impact~ semi-algorithm \cite{mcmillan06}. We have implemented both methods and report the results of an experimental comparison.