马尔可夫奖励模型的路径抽象
Path Abstraction for Markov Reward Models
浏览论文内容
中文总结 AI 辅助
本文将概率模型检测中的路径抽象技术扩展至马尔可夫奖励模型的期望奖励，证明其保持模型结构与单调吸收性，给出PARI/GP实现的数值求解方法，为相关研究提供支撑。
中文摘要 AI 辅助
路径抽象最初是概率模型检测中用于反例精化的技术。给定一个离散时间马尔可夫链，它会将通过某一状态子集的概率汇总到更小链的新转移上。在早期工作中，我们证明了其正确性及单调吸收性。本文将路径抽象从离散时间马尔可夫链上的可达性概率扩展到马尔可夫奖励模型上的期望奖励。在整个研究过程中，我们采用马尔可夫链的新颖自由幺半群视角，证明了路径抽象在对任意状态集进行抽象时能保持马尔可夫奖励模型的结构，且仍具有单调吸收性。最后，我们给出了一种数值方法，附带PARI/GP中的参考实现，该方法通过求解线性方程组来计算路径抽象，其正确性基于期望奖励与期望转移访问时间之间的关系。
英文摘要
Path abstraction originated as a technique for counterexample refinement in probabilistic model checking. Given a discrete-time Markov chain, it summarises the probabilities passing through a subset of the states onto new transitions of a smaller chain. In earlier work, we proved its correctness and that it is monotonically absorbing. In this paper, we extend path abstraction from reachability probabilities on discrete-time Markov chains to expected rewards on Markov reward models. Working in a novel free monoid view of Markov chains throughout, we prove that path abstraction preserves the Markov reward model structure when abstracting over arbitrary sets of states, and that it remains monotonically absorbing. Finally, we give a numerical recipe, accompanied by a reference implementation in PARI/GP, that computes path abstraction by solving linear equation systems. Its correctness rests on the relationship between expected rewards and expected visiting times of transitions.
