Article ID: | iaor20127402 |
Volume: | 113 |
Issue: | 1-2 |
Start Page Number: | 44 |
End Page Number: | 50 |
Publication Date: | Jan 2013 |
Journal: | Information Processing Letters |
Authors: | Zhang Lijun, Gao Yang, Xu Ming, Zhan Naijun |
Keywords: | simulation, stochastic processes |
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.