Weak bisimulation as a congruence in MSOS

By Peter D. Mosses and Ferdinand Vesely


MSOS is a variant of structural operational semantics with a natural representation of unobservable transitions. To prove various desirable laws for programming constructs specified in MSOS, bisimulation should disregard unobservable transitions, and it should be a congruence. One approach, following Van Glabbeek, is to add abstraction rules and use strong bisimulation with MSOS specifications in an existing congruence format. Another approach is to use weak  bisimulation with specifications in an adaptation of Bloom’s WB Cool congruence format to MSOS. We compare the two approaches, and relate unobservable transitions in MSOS to equations in Rewriting Logic.

Accompanying material

This technical report is an extended version of the paper Weak bisimulation as a congruence in MSOS, to appear in the Festschrift in Honor of José Meseguer published by Springer’s Lecture Notes in Computer Science in their Festschrift Series. The appendix contains proofs of the results presented in the main body of the paper.