Chance and Mass Interpretations of Probabilities in Markov Decision Processes (Extended Version)

TL;DR

This paper introduces a unified semantic framework for Markov decision processes that incorporates chance and mass interpretations, explores new semantics, and provides algorithms for reachability problems.

Contribution

It unifies different probabilistic semantics of MDPs using the chance-mass classifier and studies the computational complexity of reachability in new semantics.

Findings

Unified semantics via chance-mass classifier

New semantics are computationally hard for reachability

Provided algorithms for reachability in new semantics

Abstract

Markov decision processes (MDPs) are a popular model for decision-making in the presence of uncertainty. The conventional view of MDPs in verification treats them as state transformers with probabilities defined over sequences of states and with schedulers making random choices. An alternative view, especially well-suited for modeling dynamical systems, defines MDPs as distribution transformers with schedulers distributing probability masses. Our main contribution is a unified semantical framework that accommodates these two views and two new ones. These four semantics of MDPs arise naturally through identifying different sources of randomness in an MDP (namely schedulers, configurations, and transitions) and providing different ways of interpreting these probabilities (called the chance and mass interpretations). These semantics are systematically unified through a mathematical construct called chance-mass (CM) classifier. As another main contribution, we study a reachability problem in each of the two new semantics, demonstrating their hardness and providing two algorithms for solving them.