2026-08-16T21:50:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23983 2025-08-18T07:11:52Z ddc:004 open_access

Chance and Mass Interpretations of Probabilities in Markov Decision Processes Tsai, Yun Chen Phalakarn, Kittiphon Akshay, S. Hasuo, Ichiro MDP distribution transformer antichain template-based synthesis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Yun Chen Tsai and Kittiphon Phalakarn and S. Akshay and Ichiro Hasuo 2025 Is Part Of LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2025.33 urn:nbn:de:0030-drops-239838 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.33 eng https://creativecommons.org/licenses/by/4.0/legalcode