Journal article
Model checking conditional CSL for continuous-time Markov chains
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.
Language: | English |
---|---|
Year: | 2013 |
Pages: | 44-50 |
ISSN: | 18726119 and 00200190 |
Types: | Journal article |
DOI: | 10.1016/j.ipl.2012.09.009 |