computer science

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.

This paper is available at doi location.

Also, it can be obtained either in ps or ps.gz form.

Author: Irek Ulidowski (I.Ulidowski@mcs.le.ac.uk).
© University of Leicester. Last modified: 15th April 2008, 18:42:03
CS Web Maintainer.