Thursday, 1st October | |
| 1.00-2.20 | Lunch |
| 2.20-2.30 | Welcome |
| 2.30-3.15 |
An overview and status report of the stochastic process algebra SPADES Joost-Pieter Katoen, University of Erlangen-Nuremberg |
| 3.15-3.45 | Coffee break/Registration |
| 3.45-4.30 | Specifying performance measures Jane Hillston, University of Edinburgh |
| 4.30-5.15 | Logics for Performance Measures Graham Clark, University of Edinburgh |
Friday, 2nd October | |
| 10.00-10.45 | Compositional Representation and Reduction of StochasticLabelled Transition Systems using Extended BDDs Markus Siegle, University of Erlangen-Nuremberg |
| 10.45-11.15 | Coffee break |
| 11.15-12.00 | Solving Stochastic Process Algebra models through Matrix-Geometric Methods Amani El-Rayes, University of Birmingham |
| 12.00-2.00 | Lunch |
| 2.00-2.45 | The Algebraic Mu-calculus and MTBDDs Christel Baier, Universitaet Mannheim |
| 2.45-3.30 | Some experimental results for BDD-based probabilistic model checking Marta Kwiatkowska, University of Birmingham |
| 3.30-4.00 | Coffee break |
| 4.00-5.00 | Discussion and Business Meeting |
Saturday, 3rd October | |
| 10.00-10.45 | On probabilistic extensions of hybrid systems Jeremy Sproston, University of Birmingham |
| 10.45-11.15 | Coffee break |
| 11.15-12.00 | Model checking imperative programs Mark Ryan, University of Birmingham |
| 12.00-12.30 | Closing |
An overview and status report of the stochastic process algebra SPADES
Joost-Pieter Katoen
Stochastic process algebras (SPAs) like PEPA, TIPP and EMPA allow the user to specify the occurrence of actions after a random delay. These delays are determined by exponential distributions. This facilitates a formal interpretation in terms of standard transition systems and establishes a close link to continuous-time Markov chains. To put it in a nutshell, these process algebras allow the compositional specification (and analysis) of continuous-time Markov chains.
In this talk we discuss an extension of SPAs with general distributions. We present an extension of transition systems with backwards running clocks that are basically random variables of continuous or discrete nature. This model, referred to as stochastic automata, is strongly related to generalised semi-Markov processes (GSMPs) and timed automata. We present a non-Markovian SPA called SPADES (SPA for Discrete-Event Simulation) and discuss its compositional operational semantics using stochastic automata. Besides we present some equivalence relations, and a sound and complete axiomatisation for structural bisimulation. In particular we show how an expansion law, an important law for reducing parallel composition into more elementary operations, is obtained.
As a result, the process algebra SPADES allows the compositional specification (and analysis) of time-homogeneous, mono-rated GSMPs with deterministic branching. To conclude our talk we briefly present a case study, a multiprocessor system that is subject to failures, that has been formally specified in SPADES, and whose performance has been analysed using our prototype tool.
Specifying Performance Measures
Jane Hillston
In the last five years stochastic process algebras (SPA) have gained some acceptance within the performance modelling community. However there are evidently some aspects of the formalism which make it difficult for novices to use. The principal of these is the lack of support available for specifying performance measures for a model.
In this talk I outline a proposal for how such support could be provided in such a way as to take full advantage of the existing theoretical underpinnings of SPA. The approach involves a "high-level" specification language to express requirements or questions in terms of the SPA expressions. This is given a semantics in terms of a suitably augmented process logic, which is then used to calculate performance measures in terms of the underlying Markov process. I describe a preliminary version of such a query language and explain how it can be used to express both steady state and transient behaviour. I show how, in some cases, a complex property of transient behaviour can be expressed as a simpler one over a model acting in cooperation with a test process. The form of the test process can be derived automatically from the structure of the original property.
Logics for performance measures
Graham Clark
Stochastic process algebras such as PEPA provide a well-developed theory for the compositional construction of performance models. However, important gaps exist in the methodology - given a model, these are the specification of, and ability to check logical properties; and the formulation and computation of relevant performance measures, such as throughput and mean waiting time. This talk explains existing methods which attempt to address these problems, and then investigates which features would be required of such a logical underpinning of PEPA. A large body of research exists on the subject of probabilistic verification; we enquire how this may be used in view of some important differences present in PEPA models, such as the absence of non-determinism, and the presence of continuous time (exponential) random variables.
Compositional Representation and Reduction of Stochastic Labelled
Transition Systems using Extended BDDs
Markus Siegle
Compact symbolic representations of large labelled transition systems, based on binary decision diagrams (BDD), are discussed. Extensions of BDDs are considered, in order to represent stochastic transition systems for performability analysis. It is shown how parallel composition of components can be performed in this context, without leading to state space explosion. Furthermore, we discuss state space reduction by Markovian bisimulation, also entirely based on symbolic techniques. Together, parallel composition and state space reduction enable a compositional approach to the stochastic modelling of concurrent systems.
Solving Stochastic Process Algebra models through Matrix-Geometric Methods
Amani El-Rayes
There are two problems with SPAs at present: the first is that many SPAs only allow durations of activities to be exponentially distributed, and the second is the rapid increase of the size of the state space of the underlying Markov chain (known as the state explosion problem). We attempt to overcome these problems by solving SPA models through Matrix-Geometric methods (mgm), which in addition allows us to solve systems with infinitely many arrivals in infinite queue system.
We allow durations of activities to be given in terms of Phase distributions (Ph distributions) as defined by M. Neuts. Exponential, Erlang, Hypoexponential, Hyperexponential and Coxian are examples of Ph-type distributions. The most important properties of Ph-distributions are that they are closed under maximum, minimum and convolution. This allows us to define synchronisation, choice and prefixing of two SPA models as the maximum, minimum and convolution of the Ph-distributions of the components. The activities in the composed system thus have Ph-distributed durations. (Exponential distributions are closed under minimum only.) Another advantage of Ph-distributions is that any other distribution defined on the interval [0,\infinity) can be approximated by Ph-distributions.
In the Matrix-Geometric method each state is described as a pair (i,s), where i >= 0 is infinite and s represents the number of phases in the system which must be finite. The method relies on identifying two portions (parts) within the structure of the system: the initial portion and the repetitive portion. The initial portion (which is finite) has a non-regular structure and each component in it must be represented in detail. The repetitive portion has a repetitive structure and can be represented in SPAs as a composition of several components. The size of the state space in mgm, even if the system is infinite, is reasonably small comparing with Markov chain. By solving the mgm we get the steady state probability and we can obtain the performance measures of the model.
The Algebraic Mu-Calculus and MTBDDs
Christel Baier and Ed Clarke (CMU, Pittsburgh)
The algebraic mu-calculus is a ``language'' for manipulating real-valued functions. The main concepts are arithmetic combinators and an iteration operator which can be used to solve fixed point problems. In particular, the algebraic mu-calculus can serve as a specification language for parallel programs as it subsumes several program logics, as e.g. the relational and modal mu-calculus and several temporal and modal logics to reason about probabilistic systems. We describe an algorithm that evaluates the terms of the algebraic mu-calculus where the underlying data structure are MTBDDs. This algorithm yields symbolic model checking algorithms for the program logics that are contained in the algebraic mu-calculus.
Some experimental results for BDD-based probabilistic model checking
Marta Kwiatkowska
In their paper entitled A Logic for Reasoning about Time and Reliability (FAC 1994), Hansson and Jonsson proposed the probabilistic temporal logic PCTL and the corresponding model checking algorithm based on solving a linear equation system in order to compute the probability measure for unbounded until. In a later paper, Symbolic Model Checking of Probabilistic Processes by Baier et al (ICALP'97), a BDD variant of this algorithm was derived, which combines BDDs (Binary Decision Diagrams) with MTBDDs (Multi-Terminal Binary Decision Diagrams) of Clarke et al.
We report on an ongoing project, describing first experimental results with an implementation of the PCTL model checking algorithm as presented in the ICALP'97 paper using the CUDD package. The package is available from Colorado University and has support for BDDs and ADDs, including matrix-by-matrix multiplication. The software takes as input the sparse probability matrix of a probabilistic process and a PCTL formula. We have compared performance of our algorithm with a matlab implementation with encouraging results. However, we have discovered that there exist PCTL formulas for which the probability calculation can be slow.
On probabilistic extensions of hybrid systems
Jeremy Sproston
The proliferation of computer technology embedded in real-life environments has lead to increased interest in formal approaches for hybrid systems, which consist of both discrete and continuous components. Traditional approaches to hybrid system description express the model purely in terms of nondeterminism; however, we may wish to express the likelihood of the system making certain transitions. This can be achieved by augmenting our system model with probabilistic information.
The problem of extending a subclass of hybrid system - real-time systems - with certain probabilistic information is addressed, and an automatic verification procedure for this model is presented. The approach taken is to add discrete probability distributions to an Alur-Dill timed automaton, which can then be represented as a finite-state probabilistic-nondeterministic system. This finite system can be model-checked against temporal formulas including bounds on probability, expressing properties such as "with probability 0.6 or greater, the clock x remains below 5 until clock y exceeds 2".