Learning Algorithms for Verification of Markov Decision Processes

本文提出了一个通用框架，用于将学习算法和启发式指导应用于马尔可夫决策过程（MDPs）的验证，基于Br\'azdil，T.等人（2014）的思想。该工作中所提出的技术的主要目标是通过避免对状态空间进行全面探索并由启发式指导来提高性能。本文在该方法的基础上进行了显著扩展。基础理论的几个细节得到了完善和修正。第1.3节概述了所有差异。本文提出的框架侧重于概率可达性，这是验证中的核心问题，并在两个不同的场景中实例化。第一种情况假设我们可以获得MDP的完全知识，特别是精确的转移概率。它对模型进行启发式驱动的部分探索，得出所需概率的精确下限和上限。第二种情况则处理我们可能只能对MDP进行采样而不知道确切转移动态的情况。在这里，我们获得概率保证，同样以下限和上限为基础，这为近似提供了高效的停止准则。特别是，后者是MDP中无界属性的统计模型检查（SMC）的扩展。与其他相关方法不同的是，我们不仅限于有限时间界（有限时间）或折扣属性，并且不假设MDP具有任何特定的结构属性。

本文的主要问题是如何利用学习算法和启发式指导来验证马尔可夫决策过程（MDP），特别是在概率可达性方面。该方法的目标是通过避免对状态空间的全面探索来提高性能。

本文提出了一个通用框架，通过学习算法和启发式指导来验证MDP，并在两个不同的场景中进行了实例化。该框架不仅可以处理具有精确转移概率的MDP，还可以处理只能对MDP进行采样的情况。

本文的亮点包括：1.针对概率可达性问题提出了一种启发式驱动的部分探索模型，得出了概率的精确下限和上限；2.针对只能对MDP进行采样的情况，提出了一种基于统计模型检查（SMC）的方法，得出了概率的下限和上限；3.与其他相关方法不同，本文不仅限于有限时间或折扣属性，也不假设MDP具有特定的结构属性。

近期在这个领域中，一些相关的研究包括：1. 'A Survey of Techniques for Approximate Probabilistic Model Checking'；2. 'Probabilistic Model Checking with Statistical Abstraction and Reinforcement Learning'；3. 'Scalable Verification of Linear MDP Properties by Leveraging Structural Properties'