CCS Dynamic Bisimulation is Progressing

Weak Observational Congruence (woc) defined on CCS agents is not a bisimulation since it does not require two states reached by bisimilar computations of woc agents to be still woc, e.g. α.τ.β.nil and α.β.nil are woc but τ.β.nil and β.nil are not. This fact prevents us from characterizing CCS semantics (when τ is considered invisible) as a final algebra, since the semantic function would induce an equivalence over the agents that is both a congruence and a bisimulation. In the paper we introduce a new behavioural equivalence for CCS agents, which is the coarsest among those bisimulations which are also congruences. We call it Dynamic Observational Congruence because it expresses a natural notion of equivalence for concurrent systems required to simulate each other in the presence of dynamic, i.e. run time, (re)configurations. We provide an algebraic characterization of Dynamic Congruence in terms of a universal property of finality. Furthermore we introduce Progressing Bi...

• Type: Conference
• Year: 1991
• Where: MFCS
• Authors: Ugo Montanari, Vladimiro Sassone
• Keywords: CCS Agents, MFCS 1991, Observational Congruence, Theoretical Computer Science, Weak Observational Congruence