Iteration theories of synchronization trees (Q1207946)

\textit{R. Milner} introduced [A calculus of communicating systems, Lect. Notes Comput. Sci. 92 (1980; Zbl 0452.68027)], and used (1984) synchronization trees (STs) for describing the behaviour of communicating processes, and conjectured that the bisimulation equivalence classes of trees can be characterized within C. C. Elgot's iteration theories. The present paper proves that Milner's conjecture was essentially correct and shows that STs form an iteration theory in a natural way, namely an \(\omega\)-continuous 2-theory. Grove theories and synchronization theories (as preserving a grove iteration theory morphism) are introduced. The regular STs are characterized as free synchronization theories, and their corresponding axioms are provided. Finally, the bisimulation equivalence classes of regular STs are shown to be freely generated within the \(\omega\)-idempotent synchronization theories.