Model checking continuous-Time Markov chains by transient analysis

Abstract

The verification of continuous-time Markov chains (CTMCs) against continuous stochastic logic (CSL) [3,6], a stochastic branchingtime temporal logic, is considered. CSL facilitates among others the specification of steady-state properties and the specification of probabilistic timing properties of the form P(image found)p(Φ1 UI Φ2), for state formulas Φ1 and Φ2, comparison operator (image found), probability p, and real interval I. The main result of this paper is that model checking probabilistic timing properties can be reduced to the problem of computing transient state probabilities for CTMCs. This allows us to verify such properties by using efficient techniques for transient analysis of CTMCs such as uniformisation. A second result is that a variant of ordinary lumping equivalence (i.e., bisimulation), a well-known notion for aggregating CTMCs, preserves the validity of all CSL-formulas.