Peter D. Mosses, MohammadReza Mousavi and Michel A. Reniers. Proceedings of the 17th International Workshop on Expressiveness in Concurrency (EXPRESS 2010), , Paris, France, volume 41 of Electronic Proceedings in Theoretical Computer Science, pages 106--120, August 2010.
Sound behavioral equations on open terms may become unsound after conservative extensions of the underlying operational semantics. Providing criteria under which such equations are preserved is extremely useful; in particular, it can avoid the need to repeat proofs when extending the specified language. This paper investigates preservation of sound equations for several notions of bisimilarity on open terms namely, Closed Instance (CI) bisimilarity and Formal Hypothesis (FH) bisimilarity, both due to Robert de Simone and Hypothesis Preserving bisimilarity, due to Arend Rensink. For both FH bisimilarity and HP bisimilarity, we prove that arbitrary sound equations on open terms are preserved by 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 by arbitrary disjoint extensions. Finally, we give two sets of syntactic criteria (on equations, resp.\ operational extensions) and prove each of them to be sufficient for preserving CI bisimilarity.
(Paper in .pdf format)
An extended version of this paper appeared as: Robustness of Behavioral Equivalences on Open Terms, Technical Report CSR-10-18, Department of Computer Science, Eindhoven University of Technology, December 2010. (Technical report in .pdf format)
Bibtex Entry:
@InProceedings{MousaviEXPRESS2010,
author = "Mosses, Peter D. and Mousavi, MohammadReza and Reniers, Michel A.",
title = "Robustness of Equations Under Operational Extensions",
booktitle = "Proceedings of the 17th International Workshop on Expressiveness in Concurrency ({EXPRESS 2010})",
series = "Electronic Proceedings in Theoretical Computer Science",
volume = "41",
pages = "106--120",
address = "Paris, France",
year = "2010"
}