[GaoXZZ13] Model Checking Conditional CSL for Continuous-Time Markov Chains Gao, Y.; Xu, M.; Zhan, N. and Zhang, L. In Information Processing Letters, 113: 44-50, 2013.
Downloads: pdf, bibURL: http://dx.doi.org/10.1016/j.ipl.2012.09.009 Abstract. 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) [1] 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.