一句话：研究了带标签 MDP 间迹精化问题的可判定性，证明第二 MDP 为马尔可夫链时多项式时间可判定，一般情形不可判定。
本文研究带标签马尔可夫决策过程（MDP）之间的迹精化问题：给定两个带标签 MDP，问是否对第一个 MDP 的每条策略，都存在第二个 MDP 的一条策略，使得两者诱导的带标签马尔可夫链迹等价。作者利用关于状态分布之间一种新的双模拟概念，证明了当第二个 MDP 是马尔可夫链时该问题可在多项式时间内判定；但一般迹精化问题不可判定，即使第一个 MDP 是马尔可夫链也不例外。这一结果解决了 2008 年提出的开放问题。论文还进一步考察了将策略限制为无记忆策略时该问题的可判定性与复杂度。
Given two labelled Markov decision processes (MDPs), the trace-refinement problem asks whether for all strategies of the first MDP there exists a strategy of the second MDP such that the induced labelled Markov chains are trace-equivalent. We show that this problem is decidable in polynomial time if the second MDP is a Markov chain. The algorithm is based on new results on a particular notion of bisimulation between distributions over the states. However, we show that the general trace-refinement problem is undecidable, even if the first MDP is a Markov chain. Decidability of those problems was stated as open in 2008. We further study the decidability and complexity of the trace-refinement problem provided that the strategies are restricted to be memoryless.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FijalkowKS16,
title = {Trace Refinement in Labelled Markov Decision Processes},
author = {Nathanaël Fijalkow and Stefan Kiefer and Mahsa Shirmohammadi},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 2},
year = {2020},
doi = {10.23638/lmcs-16(2:10)2020}
}