Axiomatising ST-bisimulation equivalence

N. Busi, R.J. van Glabbeek, R. Gorrieri

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationProgramming Concepts, Methods and Calculi: Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods, and Calculi (PROCOMET '94), San Miniato, Italy, 6-10 June 1994
EditorsErnst-Rüdiger Olderog
PublisherNorth-Holland Publishing Company
Number of pages20
ISBN (Print)978-0-444-82020-4
Publication statusPublished - 6 Jun 1994
EventWorking Conference on Programming Concepts, Methods and Calculi, 1994 - San Miniato, Italy
Duration: 6 Jun 199410 Jun 1994

Publication series

NameIFIP Transactions A-56


ConferenceWorking Conference on Programming Concepts, Methods and Calculi, 1994
Abbreviated titlePROCOMET 1994
CitySan Miniato


Dive into the research topics of 'Axiomatising ST-bisimulation equivalence'. Together they form a unique fingerprint.

Cite this