N Klarlund, M Mukund and M Sohoni
Proc. FSTTCS 15, Springer LNCS 1026 (1995) 456-470.
© Springer-Verlag Berlin Heidelberg
Büchi asynchronous automata are a natural distributed machine model for recognizing w-regular trace languages. Like their sequential counterparts, these automata need to be non-deterministic in order to capture all w-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.
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.