Publications:Robustness of equations under operational extensions

Jump to: navigation, search

Do not edit this section

Keep all hand-made modifications below

Title Robustness of equations under operational extensions
Author P. D. Mosses and Mohammad Reza Mousavi and M. A. Reniers
Year 2010
PublicationType Conference Paper
HostPublication Proceedings 17th International Workshop on Expressiveness in Concurrency
Conference 17th International Workshop (EXPRESS’10), Paris, France, August 30th, 2010
Diva url
Abstract Sound behavioral equations on open terms may become unsoundafter conservative extensions ofthe underlying operational semantics. Providing criteriaunder which such equations are preserved isextremely useful; in particular, it can avoid the need to repeat proofs when extending the specifiedlanguage.This paper investigates preservation of sound equations for several notions of bisimilarity onopen terms: closed-instance (ci-)bisimilarity and formal-hypothesis (fh-)bisimilarity, both due toRobert de Simone, and hypothesis-preserving (hp-)bisimilarity, due to Arend Rensink. For both fh-bisimilarity and hp-bisimilarity, we prove that arbitrarysound equations on open terms are preservedby all disjoint extensions which do not add labels. We also define slight variations of fh- and hp-bisimilarity such that all sound equations are preserved byarbitrary disjoint extensions. Finally, wegive two sets of syntactic criteria (on equations, resp. operational extensions) and prove each of themto be sufficient for preserving ci-bisimilarity.