Beyond Decisiveness of Infinite Markov Chains

TL;DR

This prototype is the first implementation of the deterministic algorithm for decisive Markov chains and required us to solve several qualitative and numerical issues.

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.

Figures (3)

• Figure 1: $\mathcal{C}, \mathcal{C^\bullet},\mathcal{C'}$ are three Markov chains and $\alpha$ is defined by $\alpha(q_0)=0$ and for all $n>0$, $\alpha(p_n)=\alpha(q_n)=n$. $\mathcal{C'}$ is a biased Markov chain of $(\calC,\{q_0\}) \stackrel{\alpha}{\hookrightarrow} (\calC^\bullet,\{0\})$.
• Figure 2: Computation time for Example \ref{['example:pta']} in logarithmic scale. Given a value for $p$, the threshold $N_0$ is chosen as the smallest integer such that $(\mathcal{W}^p,[0,N_0])$ defines an $\alpha$-abstraction.
• Figure 3: Computation time as a function of $p$ for Example \ref{['example:pta7']}.

Theorems & Definitions (26)

• Definition 1
• Definition 2
• Definition 3
• Proposition 3: Termination and correctness of Algorithm \ref{['algo:approx']}
• Lemma 3
• Proposition 4
• Proposition 5: Termination and correctness of Algorithm \ref{['algo:smc']}
• Definition 6: biased Markov chain and likelihood
• Example 7
• Proposition 7