Model-checking algorithms for continuous-time markov chains
Top Cited Papers
- 20 June 2003
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 29 (6), 524-541
- https://doi.org/10.1109/tse.2003.1205180
Abstract
Continuous-time Markov chains (CTMCs) have been widely used to determine system performance and dependability characteristics. Their analysis most often concerns the computation of steady-state and transient-state probabilities. This paper introduces a branching temporal logic for expressing real-time probabilistic properties on CTMCs and presents approximate model checking algorithms for this logic. The logic, an extension of the continuous stochastic logic CSL of Aziz et al. (1995, 2000), contains a time-bounded until operator to express probabilistic timing properties over paths as well as an operator to express steady-state probabilities. We show that the model checking problem for this logic reduces to a system of linear equations (for unbounded until and the steady-state operator) and a Volterra integral equation system (for time-bounded until). We then show that the problem of model-checking time-bounded until properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows the verification of probabilistic timing properties by efficient techniques for transient analysis for CTMCs such as uniformization. Finally, we show that a variant of lumping equivalence (bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all formulas in the logic.Keywords
This publication has 47 references indexed in Scilit:
- Optimal state-space lumping in Markov chainsInformation Processing Letters, 2003
- Automatic verification of real-time systems with discrete probability distributionsTheoretical Computer Science, 2002
- Process algebra for performance evaluationTheoretical Computer Science, 2002
- Model checking for a probabilistic branching time logic with fairnessDistributed Computing, 1998
- On the verification of qualitative properties of probabilistic processes under fairness constraintsInformation Processing Letters, 1998
- A logic for reasoning about time and reliabilityFormal Aspects of Computing, 1994
- A theory of timed automataTheoretical Computer Science, 1994
- Characterizing finite Kripke structures in propositional temporal logicTheoretical Computer Science, 1988
- Modalities for model checking: branching time logic strikes backScience of Computer Programming, 1987
- Using branching time temporal logic to synthesize synchronization skeletonsScience of Computer Programming, 1982