University of Leicester

computer science

Formats of Ordered SOS Rules with Silent Actions,
Irek Ulidowski and Iain Phillips,
A revised version of the paper in TAPSOFT'97, Lille, France, 1997. LNCS 1214.


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.

This paper can be obtained in dvi form.
| [University Home]|[Faculty of Science]|[MCS Home]|[CS Home]||[University Index A-Z]|[University Search]|[University Help]|

Author: Irek Ulidowski (
© University of Leicester. Last modified: 13th January 2004, 16:38:21
CS Web Maintainer.