A complete axiomatisation for observational congruence of finite-state behaviours (Q1263984)

Finite state automata, with non-determinism and silent transitions, are seen as congruence classes under the weak bisimulation or observational equivalence (Park, Miller). This paper is an extension of the case where all computations are finite. A comparison shows that CCS is more general, however, the method shown here is suitable enough to describe communicating protocols.