Multi-cost Bounded Reachability in MDP

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
LanguageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II
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
StatePublished - 2018

Publication series

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

Fingerprint

Costs
Model checking
Scalability

Cite this

Hartmanns, A., Junges, S., Katoen, J-P., & Quatmann, T. (2018). Multi-cost Bounded Reachability in MDP. In D. Beyer, & M. Huisman (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II (pp. 320-339). (Lecture Notes in Computer Science; Vol. 10806). Cham: Springer. DOI: 10.1007/978-3-319-89963-3_19
Hartmanns, Arnd ; Junges, Sebastian ; Katoen, Joost-Pieter ; Quatmann, Tim. / Multi-cost Bounded Reachability in MDP. Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. editor / Dirk Beyer ; Marieke Huisman. Cham : Springer, 2018. pp. 320-339 (Lecture Notes in Computer Science).
@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’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 = "Tools and Algorithms for the Construction and Analysis of Systems",

}

Hartmanns, A, Junges, S, Katoen, J-P & Quatmann, T 2018, Multi-cost Bounded Reachability in MDP. in D Beyer & M Huisman (eds), Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. Lecture Notes in Computer Science, vol. 10806, Springer, Cham, pp. 320-339. DOI: 10.1007/978-3-319-89963-3_19

Multi-cost Bounded Reachability in MDP. / Hartmanns, Arnd; Junges, Sebastian; Katoen, Joost-Pieter; Quatmann, Tim.

Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. ed. / Dirk Beyer; Marieke Huisman. Cham : Springer, 2018. p. 320-339 (Lecture Notes in Computer Science; Vol. 10806).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Multi-cost Bounded Reachability in MDP

AU - Hartmanns,Arnd

AU - Junges,Sebastian

AU - Katoen,Joost-Pieter

AU - Quatmann,Tim

N1 - Open Access

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-89963-3_19

DO - 10.1007/978-3-319-89963-3_19

M3 - Conference contribution

SN - 978-3-319-89962-6

T3 - Lecture Notes in Computer Science

SP - 320

EP - 339

BT - Tools and Algorithms for the Construction and Analysis of Systems

PB - Springer

CY - Cham

ER -

Hartmanns A, Junges S, Katoen J-P, Quatmann T. Multi-cost Bounded Reachability in MDP. In Beyer D, Huisman M, editors, Tools and Algorithms for the Construction and Analysis of Systems: 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II. Cham: Springer. 2018. p. 320-339. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-89963-3_19