Multi-cost Bounded Tradeoff Analysis in MDP

Journal of Automated Reasoning, vol. 64, pp. 1483–1522

Abstract

Abstract We provide a memory-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. We cover multi-objective reachability and expected cost objectives, and combinations thereof. We further transfer approaches for computing quantiles over single cost bounds to the multi-cost case and highlight the ensuing challenges. An empirical evaluation shows the scalability of our new approach both in terms of memory consumption and runtime. We discuss the need for more detailed visual presentations of results beyond Pareto curves and present a first visualisation approach that exploits all the available information from the algorithm to support decision makers.

Authors 4

1. Arnd Hartmanns corresponding

   University of Twente

   Affiliation as printed

   University of Twente, Enschede, The Netherlands

2. Sebastian Junges Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen, Aachen, Germany

3. Joost-Pieter Katoen Aachen

   RWTH Aachen University · University of Twente

   Affiliation as printed

   RWTH Aachen, Aachen, Germany

   University of Twente, Enschede, The Netherlands

4. Tim Quatmann Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen, Aachen, Germany