@inproceedings{36721b57a67a4bb3b363341908a693ca,

title = "Multi-cost Bounded Reachability in MDP",

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{\textquoteright}s scalability. We discuss the need for output beyond Pareto curves and exploit the available information from the algorithm to support decision makers.",

author = "Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann",

note = "Open Access",

year = "2018",

doi = "10.1007/978-3-319-89963-3_19",

language = "English",

isbn = "978-3-319-89962-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "320--339",

editor = "Dirk Beyer and Marieke Huisman",

booktitle = "Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)",

}