Probabilistic modelling is widely used in the design and analysis of computer systems, decision support and scheduling problems, and has been rapidly gaining in importance in recent years. In a distributed environment, various randomized schemes have been found to act as symmetry breakers, leading to efficient, symmetric solutions to distributed co- ordination problems, for example leader election and consensus algorithms. Probability also provides means to model unreliable or unpredictable behaviour, aiding in the study of fault-tolerant systems, computer networks and queuing systems, and to predict their behaviour based on the calculation of performance characteristics. In decision-theoretic planning and reinforcement learning, probability is used to represent and quantify uncertainty, and to model computational processes under various scenarios.

Probabilistic techniques are extensively used in the following three areas:

1. Performance evaluation has its roots in the early 1910's when A.K. Erlang in Denmark developed stochastic capacity planning techniques for telephone exchanges. This so-called queuing theory developed further throughout the 20th century, aided by the efficient solution due to Buzen (1973) and the development of mean-value analysis by Reisen and Lavenberg (1977). The now established field of performance evaluation aims to develop formalisms and tools for modelling systems and analysing their performance measures, as a means to support the process of design and engineering. The analysis involves building a probabilistic model of the system being considered, typically a continuous time Markov chain (CTMC), but often a stochastic process of a more general nature as well. The model serves as a basis for analytical, simulation-based or numerical calculations which result in steady-state probabilities and the associated performance measures (resource utilisation, average call waiting time, etc). Alternatively, transient behavioural aspects, such as the probability of message delivery or quality of service dropping below minimum within a given time bound, can be analysed. The research in the area encompasses a variety of techniques, including measurement and testing, focusing on quantitative characteristics, and covers a broad spectrum of issues, for example designing description languages, formulating efficient numerical methods and tools for solving thus derived models, and queueing theory.
2. Probabilistic model checking (or probabilistic verification) is an extension of model checking techniques to probabilistic systems, first introduced by Hart, Sharir and Pnueli (1982). As in conventional model checking, a model of the probabilistic system, usually in the form of a discrete or continuous time Markov chain (DTMC/CTMC) or a Markov decision process (MDP), is built and then subjected to algorithmic analysis in order to establish whether it satisfies a given specification. The specifications are usually stated as formulae of probabilistic temporal logic, which in addition to conventional modalities may include probabilistic operators, whose outcome is true/false depending on the probability of certain executions occurring. The model checking procedure combines traversal of the underlying transition graph with numerical solutions of linear optimisation problems (for Markov decision process models) and linear equation systems and linear differential equation systems (for DTMC/CTMC models). The model checker can either produce a binary answer (yes or no, true or false), by comparing the obtained probability with the given threshold, or simply return the likelihood of the executions instead. Although algorithms for model checking probabilistic systems have been known since the mid-1980's (Vardi, 1985), it is only recently that experimental, tool implementation work has begun. The main thrust of the research in this area is to further the experimental work by learning from and incorporating the successful techniques of conventional model checking, for example by adapting symbolic techniques (such as MTBDDs) for model checking probabilistic systems, or the use of uniformisation (a well-developed technique in performance evaluation) for model checking timed properties for continuous time Markov chains. The foundational work continues to seek out new algorithms, notations and languages, and to adapt them to specific applications which require probabilistic modelling.
3. Decision support and adaptive control ("planning") heavily depend on adequate modelling of uncertainty due to environmental factors. Markov decision processes, which originated in operations research in the 1950's, serve as a representation for planning and control problems which can be analysed by solving appropriately derived variants of Bellman equations. Since the 1980's, following the pioneering work of Dean and Kanazawa (1989) and Tatman and Shachter (1990) on exploiting structure in representation and solution of such problems, Markov decision processes have been central to the research in automated planning in Artificial Intelligence. In subsequent years, a great deal of progress was made exploring structured versions of earlier algorithms for unstructured problems, and also using the basic technology for model checking, including binary decision diagrams (BDDs). True MDPs, i.e., problems in which the current state of the system is completely observable to the decision maker, are rare in practice and hence the partially observable variant (POMDP) is of great importance. Recently, there has been a resurgence of interest in POMDPs, and a host of new algorithms have been developed, including variational methods which open up the possibility of solving a wide range of problems. Variational statistical methods can in some cases reduce the need for state space exploration using a combination of sampling techniques and a reformulation in terms of a (continuous) parameterized space of actions.

It should be clear from the above that there are commonalities between the main research challenges of the three areas:

• they have to deal with very large state spaces, and therefore have to resort to structure in order to arrive at compact model representations: in model checking variants of BDDs are used, and in performance evaluation the Kronecker representation as well as matrix diagrams;
• they draw on probabilistic techniques and require appropriate efficient numerical solution methods (linear equations, linear differential equations and linear programming) capable of handling very large models.

At the same time, there are differences in their respective focus and research goals. Performance modelling has developed mature analytical, numerical and simulation methods for analysing various probabilistic systems; it can evidently serve as a useful source of expertise in Markovian/non-Markovian analysis techniques and numerical computations not normally employed in conventional model checking. Likewise, planning and scheduling has led to the emergence of sophisticated MDP/POMDP algorithms; since MDPs arise as models of randomized distributed algorithmic schemes, these may well be relevant for probabilistic model checking. In turn, model checking, and probabilistic model checking in particular, can offer advanced efficient techniques for analysing the underlying transition graph.

The seminar programme included five one-hour tutorials, by Moshe Vardi, Christel Baier and Joost-Pieter Katoen on probabilistic model checking, Bob Givan and Ron Parr on Markov decision processes, and Bill Sanders on dependability and performability evaluation. The remainder of talks were either long (45 min) or normal (30 min) research presentations. There was also a panel discussion chaired by Marta Kwiatkowska which involved two researchers from each of the three areas: Christel Baier and Prakash Panangaden from probabilistic verification, Bob Givan and Richard Dearden from planning and Bill Sanders and Gianfranco Ciardo from performance modelling.

• Monday
• Thuesday
• Wednesday
• Thursday
• Friday

It became clear during the seminar that the three areas (probabilistic model checking, decision support and performance evaluation) are indeed closely related. All are concerned with variants of probabilistic models, typically Markov processes of some kind, their efficient representation utilising structure, and automated procedure for their analysis. Whereas the probabilistic model checking and performance evaluaation communities were aware of this connection, and indeed some of the researchers straddle the two areas, it was not until the meeting that it was realised how close the decision support field is to the other two fields as well. We saw many examples of this in the talks; for example, conventional MDP algorithms from the decision support filed, such as value iteration, are being used in probabilistic model checkers. We expect much future exchanges between the areas. The panel discussion focused on the question of what each area can offer to the other two, and vice-versa. A common view that emerged is that in the probabilistic model checking field predominantly discrete mathematical theories aare used, whereas in the decision support and performance evaluation field continuous phenomena play a major role, in which the notion of approximation is fundamental. It was felt that also in probabilistic model checking the notion of approximation should become more important.