Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Synthesising Asynchronous Automata from Fair Specifications

Béatrice Bérard, Benjamin Monmege, B Srivathsan, Arnab Sur

TL;DR

A new construction to synthesise an AA is presented, conceptually simpler, and 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 parameter of fairness.

Abstract

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 as a deterministic finite-state automaton (DFA) and a distribution of the alphabet into local alphabets for each process. The translation is particularly complex and has been revisited several times. In this work, we revisit this construction on a restricted class of fair specifications: a DFA described 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 is conceptually simpler and 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 parameter of fairness (the length of the longest word that can be read in the DFA in which not every process participates). Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures.

Synthesising Asynchronous Automata from Fair Specifications

TL;DR

A new construction to synthesise an AA is presented, conceptually simpler, and 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 parameter of fairness.

Abstract

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 as a deterministic finite-state automaton (DFA) and a distribution of the alphabet into local alphabets for each process. The translation is particularly complex and has been revisited several times. In this work, we revisit this construction on a restricted class of fair specifications: a DFA described 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 is conceptually simpler and 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 parameter of fairness (the length of the longest word that can be read in the DFA in which not every process participates). Finally, we show how this construction can be combined with an existing construction for hierarchical process architectures.

Paper Structure

This paper contains 15 sections, 27 theorems, 6 equations, 6 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Fair specifications
  4. A Zielonka's theorem for fair trace languages
  5. Combining fairness with acyclic communication
  6. Conclusion
  7. Appendix for Section \ref{['sec:prelim']}
  8. Proof of Section \ref{['sec:fair']}
  9. Deciding k-fairness of a DFA
  10. Full proof of Theorem \ref{['thm:fair-AA']}
  11. The construction of an infinite AA based on the Foata normal form
  12. Introduction of unbounded counters to cut the views of processes
  13. Modulo counting to obtain a finite AA
  14. Proofs of Section \ref{['sec:combination']}
  15. The detailed construction for Section \ref{['sec:combination']}.

Key Result

Lemma 4

Let $t$ be a trace and $s$ an ideal of $t$. Then for all $i \leq |s|_{\mathsf F}$, $\mathsf F(s)_i \subseteq \mathsf F(t)_i$.

Figures (6)

  • Figure 1: Left: An AA. Right: its semantics seens as a DFA
  • Figure 2: (Left) A DFA satisfying the diamond property; (Right) a word $w$, the trace $[w]$ and its Foata normal form $\mathsf F([w])$.
  • Figure 3: Run of the infinite asynchronous automaton corresponding to the finite state automaton of Figure \ref{['fig:running-eg-intro']}, on the word $abcdbdcb$
  • Figure 4: Illustrating one transition in the AA that maintains an unbounded counter
  • Figure 5: Illustrating one transition in the finite AA $\mathcal{B}$ that counts modulo $2k$
  • ...and 1 more figures

Theorems & Definitions (42)

  • Example 1
  • Example 2
  • Example 3
  • Example 4
  • Lemma 4
  • Example 5
  • Lemma 5
  • Example 6
  • Definition 7
  • Definition 8
  • ...and 32 more