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:


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

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


  • I={I ssS}I = \{I_s\mid s\in S\} is a family of irreflexive, symmetric binary relations, I sI_s on EE such that whenever a 1I sa 2a_1I_s a_2 (with a 1,a 2Ea_1,a_2 \in E), there exist transitions (s,a 1,s 1)(s,a_1,s_1), (s,a 2,s 2)(s,a_2,s_2), (s 1,a 2,r)(s_1,a_2,r), and (s 2,a 1,r)(s_2,a_1,r) in TranTran.


Last revised on June 11, 2022 at 10:38:33. See the history of this page for a list of all contributions to it.