Book chapter 806 views
Weak Bisimulation as a Congruence in MSOS
,
Ferdinand Vesely
Logic, Rewriting, and Concurrency, Volume: 9200, Pages: 519 - 538
Swansea University Authors:
Peter Mosses , Ferdinand Vesely
Full text not available from this repository: check for access using links below.
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...
| 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!
|
| 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’s WB Cool congruence format to MSOS. We compare the two approaches, and relate unobservable transitions in MSOS to equations in Rewriting Logic. |
|---|---|
| College: |
College of Science |
| Start Page: |
519 |
| End Page: |
538 |