A new view on the robustness of behavioural equations

Photograph of Ken Madlener

Ken Madlener

(Radboud University Nijmegen)

Sound behavioural equations may become unsound after conservative extensions of the underlying operational semantics. The preservation of sound equations has been studied by Mosses, Mousavi and Reniers for several notions of bisimilarity. In particular, Formal Hypothesis (FH) bisimilarity, due to Robert de Simone, is preserved by disjoint extensions that do not add labels. In this talk I will revisit this result, but from the point of view of bi-algebraic semantics, due to Turi and Plotkin. In addition, I will present a work-in-progress formalization in the proof assistant Coq.
Thursday 17th November 2011, 14:00
Department of Computer Science