Verification of infinite-state Markov chains is still a challenge despite several fruitful numerical or statistical approaches. For decisive Markov chains, there is a simple numerical algorithm that frames the reachability probability as accurately as required (however with an unknown complexity). On the other hand when applicable, statistical model checking is in most of the cases very efficient. Here we study the relation between these two approaches showing first that decisiveness is a necessary and sufficient condition for almost sure termination of statistical model checking. Afterwards we develop an approach with application to both methods that substitutes to a non decisive Markov chain a decisive Markov chain with the same reachability probability. This approach combines two key ingredients: abstraction and importance sampling (a technique that was formerly used for efficiency). We develop this approach on a generic formalism called layered Markov chain (LMC). Afterwards we perform an empirical study on probabilistic pushdown automata (an instance of LMC) to understand the complexity factors of the statistical and numerical algorithms. To the best of our knowledge, this prototype is the first implementation of the deterministic algorithm for decisive Markov chains and required us to solve several qualitative and numerical issues.

翻译：尽管已有若干富有成效的数值或统计方法，无限状态马尔可夫链的验证仍是一项挑战。对于决断性马尔可夫链，存在一种简单的数值算法，可按所需精度（尽管复杂度未知）框定可达概率。另一方面，在适用的情况下，统计模型检验在大多数情况下非常高效。本文研究这两种方法之间的关系，首先证明决断性是统计模型检验几乎必然终止的充分必要条件。随后，我们提出一种适用于两种方法的方案，用具有相同可达概率的决断性马尔可夫链替代非决断性马尔可夫链。该方案结合了两个关键要素：抽象与重要性采样（一种先前用于提升效率的技术）。我们在一种称为分层马尔可夫链的通用形式化模型上发展此方法。之后，我们基于概率下推自动机（LMC的一个实例）进行实证研究，以理解统计与数值算法的复杂度因素。据我们所知，该原型是首个针对决断性马尔可夫链的确定性算法实现，并需要我们解决若干定性与数值问题。