Synthesising Asynchronous Automata from Fair Specifications
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911407787737088 |
|---|---|
| author | Bérard, Béatrice Monmege, Benjamin Srivathsan, B Sur, Arnab |
| author_facet | Bérard, Béatrice Monmege, Benjamin Srivathsan, B Sur, Arnab |
| contents | Asynchronous automata are a model of distributed finite state processes synchronising on shared actions. A celebrated result by Zielonka shows how a deterministic asynchronous automaton (AA) can be synthesised, starting from two inputs: a global specification given as a deterministic finite-state automaton (DFA) and a distribution of the alphabet into local alphabets for each process. The DFA to AA translation is particularly complex and has been revisited several times, with no complete prototype tool provided for the full construction. In this work, we revisit this construction on a restricted class of "fair" specifications: a DFA describes a fair specification if in every loop, all processes participate in at least one action, so no process is starved. For fair specifications, we present a new construction to synthesise an AA. Our construction results in an AA where every process has a number of local states that is linear in the number of states of the DFA, and where the only exponential explosion is related to a fairness parameter: the length of the longest word that can be read in the DFA in which not every process participates. We have implemented a prototype tool showing how it can be applied to some examples, in particular, a concrete one: the dining philosophers problem. Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures, in order to relax the fairness assumption. We have implemented a prototype tool showing how it can be applied to some examples, in particular, a concrete one: the dining philosophers problem. Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures, in order to relax the fairness assumption. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_14623 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Synthesising Asynchronous Automata from Fair Specifications Bérard, Béatrice Monmege, Benjamin Srivathsan, B Sur, Arnab Formal Languages and Automata Theory Asynchronous automata are a model of distributed finite state processes synchronising on shared actions. A celebrated result by Zielonka shows how a deterministic asynchronous automaton (AA) can be synthesised, starting from two inputs: a global specification given as a deterministic finite-state automaton (DFA) and a distribution of the alphabet into local alphabets for each process. The DFA to AA translation is particularly complex and has been revisited several times, with no complete prototype tool provided for the full construction. In this work, we revisit this construction on a restricted class of "fair" specifications: a DFA describes a fair specification if in every loop, all processes participate in at least one action, so no process is starved. For fair specifications, we present a new construction to synthesise an AA. Our construction results in an AA where every process has a number of local states that is linear in the number of states of the DFA, and where the only exponential explosion is related to a fairness parameter: the length of the longest word that can be read in the DFA in which not every process participates. We have implemented a prototype tool showing how it can be applied to some examples, in particular, a concrete one: the dining philosophers problem. Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures, in order to relax the fairness assumption. We have implemented a prototype tool showing how it can be applied to some examples, in particular, a concrete one: the dining philosophers problem. Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures, in order to relax the fairness assumption. |
| title | Synthesising Asynchronous Automata from Fair Specifications |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2504.14623 |