Model checking algorithms for CTMDPs

Peter Buchholz*, Ernst Moritz Hahn, Holger Hermanns, Lijun Zhang

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

27 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationComputer Aided Verification - 23rd International Conference, CAV 2011, Proceedings
Number of pages18
Publication statusPublished - 2011
Externally publishedYes
Event23rd International Conference on Computer Aided Verification, CAV 2011 - Snowbird, UT, United States
Duration: 14 Jul 201120 Jul 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6806 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International Conference on Computer Aided Verification, CAV 2011
CountryUnited States
CitySnowbird, UT

Fingerprint Dive into the research topics of 'Model checking algorithms for CTMDPs'. Together they form a unique fingerprint.

Cite this