Difference between revisions of "Publications:Robustness of equations under operational extensions"

From CERES
Jump to: navigation, search
(Created page with "<div style='display: none'> == Do not edit this section == </div> {{PublicationSetupTemplate|Author=P. D. Mosses, Mohammad Reza Mousavi, M. A. Reniers |PID=584477 |Name=Mosses...")
 
(No difference)

Latest revision as of 04:43, 26 June 2014

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
Journal
HostPublication Proceedings 17th International Workshop on Expressiveness in Concurrency
DOI http://dx.doi.org/10.4204/EPTCS.41.8
Conference 17th International Workshop (EXPRESS’10), Paris, France, August 30th, 2010
Diva url http://hh.diva-portal.org/smash/record.jsf?searchId=1&pid=diva2:584477
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.