Multi-cost Bounded Reachability in MDP

Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann

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

    13 Citations (Scopus)
    193 Downloads (Pure)


    We provide an efficient algorithm for multi-objective model-checking problems on Markov decision processes (MDPs) with multiple cost structures. The key problem at hand is to check whether there exists a scheduler for a given MDP such that all objectives over cost vectors are fulfilled. Reachability and expected cost objectives are covered and can be mixed. Empirical evaluation shows the algorithm’s scalability. We discuss the need for output beyond Pareto curves and exploit the available information from the algorithm to support decision makers.
    Original languageEnglish
    Title of host publicationProceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)
    EditorsDirk Beyer, Marieke Huisman
    Place of PublicationCham
    Number of pages20
    ISBN (Electronic)978-3-319-89963-3
    ISBN (Print)978-3-319-89962-6
    Publication statusPublished - 2018

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Dive into the research topics of 'Multi-cost Bounded Reachability in MDP'. Together they form a unique fingerprint.

    Cite this