CCS dynamic bisimulation is progressing
[For the entire collection see Zbl 0753.00030.] 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 congruences 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 processing bisimulation, which forces processes to simulate each other performing explicit steps. We provide an algebraic characterization of it in terms of finality, two characterizations via modal logic in the style of Hennessy-Melner logic and a complete axiomatization for finite agents. Finally, we prove that dynamic congruence and progressing bisimulation coincide for CCS agents.
- Observational congruences for dynamically reconfigurable tile systems
- Verifying persistent security properties
- Architectural CCS
- scientific article; zbMATH DE number 92600 (Why is no real title available?)
- A general account of coinduction up-to
- Action Refinement in Process Algebra and Security Issues
- On weak bisimilarities in CCSK
This page was built for publication: CCS dynamic bisimulation is progressing
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4035257)
