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.
CITATION STYLE
Hartmanns, A., Junges, S., Katoen, J. P., & Quatmann, T. (2018). Multi-cost bounded reachability in MDP. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10806 LNCS, pp. 320–339). Springer Verlag. https://doi.org/10.1007/978-3-319-89963-3_19
Mendeley helps you to discover research relevant for your work.