Overview of

Background

Markov chains are widely used as adequate models in many diverse areas, ranging from mathematics and computer science to other disciplines such as operations research, industrial engineering, biology and demographics. Markov chains can be used to estimate performance characteristics of various nature, for instance to quantify throughput of manufacturing systems, locate bottlenecks in communication systems, or to estimate reliability in aerospace systems.

Model checking is a very successful technique to establish the correctness of systems from similar application domains, usually described in terms of a non-deterministic finite-state model. If non-determinism is replaced by randomized, i.e. probabilistic decisions, the resulting model boils down to a finite-state discrete-time Markov chain (DTMC). For these models, a number of qualitative and quantitative model checking algorithms have been proposed. In a qualitative setting it is checked whether a property holds with probability 0 or 1; in a quantitative setting it is verified whether the probability for a certain property meets a given lower or upper bound. PCTL [5] is a representative of the latter kind. It is an extension of CTL [4], allowing one to specify and verify properties such as `After a system failure, the probability that the system will not come up again is at most 10^-6.''

Markov chains are memoryless. In the discrete-time setting this is reflected by the fact that probabilistic decisions do not depend on the outcome of decisions taken earlier, only the state currently occupied is decisive to completely determine the probability of next transitions. For continuous-time Markov chains (CTMCs), where time ranges over (positive) reals (instead of discrete subsets thereof) the memoryless property further implies that the probabilities of taking next transitions do not depend on the amount of time spent in the current state. DTMCs are mostly applied to strictly synchronous scenarios, while CTMCs have shown to fit in well with (interleaving) asynchronous scenarios. In particular, CTMCs are the underlying semantic model of major high-level performance modelling formalisms such as stochastic Petri nets, stochastic automata networks, stochastic process algebras, Markovian queueing networks, and various extensions thereof.

Recently, the logic CSL has been proposed [1,3], an extension of both PCTL and CTL tailored to quantitative properties of CTMCs. Apart from CTL and PCTL properties, a selection of typical properties that can be verified using this logic is:

• ``After a system failure, there is at least a 99.99 % chance that the system will come up again within 5 time units.''
• `'On the long run, the probability of the system being unavailable is at most 10<sup>-4</sup>.''
• ``The probability that signal `ready' will be received within the next 4 time units is more than 0.3.''

, the Erlangen-Twente Markov Chain Checker, is the first implementation of a model checker for DTMCs and CTMCs. It uses numerical methods to model check PCTL and CSL-formulas, based on [5,3,2]. Apart from standard graph algorithms, model checking CSL involves matrix-vector multiplications, solutions of linear systems of equations, and solutions of systems of Volterra integral equations. Linear systems of equations are solved iteratively by standard numerical methods [12]. Two alternatives to solve systems of integral equations are implemented: One is based on piecewise integration of discretized distribution functions, the other is based on uniformisation [2]. Uniformisation is the default option, because it allows the tool to a priori calculate the computational effort needed to check a given property. This effort depends on the numerical parameters of the current model, on the property to be checked, and on the required numerical precision  (the latter is a parameter set by the user).

is a global model checker, i.e. it checks the validity of a formula for all states in the model. It has been developed such that it can easily be linked to a wide range of existing high-level modelling tools based on, for instance, stochastic process algebras, stochastic Petri nets, or queueing networks. A whole variety of such tools exists [6], most of them using dedicated formats to store the transition matrix R of the Markov chain that is obtained from a high-level specification. This matrix encodes the probabilistic behaviour of the system as time passes. Together with a labelling function L, which associates the states of the Markov chain with sets of atomic propositions, the matrix R constitutes the interface between the high-level formalism at hand and the model checker. Currently, the tool accepts DTMCs and CTMCs represented in a format generated by the stochastic process algebra tool TIPPTOOL [11] and by the stochastic Petri net tool DaNAMiCS (developed by the Department of Computer Science of the University of Cape Town, South Africa),  but the tool is designed in such a way that it can easily bridge to various other input formats.

Case Studies

Even though the tool is still a prototype, it has already been used in a number of nontrivial case studies, including

• validation and performance analysis of a cyclic server polling system [7],
• reliability estimation of the Hubble space telescope [8],
• dependability analysis of a workstationclusters [9], and
• performance and availability assessment of a distributed database server [10].

Tool Architecture

The tool has been written entirely in JAVA (version 1.2), in order to provide platform independence and to enable fast and efficient program development. Furthermore, support for the development of graphical user interfaces as well as grammar parsers is at hand. For the sake of simplicity, flexibility and extensibility we abstained from low-level optimizations, such as minimization of object invocations. The design and implementation took approximately 20 man-months, with about 11000 lines of code for the kernel and 1500 lines of code for the GUI implementation, using the SWING library. The tool architecture consists of five components:

Graphical User Interface

The GUI enables the user to load, modify and save verification projects. Each project consists of a model R, a labelling L, and the properties to be checked. The GUI contains the `CSL Property Manager' which allows the user to construct and edit CSL-formulas. The GUI also prints results and additional logging information on screen or writes them into file. Several verification parameters for the numerical analysis, such as solution method, precision, and number of interpolation points for the piecewise integration, can be set by the user.

More Information

More information about is available here.

Literature

1

A. Aziz, K. Sanwal, V. Singhal and R. Brayton.
Verifying continuous time Markov chains.
In Computer Aided Verification, CAV 96, Springer LNCS 1102: 269-276, 1996.

2

C. Baier, B.R. Haverkort, H. Hermanns and J.-P. Katoen.
Model checking continuous-time Markov chains by transient analysis.
In Computer Aided Verification, CAV 2000, Springer LNCS 1855: 358-372, 2000.

3

C. Baier, J.-P. Katoen and H. Hermanns.
Approximate symbolic model checking of continuous-time Markov chains.
In CONCUR 99, Springer LNCS 1664: 146-162, 1999.

4

E.M. Clarke, E.A. Emerson and A.P. Sistla.
Automatic verification of finite-state concurrent systems using temporal logic specifications.
ACM Tr. on Progr. Lang. and Sys., 8(2): 244-263, 1986.

5

H. Hansson and B. Jonsson.
A logic for reasoning about time and reliability.
Form. Asp. of Comp., 6(5): 512-535, 1994.

6

B.R. Haverkort and I.G. Niemegeers.
Performability modelling tools and techniques.
Performance Evaluation 25: 17-40, 1996.

7

H. Hermanns, J.P. Katoen, J. Meyer-Kayser and M. Siegle.
A Markov Chain Model Checker.
In TACAS 2000, Springer LNCS 1785: 347-362, 2000.

8

H. Hermanns.
Performance and reliability model checking and model construction.
In Formal Methods for Industrial Critical Systems, FMICS 2000, GMD Report 91, pages 11-28, Berlin, April 2000.

9

B. Haverkort, H. Hermanns, and J.P. Katoen.
The Use of Model Checking Techniques for Quantitative Dependability Evaluation.
In IEEE Symposium on Reliable Distributed Systems, SRDS 2000, IEEE CS Press, October 2000.

10

H. Hermanns, J.P. Katoen, J. Meyer-Kayser, and M. Siegle.
Towards Model Checking Stochastic Process Algebra.
In IFM 2000, Springer LNCS 1945: 420-439, November 2000.

11

H. Hermanns, U. Herzog, U. Klehmet, V. Mertsiotakis and M. Siegle.
Compositional performance modelling with the TIPPTOOL.
Performance Evaluation, 39(1-4): 5-35, 2000.

12

W. Stewart.
Introduction to the Numerical Solution of Markov Chains.
Princeton Univ. Press, 1994.