Weak Bisimulation as a Congruence in MSOS

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