We present a general framework for applying learning algorithms and heuristical guidance to the verification of Markov decision processes (MDPs). The primary goal of our techniques is to improve performance by avoiding an exhaustive exploration of the state space, instead focussing on particularly relevant areas of the system, guided by heuristics. Our work builds on the previous results of Br{\'{a}}zdil et al., significantly extending it as well as refining several details and fixing errors. The presented framework focuses on probabilistic reachability, which is a core problem in verification, and is instantiated in two distinct scenarios. The first assumes that full knowledge of the MDP is available, in particular precise transition probabilities. It performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP without knowing the exact transition dynamics. Here, we obtain probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. In particular, the latter is an extension of statistical model-checking (SMC) for unbounded properties in MDPs. In contrast to other related approaches, we do not restrict our attention to time-bounded (finite-horizon) or discounted properties, nor assume any particular structural properties of the MDP.

翻译：我们提出了一种通用框架，用于将学习算法与启发式引导应用于马尔可夫决策过程（MDP）的验证。该方法的主要目标是通过避免状态空间的穷举探索，转而聚焦于系统中由启发式引导的关键区域，从而提升性能。我们的工作建立在Brázdil等人的先前成果基础上，进行了显著扩展，同时细化了若干细节并修正了错误。该框架聚焦于概率可达性这一验证中的核心问题，并在两种不同场景下进行了实例化。第一种场景假设已知MDP的完整信息（特别是精确的转移概率），通过对模型进行启发式驱动的部分探索，精确得出所需概率的下界与上界。第二种场景则处理仅能对MDP进行采样而无法获知精确转移动态的情况，此时我们给出概率性保证（同样基于下界与上界），并为近似计算提供高效的停止准则。值得强调的是，后者是统计模型检验（SMC）在MDP无界性质上的扩展。与其他相关方法不同，我们既不局限于时间有界（有限时域）或折扣性质，也不假设MDP具有任何特定的结构性质。