Beyond Decisiveness of Infinite Markov Chains

TL;DR

This paper explores the relationship between numerical and statistical methods for verifying infinite-state Markov chains, introducing a new approach that transforms non-decisive chains into decisive ones to improve analysis efficiency.

Contribution

It establishes that decisiveness is key for almost sure termination of statistical model checking and develops a novel method combining abstraction and importance sampling for Markov chain analysis.

Findings

Decisiveness is necessary and sufficient for almost sure termination.

A new approach transforms non-decisive chains into decisive ones with same reachability.

First implementation of a deterministic algorithm for decisive Markov chains.

Abstract

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.