Determinizing Asynchronous Automata on Infinite Inputs
DOI:
https://doi.org/10.7146/brics.v2i58.19959Resumé
Asynchronous automata are a natural distributed machine modelfor 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.
Downloads
Publiceret
1995-11-28
Citation/Eksport
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
Nummer
Sektion
Artikler
Licens
Authors who publish with this journal agree to the following terms:- Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
- Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
- Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).