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!
first_indexed 2013-07-23T11:46:30Z
last_indexed 2018-02-09T04:28:10Z
id cronfa1170
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2015-04-22T13:30:26.9301072</datestamp><bib-version>v2</bib-version><id>1170</id><entry>2012-02-23</entry><title>Robustness of equations under operational extensions</title><swanseaauthors><author><sid>3f13b8ec315845c81d371f41e772399c</sid><ORCID>0000-0002-5826-7520</ORCID><firstname>Peter</firstname><surname>Mosses</surname><name>Peter Mosses</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2012-02-23</date><deptcode>FGSEN</deptcode><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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Electronic Proceedings in Theoretical Computer Science</journal><volume>41</volume><paginationStart>106</paginationStart><paginationEnd>120</paginationEnd><publisher/><issnPrint>2075-2180</issnPrint><issnElectronic/><keywords/><publishedDay>30</publishedDay><publishedMonth>11</publishedMonth><publishedYear>2010</publishedYear><publishedDate>2010-11-30</publishedDate><doi>10.4204/EPTCS.41.8</doi><url/><notes></notes><college>COLLEGE NANME</college><department>Science and Engineering - Faculty</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>FGSEN</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2015-04-22T13:30:26.9301072</lastEdited><Created>2012-02-23T17:02:03.0000000</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Peter</firstname><surname>Mosses</surname><orcid>0000-0002-5826-7520</orcid><order>1</order></author><author><firstname>Mohammad R</firstname><surname>Mousavi</surname><order>2</order></author><author><firstname>Michel A</firstname><surname>Reniers</surname><order>3</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2015-04-22T13:30:26.9301072 v2 1170 2012-02-23 Robustness of equations under operational extensions 3f13b8ec315845c81d371f41e772399c 0000-0002-5826-7520 Peter Mosses Peter Mosses true false 2012-02-23 FGSEN 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. Conference Paper/Proceeding/Abstract Electronic Proceedings in Theoretical Computer Science 41 106 120 2075-2180 30 11 2010 2010-11-30 10.4204/EPTCS.41.8 COLLEGE NANME Science and Engineering - Faculty COLLEGE CODE FGSEN Swansea University 2015-04-22T13:30:26.9301072 2012-02-23T17:02:03.0000000 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Peter Mosses 0000-0002-5826-7520 1 Mohammad R Mousavi 2 Michel A Reniers 3
title Robustness of equations under operational extensions
spellingShingle Robustness of equations under operational extensions
Peter Mosses
title_short Robustness of equations under operational extensions
title_full Robustness of equations under operational extensions
title_fullStr Robustness of equations under operational extensions
title_full_unstemmed Robustness of equations under operational extensions
title_sort Robustness of equations under operational extensions
author_id_str_mv 3f13b8ec315845c81d371f41e772399c
author_id_fullname_str_mv 3f13b8ec315845c81d371f41e772399c_***_Peter Mosses
author Peter Mosses
author2 Peter Mosses
Mohammad R Mousavi
Michel A Reniers
format Conference Paper/Proceeding/Abstract
container_title Electronic Proceedings in Theoretical Computer Science
container_volume 41
container_start_page 106
publishDate 2010
institution Swansea University
issn 2075-2180
doi_str_mv 10.4204/EPTCS.41.8
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 0
active_str 0
description 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.
published_date 2010-11-30T03:02:52Z
_version_ 1763749472860372992
score 11.035634

Similar Items