Bisimulation

Stream: computer science

[Fabrizio Montesi]

I've completed the proof that (strong) Bisimulations equipped with union form a BoundedOrder and a SemilatticeSup (a join-semilattice). As expected, the bottom element is the empty relation and the top element is Bisimilarity. :)

I've used Subtype to formalise the type of all bisimulations, so things look like this:

instance : SemilatticeSup ({r // Bisimulation lts r}) where ...
instance : BoundedOrder ({r // Bisimulation lts r}) where ...

[Fabrizio Montesi]

calc, grind, and simp are very nice helpers in bisimilarity proofs. Here's a proof for CCS that 0 | P ~ P knowing that P | Q ~ Q | P and P | 0 ~ P.

theorem bisimilarity_nil_par : (par nil p) ~[@lts Name Constant defs] p :=
  calc
    (par nil p) ~[@lts Name Constant defs] (par p nil) := by grind -- 0 | P ~ P | 0
    _ ~[@lts Name Constant defs] p := by simp -- P | 0 ~ P

[Fabrizio Montesi]

Testing a bundled definition of Bisimulation, and holy cow does grind shine. With the right annotations, it managed to prove that bisimilarity is a bisimulation.

def Bisimilarity (lts : Lts State Label) : Bisimulation lts where
  rel s1 s2 := ∃ r : Bisimulation lts, r s1 s2
  is_bisimulation := by grind