### Abstract

Language | English |
---|---|

Title of host publication | Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018) |

Editors | Dirk Beyer, Marieke Huisman |

Place of Publication | Cham |

Publisher | Springer |

Pages | 320-339 |

Number of pages | 20 |

ISBN (Electronic) | 978-3-319-89963-3 |

ISBN (Print) | 978-3-319-89962-6 |

DOIs | |

Publication status | Published - 2018 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 10806 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Fingerprint

### Cite this

*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

}

*Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018).*Lecture Notes in Computer Science, vol. 10806, Springer, Cham, pp. 320-339. https://doi.org/10.1007/978-3-319-89963-3_19

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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 - Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018)

A2 - Beyer, Dirk

A2 - Huisman, Marieke

PB - Springer

CY - Cham

ER -