Model Checking Algorithms for CTMDPs

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

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    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.
    Original languageEnglish
    Title of host publicationComputer Aided Verification : 23rd International Conference, CAV 2011 - Snowbird, UT, USA, July 14-20, 2011 - Proceedings
    PublisherSpringer
    Publication date2011
    Pages225-242
    ISBN (Print)978-3-642-22109-5
    ISBN (Electronic)978-3-642-22110-1
    DOIs
    Publication statusPublished - 2011
    Event23rd International Conference on Computer Aided Verification - Snowbird, United States
    Duration: 14 Jul 201120 Jul 2011
    Conference number: 23

    Conference

    Conference23rd International Conference on Computer Aided Verification
    Number23
    Country/TerritoryUnited States
    CitySnowbird
    Period14/07/201120/07/2011
    SeriesLecture Notes in Computer Science
    Number6806
    ISSN0302-9743

    Fingerprint

    Dive into the research topics of 'Model Checking Algorithms for CTMDPs'. Together they form a unique fingerprint.

    Cite this