Computing Publications

Publications Home » Ordered SOS process languages for...

Ordered SOS process languages for branching and eager bisimulations

Irek Ulidowski, Iain Phillips

Journal Article
Information and Computation
Volume 178
Issue 1
pp.180–213
2002
Elsevier
ISSN 0890-5401
DOI 10.1006/inco.2002.3161
Abstract

We present a general and uniform method for defining structural operational semantics (SOS) of process operators by traditional Plotkin-style transition rules equipped with orderings. This new feature allows one to control the order of application of rules when deriving transitions of process terms. Our method is powerful enough to deal with rules with negative premises and copying. We show that rules with orderings, called ordered SOS rules, have the same expressive power as GSOS rules. We identify several classes of process languages with operators defined by rules with and without orderings in the setting with silent actions and divergence. We prove that branching bisimulation and eager bisimulation relations are preserved by all operators in process languages in the relevant classes.

BibTEX file for the publication
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.