Introduction - Semantics of Probabilistic Processes: An Operational Approach - page 1

Chapter 1
Introduction

Abstract This introduction briefly reviews the history of probabilistic concurrency
theory and three approaches to the semantics of concurrent systems: denotational,
axiomatic and operational. This topic focuses on the last one and more specifically
on (bi)simulation semantics and testing semantics. The second section surveys the
contents and main results for other chapters of the topic.

Keywords Probabilistic concurrency theory · Semantics · Bisimulation · Testing

1.1 Background

Computer science aims to explain in a rigorous way how computational systems
should behave, and then to design them so that they do behave as expected. Nowa-
days the notion of computational systems includes not only sequential systems but
also concurrent systems . The attention of computer scientists goes beyond single
programs in free-standing computers. For example, computer networks, particles
in physics and even proteins in biology can all be considered as concurrent sys-
tems. Some classical mathematical models (e.g. the ʻ -calculus [ 1 ]) are successful
for describing sequential systems, but they turn out to be insufficient for reasoning
about concurrent systems, because what is more important now is how different
components of a system interact with each other rather than their input-output
behaviour.
In the 1980s process calculi (sometimes also called process algebras ), notably
calculus of communicating systems (CCS) [ 2 ], communicating sequential processes
(CSP) [ 3 ] and algebra of communicating processes (ACP) [ 4 , 5 ], were proposed for
describing and analysing concurrent systems. All of them were designed around the
central idea of interaction between processes. In those formalisms, complex systems
are built from simple subcomponents, using a small set of primitive operators such
as prefix, nondeterministic choice, restriction, parallel composition and recursion .
Those traditional process calculi were designed to specify and verify qualitative
behaviour of concurrent systems.
Since the 1990s, there has been a trend to study the quantitative behaviour of
concurrent systems. Many probabilistic algorithms have been developed in order to