Determinizing Asynchronous Automata on Infinite Inputs

Abstract

Asynchronous automata are a natural distributed machine model
for recognizing trace languages - languages defined over an alphabet
equipped with an independence relation.
To handle infinite traces, Gastin and Petit introduced Buchi asynchronous
automata, which accept precisely the class of omega-regular trace
languages. Like their sequential counterparts, these automata need to
be non-deterministic in order to capture all omega-regular languages. Thus
complementation of these automata is non-trivial. Complementation
is an important operation because it is fundamental for treating the
logical connective "not" in decision procedures for monadic second-order
logics. Subsequently, Diekert and Muscholl solved the complementation
problem by showing that with a Muller acceptance condition, deterministic
automata suffice for recognizing omega-regular trace languages.
However, a direct determinization procedure, extending the classical
subset construction, has proved elusive.
In this paper, we present a direct determinization procedure for
Buchi asynchronous automata, which generalizes Safra's construction
for sequential Buchi automata. As in the sequential case, the blow-up
in the state space is essentially that of the underlying subset construction.