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

gain efficiency or to solve problems that are otherwise impossible to solve by de-
terministic algorithms. For instance, probabilities are introduced to break symmetry
in distributed coordination problems (e.g. the dining philosophers' problem, leader
election and consensus problems). Probabilistic modelling has helped to analyse and
reason about the correctness of probabilistic algorithms, to predict system behaviour
based on the calculation of performance characteristics and to represent and quantify
other forms of uncertainty. The study of probabilistic model checking techniques has
been a rich research area.
A great many probabilistic vari ants of the classical process calculi have also
appeared in the literature. The typical approach is to add probabilities to existing
models and techniques that have already proved successful in the nonprobabilistic
settings. The distinguishing feature of probabilistic process calculi is the presence of
a probabilistic-choice operator, as in the probabilistic extensions of CCS [ 6 , 7 ], the
probabilistic CSP [ 8 ], the probabilistic ACP [ 9 ] and the probabilistic asynchronous
ˀ -calculus [ 10 ].
In order to study a programming language or a process calculus, one needs to
assign a consistent meaning to each program or process under consideration. This
meaning is the semantics of the language or calculus. Semantics is essential to verify
or prove that programs behave as intended. Generally speaking, there are three ma-
jor approaches for giving semantics to a programming language. The denotational
approach [ 11 ] seeks a valuation function that maps a program to its mathematical
meaning. This approach has been very successful in modelling many sequential lan-
guages; programs are interpreted as functions from the domain of input values to the
domain of output values. However, the nature of interaction is much more complex
than a mapping from inputs to outputs, and so far the denotational interpretation of
concurrent programs has not been as satisfactory as the denotational treatment of
sequential programs.
The axiomatic approach [ 12 , 13 ] aims at understanding a language through a few
axioms and inference rules that help to reason about the properties of programs.
It offers an elegant way of gaining insight into the nature of the operators and the
equivalences involved. For example, the difference between two notions of program
equivalence may be characterised by a few axioms, particularly if adding these
axioms to a complete system for one equivalence gives a complete system for the
other equivalence. However, it is often difficult and even impossible to achieve a
fully complete axiomatic semantics if the language in question is beyond a certain
expressiveness.
The operational approach has been shown to be very useful for giving seman-
tics of concurrent systems. The behaviour of a process is specified by its structural
operational semantics [ 14 ], described via a set of labelled transition rules induc-
tively defined on the structure of a term. In this way each process corresponds to a
labelled transition graph . The shortcoming of operational semantics is that it is too
concrete, because a transition graph may contain many states that intuitively should
be identified. Thus, a great number of equivalences have been proposed, and dif-
ferent transition graphs are compared modulo some equivalence relations. Usually