No Cover Image

Book chapter 692 views

Weak Bisimulation as a Congruence in MSOS

Peter Mosses Orcid Logo, Ferdinand Vesely

Logic, Rewriting, and Concurrency, Volume: 9200, Pages: 519 - 538

Swansea University Authors: Peter Mosses Orcid Logo, Ferdinand Vesely

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

Check full text

DOI (Published version): 10.1007/978-3-319-23165-5_24

Abstract

MSOS is a variant of structural operational semantics with a natural representation of unobservable transitions. To prove various desirable laws for programming constructs specified in MSOS, bisimulation should disregard unobservable transitions, and it should be a congruence. One approach, followin...

Full description

Published in: Logic, Rewriting, and Concurrency
ISBN: 978-3-319-23164-8 978-3-319-23165-5
ISSN: 0302-9743 1611-3349
Published: 2015
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa48794
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2019-02-11T20:04:25Z
last_indexed 2019-02-21T14:07:28Z
id cronfa48794
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2019-02-21T12:20:28.4885857</datestamp><bib-version>v2</bib-version><id>48794</id><entry>2019-02-11</entry><title>Weak Bisimulation as a Congruence in MSOS</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><author><sid>e54f54330e5abba1afddbfcb78ba54c1</sid><firstname>Ferdinand</firstname><surname>Vesely</surname><name>Ferdinand Vesely</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2019-02-11</date><deptcode>FGSEN</deptcode><abstract>MSOS is a variant of structural operational semantics with a natural representation of unobservable transitions. To prove various desirable laws for programming constructs specified in MSOS, bisimulation should disregard unobservable transitions, and it should be a congruence. One approach, following Van Glabbeek, is to add abstraction rules and use strong bisimulation with MSOS specifications in an existing congruence format. Another approach is to use weak bisimulation with specifications in an adaptation of Bloom&#x2019;s WB Cool congruence format to MSOS. We compare the two approaches, and relate unobservable transitions in MSOS to equations in Rewriting Logic.</abstract><type>Book chapter</type><journal>Logic, Rewriting, and Concurrency</journal><volume>9200</volume><paginationStart>519</paginationStart><paginationEnd>538</paginationEnd><publisher/><isbnPrint>978-3-319-23164-8</isbnPrint><isbnElectronic>978-3-319-23165-5</isbnElectronic><issnPrint>0302-9743</issnPrint><issnElectronic>1611-3349</issnElectronic><keywords/><publishedDay>27</publishedDay><publishedMonth>8</publishedMonth><publishedYear>2015</publishedYear><publishedDate>2015-08-27</publishedDate><doi>10.1007/978-3-319-23165-5_24</doi><url/><notes/><college>COLLEGE NANME</college><department>Science and Engineering - Faculty</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>FGSEN</DepartmentCode><institution>Swansea University</institution><apcterm/><lastEdited>2019-02-21T12:20:28.4885857</lastEdited><Created>2019-02-11T15:35:56.8094862</Created><path><level id="1">College of Science</level><level id="2">College of Science</level></path><authors><author><firstname>Peter</firstname><surname>Mosses</surname><orcid>0000-0002-5826-7520</orcid><order>1</order></author><author><firstname>Ferdinand</firstname><surname>Vesely</surname><order>2</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2019-02-21T12:20:28.4885857 v2 48794 2019-02-11 Weak Bisimulation as a Congruence in MSOS 3f13b8ec315845c81d371f41e772399c 0000-0002-5826-7520 Peter Mosses Peter Mosses true false e54f54330e5abba1afddbfcb78ba54c1 Ferdinand Vesely Ferdinand Vesely true false 2019-02-11 FGSEN MSOS is a variant of structural operational semantics with a natural representation of unobservable transitions. To prove various desirable laws for programming constructs specified in MSOS, bisimulation should disregard unobservable transitions, and it should be a congruence. One approach, following Van Glabbeek, is to add abstraction rules and use strong bisimulation with MSOS specifications in an existing congruence format. Another approach is to use weak bisimulation with specifications in an adaptation of Bloom’s WB Cool congruence format to MSOS. We compare the two approaches, and relate unobservable transitions in MSOS to equations in Rewriting Logic. Book chapter Logic, Rewriting, and Concurrency 9200 519 538 978-3-319-23164-8 978-3-319-23165-5 0302-9743 1611-3349 27 8 2015 2015-08-27 10.1007/978-3-319-23165-5_24 COLLEGE NANME Science and Engineering - Faculty COLLEGE CODE FGSEN Swansea University 2019-02-21T12:20:28.4885857 2019-02-11T15:35:56.8094862 College of Science College of Science Peter Mosses 0000-0002-5826-7520 1 Ferdinand Vesely 2
title Weak Bisimulation as a Congruence in MSOS
spellingShingle Weak Bisimulation as a Congruence in MSOS
Peter Mosses
Ferdinand Vesely
title_short Weak Bisimulation as a Congruence in MSOS
title_full Weak Bisimulation as a Congruence in MSOS
title_fullStr Weak Bisimulation as a Congruence in MSOS
title_full_unstemmed Weak Bisimulation as a Congruence in MSOS
title_sort Weak Bisimulation as a Congruence in MSOS
author_id_str_mv 3f13b8ec315845c81d371f41e772399c
e54f54330e5abba1afddbfcb78ba54c1
author_id_fullname_str_mv 3f13b8ec315845c81d371f41e772399c_***_Peter Mosses
e54f54330e5abba1afddbfcb78ba54c1_***_Ferdinand Vesely
author Peter Mosses
Ferdinand Vesely
author2 Peter Mosses
Ferdinand Vesely
format Book chapter
container_title Logic, Rewriting, and Concurrency
container_volume 9200
container_start_page 519
publishDate 2015
institution Swansea University
isbn 978-3-319-23164-8
978-3-319-23165-5
issn 0302-9743
1611-3349
doi_str_mv 10.1007/978-3-319-23165-5_24
college_str College of Science
hierarchytype
hierarchy_top_id collegeofscience
hierarchy_top_title College of Science
hierarchy_parent_id collegeofscience
hierarchy_parent_title College of Science
department_str College of Science{{{_:::_}}}College of Science{{{_:::_}}}College of Science
document_store_str 0
active_str 0
description MSOS is a variant of structural operational semantics with a natural representation of unobservable transitions. To prove various desirable laws for programming constructs specified in MSOS, bisimulation should disregard unobservable transitions, and it should be a congruence. One approach, following Van Glabbeek, is to add abstraction rules and use strong bisimulation with MSOS specifications in an existing congruence format. Another approach is to use weak bisimulation with specifications in an adaptation of Bloom’s WB Cool congruence format to MSOS. We compare the two approaches, and relate unobservable transitions in MSOS to equations in Rewriting Logic.
published_date 2015-08-27T03:59:27Z
_version_ 1763753032154087424
score 11.012678

Similar Items