Multiple Long-Run and $$\omega $$-Regular Objectives in MDPs

Lecture notes in computer science, pp. 526–546

Abstract

We consider Markov decision processes (MDPs) with three types of objectives: (1) the probability of satisfying an $$\omega $$ -regular objective, (2) the expected long-run average (LRA) reward, and (3) the probability that the long-run average reward exceeds a given threshold. All types of objectives address infinite system behavior. The challenge lies in capturing all possible trade-offs between satisfiable LTL formulas and achievable LRA rewards inside the end components (ECs) of the MDP. Our approach translates LTL to Rabin objectives and then splits ECs into various sub-components in which (a subset of) the Rabin objectives are satisfied. LRA expectation and threshold satisfaction objectives are then optimized in those sub-components independently, where we exploit iterative techniques for multiple expected LRA reward objectives. We realized the approach into the Storm model checker and empirically show feasibility of verification of large models with more than half a million states—outperforming a reference implementation based on linear programming by several orders of magnitude.

Authors 4

1. Julius Ide Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

2. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

3. Hannah Mertens Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany

4. Tim Quatmann corresponding Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University, Aachen, Germany