computer science

Abstract

We present a general and uniform method for defining structural operational semantics (SOS) of process algebra operators by traditional Plotkin-style rules equipped with an ordering, the new feature which states the order of application of rules when deriving transitions of process terms. Our method allows to represent negative premises and copying in the presence of silent actions. We identify a number of general formats of unordered and ordered rules with silent actions and show that divergence sensitive branching and weak bisimulation relations are preserved by all operators in the relevant formats. A comparison with the existing formats for branching and weak bisimulations shows that our formats are more general.

Author: Irek Ulidowski (I.Ulidowski@mcs.le.ac.uk).
© University of Leicester. Last modified: 13th January 2004, 16:38:21
CS Web Maintainer.