Publication: Research - peer-review › Journal article – Annual report year: 2013
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.
|Citations||Error in DOI please contact firstname.lastname@example.org|
- Formal methods, Probabilistic systems, Continuous-time Markov chains, Continuous stochastic logic, Conditional logic
No data available