WG211/M11Mosses

Component-based bisimilarity by Peter Mosses

Given an SOS for the dynamic semantics of some programming language, various equational laws may be proved sound for strong bisimilarity (e.g., associativity of sequencing). But suppose the language specification is subsequently extended with new constructs and their SOS rules: sound laws may then become unsound - even when rules are restricted to simple congruence formats such as GSOS.

In this talk, we consider a non-standard notion of bisimilarity (due to De Simone, 1985) which ensures that sound laws are preserved by language extensions. In contrast to the standard notion, it enables a component-based approach to establishing equational laws: bisimilarity of two terms can be proved with reference only to the SOS rules for the construct(s) involved, and the terms remain bisimilar when those constructs are combined with other constructs in a complete language.