No Cover Image

Book chapter 163 views

Weak Bisimulation as a Congruence in MSOS / Peter Mosses; 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.

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!
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