• People
• Events
• Research

Context-Dependent Bisimulation between Processes

Abstract: In recent years several equivalences between nondeterministic and concurrent processes have been proposed in order to capture different notions of the extensional behaviour of a process. Usually the equivalences are congruences wrt. the process constructing operations in order to support hierarchic development and verification of systems. With the purpose of achieving more flexible hierarchic development methods we suggest parameterizing the equivalence with information about contexts.

We carry this suggestion out in full for the bisimulation equivalence, which we parameterize with a special type of context information called environments. The resulting parameterized equivalence is shown to have a large number of pleasant properties including a useful characterization of the information ordering on environments and a construction for producing the maximal environment identifying any two given processes.

Based on an investigation of how contexts transform environments it is shown how to reduce parameterized equivalence problems over composite processes to parameterized equivalence problems involving only the inner components of the processes. These results constitute the main tools provided by this thesis for hierarchic verification of systems.

All the results obtained for the parameterized bisimulation equivalence are extended to a similarly parameterized version of weak bisimulation equivalence . A worked example demonstrates the use of these extensions in correctness proofs.

Complete proof systems for the parameterized bisimulation equivalence for various combinations of the process and environment system are presented, extending existing proof systems for (unparameterized) bisimulation equivalence.

Finally, a PROLOG system for constructing bisimulations over CCS expressions has been implemented, verified and demonstrated.
Ph.D. Thesis - Price £7.00

LFCS report ECS-LFCS-86-4