Model-Checking Algorithms for CTMDPS

Title: Model-Checking Algorithms for CTMDPS
Speaker: Dr. Lijun Zhang Denmark Technical University
Time: 10:00am, July 27th (Wednesday), 2011.
Venue: Lecture Room, 3rd Floor, Building No. 5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract: Continuous Stochastic Logic (CSL) can be interpreted over continuous-time 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.Bio of the speaker, the slides and the corresponding paper of this talk are attached.