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

    5 Citations (Scopus)
    102 Downloads (Pure)

    Abstract

    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
    PublisherSpringer
    Pages320-339
    Number of pages20
    ISBN (Electronic)978-3-319-89963-3
    ISBN (Print)978-3-319-89962-6
    DOIs
    Publication statusPublished - 2018

    Publication series

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

      Fingerprint

    Cite this

    Hartmanns, A., Junges, S., Katoen, J-P., & Quatmann, T. (2018). Multi-cost Bounded Reachability in MDP. In D. Beyer, & M. Huisman (Eds.), Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018) (pp. 320-339). (Lecture Notes in Computer Science; Vol. 10806). Cham: Springer. https://doi.org/10.1007/978-3-319-89963-3_19