Strong bisimulation is preserved by restriction

The image shows our proof that bisimulation is preserved by restriction.

• Isabelle notation
  • -- Meta level universal quantification
  • -- Meta level implication
  • by ... -- The text following by tells Isabelle how to prove a particular statement. For example "blast" refers to Isabelle's brute force search for proofs.
• Formalisation notation
  • -- The binary relation Rel is equivariant, i.e. closed under permutations. Normally when doing proofs on pi one reasons about injective substitutions. We instead use permutations since they are supported by the nominal package.
  • -- A predicate for simulation. For every action Q can do, P can mimic that action and the derivatives of the two processes are in the binary relation Rel.

One of our contributions is how we encode bisimulation in Isabelle. We use the following coinductive definition: . Most bisimulation proofs only involve proving simulation one way and then Isabelle infers the symmetric argument automatically.

Another key contribution is the way that proofs at the simulation level are made. Since the definition of simulation applies to an arbitrary binary relation Rel, properties about that Rel has to be assumed in order to do the proof. The lemma for proving that simulation is preserved by restriction is shown on the right. The intuition is that if Q simulates P and the derivatives are in Rel, then restricting any name to the processes preserves simulation for some relation Rel'. The proof obligations are that Rel and Rel' are equivariant, and that all pairs of processes in Rel are in Rel', for all possible name restrictions x. When taking the step to bisimulation one has to prove that bisimulation has the properties required by the relations in the simulation proof as demonstrated bellow.