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.
- Formal methods
- Probabilistic systems
- Continuous-time Markov chains
- Continuous stochastic logic
- Conditional logic
Gao, Y., Xu, M., Zhan, N., & Zhang, L. (2013). Model checking conditional CSL for continuous-time Markov chains. Information Processing Letters, 113(1-2), 44-50. https://doi.org/10.1016/j.ipl.2012.09.009