On the Succinctness of Alternating Parity Good-for-Games Automata

TL;DR

This paper investigates alternating parity good-for-games automata, demonstrating their potential for exponential succinctness over nondeterministic and universal automata, and analyzing the complexity of related decision problems.

Contribution

It introduces the concept of alternating GFG automata, provides a determinisation procedure, and analyzes the complexity of recognizing GFG and half-GFG properties.

Findings

Alternating GFG automata can be exponentially more succinct.

A single exponential determinisation procedure is presented.

Recognizing GFG automata is in EXPTIME; half-GFGness is PSpace-hard.

Abstract

We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG. We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is PSpace-hard already for alternating automata on finite words.