Saturday, 29th May | |
| 10.00-10.20 | Opening |
| 10.20-11.20 | A Feature Construct for PEPA Stephen Gilmore, University of Edinburgh |
| 11.20-12.20 | Stochastic Process Algebra Structure for Insensitivity Graham Clark, University of Edinburgh |
| 12.20-14.00 | Lunch |
| 14.00-15.00 | Verifying Quantitative Properties ofContinuous Probabilistic Real-Time Graphs Marta Kwiatkowska, University of Birmingham |
| 15.00-16.00 | Symbolic Model Checking of Concurrent Probabilistic SystemsUsing MTBDDs and Simplex Gethin Norman, University of Birmingham |
| 16.00-16.30 | Coffee Break |
| 16.30-17.30 | On weak bisimulations for probabilistic systems Christel Baier, Universitaet Mannheim |
| 17.30-18.30 | Discussion |
Sunday, 30th May | |
| 10.00-11.00 | Approximate symbolic model checking of continuous-time Markov chains Joost-Pieter Katoen, University of Twente |
| 11.00-12.00 | Implementation of a prototype for model checking csl formulas Joachim Meyer-Kayser, Universitaet Erlangen |
| 12.00-14.00 | Lunch |
| 14.00-15.00 | How efficient are MTBDDs to represent and analyse CTMCs? Holger Hermanns, University of Twente |
A Feature Construct for PEPA
Stephen Gilmore
We show how the PEPA performance modelling language could be extended with a ``feature construct'' which can be used to describe modifications to PEPA models. We provide this construct with an operational description which conservatively extends the operational semantics of the PEPA language. We apply the feature construct in a small case study.
Stochastic Process Algebra Structure for Insensitivity
Graham Clark
Recent research allow the arbitrary use of more general probability distributions in stochastic process algebra, improving expressibility, but in general this makes performance evaluation difficult. We investigate the use of such distributions from the opposite direction, using the stochastic phenomenon of insensitivity. We present a methodology which guarantees the insensitivity of certain concurrently enabled non-conflicting stochastic process algebra activities, and give a derived combinator for constructing process algebra models. Use of this combinator guarantees that the stochastic process underlying the model is insensitive to a particular set of activities. We find that the model structure we identify has a product form solution which seems dissimilar to those currently known to exist for stochastic process algebra. Our analysis uses the stochastic process algebra PEPA, and its associated conventions.
Verifying Quantitative Properties of
Continuous Probabilistic Real-Time Graphs
Marta Kwiatkowska (joint work with Gethin Norman, Roberto Segala and Jeremy Sproston)
We consider the problem of automatically verifying real-time systems with continuously distributed random delays. Our system model is an extension of the timed automata variant of (Kwiatkowska et al, ARTS'99), and exhibits nondeterministic and probabilistic choice, the latter being made according to both discrete distributions and continuous density functions with finite support. To facilitate algorithmic verification, we modify the standard region graph construction by subdividing the unit intervals in order to approximate the probability to within an interval. We describe a proposal for a model checking method for such systems, which takes as a specification language Probabilistic Timed Computation Tree Logic (PTCTL). Our method improves on the previously known techniques in that it allows the verification of quantitative probability bounds, as opposed to qualitative properties which can only refer to bounds of probability 0 or 1.
Symbolic Model Checking of Concurrent Probabilistic Systems
Using MTBDDs and Simplex
Gethin Norman (joint work with Marta Kwiatkowska, Dave Parker and Roberto Segala)
Symbolic model checking for purely probabilistic processes using MTBDDs was introduced in (Baier et al, 1997). In this paper we consider models for concurrent probabilistic systems, which extend the purely probabilistic processes through the addition of nondeterministic choice. As a specification formalism we use the probabilistic branching-time temporal logic PBTL, which allows us to express properties such as ``under any scheduling of nondeterministic choices, the probability of $\phi$ holding until $\psi$ is true is at least 0.78''. It has been shown in (Bianco & de Alfaro, 1994) that the verification of ``until'' properties can be reduced to a linear programming problem and solved with the help of e.g. the simplex algorithm. Based on the algorithms of (Bianco & de Alfaro, 1994; Baier& Kwiatkowska, 1998), we derive a symbolic model checking procedure for PBTL over concurrent probabilistic systems using MTBDDs, and extend it with fairness constraints. We furthermore implement an experimental model checker using the Colorado University Decision Diagram (CUDD) package. Our key contribution is an implementation of the simplex algorithm in terms of MTBDDs.
On weak bisimulations for probabilistic systems
Christel Baier
In this talk, we consider action-labelled probabilistic systems (fully probabilistic systems and probabilistic systems with non-determinism) and weak bisimulation equivalences on them. First, we recall the definitions given in the literature and discuss several properties (decidability, compositionality, etc.). In the second part, we present a novel notion of bisimulation equivalence for probabilistic systems with non-determinism that abstracts from internal computations and which turns out to be decidable in polynomial time.
Approximate symbolic model checking of continuous-time
Markov chains
Joost-Pieter Katoen
The mechanised verification of a given (usually finite-state) model against a property expressed in some temporal logic is known as model checking. In this talk we discuss how model checking techniques can be used to automatically check performance and reliability requirements. To that purpose we present a symbolic model checking algorithm for continuous-time Markov chains (CTMCs), that are at the basis of contemporary performance evaluation and reliability analysis methodologies. In the talk we review the basic concepts of model checking and introduce a branching-time logic to express performance requirements. We discuss the main algorithms needed for model checking this logic and discuss the possibilities to apply symbolic techniques like binary decision diagrams (BDDs) to model checking CTMCs.
Implementation of a prototype for model checking csl formulas
Joachim Meyer-Kayser
This talk gives a short overview of a prototype model checker that checks a subset of csl specifications against labelled ctmc's. Design and implementation issues are discussed and a tool demonstration is given.
How efficient are MTBDDs to represent and analyse CTMCs?
Holger Hermanns
Binary Decision Diagrams (BDDs) have gained high attention in the context of design and verification of digital circuits. They have successfully been employed to encode very large state spaces in an efficient, symbolic way. Multi terminal BDDs (MTBDDs) are generalisations of BDDs from Boolean values to values of any finite domain. In this paper, we investigate the applicability of MTBDDs to the symbolic representation of continuous time Markov chains, derived from high-level formalisms, such as queueing networks or process algebras. Based on this data structure, we discuss iterative solution algorithms to compute the steady-state probability vector that work in a completely symbolic way. We highlight a number of lessons learned, using a set of small examples.