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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Multiple Long-Run and \(\omega \) -Regular Objectives in MDPs

  • Julius Ide,
  • Joost-Pieter Katoen,
  • Hannah Mertens,
  • Tim Quatmann

摘要

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.