Determinizing Asynchronous Automata on Infinite Inputs

  • Nils Klarlund
  • Madhavan Mukund
  • Milind Sohoni

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.
Published
1995-11-28
How to Cite
Klarlund, N., Mukund, M., & Sohoni, M. (1995). Determinizing Asynchronous Automata on Infinite Inputs. BRICS Report Series, 2(58). https://doi.org/10.7146/brics.v2i58.19959