Since the mid-90’s, the automata techniques have been one of the dominant approaches to temporal verification. In order to check whether program P satisfies temporal specification S, one builds a structure A_P capturing the executions of P, and an automaton A_S capturing the traces allowed by S. This way, the verification problem reduces to check whether A_P ⊂ A_S, or equivalently A_P ∩ (∁ A_S) is empty. The verification problem is then reduced to intersection and complementation of automata.

The classical translations from LTL into w-automata proceeds by first transforming the expression into negation normal form, and then constructing a non-deterministic Büchi automata (NBW). Alternatively, one can use an alternating Büchi automata (ABW), which avoids the state explosion in the construction. However, these approaches are not “algebraic” in the sense the automata is not built from automata for smaller expressions by application of simple automata constructions. Moreover, it only works for logics (LTL) with negation normal forms.

I will justify the advantages of using strong alternating parity automata (APW), and sketch the proof of complexity of the emptyness problem for APW.

I will introduce the necessary concepts from automata theory, game theory and complexity theory, to make the talk as self-contained as possible.

This is joint work with Moshe Vardi and Martin Leucker.