# Beyond Decisiveness of Infinite Markov Chains

Benoît Barbot, Patricia Bouyer, Serge Haddad

► To cite this version:

Benoît Barbot, Patricia Bouyer, Serge Haddad. Beyond Decisiveness of Infinite Markov Chains. 44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2024), Dec 2024, Gandhinagar, Gujarat, India. pp.8:1-8:22, 10.4230/lipics.fsttcs.2024.8 .
hal-04822969

HAL Id: hal-04822969

https://hal.science/hal-04822969v1

Submitted on 6 Dec 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Beyond Decisiveness of Infinite Markov Chains

Benoît Barbot

<figure><img src="image_2.png" /></figure>

Univ Paris Est Creteil, LACL, F-94010 Creteil, France

Patricia Bouyer

<figure><img src="image_3.png" /></figure>

Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles,
91190 Gif-sur-Yvette, France

Serge Haddad

<figure><img src="image_4.png" /></figure>

Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles,
91190 Gif-sur-Yvette, France

## 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.

**2012 ACM Subject Classification** Mathematics of computing → Markov processes; Theory of computation → Concurrency

**Keywords and phrases** Markov Chains, Infinite State Systems, Numerical and Statistical Verification

**Digital Object Identifier** 10.4230/LIPIcs.FSTTCS.2024.8

**Related Version** Full Version: https://doi.org/10.48550/arXiv.2409.18670 [3]

**Supplementary Material** Software (Source Code): https://git.lacl.fr/barbot/Cosmos
archived at swh:1:dir:36e5a6f37d834251fb9a96becb481e96f5c68e6c

**Funding** This work has been partly supported by ANR projects MAVeriQ (ANR-20-CE25-0012) and BisoUS (ANR-22-CE48-0012).

# 1 Introduction

**Infinite-state discrete time Markov chains.** In finite Markov chains, computing reachability probabilities can be performed in polynomial time using linear algebra techniques [14]. The case of infinite Markov chains is much more difficult, and has initiated several complementary proposals:

- A first approach consists in analyzing the high-level probabilistic model that generates the infinite Markov chains. For instance in [5], the authors study probabilistic pushdown automata and show that the reachability probability can be expressed in the first-order theory of the reals. Thus (by a dichotomous algorithm) this probability can be approximated within an arbitrary precision.

<figure><img src="image_5.png" /></figure>

© Benoît Barbot, Patricia Bouyer, and Serge Haddad;
licensed under Creative Commons License CC-BY 4.0

44th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
(FSTTCS 2024).

Editors: Siddharth Barman and Slawomir Lasota; Article No. 8; pp. 8:1–8:22

<figure><img src="image_6.png" /></figure>

Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
8:2 Beyond Decisiveness of Infinite Markov Chains

A second approach consists in designing algorithms, whose correctness relies on a semantic
property of the Markov chains, and which outputs an interval of the required precision
that contains the reachability probability. *Decisiveness* [1] is such a property: given
a target set *T*, it requires that almost surely, a random path either visits *T* or some
state from which *T* is unreachable. In order to be effective, this algorithm needs the
decidability of the (qualitative) reachability problem. For instance finite Markov chains
are decisive w.r.t. any set of states. Several other classes of denumerable Markov
chains are decisive by construction: Petri nets (or equivalently VASS) with constant
weights<fnref n="1" /> on transitions w.r.t. any upward-closed target set [1], lossy channel systems
with constant weights and constant message loss probability [1] w.r.t. any finite target
set, regular Petri nets with arbitrary weights w.r.t. any finite target set [7]. Also a
critical associated decision problem is the decidability of decisiveness in the high-level
model that generates the Markov chains. Decisiveness is decidable for several classes of
systems: probabilistic pushdown automata with constant weights [5], random walks with
polynomial weights [7] which can be generalized to probabilistic homogeneous one-counter
machines with polynomial weights [7]. This class is particularly interesting since it extends
the well-known model of quasi-birth death processes (QBDs).

- The statistical model checking (SMC) [17, 16] approach consists in generating numerous random paths and computing an interval of the required precision that contains the reachability probability with an arbitrary high probability (the confidence level). As we will show later on, the effectiveness of SMC also requires some semantic property, which will happen to be decisiveness.

**SMC and importance sampling.** When the reachability probability is very small, the SMC approach requires a huge number of random paths, which prohibits its use. In order to circumvent this problem (called the *rare event problem*), several approaches have been proposed (see for instance [13]), among which the *importance sampling* method. This seems to be in practice, one of the most efficient approaches to tackle this problem. Importance sampling consists in sampling the paths in a biased<fnref n="2" /> Markov chain (w.r.t. the original one) that increases the reachability probability. In order to take into account the bias, a likelihood for any path is computed (on-the-fly) and the importance sampling algorithm returns the empirical average value of the likelihood. While the expected returned value is equal to the reachability probability under evaluation, the confidence interval returned by the algorithm is, without further assumption, only “indicative” (i.e., it does not necessary fulfill the features of a confidence interval) – boundedness of the likelihood is indeed required (but hard to ensure). In [4], a simple relation between the biased and the original finite Markov chain is stated that (1) ensures that the confidence interval returned by the algorithm is a “true” interval and that (2) the variance of the estimator (here the likelihood) is reduced w.r.t. the original estimator, entailing an increased efficiency of the SMC.

**Related work when the Markov chain is not decisive.** Very few works have addressed the effectiveness of SMC for infinite non decisive Markov chains. The main proposal [15] consists in stopping the computation at each step with some fixed (small) probability. The successful paths are equipped with a numerical value, whose average over the paths is returned by the

<footnote n="1">¹ That is, each transition is assigned a weight, and the probability for a transition to be fired is its relative weight w.r.t. all enabled transitions.</footnote>

<footnote n="2">² In the sense that probability values in the biased chain differ from the original chain.</footnote>
algorithm. It turns out that it is an importance sampling method, which has surprisingly not been pointed out by the authors. However here again, since the likelihood is (in general) not bounded, the interval returned by the algorithm is not a confidence interval. An alternative notion called divergence has been proposed in [8] to partly cover the case of non-decisive Markov chains.

**Our contributions.** We introduce the *reward reachability problem* (a slight generalization of the reachability problem) by associating a reward with every successful path and looking for the expected reward. We first establish that decisiveness is a necessary and sufficient condition for the almost-sure termination of SMC for bounded rewards.

- Our major contribution consists in establishing a relation between a non-decisive Markov chain and an auxiliary Markov chain, called an *abstraction*, with the following property: they can be combined into a biased Markov chain, which happens to be **decisive**; the SMC with importance sampling on this chain provides a confidence interval for the reachability probability of the original Markov chain.

- We furthermore show that importance sampling can be applied to adapt (based on the abstraction) the deterministic algorithm of [1].

- Afterwards we illustrate the interest of this approach, by exhibiting a generic model called *layered Markov chains* (LMC), which can be instantiated for instance by probabilistic pushdown automata with polynomial weights. These automata cannot be handled with the technique of [5].

- Finally we present several experiments, based on the tool Cosmos [2], which compare the SMC and the deterministic approaches. It allows to identify how various factors impact the efficiency of the algorithms. We provide within the tool Cosmos the first implementation of the deterministic approach for decisive Markov chains, which required us to solve several numerical issues. As a rough summary, at the price of a confidence level against certainty, the computing time of SMC is generally several magnitude orders smaller than the one of the deterministic algorithm.

**Organization.** In section 2, we introduce the numerical and statistical specification of the reward reachability problem, and we recall the notion of decisiveness. In section 3, we focus on the decisiveness property establishing that decisiveness is a necessary and sufficient condition for almost sure termination of statistical model checking. Section 4 contains our main contribution: the specification of an abstraction of a Markov chain, its use for solving the reward reachability problems for non decisive Markov chains via importance sampling and the development of this method for LMCs. Afterwards in Section 5, we present some implementation details and experimentally compare the deterministic and the statistical approaches. We conclude and give some perspectives to this work in Section 6.

Some missing proofs and more details on the implementation can be found in the appendix.
Full proofs are given in [3].

## 2 Preliminaries

In this preliminary section we define Markov chains, and the decisiveness property.

► **Definition 1.** A discrete-time Markov chain (or simply Markov chain) $\mathcal{C} = (S, P)$ is defined by a countable set of states $S$ and a transition probability matrix $P$ of size $S \times S$. Given an initial state $s_0 \in S$, the state of the chain at time $n$ is a random variable (r.v. in short) $X_n^{C,s_0}$ defined by: $\Pr(X_0^{C,s_0} = s_0) = 1$ and $\Pr(X_{n+1}^{C,s_0} = s' | \bigwedge_{i \le n} X_i^{C,s_0} = s_i) = P(s_n, s')$.
8:4 Beyond Decisiveness of Infinite Markov Chains

If $\mathcal{C} = (S, P)$ is a Markov chain, we write $E_{\mathcal{C}} = \{(s, s') \in S \times S \mid P(s, s') > 0\}$ for the set of edges of $\mathcal{C}$, and $\rightarrow_{\mathcal{C}}$ for the corresponding edge relation. A state $s$ is absorbing if $P(s, s) = 1$. A Markov chain $\mathcal{C}$ is said effective whenever for every $s \in S$, the support of $P(s, \cdot)$ is finite and computable, and for every $s, s' \in S$, $P(s, s')$ is computable. A target set $T \subseteq S$ is said effective whenever its membership problem is decidable. In the following, we will always consider effective Markov chains and effective target sets when speaking of algorithms, without always specifying it.

A finite (resp. infinite) path is a finite (resp. infinite) sequence of states $\rho = s_0 s_1 s_2 \dots \in S^+$ (resp. $S^\omega$) such that for every $0 \le i, (s_i, s_{i+1}) \in E_{\mathcal{C}}$. We write $\text{first}(\rho)$ for $s_0$, and whenever $\rho \in S^+$, we write $\text{last}(\rho)$ for the last state of $\rho$. For every $n \in \mathbb{N}$, we write $\rho[n] \stackrel{\text{def}}{=} s_n$ and $\rho_{\le n} \stackrel{\text{def}}{=} s_0 s_1 s_2 \dots s_n$. If $\rho = s_0 \dots s_n$, $\mathbf{Pr}(\rho)$ is equal to $\prod_{i<n} P(s_i, s_{i+1})$ and corresponds to the probability that this path is followed when starting from its initial state $s_0$.

The random infinite path generated by process $(X_n^{C,s_0})_{n \in \mathbb{N}}$ will be denoted $\varrho^{C,s_0}$. Note that $s \rightarrow_{\mathcal{C}}^* s'$ if and only if $\mathbf{Pr}(\varrho^{C,s} \models \Diamond\{s'\}) > 0$ (we use the $\Diamond$ modality of temporal logics, which expresses *Eventually*, and later, we will also write $\Diamond_{>0}$ for the *strict Eventually* modality – eventually but not now –, as well as $\Diamond_{\le n}$ for *n-steps Eventually*). Finally, for every $s, s' \in S$, we define the time from $s$ to $s'$ as the random variable $\tau^{C,s,s'} = \min\{i \in \mathbb{N} \mid i > 0 \text{ and } X_i^{C,s} = s'\}$, with values in $\mathbb{N}_{>0} \cup \{+\infty\}$. To ease the reading, we will omit subscripts $\mathcal{C}$ and $T$, or superscripts $^C$ in the various notations, whenever it is obvious in the context.

In this paper we are interested in evaluating the probability to reach a designed target set $T$ from an initial state $s_0$ in a Markov chain $\mathcal{C}$, that is, $\mu_{\mathcal{C},T}(s_0) \stackrel{\text{def}}{=} \mathbf{Pr}(\varrho^{C,s_0} \models \Diamond T)$. In general, it might be difficult to compute such a value, which will often not even be a rational number. That is why like many other research works we will show how to compute accurate approximations (surely or with a high level of confidence). We present our solutions in a more general setting which would anyway be necessary in the following developments.

**Definition 2.** Let $T \subseteq S$ and $\rho \in S^\omega$. We let $\text{first}_T(\rho) := \min\{i \in \mathbb{N} \mid \rho[i] \in T\} \in \mathbb{N} \cup \{\infty\}$. Let $L: S^+ \rightarrow \mathbb{R}$ be a function. The function $f_{L,T}: S^\omega \rightarrow \mathbb{R}$ is then defined by:<fnref n="3" />

$$f_{L,T}(\rho) := \begin{cases} L(\rho_{\le \text{first}_T(\rho)}) & \text{if } \text{first}_T(\rho) \in \mathbb{N} \\ 0 & \text{otherwise} \end{cases}$$

We say that $f_{L,T}(\rho)$ is the *reward* of $\rho$. The function $f_{L,T}$ is called the *T-function for L*; let $B \in \mathbb{R}_{>0}$, $f_{L,T}$ is said *B-bounded* whenever $\max(|f_{L,T}(\rho)| \mid \rho \in S^\omega) \le B$. Observe that $f_{L,T}$ could be *B-bounded* for some $B$ even if $L$ is unbounded.

We will be interested in evaluating the expected reward $\nu_{C,L,T}(s_0) \stackrel{\text{def}}{=} \mathbf{E}(f_{L,T}(\varrho^{C,s_0}))$.<fnref n="4" /> Note that if $L$ is constant equal to 1, then $f_{L,T} = \mathbb{1}_{\Diamond T}$ is the indicator function for paths that visit $T$, in which case $\nu_{C,L,T}(s_0) = \mu_{C,T}(s_0)$.

We define two problems related to the accurate estimation of these values:

■ The EvalER problem (EvalER stands for “Evaluation of the Expected Reward”) asks for a deterministic algorithm, which:

1. takes as input a Markov chain $\mathcal{C}$, an initial state $s_0$, a computable function $L: S^+ \rightarrow \mathbb{R}_{\ge 0}$, a target set $T$, a precision $\varepsilon > 0$, and

2. outputs an interval $I \subseteq \mathbb{R}$ of length bounded by $\varepsilon$ such that $\nu_{C,L,T}(s_0) \in I$.

The particular case of the reachability probability (when $L$ is constant equal to 1) is denoted EvalRP.

<footnote n="3">³ This function is measurable as a pointwise limit of measurable functions.</footnote>

<footnote n="4">⁴ $\mathbf{E}$ denotes the expectation.</footnote>
■ The EstimER problem (EstimER stands for “Estimation of the Expected Reward”) asks for a probabilistic Las Vegas algorithm, which:

1. takes as input a Markov chain $\mathcal{C}$, an initial state $s_0$, a computable function $L: S^+ \to \mathbb{R}_{\ge 0}$, a target set $T$, a precision $\varepsilon > 0$, a confidence value $\delta > 0$, and

2. outputs a random interval $I \subseteq \mathbb{R}$ of length bounded by $\varepsilon$ such that $\mathrm{Pr}(\nu_{C,L,T}(s_0) \notin I) \le \delta$, and $\mathrm{E}(\mathrm{mid}(I)) = \nu_{C,L,T}(s_0)$, where $\mathrm{mid}(I)$ is the middle of interval $I$.<fnref n="5" />

The particular case of the reachability probability (when $L$ is constant equal to 1) is denoted EstimRP.

In [1], the concept of decisiveness for Markov chains was introduced. Roughly, decisiveness allows to lift some “good” properties of finite Markov chains to countable Markov chains. We recall this concept here. Let $T \subseteq S$ and denote the “avoid set” of $T$ by $\mathrm{Av}_C(T) \stackrel{\mathrm{def}}{=} \{s \in S \mid \mathrm{Pr}(\varrho^{C,s} \models \Diamond T) = 0\}$.

► **Definition 3.** The Markov chain $\mathcal{C}$ is decisive w.r.t. $T$ from $s_0$ if $\mathrm{Pr}(\varrho^{C,s_0} \models \Diamond T \lor \Diamond \mathrm{Av}_C(T)) = 1$.

### 3 Analysis of decisive Markov chains

We fix for this section a Markov chain $\mathcal{C} = (S, P)$, an initial state $s_0$, a computable function $L: S^+ \to \mathbb{R}_{\ge 0}$ and a target set $T$, and we assume w.l.o.g. that $T$ is a set of absorbing states. We present two approaches (extended from the original ones) to compute the expected value of the function $f_{L,T}$ that require $\mathcal{C}$ to be decisive w.r.t. $T$ from $s_0$.

#### 3.1 Decisiveness and approximation algorithm

In the original paper proposing the concept of decisiveness [1], “theoretical” approximation schemes were designed. We slightly extend the one designed for reachability objectives in our more general setting, see Algorithm 1.

■ **Algorithm 1** Approximation scheme for the EvalER problem; the fair\_extract operation ensures that any element put in the set cannot stay forever in an execution including an infinite number of extractions; a simple implementation can be done with a queue.

input : $\mathcal{C} = (S, P)$ a countable Markov chain, $s_0 \in S$ an initial state, $L: S^+ \to \mathbb{R}_{\ge 0}$ a computable function, $T \subseteq S$ a target set s.t. $\mathrm{Av}_C(T)$ is effective and $f_{L,T}$ is B-bounded, $\varepsilon > 0$ a precision.
1 $e := 0, p_{\mathrm{fail}} := 0, p_{\mathrm{succ}} := 0; \mathrm{set} := \{(1, s_0)\}$;
2 while $1 - (p_{\mathrm{succ}} + p_{\mathrm{fail}}) > \varepsilon/2B$ do
3   $(p, \rho) := \mathrm{fair\_extract}(\mathrm{set}); s := \mathrm{last}(\rho)$;
4   if $s \in T$ then $e := e + p \cdot L(\rho)$; $p_{\mathrm{succ}} := p_{\mathrm{succ}} + p$;
5   else if $s \in \mathrm{Av}(T)$ then $p_{\mathrm{fail}} := p_{\mathrm{fail}} + p$;
6   else
7   | for $s \to_C s'$ do $\mathrm{insert}(\mathrm{set}, (p \cdot P(s, s'), \rho s'))$;
8 end
9 return $[e - \varepsilon/2, e + \varepsilon/2]$

<footnote n="5">⁵ The last condition on the middle of *I* means that the estimator is unbiased.</footnote>
8:6 Beyond Decisiveness of Infinite Markov Chains

The termination and correctness of this algorithm is established by the following proposi-
tion, whose proof is given in [3] and a special case of which is given in [1].

► **Proposition 4** (Termination and correctness of Algorithm 1). *Algorithm 1 solves the EvalER problem if and only if C is decisive w.r.t. T from s₀.*

Up to our knowledge, the version of this algorithm for computing reachability probabilities
has not been implemented, hence the terminology “theoretical” scheme above. Also, there is
no known convergence speed. Later in section 5, we briefly describe an efficient implementation
of this scheme by designing some tricks.

3.2 Decisiveness and (standard) statistical model-checking

The standard statistical model-checking (SMC in short) consists in sampling a large number of paths to simulate the random variables $X^{s_0} = (X_n^{s_0})_{n \ge 0}$; a sampling is stopped when it hits $T$ or $\text{Av}(T)$, and a value 1 (resp. 0) is assigned when $T$ (resp. $\text{Av}(T)$) is hit; finally the average of all the values is computed. This requires that almost-surely a path hits $T$ or $\text{Av}(T)$, which is precisely decisiveness of the Markov chain w.r.t. $T$ from $s_0$. This allows to compute an estimate of the probability to reach $T$. We describe more precisely the approach and extend the context to allow the estimation of the expected value of $f_{L,T}$.

**Algorithm 2** Statistical model-checking for the EstimER problem.

**input** : $\mathcal{C} = (S, P)$ a countable Markov chain, $s_0 \in S$ an initial state, $L: S^+ \to \mathbb{R}$ a computable function, $T \subseteq S$ a target set s.t. $\text{Av}_C(T)$ is effective and $f_{L,T}$ is B-bounded, $\varepsilon > 0$ a precision, $\delta > 0$ a confidence value.
1 $N := \lceil \frac{8B^2}{\varepsilon^2} \log(\frac{2}{\delta}) \rceil$; $\hat{f} := 0$;
2 **for** $i$ **from** 1 **to** $N$ **do**
3 &nbsp;&nbsp;&nbsp; $\rho := s_0$; $s := s_0$;
4 &nbsp;&nbsp;&nbsp; **while** $s \notin T \cup \text{Av}(T)$ **do** $s' := \text{sample}(P(s, \cdot))$; $\rho := \rho s'$; $s := s'$;
5 &nbsp;&nbsp;&nbsp; **if** $s \in T$ **then** $\hat{f} := \hat{f} + L(\rho)$;
6 **end**
7 $\hat{f} := \frac{\hat{f}}{N}$; **return** [$\hat{f} - \varepsilon/2, \hat{f} + \varepsilon/2$]

The SMC approach is presented as Algorithm 2 (where $\text{Av}(T)$ is assumed to be effective).
This is in general a semi-algorithm, since it may happen that the **while** loop is never left at
some iteration $i$. Nevertheless, decisiveness ensures almost sure (a.s.) termination:

► **Lemma 5.** *The *while* loop a.s. terminates if and only if C is decisive w.r.t. T from s₀.*

The correctness of the algorithm will rely on this proposition that can be straightforwardly
deduced from the Hoeffding inequality [10].

► **Proposition 6.** Let $V_1, \dots, V_N$ be B-bounded independent random variables and let $V = \frac{1}{N} \sum_{i=1}^N V_i$. Let $\varepsilon, \delta > 0$ be such that $N \ge \frac{8B^2}{\varepsilon^2} \log(\frac{2}{\delta})$. Then: $\text{Pr}(|V - \text{E}(V)| \ge \frac{\varepsilon}{2}) \le \delta$.

We can now state the following important result.

► **Proposition 7 (Termination and correctness of Algorithm 2).** *Algorithm 2 solves the EstimER problem if and only if C is decisive w.r.t. T from s₀.*
**Proof.** The termination is a consequence of Lemma 5. The correctness is a consequence of Proposition 6, by taking random variable $V_i$ as $f_{L,T}(\rho^{C,s_0})$. In this case, $V$ is equal to the value of $\hat{f}$ at the end of the algorithm, which completes the argument. ◀

While termination is guaranteed by the previous corollary the (time) efficiency of the simulation remains a critical factor. In particular, the expected value $D$ of the random time $T^{s_0, T \cup Av(T)}$ to reach $T \cup Av(T)$ from $s_0$ should be finite; in this case, the average simulation time will be $D$ and therefore the complexity of the whole approach will be linear in the number of simulations. Decisiveness does not ensure this; so a dedicated analysis needs to be done to ensure efficiency of the approach.

# 4 Beyond decisiveness

In the previous section, we have presented two generic approaches for analyzing infinite (denumerable) Markov chains. They both only apply to **decisive** Markov chains. In this section, we twist the previous approaches, so that they will be applicable to analyze some **non decisive** Markov chains as well. Our proposition follows the following steps:

- based on the *importance sampling* approach, we explain how the analysis of the original Markov chain can be transferred to that of a *biased* Markov chain (Subsection 4.1);

- we explain how a biased Markov chain can be automatically constructed via an *abstraction*, and give conditions ensuring that the obtained biased Markov chain can be analyzed (Subsection 4.2);

- we give a generic framework based on *layered Markov chains* and *random walks*, with conditions on various parameters to safely apply the designed approach (Subsection 4.3).

We fix an effective countable Markov chain $C = (S, P)$, $s_0 \in S$ an initial state, $L: S^+ \to \mathbb{R}_{\ge 0}$ a computable function, and $T \subseteq F \subseteq S$ two effective sets, with both $Av_C(F)$ and $Av_C(T)$ being effective (note that $Av_C(F) \subseteq Av_C(T)$). Since we are interested in the probability to reach $T$, from now on, we assume that $T$ is absorbing in $C$ and that $s_0 \notin Av_C(F)$.

## 4.1 Model-checking via a biased Markov chain

Importance sampling has been introduced in the fifties [12] to evaluate rare-event probabilities (see the book [13] for more details). We revisit the approach in our more general setting of reward reachability, with the extra set $F$.<fnref n="6" /> The role of $F$ will be discussed page 10. This approach applies the standard SMC approach with a correction factor, called *likelihood*, to another Markov chain.

► **Definition 8 (biased Markov chain and likelihood).** Let $C = (S, P)$ with $T \subseteq F \subseteq S$ and $C' = (S', P')$ be Markov chains such that:

- $S' = (S \setminus Av_C(F)) \uplus \{s_\_\}$, where $s_\_ \notin S$;

- In $C'$ all states of $T \cup \{s_\_\}$ are absorbing;

- $\forall s, s' \in S \setminus Av_C(F), P(s, s') > 0 \Rightarrow P'(s, s') > 0$ (1)

Then $C'$ is a biased Markov chain of $(C, T, F)$ and the likelihood $\gamma_{C,C'}$ is the non negative function defined for finite paths $\rho \in S'^+$ s.t. $\mathbf{Pr}'(\rho) > 0$ by: $\gamma_{C,C'}(\rho) \stackrel{\text{def}}{=} \frac{\mathbf{Pr}(\rho)}{\mathbf{Pr}'(\rho)}$ if $\rho$ does not visit $s_\_$, and $\gamma_{C,C'}(\rho) \stackrel{\text{def}}{=} 0$ otherwise.

<footnote n="6">⁶ The standard importance sampling method is recovered when $F = T$.</footnote>
8:8 Beyond Decisiveness of Infinite Markov Chains

<figure><img src="image_7.png" /><figcaption>■ **Figure 1** $C, C^*, 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$. $C'$ is a biased Markov chain of $(C, \{q_0\}) \stackrel{\alpha}{\hookrightarrow} (C^*, \{0\})$.</figcaption></figure>

Eqn. (1) ensures that this modification cannot remove transitions between states of $S \setminus \text{Av}_C(F)$, but it can add transitions. So, $\text{Av}_{C'}(F) = \{s_{-}\}$. We fix a biased Markov chain $C'$ for the rest of this subsection and omit the subscripts for the likelihood function $\gamma$. The likelihood can be computed greedily from the initial state: if $\rho \cdot s$ is a finite path of $C'$ such that $\gamma(\rho)$ has been computed, then $\gamma(\rho \cdot s)$ is equal to 0 if $s = s_{-}$, and $\gamma(\rho) \cdot \frac{P(last(\rho),s)}{P(last(\rho),s_{-})}$ otherwise.

► **Example 9.** Figure 1(c) depicts a Markov chain which is a biased Markov chain of Figure 1(a) with $T = F = \{q_0\}$ and $\text{Av}_C(F) = \text{Av}_C(T) = \{p_0\}$.

Using the likelihood, we can define the new function of interest in Markov chain $C'$. We let $L' \stackrel{\text{def}}{=} L \cdot \gamma$ and we realize that the expected reward of $f_{L',T}$ in $C'$ from $s_0$ coincides with the expected reward of $f_{L,T}$ in $C$ from $s_0$, as stated below.

► **Proposition 10.** $\mathbf{E}(f_{L',T}(\varrho^{C',s_0})) = \mathbf{E}(f_{L,T}(\varrho^{C,s_0}))$.

The proof of this proposition is given in Appendix A.1. The idea is that the likelihood in $C'$ compensates for the bias in the probabilities in $C'$ w.r.t. original probabilities in $C$. Thanks to this result, the computation of the expected value of $f_{L,T}$ in $C$ can be reduced to the computation of the expected value of $f_{L',T}$ in $C'$. Thus, as soon as $C'$ and $f_{L',T}$ satisfy the hypotheses of Proposition 4 (resp. Proposition 7) for the EvalER (resp. EstimER) problem, Algorithm 1 (resp. Algorithm 2) can be applied to $C'$, which will solve the corresponding problem in $C$. Specifically, the second method is what is called the *importance sampling* of $C$ via $C'$. Observe the following facts:

- the decisiveness hypothesis only applies to the biased Markov chain $C'$, not to the original Markov chain $C$;

- the requirement that $f_{L',T}$ be $B$-bounded (for some $B$) does not follow from any hypothesis on $f_{L,T}$ since the likelihood might be unbounded.
## 4.2 Construction of a biased Markov chain via an abstraction

The approach designed in the previous subsection requires the decisiveness of the biased Markov chain and the effective boundedness of the function which is evaluated. We now deport these various assumptions on another Markov chain, for which numerical (or symbolic) computations can be done, and which will serve as an abstraction. This approach generalizes [4] in several directions: first, [4] was designed for finite Markov chains; then, we consider a superset $F$ of $T$ which will allow us to relax conditions over $S \setminus T$ to its subset $S \setminus F$.

**Definition 11.** A Markov chain $\mathcal{C}^\bullet = (S^\bullet, P^\bullet)$ together with a set $F^\bullet$ is called an abstraction of $\mathcal{C}$ with set $F$ by function $\alpha: S \setminus \text{Av}_\mathcal{C}(F) \to S^\bullet$ whenever, the following conditions hold:
(A) for all $s \in F$, $\alpha(s) \in F^\bullet$;

$$ (B) \text{ for all } s \in S \setminus (F \cup \text{Av}_\mathcal{C}(F)), \sum_{s' \notin \text{Av}_\mathcal{C}(F)} P(s, s') \cdot \mu_{\mathcal{C}, \cdot, F \cdot}(\alpha(s')) \le \mu_{\mathcal{C}, \cdot, F \cdot}(\alpha(s)). $$

Condition (B) is called monotony and is only required outside $F \cup \text{Av}_\mathcal{C}(F)$. We write more succinctly that $(\mathcal{C}^\bullet, F^\bullet)$ is an $\alpha$-abstraction of $(\mathcal{C}, F)$, denoted $(\mathcal{C}, F) \stackrel{\alpha}{\hookrightarrow} (\mathcal{C}^\bullet, F^\bullet)$ and $\mu_{F \cdot} \stackrel{\text{def}}{=} \mu_{\mathcal{C}^\bullet, F \cdot}$ and $\mu_F \stackrel{\text{def}}{=} \mu_{\mathcal{C}, F}$.

**Example 12.** We claim that the Markov chain $\mathcal{C}^\bullet$ in Figure 1(b) with $F^\bullet = \{0\}$ is an abstraction of $\mathcal{C}$ in Figure 1(a) with $s_0 = p_1$. Indeed, the monotony condition is satisfied: for all $n > 0$:

$$ \text{ in } p_n: 0.3 \left(\frac{2}{3}\right)^{n+1} + 0.4 \left(\frac{2}{3}\right)^{n+1} + 0.3 \left(\frac{2}{3}\right)^{n-1} = \frac{55}{60} \left(\frac{2}{3}\right)^n < \left(\frac{2}{3}\right)^n; $$

$$ \text{ in } q_n: 0.4 \left(\frac{2}{3}\right)^{n+1} + 0.4 \left(\frac{2}{3}\right)^{n+1} + 0.2 \left(\frac{2}{3}\right)^{n-1} = \frac{25}{30} \left(\frac{2}{3}\right)^n < \left(\frac{2}{3}\right)^n. $$

Observe that $\mu_{F \cdot}(n) = \left(\frac{0.4}{0.6}\right)^n = \left(\frac{2}{3}\right)^n$.

As will be explicit in the next lemma, an abstraction is a stochastic bound of the initial Markov chain outside $\text{Av}_\mathcal{C}(F)$.

**Lemma 13.** Let $(\mathcal{C}, F) \stackrel{\alpha}{\hookrightarrow} (\mathcal{C}^\bullet, F^\bullet)$. Then for all $s \in S \setminus \text{Av}_\mathcal{C}(F)$, $\mu_F(s) \le \mu_{F \cdot}(\alpha(s))$. In particular, for all $s \in S \setminus \text{Av}_\mathcal{C}(F)$, $\mu_{F \cdot}(\alpha(s)) > 0$.

**Proof.** Let $\mu_F^{(n)}(s) \stackrel{\text{def}}{=} \text{Pr}(s \models \Diamond_{\le n} F)$. Observe that $\mu_F(s) = \lim_{n \to +\infty} \mu_F^{(n)}(s)$. We show by induction on $n$ that for all $s \in S$ and all $n \in \mathbb{N}$, $\mu_F^{(n)}(s) \le \mu_{F \cdot}(\alpha(s))$.

Case $n=0$:

- $s \in F$ implies $\alpha(s) \in F^\bullet$ (condition (A)). Hence $\mu_{F \cdot}(\alpha(s)) = 1 = \mu_F^{(0)}(s)$.

- $s \in S \setminus F$: $\mu_F^{(0)}(s) = 0 \le \mu_{F \cdot}(\alpha(s))$.

Inductive case:

- $s \in F$ implies $\alpha(s) \in F^\bullet$ (condition (A)). Hence $\mu_{F \cdot}(\alpha(s)) = 1 = \mu_F^{(n+1)}(s)$.

- $s \in S \setminus F$: $\mu_F^{(n+1)}(s) = \sum_{s'} P(s, s') \cdot \mu_F^{(n)}(s') = \sum_{s' \notin \text{Av}_\mathcal{C}(F)} P(s, s') \cdot \mu_F^{(n)}(s') \le \sum_{s' \notin \text{Av}_\mathcal{C}(F)} P(s, s') \cdot \mu_{F \cdot}(\alpha(s'))$ by induction hypothesis. Hence $\mu_F^{(n+1)}(s) \le \mu_{F \cdot}(\alpha(s))$ by condition (B). $\quad \blacksquare$

Given an abstraction $(\mathcal{C}, F) \stackrel{\alpha}{\hookrightarrow} (\mathcal{C}^\bullet, F^\bullet)$ and $s \in S \setminus \text{Av}_\mathcal{C}(F)$, let $h(s)$ be the decreasing ratio at $s$: $h(s) \stackrel{\text{def}}{=} \frac{1}{\mu_{F \cdot}(\alpha(s))} \cdot \sum_{s' \in S \setminus \text{Av}_\mathcal{C}(F)} P(s, s') \cdot \mu_{F \cdot}(\alpha(s'))$. For all $s \in S$, $h(s) \le 1$: this is obvious when $s \in S \setminus F \cup \text{Av}_\mathcal{C}(F)$ by the monotony condition (B); if $s \in F$, then $\alpha(s) \in F^\bullet$ by condition (A), and hence $\mu_{F \cdot}(\alpha(s)) = 1$.
8:10 Beyond Decisiveness of Infinite Markov Chains

We now define a biased Markov chain based on the above abstraction, which will be
interesting for both methods (approximation and estimation).

► **Definition 14.** Let $(C, F) \stackrel{\alpha}{\rightleftharpoons} (C^\bullet, F^\bullet)$. Then $C' = ((S \setminus \text{Av}_C(F)) \uplus \{s_-\}, P')$ is the Markov chain, where $s_- \text{ is absorbing and for all } s, s' \in S \setminus \text{Av}_C(F)$, $P'(s, s') = P(s, s') \cdot \frac{\mu_{F^\bullet}(\alpha(s'))}{\mu_{F^\bullet}(\alpha(s))}$ and $P'(s, s_-) = 1 - h(s)$.

By assumption, for all $s \in T$, $s$ is absorbing in $C$. This implies in particular that $s$ is also absorbing in $C'$. Also, notice that $P'$ coincides with $P$ within $F$, which means that there is no bias in the zone $F$ in $C'$ w.r.t. $C$.

**Lemma 15.** Let $(C, F) \xrightarrow{\alpha} (C^\bullet, F^\bullet)$. Then the Markov chain $C'$ defined in Definition 14 is a biased Markov chain of $(C, T, F)$.

**Proof.** First probabilities are well-defined, thanks to the remark on $h$ being bounded by 1. The only thing which needs to be checked is the following: if $s, s' \notin \text{Av}_C(F)$ and $P(s, s') > 0$, then $P'(s, s') > 0$. Since $P'(s, s') = P(s, s') \cdot \frac{\mu_{F^\bullet}(\alpha(s'))}{\mu_{F^\bullet}(\alpha(s))}$ and $s' \notin \text{Av}_C(F)$ using Lemma 13, $\mu_{F^\bullet}(\alpha(s')) \ge \mu_F(s') > 0$. So $C'$ is a biased Markov chain of $(C, T, F)$. ◀

Since the only transitions added to $C$, when defining $C'$, lead to $s_-$, the (qualitative) reachability of $T$ is unchanged and so $\text{Av}_{C'}(T) = (\text{Av}_C(T) \setminus \text{Av}_C(F)) \cup \{s_-\}$. Furthermore $C'$ does not depend on $T$. So we call $C'$ the biased Markov chain of $(C, F) \xrightarrow{\alpha} (C^\bullet, F^\bullet)$. As above, we define the likelihood $\gamma$, and accordingly the function $L' = L \cdot \gamma$. So the approach of Subsection 4.1 can be applied, provided $C'$ satisfies the required properties (decisiveness and boundedness of the evaluated function). In subsection 4.3, we will be more specific and give a generic framework guaranteeing those properties.

**Role of F.** In the original importance sampling method, there was no superset $F \supseteq T$, and the monotony condition was imposed on $S \setminus T$. However, in practice, the monotony condition may not be satisfied in $F \setminus T$ while being satisfied in $S \setminus F$; hence the formulation with a superset $F \supseteq T$ widens the applicability of the approach. It should be noted that once a set $F$ has been found, which ensures the monotony condition, any of its supersets will also do the work. Its choice will impact the efficiency of the approach, as will be illustrated in Section 5, and will therefore serve as a parameter of the approach that can be adjusted for improving efficiency.

We end up this subsection with some property of the reward function that is to be
analyzed in the biased Markov chain obtained using an abstraction.

**Proposition 16.** Let $(C, F) \stackrel{\alpha}{\rightleftharpoons} (C^\bullet, F^\bullet)$ and $L$ a computable function from $S^+$ to $\mathbb{R}$ such that $f_{L,T}$ is B-bounded. Let $C'$ be the biased Markov chain of $(C, F) \stackrel{\alpha}{\rightleftharpoons} (C^\bullet, F^\bullet)$ and $L' = L \cdot \gamma_{C,C'}$. Let $s_0 \in S$, then for every infinite path $\rho$ in $C'$ starting at $s_0$:

$$
f_{L',T}(\rho) = \begin{cases} L(\rho_{\le \text{first}_T(\rho)}) \cdot \mu_F \cdot (\alpha(s_0)) & \text{if } \rho \models \Diamond T \\ 0 & \text{otherwise} \end{cases}
$$

Thus $f_{L',T}$ is B-bounded.

The proof of this proposition is given in Appendix A.2. Thus in addition to be a biased Markov chain of $C$, $C'$ preserves a necessary condition for applying algorithms of Section 3: the boundedness of the reward function. Furthermore, when $f_{L,T} = 1_{\diamond T}$ (corresponding to the standard reachability property), $f_{L',T}$ for paths starting at $s_0$ is a biv aluated function: $f_{L',T} = \mu_F(\alpha(s_0)) \cdot 1_{\diamond T}$ which does not need to be computed on the fly by the algorithms.
## 4.3 A generic framework based on random walks

Our objective is to apply the algorithms of Section 3 to the biased Markov chain $C'$ defined in the previous subsection via an abstraction, and to exploit Proposition 16. This requires $C'$ to be effective and to be decisive w.r.t. $T$. The effectiveness will be obtained via the numerical or symbolic computation (since $C^*$ is infinite) of $\mu_F \cdot (\alpha(s))$. To that purpose, we use random walks as abstractions since they have closed forms for the reachability probabilities and *layered Markov chains* as generic models. The proofs of this section are either omitted or sketched and full proofs can be found in Appendix. The proofs of this section are only partly given in the core and in the appendix of this paper, but are fully given in [3].

**Definition 17.** A layered Markov chain (LMC in short) is a tuple $(C, \lambda)$ where $C = (S, P)$ is a countable Markov chain, $\lambda: S \to \mathbb{N}$ is a mapping such that for all $s \to_C s'$, $\lambda(s) - \lambda(s') \le 1$, and for all $n \in \mathbb{N}$, $\lambda^{-1}(n)$ is finite.

Given $s \in S$, $\lambda(s)$ is the level of $s$. In words there are two requirements on $\lambda$: (1) after one step the level can be decreased by at most one unit while it can be arbitrarily increased, and (2) for any level $\ell$, the set of states with level $\ell$ is finite. We define $P^+(s)$, $P^-(s)$ and $P^-(s)$ (with $P^+(s) + P^-(s) + P^-(s) = 1$) as follows:

$$P^+(s) = \sum_{\substack{s' \in S \text{ s.t.} \\ \lambda(s') \ge \lambda(s)+1}} P(s, s'), \quad P^-(s) = \sum_{\substack{s' \in S \text{ s.t.} \\ \lambda(s') = \lambda(s)-1}} P(s, s'), \quad P^-(s) = \sum_{\substack{s' \in S \text{ s.t.} \\ \lambda(s') = \lambda(s)}} P(s, s')$$

In the sequel we fix an LMC $(C, \lambda)$ and we consider a finite target set $T$. We want to apply the previous approach to $C$ using an $\alpha$-abstraction $(C, F) \stackrel{\alpha}{\hookrightarrow} (C^*, F^*)$, where $C^*$ is the random walk $W^p = (\mathbb{N}, P_p)$ with some probability parameter $0 < p < 1$ defined as follows: $P_p(0, 0) = 1$; for every $i > 0$, $P_p(i, i+1) = p$ and $P_p(i, i-1) = 1-p$ (it is depicted in Figure 1(b) for $p = 0.6$). We define $\kappa \stackrel{\text{def}}{=} \frac{1-p}{p}$ and recall this folk result.

**Proposition 18.** In $W^p$, the probability to reach state 0 from state $m$ is 1 when $p \le \frac{1}{2}$ and $\kappa^m$ otherwise.

Here we introduce a subclass of LMC useful for our aims.

**Definition 19.** A LMC $(C, \lambda)$ is said $(p^+, N_0)$-divergent with $p^+ > \frac{1}{2}$ and $N_0 \in \mathbb{N}$ if letting $F \stackrel{\text{def}}{=} \lambda^{-1}([0, N_0])$, for every $s \in S \setminus F$, $P^-(s) < 1$ implies $\frac{P^+(s)}{P^-(s)+P^+(s)} \ge p^+$.

The $(p^+, N_0)$-divergence constrains states of levels larger than $N_0$, and imposes that, from those states that do not stay at the same level, the relative proportion of successors increasing their levels compared with those decreasing their levels is at least the value $p^+$ (itself larger than $\frac{1}{2}$). Note that a $(p^+, N_0)$-divergent LMC is also $(p'^+, N'_0)$-divergent for all $\frac{1}{2} < p'^+ \le p^+$ and $N'_0 \ge N_0$. This will allow to adjust the corresponding set $F$ that will be used in the approach, as will be seen in the experiments (Section 5).

To be able to apply the previous approach, it remains to examine under which conditions starting from a $(p^+, N_0)$-divergent LMC $C$: (1) $W^p$ is an abstraction, and (2) $C'$ obtained via this abstraction is decisive w.r.t. $F$ from $s_0$. The next proposition shows that $W^p$ is an abstraction as soon as $1/2 < p < p^+$.

**Proposition 20.** Let $(C, \lambda)$ be a $(p^+, N_0)$-divergent LMC and write $F \stackrel{\text{def}}{=} \lambda^{-1}([0, N_0])$. We define $\alpha$ as the restriction of $\lambda$ to $S \setminus \text{Av}(F)$, and we let $\frac{1}{2} < p < p^+$. Then $(C, F) \stackrel{\alpha}{\hookrightarrow} (W^p, [0, N_0])$ is an abstraction.
8:12 Beyond Decisiveness of Infinite Markov Chains

The only point that needs to be checked is the monotony condition defining an abstraction.
The proof is given in Appendix A.3 and distinguishes the states that almost-surely stay
within the same level, and the other states; the rest is just calculation. The condition which is
satisfied is even stronger than monotony: for all $s \in S \setminus (F \cup \text{Av}(F))$ such that $\alpha(s) = n > N_0$
and $P^-(s) < 1$: $1 - h(s) \ge \frac{2p-1}{(1-p)p} \cdot (P^-(s) + P^+(s)) \cdot (p^+ - p)$, where $h(s)$ is the decreasing
ratio at $s$, see page 9.

It remains to understand under which conditions the biased Markov chain of ($C, F$) $\stackrel{\alpha}{\hookrightarrow}$ ($W^p$, $[0, N_0]$) is decisive w.r.t. $T$. To do that, let us introduce the key notion of attractor [1]: given a Markov chain $\mathcal{C} = (S, P)$ and $R \subseteq S$, $R$ is an attractor if for all $s \in S$, $\text{Pr}(\varrho^{C,s} \models \Diamond R) = 1$. There is a relation between attractor and decisiveness, stated as follows: if $R$ is a finite attractor and $B \subseteq R$, then $\mathcal{C}$ is decisive w.r.t. $B$.

The next theorem gives a simple condition for a set R to be an attractor in a Markov
chain, using a *Lyapunov function*.

**Theorem 21.** Let $\mathcal{C} = (S, P)$ be a Markov chain and $R \subseteq S$ s.t. for all $s \in S$, $\mathbf{Pr}(\varrho^{C,s} \models \Diamond R) > 0$, and let $\mathcal{L}: S \to \mathbb{R}^+$ be a Lyapunov function s.t. (1) for all $n \in \mathbb{N}$, $\mathcal{L}^{-1}([0, n])$ is finite, and (2) for all $s \in S \setminus R$, $\sum_{s' \in S} P(s, s') \cdot \mathcal{L}(s') \le \mathcal{L}(s)$. Then for all $s \in S$, $\mathbf{Pr}(\varrho^{C,s} \models \Diamond R) = 1$.

The full proof is rather involved and partly relies on martingale theory; it is given in
Appendix A.3.

Using the previous theorem, we show that choosing $W^p$ as an abstraction with $1/2 < p < p^+$ ensures decisiveness of $C'$. The Lyapunov function will be obtained via the level function.

**Proposition 22.** Let $(\mathcal{C}, \lambda)$ be a $(p^+, N_0)$-divergent LMC, write $F \stackrel{\text{def}}{=} \lambda^{-1}([0, N_0])$, let $\alpha$ be the restriction of $\lambda$ to $S \setminus \text{Av}(F)$, and fix $\frac{1}{2} < p < p^+$. Then the biased Markov chain $\mathcal{C}'$ of $(\mathcal{C}, F) \stackrel{\alpha}{\hookrightarrow} (W^p, [0, N_0])$ is decisive w.r.t. any $T \subseteq F$.

The detailed proof is given in Appendix A.3; we explain here the rough idea. This proposition will be an application of Theorem 21 to $C'$ with Lyapunov function $\mathcal{L}$ given by $\alpha$ (and additionally $\mathcal{L}(s_-) = 0$). So there will be some $N_1 \ge N_0$ such that $R \stackrel{\text{def}}{=} \mathcal{L}^{-1}([0, N_1])$ is a finite attractor in $C'$. Condition (2) of Theorem 21 is ensured by the fact that the level is unchanged after a transition from $s$ if $P^-(s) = 1$, and by the stronger condition given after Proposition 20 otherwise.

This proposition allows to apply the analysis of Subsection 4.1 to the biased Markov
chain of $(\mathcal{C}, F) \stackrel{\alpha}{\hookrightarrow} (W^p, [0, N_0])$, yielding approximation and estimation algorithms for the
original Markov chain. Nevertheless, as argued in Subsection 3.2, decisiveness is enough
to ensure correctness of the SMC, but not enough for efficiency. Efficiency can be ensured,
if the expected time for reaching $T \cup \text{Av}(T)$ is finite. We will do so by strengthening the
divergence condition of LMC.

To do so we present another theorem for the existence of an attractor, inspired by Foster's theorem [9], whose proof is given in Appendix A.3. Observe that here the requirement becomes: the average level decreases by some fixed $\varepsilon > 0$, and the other requirements are no more necessary.

**Theorem 23.** Let $\mathcal{C} = (S, P)$ be a Markov chain and $R \subseteq S$. If there exists $\mathcal{L}: S \to \mathbb{R}_{\ge 0}$ and $\varepsilon > 0$ such that for all $s \notin R$, $\mathcal{L}(s) - \sum_{s' \in S} P(s, s') \cdot \mathcal{L}(s') \ge \varepsilon$, then for all $s \notin R$ the expected time to reach $R$ is finite and bounded by $\frac{\mathcal{L}(s)}{\varepsilon}$; in particular, $R$ is an attractor of $\mathcal{C}$.

We are now in a position to establish a sufficient condition for the biased LMC $\mathcal{C}'$ of $(\mathcal{C}, F) \stackrel{\alpha}{\hookrightarrow} (W^p, [0, N_0])$ to be decisive with finite expected time to reach some finite target $T$.
**► Proposition 24.** Let $(C, \lambda)$ be a $(p^+, N_0)$-divergent LMC such that $\inf_{s \in \lambda^{-1}([N_0, \infty[)} P^+(s) > 0$, and write $F \stackrel{\text{def}}{=} \lambda^{-1}([0, N_0])$. We define $\alpha$ as the restriction of $\lambda$ to $S \setminus \text{Av}(F)$, and we fix $\frac{1}{2} < p < p^+$. Then the biased Markov chain $C'$ of $(C, F) \xrightarrow{\alpha} (W^p, [0, N_0])$ is decisive w.r.t. $T \subseteq F$ with finite expected time to reach $T \cup \text{Av}_{C'}(T)$.

The full proof is given in Appendix A.3; the idea is as follows. We use the same Lyapunov function as before, and the stronger condition mentioned after Proposition 22 together with the constraint on $P^+$: applying Theorem 23, we are able to find a finite attractor $R \stackrel{\text{def}}{=} \mathcal{L}^{-1}([0, N_1]) \cup \{s_-\}$ for some $N_1 \ge N_0$, reachable in finite expected time (given by $\alpha$). By analyzing the successive visits of $R$ before reaching $T \cup \text{Av}_{C'}(T)$, we derive a bound on the expected time to reach $T \cup \text{Av}_{C'}(T)$, which (linearly) depends on the level of the initial state.

# 5 Applications and experiments

**Probabilistic pushdown automata.** Our method is applied to the setting of probabilistic pushdown automaton (pPDA) using the height of the stack as the level function $\lambda$. We only provide an informal definition for pPDA (see [5] for a formal definition).

A pPDA configuration consists of a stack of letters from an alphabet $\Sigma$ and a state of an automaton. A set of rules describes how the top of the stack is modified. A rule $(q, a) \xrightarrow{w} (q', u)$ applies if the top of the stack matches the letter $a$ and the current state is $q$. Then it replaces $a$ by the word $u$ and $q$ by $q'$. The weight $w$ of the rule is a polynomial in $n$, the size of the stack. Probability rules are defined with the relative weight of the rule which applies w.r.t. all rules that could apply. If the target $T$ is defined as a regular language on the stack $\text{Av}(T)$ is also a regular language (see [5]) that can be computed: the membership of a configuration to $T$ and $\text{Av}(T)$ is effective and not costly.

**► Example 25.** We consider the pPDA with a single (omitted) state with stack alphabet $\{A, B, C\}$ defined by the set of rules: $\{A \xrightarrow{1} C, A \xrightarrow{n} BB, B \xrightarrow{5} \varepsilon, B \xrightarrow{n} AA, C \xrightarrow{1} C\}$. Starting with the stack containing only $A$, the target set $T = \{\varepsilon\}$ is the configuration with the empty stack and $\text{Av}(T)$ is the set of configurations containing a $C$. Let us describe some possible evolutions. From the initial configuration two rules apply by reading $A$: the new stack is $C$ with probability $\frac{1}{2}$ or $BB$ with probability $\frac{1}{2}$. From the stack $BB$, two rules apply by reading the first $B$: the new stack is then $B$ with probability $\frac{5}{7}$ (7 is the sum of the weight of $B \xrightarrow{5} \varepsilon$ and of $B \xrightarrow{n} AA$, with $n = 2$), and $\mathbf{BAA}$ with probability $\frac{2}{7}$.

The approach described previously applies to pPDA, as soon as the LMC defined by the pPDA can be proven to be $(p^+, N_0)$-divergent for some $p^+ > \frac{1}{2}$ and $N_0 \in \mathbb{N}$. This condition can be ensured by some syntactical constraints on the pPDA.

**Implementation.** Since SMC with importance sampling is already present in the tool Cosmos [4], we only added the mapping function $\lambda$ in order to apply our method. We focus here on the implementation details of Algorithm 1, which (to the best of our knowledge) has never been done.

Algorithm 1 requires to sum up a large number of probabilities accurately while those probabilities are of different magnitudes. We have experimentally observed that without dedicated summation algorithms, the implementation of this algorithm does not converge. We therefore propose a data structure with better accuracy when summing up positive values at the cost of increased memory consumption and time. This data structure encodes a
8:14 Beyond Decisiveness of Infinite Markov Chains

floating point number $r$ as a table of integers of size 512 where the cell $c$ at index $i$ stores the value $c2^{-i}$, with $c$ being a small enough integer to be represented exactly. The probability $r$ is the sum of the values of the table.

We specialized Algorithm 1 (called AlgoDec in the following), when the function to be evaluated satisfies the following *monoidal property*: for all $\rho = \rho_1\rho_2$, $f(\rho) = f(\rho_1) \cdot f(\rho_2)$; this property is in particular satisfied by the likelihood related to an importance sampling. It is thus possible to merge paths leading to the same state and store only for each state the probability to reach it and the weighted average likelihood of the merged paths. In practice, this leads to a large improvement. Another improvement is the use of a heap where states are ordered by their probability to be reached: the algorithm will converge faster. The termination of the algorithm still holds as the heap management happens to be fair, see [3] for details.

**Experimental studies.** We first ran experiments$^7$ on the example depicted on Figure 1. As there are only two states per level, the numerical algorithm (AlgoDec) with important sampling is very efficient and computes an interval of $0.0258657 \pm 10^{-8}$ in 10ms. The SMC approach computes a confidence interval of $0.02586 \pm 10^{-4}$ in 135s. As expected the SMC approach is much slower on such a small toy example.

The pPDA of Example 25 is both decisive and a $(p, N_0)$-divergent LMC for $1/2 < p \le \frac{N_0}{N_0+5}$ so that $(W^p, [0, N_0])$ defines an abstraction. We compare the use of importance sampling with different values of $p$ to standard SMC and AlgoDec. In Figure 2 each point is the result of a computation with or without importance sampling. The value 0.3151 is contained in the intervals returned by all numerical computations and all but one confidence intervals of SMC (consistent with 120 experiments and a confidence level of 0.99).

Figure 2a depicts the computation time w.r.t. the width of the confidence interval for the two algorithms over three Markov chains: the initial Markov chain, the importance sampling using $W^{0.6}$ as abstraction and the importance sampling with $W^{0.51}$ as abstraction. Looking only at SMC (dotted line on the figure) the computation time scales the same way on the three curves with the standard SMC taking more time. Looking at the AlgoDec curves (solid line) with a well-chosen value of $p = 0.6$ this algorithm is very fast but with another value of $p$ or without importance sampling the performance quickly degrades.

To better understand how the computation time increases w.r.t. $p$ we plot it in Figure 2b. The SMC is barely sensible to the value of $p$ while the computation time of AlgoDec reaches a minimum at around $p = 0.6$ and becomes intractable when $p$ moves away from this value.

**► Example 26.** We consider the pPDA with a single state with stack alphabet $\{A, B, C\}$ defined by the set of rules: $\begin{array}{rcl} A & \to & B, A \to C, B \to \varepsilon, B \to AA, C \to A, C \to BB \end{array}$ starting with stack A, target configuration $T = \{\varepsilon\}$ and $\text{Av}(T) = \emptyset$.

Example 26 is not decisive but is a $(p, N_0)$-divergent LMC for $1/2 < p \le \frac{10+N_0}{20+N_0}$ thus $(W^p, [0, N_0])$ defines an abstraction. In Figure 3 we plot the computation time w.r.t. $p$. The probability 0.516318 is contained in all the results. As in Example 25, AlgoDec is very sensitive to the value of $p$ while SMC is not. In this example SMC is always faster than AlgoDec with similar computation times for a well-chosen value of $p$.

From our experiments we observe that while importance sampling can be applied both to AlgoDec and SMC, as soon as the size of the state space grows, AlgoDec is not tractable.

<footnote>$^7$ All the experiments are run with a timeout of 1 hour and a confidence level set to 0.99.</footnote>
<figure><img src="image_8.png" /><figcaption>(a) Computation time as a function of the precision, the width is given in logarithmic scale.</figcaption></figure>

<caption>(b) Computation time as a function of $p$.</caption>

Figure 2 Computation time for Example 25 in logarithmic scale. Given a value for $p$, the threshold $N_0$ is chosen as the smallest integer such that ($W^p$, $[0, N_0]$) defines an $\alpha$-abstraction.

<figure><img src="image_9.png" /><figcaption>Figure 3 Computation time as a function of $p$ for Example 26.</figcaption></figure>

Additionally, the few experiments that we have conducted suggest the following methodology to analyze Markov chains: apply SMC with importance sampling for various values of $p$; find the “best” $p$; apply AlgoDec with that value of $p$ (when possible).

# 6 Conclusion

We have recalled two standard approaches to the analysis of reachability properties in infinite Markov chains, a deterministic approximation algorithm, and a probabilistic algorithm based on statistical model checking. For their correctness or termination, they both require the Markov chain to satisfy a *decisiveness* property. Analyzing non decisive Markov chains is therefore a challenge.

In this work, we have introduced the notion of abstraction for a Markov chain and developed a theoretical method based on importance sampling to “transform” a non decisive Markov chain into a decisive one, allowing to transfer the analysis of the non decisive Markov chain to the decisive one. Then we have presented a concrete framework where the Markov chain is a layered Markov chain (LMC), the abstraction is done via a random walk, and given conditions that ensure that this abstract chain is decisive. Finally we have implemented the two algorithms within the tool Cosmos, and compared their respective performances on some examples given as probabilistic pushdown automata (which are specific LMCs).

There are several further research directions that could be investigated. First while (one-dimensional) random walks have closed forms for reachability probabilities, other (more complex) models also enjoy such a property, and could therefore be used for abstractions. Second, the divergence requirements are based on conditions for one-step transitions and could be relaxed to an arbitrary (but fixed) number of steps. Finally, more systematic, and even automatic, approaches could be investigated, that would compute adequate abstractions to adequate classes of Markov chains allowing to use our approach.
References

1 P. A. Abdulla, N. B. Henda, and R. Mayr. Decisive Markov chains. *Logical Methods in Computer Science*, 3(4), 2007. doi:10.2168/LMCS-3(4:7)2007.

2 P. Ballarini, B. Barbot, M. Duflot, S. Haddad, and N. Pekergin. HASL: A new approach for performance evaluation and model checking from concepts to experimentation. *Performance Evaluation*, 90:53–77, 2015. doi:10.1016/j.peva.2015.04.003.

3 B. Barbot, P. Bouyer, and S. Haddad. Beyond decisiveness of infinite markov chains. *CoRR arXiv*, 2024. doi:10.48550/arXiv.2409.18670.

4 B. Barbot, S. Haddad, and C. Picaronny. Coupling and importance sampling for statistical model checking. In *18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12)*, volume 7214 of LNCS, pages 331–346. Springer, 2012. doi:10.1007/978-3-642-28756-5_23.

5 J. Esparza, A. Kucera, and R. Mayr. Model Checking Probabilistic Pushdown Automata. *Logical Methods in Computer Science*, 2(1), 2006. doi:10.2168/LMCS-2(1:2)2006.

6 G. Fayolle, V.A. Malyshev, and M. V. Menshikov. *Topics in the Constructive Theory of Countable Markov Chains*. Cambridge University Press, 1995.

7 A. Finkel, S. Haddad, and L. Ye. About decisiveness of dynamic probabilistic models. In *34th International Conference on Concurrency Theory (CONCUR’23)*, volume 279 of LIPICS, pages 14:1–14:17. Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.CONCUR.2023.14.

8 A. Finkel, S. Haddad, and L. Ye. Introducing divergence for infinite probabilistic models. In *17th International Conference on Reachability Problems (RP’23)*, volume 14235 of LNCS, pages 1–14. Springer, 2023. doi:10.1007/978-3-031-45286-4_10.

9 F. G. Foster. On the Stochastic Matrices Associated with Certain Queuing Processes. *The Annals of Mathematical Statistics*, 24(3):355–360, 1953. doi:10.1214/aoms/1177728976.

10 W. Hoeffding. Probability inequalities for sums of bounded random variables. *J. Amer. Statist. Assoc.*, 58:13–30, 1963.

11 W. Kahan. Pracniques: further remarks on reducing truncation errors. *Comm. ACM*, 8(1):40, 1965. doi:10.1145/363707.363723.

12 H. Kahn and T. E. Harris. Estimation of particle transmission by random sampling. *National Bureau of Standards applied mathematics series*, 12:27–30, 1951.

13 G. Rubino and B. Tuffin, editors. *Rare Event Simulation using Monte Carlo Methods*. Wiley, 2009. doi:10.1002/9780470745403.

14 J. M. Rutten, M. Z. Kwiatkowska, G. Norman, D. Parker, and P. Panangaden. *Mathematical techniques for analyzing concurrent and probabilistic systems*, volume 23 of CRM monograph series. American Mathematical Society, 2004. URL: http://www.ams.org/publications/authors/books/postpub/crmm-23.

15 H. L. S. Younes, E. M. Clarke, and P. Zuliani. Statistical verification of probabilistic properties with unbounded until. In *13th Brazilian Symposium on Formal Methods (SBMF’10)*, volume 6527 of LNCS, pages 144–160. Springer, 2010. doi:10.1007/978-3-642-19829-8_10.

16 H. L. S. Younes and R. G. Simmons. Statistical probabilistic model checking with a focus on time-bounded properties. *Information and Computation*, 204(9):1368–1409, 2006. doi:10.1016/j.ic.2006.05.002.

17 H. L. S. Younes and R. G. Simmons. Probabilistic verification of discrete event systems using acceptance sampling. In *14th International Conference on Computer-Aided Verification (CAV’02)*, volume 2404 of LNCS, pages 223–235. Springer, 2022. doi:10.1007/3-540-45657-0_17.
We report here some of the missing proofs and discussions. More details are given in [3].

**A Some missing proofs of Section 4**

**A.1 Proofs of results of Section 4.1**

We first state a useful lemma proved in a simple way.

**Lemma 27.** $\Pr(\rho) > 0$ and $\text{last}(\rho) \notin \text{Av}_C(F)$ imply $\Pr'(\rho) > 0$.

**Proof of Proposition 10.** We proceed by a sequence of equalities:

$$ 
\begin{aligned}
\mathbf{E}(f_{L',T}(\varrho^{C',s_0})) &= \mathbf{E}((f_{L',T} \cdot \mathbf{1}_{\neg\Diamond T})(\varrho^{C',s_0}) + (f_{L',T} \cdot \mathbf{1}_{\Diamond T})(\varrho^{C',s_0})) \\
&= \mathbf{E}((f_{L',T} \cdot \mathbf{1}_{\Diamond T})(\varrho^{C',s_0})) = \sum_{\substack{\rho \in (S \setminus \text{Av}_C(F))^{+} \text{ s.t.} \\ \mathbf{Pr}'(\rho) > 0 \text{ and } \text{last}(\rho) = \text{first}_T(\rho)}} L'(\rho) \cdot \mathbf{Pr}'(\rho)
\end{aligned}
$$

$$ = \sum_{\substack{\rho \in (S \setminus \text{Av}_C(F))^{+} \text{ s.t.} \\ \mathbf{Pr}'(\rho) > 0 \text{ and } \text{last}(\rho) = \text{first}_T(\rho)}} L(\rho) \cdot \frac{\mathbf{Pr}(\rho)}{\mathbf{Pr}'(\rho)} \cdot \mathbf{Pr}'(\rho) $$

$$ = \sum_{\substack{\rho \in (S \setminus \text{Av}_C(F))^{+} \text{ s.t.} \\ \mathbf{Pr}'(\rho) > 0, \mathbf{Pr}(\rho) > 0 \text{ and } \text{last}(\rho) = \text{first}_T(\rho)}} L(\rho) \cdot \mathbf{Pr}(\rho) $$

$$ = \sum_{\substack{\rho \in (S \setminus \text{Av}_C(F))^{+} \text{ s.t.} \\ \mathbf{Pr}(\rho) > 0, \text{ and } \text{last}(\rho) = \text{first}_T(\rho)}} L(\rho) \cdot \mathbf{Pr}(\rho) \quad (\text{by Lemma 27}) $$

$$ = \sum_{\substack{\rho \in S^{+} \text{ s.t.} \\ \mathbf{Pr}(\rho) > 0, \text{ and } \text{last}(\rho) = \text{first}_T(\rho)}} L(\rho) \cdot \mathbf{Pr}(\rho) \quad (\text{since } \text{Av}_C(F) \subseteq \text{Av}_C(T)) = \mathbf{E}(f_{L,T}(\varrho^{C,s_0})) $$

<figure><img src="image_10.png" /></figure>

**A.2 Proofs of results of Section 4.2**

Before going to the proof of Proposition 16, we state a useful lemma.

**Lemma 28.** Let $C'$ be the biased Markov chain of $(C, F) \stackrel{\alpha}{\hookrightarrow} (C^*, F^*)$. Then for all $s \in S \setminus \text{Av}_C(F)$,

- for all $\rho$ starting from $s$ with $\mathbf{Pr}'(\rho) > 0$ and $\text{last}(\rho) \neq s_-$, $\mathbf{Pr}(\rho) = \mathbf{Pr}'(\rho) \cdot \frac{\mu_F \cdot (\alpha(s))}{\mu_F \cdot (\alpha(\text{last}(\rho)))}$;

- $\mu_{C,T}(s) = \mu_F \cdot (\alpha(s)) \cdot \mu_{C',T}(s)$ and $\mu_{C,F}(s) = \mu_F \cdot (\alpha(s)) \cdot \mu_{C',F}(s)$.

**Proof.** We establish the first property by induction. Let $\rho$ be a path starting from $s$ with $\mathbf{Pr}'(\rho) > 0$ and $\text{last}(\rho) \neq s_-$. If $\rho$ is the single state $s$ then $\mathbf{Pr}'(\rho) = \mathbf{Pr}(\rho) = 1$. Since $\text{last}(\rho) = s$, the base case is proved. Assume now that $\rho = \rho's''$ with $\mathbf{Pr}'(\rho) > 0$ and $s' \stackrel{\text{def}}{=} \text{last}(\rho') \neq s_-$. Then: $\mathbf{Pr}(\rho) = \mathbf{Pr}(\rho') \cdot \text{P}(s', s'') = \mathbf{Pr}(\rho') \cdot \text{P}(s', s'') \cdot \frac{\mu_F \cdot (\alpha(s'))}{\mu_F \cdot (\alpha(s''))}$. It is well-defined due to Lemma 13. Applying the induction hypothesis, we get the induction step:

$$ \mathbf{Pr}(\rho) = \mathbf{Pr}'(\rho') \cdot \frac{\mu_F \cdot (\alpha(s))}{\mu_F \cdot (\alpha(s'))} \cdot \text{P}(s', s'') \cdot \frac{\mu_F \cdot (\alpha(s'))}{\mu_F \cdot (\alpha(s''))} = \mathbf{Pr}'(\rho) \cdot \frac{\mu_F \cdot (\alpha(s))}{\mu_F \cdot (\alpha(s''))}. $$

The paths that reach $T$ (resp. $F$) from $s$ are the same in $C$ and $C'$, and they do not reach $s_-$. Pick such a path $\rho$. Then due to the previous property: $\mathbf{Pr}(\rho) = \mathbf{Pr}'(\rho) \cdot \mu_F \cdot (\alpha(s))$. Summing over all such paths establishes the second property. $\blacksquare$

<figure><img src="image_11.png" /></figure>
8:18 Beyond Decisiveness of Infinite Markov Chains

While the previous property allows to solve the reachability problem in C using C', the
next proposition extends it to the reward reachability problem.

**Proof of Proposition 16.** By definition, $f_{L',T}$ assigns 0 to infinite paths not visiting $T$. Assume now that $\rho$ is an infinite path visiting $T$. Then $f_{L',T}(\rho) = (L \cdot \gamma)(\rho_{\le \text{first}_T(\rho)})$. Let $\rho' = \rho_{\le \text{first}_T(\rho)}$. It does not visit $s_-$, hence $\gamma(\rho') = \frac{\text{Pr}(\rho')}{\text{Pr}'(\rho')} = \frac{\mu_F \cdot (\alpha(s))}{\mu_F \cdot (\alpha(\text{last}(\rho')))}$ by Lemma 28. Since $\text{last}(\rho') \in T$, $\gamma(\rho') = \mu_F \cdot (\alpha(s))$. This implies the first part of the proposition. The restriction to the case of the indicator function is immediate. ◀

A.3 Proofs of results of Section 4.3

We first establish that random walks parametrized by $\frac{1}{2} < p < p^+$ are abstractions for a $(p^+, N_0)$-divergent LMC and give useful information on the decreasing ratio for states $s$ with $P^+(s) < 1$.

**Proof of Proposition 20.** We denote $\mu_{W^p, [0, N_0]}$ more simply by $\mu_{[0, N_0]}^\bullet$. We pick $s \in S \setminus (F \cup \text{Av}(F))$ such that $\alpha(s) = n > N_0$, and we distinguish between two cases. If $P^=(s) = 1$, since $\alpha(s') = n$ for all $s'$ s.t. $P(s, s') > 0$, we easily infer that $\sum_{s' \notin \text{Av}_C(F)} P(s, s') \cdot \mu_{[0, N_0]}^\bullet(\alpha(s')) \ge \mu_{[0, N_0]}^\bullet(\alpha(s))$. Otherwise, we can compute (all details are given in [3]):

$$
\begin{align*}
1 - h(s) &\ge 1 - \frac{1}{\mu_{[0,N_0]}^{\bullet}(n)} \left( \mu_{[0,N_0]}^{\bullet}(n-1) \cdot P^{-}(s) + \mu_{[0,N_0]}^{\bullet}(n) \cdot P^{=}(s) + \mu_{[0,N_0]}^{\bullet}(n+1) \cdot P^{+}(s) \right) \\
&\quad \text{(since } P^{+}(s) + P^{-}(s) + P^{=}(s) = 1 \text{ and } \mu_{[0,N_0]}^{\bullet}(x) \text{ is non increasing w.r.t. } x) \\
&= \left(1 - \frac{1}{\kappa}\right) \cdot P^{-}(s) + \left(1 - \kappa\right) \cdot P^{+}(s) \\
&= \frac{2p-1}{(1-p)p} (P^{-}(s) + P^{+}(s)) \left( -p \cdot \left(1 - \frac{P^{+}(s)}{P^{-}(s) + P^{+}(s)}\right) + (1-p) \cdot \frac{P^{+}(s)}{P^{-}(s) + P^{+}(s)} \right) \\
&\ge \frac{2p-1}{(1-p)p} (P^{-}(s) + P^{+}(s)) (p^{+} - p) > 0 \quad \text{(since } \frac{1}{2} < p < p^{+})
\end{align*}
$$

This concludes the proof of monotony, implying that $(C, F) \stackrel{\alpha}{\rightleftharpoons} (W^p, [0, N_0])$ is an abstraction.

<figure><img src="image_12.png" /></figure>

Out of the above proof, a stronger condition than monotony happens to be satisfied.

**Corollary 29.** Let $(C, \lambda)$ be a $(p^+, N_0)$-divergent LMC. We define $\alpha$ as the restriction of $\lambda$ to $S \setminus \text{Av}(F)$, and we let $\frac{1}{2} < p < p^+$. Then the monotony condition satisfied by the abstraction $(C, F) \stackrel{\alpha}{\rightleftharpoons} (W^p, [0, N_0])$ can be strengthened as follows. For all $s \in S \setminus (F \cup \text{Av}(F))$ such that $\alpha(s) = n > N_0$ and $P^<(s) < 1$: $1 - h(s) \ge \frac{2p-1}{(1-p)p} \cdot (P^-(s) + P^+(s)) \cdot (p^+ - p) > 0$, where $h(s)$ is the decreasing ratio at $s$, see page 9.

Before turning to the proof of Theorem 21, we first establish a sufficient condition to be
an attractor in a Markov chain.

**Lemma 30.** Let $C = (S, P)$ be a Markov chain, $s_0 \in S$ and $R \subseteq S$ s.t. for all $s \in S$, $\text{Pr}(\rho^{C,s} \models \Diamond R) > 0$. Assume that for every $\delta > 0$, there exists a finite set $S_\delta \subseteq S$ and $m_\delta \in \mathbb{N}$ such that $\text{Pr}(\bigwedge_{i \ge m_\delta} X_i^{C,s_0} \in S_\delta) > 1 - \delta$. Then $\text{Pr}(\rho^{C,s_0} \models \Diamond R) = 1$.

**Proof.** Fix some $\delta > 0$. Let $\ell \in \mathbb{N}$ be the maximal length over $s \in S_\delta$ of a shortest path from $s$ to $R$ and $p_{\min} > 0$ the minimal probability of these paths. Let $k \in \mathbb{N}$. Then $\text{Pr}(\bigwedge_{m_\delta \le i \le m_\delta + k\ell} X_i^{C,s_0} \notin R \mid \bigwedge_{m_\delta \le i} X_i^{C,s_0} \in S_\delta) \le (1 - p_{\min})^k$.
Letting $k$ go to $\infty$, one gets $\mathbf{Pr}(\bigwedge_{m_\delta \le i} X_i^{C,s_0} \notin R | \bigwedge_{m_\delta \le i} X_i \in S_\delta) = 0$ implying $\mathbf{Pr}(\varrho^{C,s_0} \models \diamond R | \bigwedge_{m_\delta \le i} X_i^{C,s_0} \in S_\delta) = 1$. Thus $\mathbf{Pr}(\varrho^{C,s_0} \models \diamond R) > 1 - \delta$. Since $\delta$ is arbitrary, one gets $\mathbf{Pr}(\varrho^{C,s_0} \models \diamond R) = 1$. $\blacksquare$

Then using both martingale theory and the previous lemma we establish another sufficient condition based on a non negative state function non increasing on average (i.e. the expected next value). A similar proof for recurrence of irreducible Markov chains can be found in [6].

**Proof of Theorem 21.** Since we are interested in reachability of $R$, w.l.o.g. we assume that all $s \in R$ are absorbing and thus $\sum_{s' \in S} P(s, s') \cdot \mathcal{L}(s') = \mathcal{L}(s)$.

We fix some initial state $s_0$ and consider the random sequence of states $(X_n^{C,s_0})_{n \in \mathbb{N}}$, which we simply write $(X_n)_{n \in \mathbb{N}}$. Define $\mathcal{F}_n$ the $\sigma$-algebra generated by $(X_m)_{m \le n}$ and $Y_n = \mathcal{L}(X_n)$. Due to the inequlation $\sum_{s' \in S} P(s, s')\mathcal{L}(s') \le \mathcal{L}(s)$ for all $s \in S$ and the memoryless property of Markov chain $\mathbf{E}(Y_{n+1} | \mathcal{F}_n) = \mathbf{E}(Y_{n+1} | X_n) = \sum_{s' \in S} P(X_n, s') \cdot \mathcal{L}(s') \le \mathcal{L}(X_n) = Y_n$. Thus $(Y_n)_{n \in \mathbb{N}}$ is a supermartingale. Consider the limit $Y_\infty$ of this supermartingale: it satisfies $\mathbf{E}(Y_\infty) \le \mathcal{L}(s_0) < \infty$.

We use Lemma 30 to conclude that $R$ is an attractor. Towards a contradiction assume that the sufficient condition of Lemma 30 is not satisfied. There is some $\delta > 0$ such that for all finite set $S^*$ and $m \in \mathbb{N}$, $\mathbf{Pr}(\bigvee_{m \le i} X_i \notin S^*) \ge \delta$. For every $n \in \mathbb{N}$, choose $S_n^* = \mathcal{L}^{-1}([0, n])$. The event $E_1 = \{\bigwedge_{m \in \mathbb{N}} \bigvee_{m \le i} X_i \notin S_n^*\}$ is the limit of decreasing events with probability larger than or equal to $\delta$. So $\mathbf{Pr}(E_1) \ge \delta$. Consider the event $E_2 = \{Y_\infty \ge n\}$: then $E_1 \subseteq E_2$. Thus $\mathbf{Pr}(E_2) \ge \delta$. Now, by Markov's inequality applied to the random variable $Y_\infty$, $\mathbf{E}(Y_\infty) \ge n \cdot \mathbf{Pr}(Y_\infty \ge n) \ge n\delta$. Since this is true for all $n$, $\mathbf{E}(Y_\infty) = \infty$, which is a contradiction. The sufficient condition of Lemma 30 is then satisfied, which implies that $R$ is an attractor. $\blacksquare$

The next proposition shows that choosing $\mathcal{W}^p$ as an abstraction with $1/2 < p < p^+$ ensures decisiveness of $\mathcal{C}'$.

**Proof of Proposition 22.** From Proposition 20, $(\mathcal{W}^p, [0, N_0])$ is a $\alpha$-abstraction of $(\mathcal{C}, F)$, so $\mathcal{C}'$ is well-defined. We exhibit some $N_1 \ge N_0$ s.t. $\alpha^{-1}([0, N_1]) \cup \{s_\_\}$ is a finite attractor of $\mathcal{C}'$, which implies decisiveness of $\mathcal{C}'$ w.r.t. $T$ (thanks to Lemma 3.4 of [1]).

To do so, we apply Theorem 21 to the Markov chain $\mathcal{C}$, using the layered function $\mathcal{L}$, which coincides with $\alpha$ on $S \setminus \text{Av}(F)$ and extended by $\mathcal{L}(s_\_)=0$ as the Lyapunov function. It remains to show the inequation on $\mathcal{L}$.

Let $s \in S' \setminus \{s_\_\}$ with $\alpha(s) = n > N_0$. If $P^-(s) = 1$, it is easy to get that $\sum_{s' \in S'} P'(s, s') \cdot \mathcal{L}(s') \le n = \mathcal{L}(s)$. If $P^-(s) < 1$, we compute:

$$ \begin{align*} \mathcal{L}(s) - \sum_{s' \in S'} P'(s, s') \cdot \mathcal{L}(s') &= \sum_{s' \in S'} P'(s, s') \cdot (\mathcal{L}(s) - \mathcal{L}(s')) \\ &= \sum_{k \ge n+1} \sum_{\substack{s' \in S' \text{ s.t.} \\ \mathcal{L}(s')=k}} (n-k)P'(s, s') + \sum_{\substack{s' \in S' \text{ s.t.} \\ \mathcal{L}(s')=n-1}} P'(s, s') + nP'(s, s_-) \\ &= \sum_{k \ge n+1} \sum_{\substack{s' \in S' \text{ s.t.} \\ \mathcal{L}(s')=k}} -\kappa^{k-n}(k-n)P(s, s') + \sum_{\substack{s' \in S' \text{ s.t.} \\ \mathcal{L}(s')=n-1}} \frac{1}{\kappa}P(s, s') + n(1-h(s)) \end{align*} $$

Since $\lim_{x \to +\infty} x\kappa^x = 0$, we let $B = \sup_{x \ge 0} x\kappa^x \ge \kappa$. We get after some calculation, and using Corollary 29:

$$ \mathcal{L}(s) - \sum_{s' \in S'} P(s, s') \cdot \mathcal{L}(s') \ge P^+(s) (-B + n \frac{2p-1}{(1-p)p} \cdot (p^+ - p)) $$
8:20 Beyond Decisiveness of Infinite Markov Chains

It is then sufficient to define $N_1$ such that $-B + N_1 \frac{2p-1}{(1-p)p} \cdot (p^+ - p) \ge 0$. The condition of Theorem 21 holds for all states. By the theorem, $\mathcal{L}^{-1}([0, N_1]) = \alpha^{-1}([0, N_1]) \cup \{s_-\}$ is then a finite attractor of $\mathcal{C}'$, which concludes the proof. ◀

This theorem shows that the existence of a Lyapunov state function $\mathcal{L}$ for some set $R$ ensures that $R$ is an attractor and that the expected time to reach it with an explicit upper bound (given in the proof) depending on the value of $\mathcal{L}$ for the initial state.

**Proof of Theorem 23.** W.l.o.g. we assume that all states in $R$ are absorbing. Pick some $s \in S$. Define $X_n(s)$ as the random state at time $n$ when starting from $s$ (that is, $X_n^{\mathcal{C},s}$) and $T_{s,R}$ the random time (in $\mathbb{N} \cup \{\infty\}$) to reach $R$ from $s$. Observe that: $\mathbf{E}(T_{s,R}) = \sum_{n \in \mathbb{N}} \mathbf{Pr}(X_n(s) \notin R)$.

On the other hand, the inequality satisfied by $\mathcal{L}$ can be rewritten as follows. For $Y$ random variable over $S \setminus R$, $\mathbf{E}(\mathcal{L}(X_1(Y)) - \mathcal{L}(Y)) \le -\varepsilon$.

Let $n \in \mathbb{N}$. Since states of $R$ are absorbing,

$$ 
\begin{aligned}
\mathbf{E}(\mathcal{L}(X_{n+1}(s)) - \mathcal{L}(X_0(s))) &= \sum_{k \le n} \mathbf{E}(\mathcal{L}(X_{k+1}(s)) - \mathcal{L}(X_k(s)) \cdot \mathbf{1}_{X_k(s) \notin R}) \\
&= \sum_{k \le n} \mathbf{E}(\mathcal{L}(X_{k+1}(s)) - \mathcal{L}(X_k(s)) | X_k(s) \notin R) \cdot \mathbf{Pr}(X_k(s) \notin R) \\
&\le -\varepsilon \sum_{k \le n} \mathbf{Pr}(X_k(s) \notin R)
\end{aligned}
$$

Since $\mathcal{L}$ is nonnegative and $\mathbf{E}(\mathcal{L}(X_0(s))) = \mathcal{L}(s)$, one gets: $\sum_{k \le n} \mathbf{Pr}(X_k(s) \notin R) \le \frac{\mathcal{L}(s)}{\varepsilon}$. Letting $n$ go to $\infty$, one gets $\mathbf{E}(T_{s,R}) \le \frac{\mathcal{L}(s)}{\varepsilon}$, which concludes the proof. ◀

The next proposition shows that choosing $W^p$ as an abstraction with $\frac{1}{2} < p < p^+$ ensures decisiveness of $\mathcal{C}'$ and finite expected time for statistical model checking due to the previous theorem.

**Proof of Proposition 24.** Let $\hat{p} = \inf_{s \in \lambda^{-1}([N_0, \infty[)} P^+(s)$. Due to Proposition 22, we already know that $\mathcal{C}'$ is decisive w.r.t. $T$. It remains to establish that the expected time to reach $T \cup \text{Av}_{\mathcal{C}'}(T) = T \cup \{s_\-\}$ is finite. For every $s \in S \setminus \text{Av}(F)$ with $\alpha(s) > N_0$, $0 < \hat{p} \le P^+(s)$, hence $P^-(s) < 1$. Therefore, using Corollary 29, for all $s \in S' \setminus \{s_\-\} = S \setminus \text{Av}_{\mathcal{C}}(F)$ with $\alpha(s) > N_0$,

$$ 
\begin{aligned}
\mathcal{L}(s) - \sum_{s' \in S'} \mathbf{P}(s, s') \cdot \mathcal{L}(s') &\ge \mathbf{P}^+(s) \cdot \left(-B + n \cdot \frac{2p-1}{(1-p)p} \cdot (p^+ - p)\right) \\
&\ge \hat{p} \cdot \left(-B + n \cdot \frac{2p-1}{(1-p)p} \cdot (p^+ - p)\right)
\end{aligned}
$$

Let $N_1 \ge N_0$ be such that $\hat{p} \cdot \left(-B + N_1 \cdot \frac{2p-1}{(1-p)p} \cdot (p^+ - p)\right) \ge 1$ and $R = \mathcal{L}^{-1}([0, N_1]) = \alpha^{-1}([0, N_1]) \cup \{s_\-\}$. Then the condition of Theorem 23 holds with $\varepsilon = 1$. Applying it, the expected time to reach $R$ from $s \in S \setminus \text{Av}(F)$ with $\alpha(s) > N_1$ is finite and bounded by $\mathcal{L}(s) = \alpha(s)$.

It remains to establish that the expected time to reach $T$ from every state is finite. We fix an initial state $s_0 \in S'$ and we consider the infinite random sequence $(\gamma(n))_{n \in \mathbb{N}}$, defined inductively as follows: $\gamma(0) = \min\{k | X_k(s_0) \in R\}$ and $\gamma(n+1) = \min\{k > \gamma(n) | X_k(s_0) \in R\}$; those are the successive times of visits in $R$. Since $R$ is an attractor, this sequence is defined almost everywhere. Let $h_{\max} = \max\{\mathcal{L}(s') | \exists s \in R \text{ s.t. } P'(s, s') > 0\}$ the maximal level that can be reached in one step from $R$. Due to the previous paragraph, for all $n$ and $s \in R$, $\mathbf{E}(\gamma(n+1) - \gamma(n) | X_{\gamma(n)} = s) \le 1 + h_{\max}$ and $\mathbf{E}(\gamma(0)) \le \mathcal{L}(s_0)$.
Define $\tilde{T} = T \cup \mathbf{Av}_{C'}(T) = T \cup \{s_\cdot\}$, $\tau \stackrel{\text{def}}{=} \tau^{C',s_0,\tilde{T}}$ the (random) time to reach $\tilde{T}$ from $s_0$ in $C'$, $\ell_{\max}$ as the maximal length of a shortest path from $s \in R$ to $T \cup \mathbf{Av}_{C'}(T)$ and $p_{\min}$ the minimal probability of these paths. Then:

$$
\begin{align*}
\mathbf{E}(\tau) \\
&= \mathbf{E}(\gamma(0)) + \sum_{n \in \mathbb{N}} \mathbf{E} \left( \gamma(n+1) - \gamma(n) \mid \bigwedge_{m \le n} X_{\gamma(m)} \notin \tilde{T} \right) \cdot \mathbf{Pr} \left( \bigwedge_{m \le n} X_{\gamma(m)} \notin \tilde{T} \right) \\
&= \mathbf{E}(\gamma(0)) + \sum_{n \in \mathbb{N}} \mathbf{E} \left( \gamma(n+1) - \gamma(n) \mid X_{\gamma(n)} \notin \tilde{T} \right) \cdot \mathbf{Pr} \left( X_{\gamma(n)} \notin \tilde{T} \right) \\
&\le \mathcal{L}(s_0) + (1+h_{\max}) \sum_{n \in \mathbb{N}} \mathbf{Pr} \left( X_{\gamma(n)} \notin \tilde{T} \right) \\
&= \mathcal{L}(s_0) + (1+h_{\max}) \sum_{n \in \mathbb{N}} \sum_{0 \le j < \ell_{\max}} \mathbf{Pr} \left( X_{\gamma(n\ell_{\max}+j)} \notin \tilde{T} \right) \\
&\le \mathcal{L}(s_0) + (1+h_{\max}) \ell_{\max} \sum_{n \in \mathbb{N}} \mathbf{Pr} \left( X_{\gamma(n\ell_{\max})} \notin \tilde{T} \right) \\
&\le \mathcal{L}(s_0) + (1+h_{\max}) \ell_{\max} \sum_{n \in \mathbb{N}} (1-p_{\min})^n < \infty
\end{align*}
$$

<figure><img src="image_13.png" /></figure>

**B** Details on the implementation presented in Section 5

B.1 Data-structure for exact summation

Algorithm 1 heavily relies on the capacity to accurately sum probabilities of very different magnitudes a large number of times. Indeed in early versions of the implementation, we have observed that without refined dedicated summation algorithms, the program does not terminate. Some methods exist to improve the accuracy of summation like Kahan summation algorithms [11] but are not sufficient in our setting. So we propose a data structure with better accuracy when summing up positive values, at the cost of increased memory consumption and time.

We present our data structure in the context of values in the interval $[0, 1]$, which is sufficient for probabilities. It encodes such a value $r$ as a table of 512 integers (each encoded on 64 bits) such that the content each cell $c[i]$ represents a floating point value (float) with the content of the cell being the mantissa and the index of the cell $i$ being the exponent. The value is encoded as the sum of the floats encoded by the cells, i.e. $r = \sum_{i \le 512} c[i] 2^{-i}$.

The addition of a float $x$ to a table $T$ encoding a number is done as follows (more details in [3]). The float is broken down into its exponent and mantissa i.e., $x = m2^{-u}$ with $m \le 2^{52}$ and $1 \le u \le 512$. There are two cases. First if $T[u] = 0$ then $T[u]$ is set to $m$. Otherwise the float stored at index $u$ is built ($y = T[u]2^{-u}$) and $x$ and $y$ are added. If this sum is at most $2^{52}$, then it is stored in $T[u]$; otherwise there is an overflow, and $T[u]$ is assigned $x + y - 2^{52}$, while the procedure is applied recursively with exponent $u+1$. In the worst case there are recursive calls over the whole range of $T$.

B.2 Heap with update

Algorithm 1 requires a data structure storing the set of states that have been visited with the probability and likelihood of the path reaching them. This data structure maps states to two real numbers representing the probability and the likelihood of the state. It requires to support three operations:

- insertion of a new mapping $s \mapsto (p, l)$ of a state to its probability and likelihood in the data structure;

- removing and retrieving the mapping with maximal probability;

- given a state $s$ updating the probability and likelihood of this state.
Such a data structure can be implemented with a heap and a hash table, which points to the
node in the heap allowing update. All operations are performed in logarithmic time w.r.t. to
the number of elements in the data structure.

B.3 Implementation of the numerical algorithm for decisive Markov chains

Algorithm 1 can be specialized to likelihood functions that are “monoidal” functions of the path, in the sense that paths leading to the same state can be merged while only retaining the probability to reach it together with a weighted average (over the paths) of the likelihood. Furthermore, using a heap where states are ordered by their probability to be reached (and merging them) represents a large improvement. The data structure for the heap is described in section B.2. One can show that the heap management policy is fair, and that the corresponding algorithm terminates on decisive Markov chains (see [3]).