IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2009 > Emptiness of Alternating Parity Automata on Words is in PSPACE with applications to temporal verification

Cesar Sanchez

Tuesday, February 3, 2009

11:00am Meeting room 302 (Mountain View), level 3

Cesar Sanchez, Assistant Research Professor, IMDEA Software Institute

Emptiness of Alternating Parity Automata on Words is in PSPACE with applications to temporal verification

Abstract:

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.