1 Department of Applied Mathematics and Computer Science, Technical University of Denmark2 Language-Based Technology, Department of Applied Mathematics and Computer Science, Technical University of Denmark3 Chinese Academy of Sciences4 East China Normal University5 Department of Informatics and Mathematical Modeling, Technical University of Denmark6 East China Normal University
In this paper, we consider the model-checking problem of continuous-time Markov chains (CTMCs) with respect to conditional logic. To the end, we extend Continuous Stochastic Logic introduced in Aziz et al. (2000)  to Conditional Continuous Stochastic Logic (CCSL) by introducing a conditional probabilistic operator. CCSL allows us to express a richer class of properties for CTMCs. Based on a parameterized product obtained from the CTMC and an automaton extracted from a given CCSL formula, we propose an approximate model checking algorithm and analyse its complexity.
Information Processing Letters, 2013, Vol 113, Issue 1-2, p. 44-50