J-P: MDP.FP.PP.: 将马尔可夫决策过程中的总期望奖励表述为最小不动点及其对概率程序操作语义的应用（技术报告）
计算机科学中的逻辑
2024-11-26 v1 编程语言
摘要
带奖励的马尔可夫决策过程 (MDP) 是一种广泛且被广泛研究的模型，用于处理具有概率和非决定性选择的系统。关于 MDP 的一个基本结果是，其最小和最大期望奖励满足 Bellman 最优方程。对于各种 MDP 类——特别是有限状态 MDP、正有界模型和负模型——已知期望奖励是这些方程的最小解。然而，这些 MDP 类过于限制，难以用于概率程序验证。特别是，它们假设所有奖励都是有限的。对于建模 1 维随机漫步的概率程序的预期运行时间这一情况，已不成立。本文发展了一种不包含这些限制的 MDP 期望奖励的广义最小不动点表述。此外，我们演示了可利用该表述来证明 weakest-preexpectation 风格计算与操作语义 MDP 模型的正确性。
引用
@article{arxiv.2411.16564,
title = {J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report)},
author = {Kevin Batz and Benjamin Lucien Kaminski and Christoph Matheja and Tobias Winkler},
journal= {arXiv preprint arXiv:2411.16564},
year = {2024}
}