We present a general framework for applying learning algorithms and
heuristical guidance to the verification of Markov decision processes (MDPs),
based on the ideas of Br\'azdil, T. et al. (2014). Verification of Markov
Decision Processes Using Learning Algorithms. The primary goal of the
techniques presented in that work is to improve performance by avoiding an
exhaustive exploration of the state space, guided by heuristics. This approach
is significantly extended in this work. Several details of the base theory are
refined and errors are fixed. Section 1.3 provides an overview of all
differences.
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)，主要关注概率可达性问题，包括精确和近似的情况，不受时间限制或折扣因子等条件的限制。