Model Checking Algorithms for CTMDPs
In Computer Aided Verification - 23rd International Conference (CAV)
, pages 225-242, Springer
, Lecture Notes in Computer Science 6806, 2011.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-22110-1_19
Abstract. Continuous Stochastic Logic (CSL) can be interpreted over
continuoustime Markov decision processes (CTMDPs) to specify quantitative
properties of stochastic systems that allow some external control. Model
checking CSL formulae over CTMDPs requires then the computation of optimal
control strategies to prove or disprove a formula. The paper presents a
conservative extension of CSL over CTMDPs--with rewards--and exploits
established results for CTMDPs for model checking CSL. A new numerical
approach based on uniformization is devised to compute time bounded
reachability results for time dependent control strategies. Experimental
evidence is given showing the efficiency of the approach.