nLab asynchronous automaton

Asynchronous automata are a generalisation of both transition systems and Mazurkiewicz traces. Their study has influences other models for concurrency such as transition systems with independence (also called asynchronous transition systems). The idea is to decorate transition systems with an independence relation (much as in (Mazurkiewicz) trace alphabets) between actions that allow one to distinguish true concurrency from mutual exclusion (i.e. non-determinism). Following the paper by Goubault and Mimram, we use a slight modification called automata with concurrency relations:

Definition

An automaton with concurrency relations $(S,i,E,Tran,I)$ consists of

• a transition system $(S,i,E,Tran)$, such that whenever $(s,a,s')$, and $(s,a,s'')$ are in $Tran$, then $s' = s''$;

and

• $I = \{I_s\mid s\in S\}$ is a family of irreflexive, symmetric binary relations, $I_s$ on $E$ such that whenever $a_1I_s a_2$ (with $a_1,a_2 \in E$), there exist transitions $(s,a_1,s_1)$, $(s,a_2,s_2)$, $(s_1,a_2,r)$, and $(s_2,a_1,r)$ in $Tran$.

References

• Eric Goubault and Samuel Mimram, Formal Relationships Between Geometrical and Classical Models for Concurrency