Abstract:
Asynchrono us 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 Büchi asynchronous automata, which
accept precisely the class of 
-regular trace languages. Like their
sequential counterparts, these automata need to be non-deterministic in order
to capture all -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 secondorder logics.
Subsequently, Diekert and
Muscholl solved the complementation problem by showing that with a Muller
acceptance condition, deterministic automata suffice for recognizing
-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 Büchi asynchronous automata, which generalizes Safra's construction for sequential Büchi automata. As in the sequential case, the blow-up in the state space is essentially that of the underlying subset construction.
Available as PostScript, PDF, DVI.