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

Le résumé fourni par la source

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.

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.