Determinizing Asynchronous Automata on Infinite Inputs

Nils Klarlund, Madhavan Mukund, Milind Sohoni


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.

Full Text:


This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the State and University Library and Aarhus University Library