arXiv:2403.09184v4 宣告类型: replace-cross 摘要: 我们提出了一种通用框架，用于将学习算法和启发式指导应用于马尔可夫决策过程（MDP）的验证。我们的技术主要目标是通过避免对状态空间的详尽探索来提高性能，而是专注于系统的特别相关区域，同时受到启发式的指导。我们的工作基于Brázdil等人之前的成果，显著扩展了它，并对一些细节进行了细化并修正了一些错误。 该框架主要关注概率可达性问题，这是验证的核心问题，并且在两种不同的场景中进行了具体化。第一个假设我们可以完全了解MDP，特别是精确的转移概率。它进行了一种基于启发式的部分探索，提供了所需概率的精确下界和上界。第二个场景则处理我们只能抽样MDP而不知道确切的转移动力学的情况。这里，我们在下界和上界方面获得了概率保证，这提供了近似终止标准的高效方法。特别是后者是统计模型检查（SMC）在MDP中未加约束性质的扩展。与相关方法相比，我们没有限制我们的注意力仅限于时间限制（有限时程）或折现性质，也没有假设MDP的任何特定结构性质。