N. Busi (U. Siena), R.J. van Glabbeek (Stanford)
& R. Gorrieri (U. Bologna)
December 1993
A simple ST operational semantics for a process algebra is
provided, by defining a set of operational rules in
Plotkin's style. This algebra comprises TCSP parallel
composition, ACP sequential composition and a refinement
operator, which is used for replacing an action with an
entire process, thus permitting hierarchical specification
of systems. We prove that ST-bisimulation equivalence is a
congruence, resorting to standard techniques on rule
formats. Moreover, we provide a set of axioms that is sound
and complete with respect to ST-bisimulation. The
intriguing case of the forgetful refinement (i.e., when an
action is refined into the properly terminated process) is
dealt with in a new, improved manner.
KEYWORDS: Concurrency, complete axiomatizations, labelled
transition systems, structural operational semantics,
bisimulation, action refinement, empty process, termination
- Technical Report UBLCS-93-26, Laboratory for Computer
Science, University of Bologna
- Available at
ftp://ftp.cs.unibo.it/pub/TR/UBLCS/93-26.ps.gz,
ftp://Boole.stanford.edu/pub/TEX/axiomst.tex.gz and
ftp://Boole.stanford.edu/pub/DVI/axiomst.dvi.gz.
- In: Proceedings IFIP Working Conference on Programming
Concepts, Methods and Calculi, San Miniato, Italy, June 1994
(E.-R. Olderog, ed.), Elsevier Science Publishers B.V.
(North-Holland), 1994, pp. 169-188.