No Cover Image

Conference Paper/Proceeding/Abstract 884 views

Robustness of equations under operational extensions

Peter Mosses Orcid Logo, Mohammad R Mousavi, Michel A Reniers

Electronic Proceedings in Theoretical Computer Science, Volume: 41, Pages: 106 - 120

Swansea University Author: Peter Mosses Orcid Logo

Full text not available from this repository: check for access using links below.

Check full text

DOI (Published version): 10.4204/EPTCS.41.8

Abstract

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 langu...

Full description

Published in: Electronic Proceedings in Theoretical Computer Science
ISSN: 2075-2180
Published: 2010
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa1170
Tags: Add Tag
No Tags, Be the first to tag this record!
Abstract: 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: closed-instance (ci-)bisimilarity and formal-hypothesis (fh-)bisimilarity, both due to Robert de Simone, and hypothesis-preserving (hp-)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.
College: Faculty of Science and Engineering
Start Page: 106
End Page: 120

Similar Items