Alternating Good-for-MDP Automata

TL;DR

This paper introduces alternating good-for-MDP automata, which are more succinct than nondeterministic B"uchi automata and can be efficiently derived from deterministic Streett automata, improving automata translation for reinforcement learning.

Contribution

It extends the good-for-MDP automata concept to alternating automata, enabling more efficient translations from deterministic Streett automata with exponential size reductions.

Findings

Alternating good-for-MDP automata are bi-linear in size, similar to nondeterministic GFM automata.

They can be exponentially more succinct than minimal nondeterministic B"uchi automata.

The approach reduces translation complexity from deterministic Streett automata.

Abstract

When omega-regular objectives were first proposed in model-free reinforcement learning (RL) for controlling MDPs, deterministic Rabin automata were used in an attempt to provide a direct translation from their transitions to scalar values. While these translations failed, it has turned out that it is possible to repair them by using good-for-MDPs (GFM) B\"uchi automata instead. These are nondeterministic B\"uchi automata with a restricted type of nondeterminism, albeit not as restricted as in good-for-games automata. Indeed, deterministic Rabin automata have a pretty straightforward translation to such GFM automata, which is bi-linear in the number of states and pairs. Interestingly, the same cannot be said for deterministic Streett automata: a translation to nondeterministic Rabin or B\"uchi automata comes at an exponential cost, even without requiring the target automaton to be good-for-MDPs. Do we have to pay more than that to obtain a good-for-MDP automaton? The surprising answer is that we have to pay significantly less when we instead expand the good-for-MDP property to alternating automata: like the nondeterministic GFM automata obtained from deterministic Rabin automata, the alternating good-for-MDP automata we produce from deterministic Streett automata are bi-linear in the the size of the deterministic automaton and its index, and can therefore be exponentially more succinct than minimal nondeterministic B\"uchi automata.