Submitted: June 2007
Abstract
Sound and complete axiomatisations for divergence sensitive variations of weak bisimulation semantics have been studied in the past. Taking van Glabbeek’s “Linear Time – Branching Time Spectrum with Silent Moves” as a reference, only for one of them no complete axiomatisation has been known so far: strongly convergent weak bisimulation preorder. This thesis closes this gap by providing a sound and complete axiomatisation of strongly convergent weak bisimulation preorder. As a side result, this thesis also fixes a flawed completeness proof for an axiomatisation of convergent weak bisimulation preorder, first published by Walker in LICS ‘88. Furthermore, this thesis proposes an alternative predicate for syntactical divergence that is simpler than the original one used in op.cit. and shows that the two predicates indeed coincide.