<figure><img src="image_43.png" /><figcaption>Figure 3.15: A uniform $\frac{1}{2}$FF-diagnosable pLTS, that is not AFF-diagnosable.</figcaption></figure>

# 3 Characterisation of diagnosability

Our goal in this section is to establish “simple” characterisations of the diagnosability notions for a pLTS. More precisely, we aim at studying whether there exists a Borel set $B \in \mathcal{B}$ that only depends on the underlying LTS such that almost surely a random run belongs to $B$ if and only if the pLTS is diagnosable. Allowing $B$ to depend on the probabilities of the pLTS would give more expressivity, but strongly increases the complexity of the information contained in the set which goes against the goal of a “simple” characterisation. Similarly, as much as possible, we look for a set $B$ belonging to a low level of the Borel hierarchy.

Approximate notions of diagnosability heavily depend on the probabilities of the transitions. This can be seen on the two pLTS of Figure 3.8, page 69 for example: while the one on the left is $\varepsilon$FF-diagnosable for every $\varepsilon > 0$, the one on the right, which is obtained simply by swapping two probabilities, is not $\varepsilon$FF-diagnosable system for all $\varepsilon > 0$. We thus focus here on FA/FF/IA/IF-diagnosis. For these notions, the characterising Borel sets cannot be obtained directly from the definitions and require some machinery. Indeed, the notions of FF- and FA-diagnosability are expressed by the limit of the probability of a family of open sets and the notions of IF- and IA-diagnosability are expressed by a set which is not a *priori* a Borel set.

We will specify these Borel sets using a logic called **pathL**. Logics are tools that are efficient at giving specifications for a system and, thanks to model checking, at deciding if these specifications are satisfied by the system. The complexity of model checking a logic depends on the kind of systems considered (finite, probabilistic, ...) and on the power of expressivity of the logic. This makes thus yet another argument for requiring simple characterisations of the diagnosability notions.

In this section, we define the logic **pathL** in Subsection 3.1. Then, in Subsection 3.2 we give, whenever possible, a characterisation of the different diagnosability problems. Finally in Subsection 3.3, we provide impossibility results that justify why characterisations were not given for some of the diagnosability notions.

## 3.1 The logic pathL

We define the logic **pathL** in this section. Similarly to Probabilistic Linear Time Logic (PLTL) [CY95], **pathL** first defines a specification, then specifies a probabilistic condition over this specification. The main difference with PLTL is that **pathL** is based on the notion of *path formulae* instead of using atomic propositions. A path formula $p$ is a predicate over finite prefixes of runs. Before defining their syntax formally, let us first
give some examples of path formulae.

**Example 3.6.** Given a finite run $\rho = q_0 a_0 q_1 \dots q_k$, let $f$ be defined by $f(\rho) = \text{true}$ if $a_i = f$ for some $i < k$. This path formula characterises the faulty finite runs.

Let $\mathfrak{A}$ be defined by $\mathfrak{A}(\rho) = \text{true}$ if there exists a correct signalling run $\rho'$ with $\mathcal{P}(\rho) = \mathcal{P}(\rho')$. If this path formula is false, the current run is surely faulty.

Let us introduce a more intricate path formula. For $\sigma \in \Sigma_o^*$, we define $\text{firstf}(\sigma)$ as the smallest value such that there exists a faulty run with observation $\sigma$ such that its prefix of length $\text{firstf}(\sigma)$ is faulty, i.e. $\text{firstf}(\sigma) = \min\{k \mid \exists \rho \text{ signalling run } \mathcal{P}(\rho) = \sigma \wedge \rho_{\downarrow k} \text{ is faulty}\}$ with the convention that $\min(\emptyset) = \infty$. Then the path formula $\mathfrak{W}$ is defined by: $\mathfrak{W}(\varepsilon) = \text{false}$ and $\mathfrak{W}(q_0 a_0 \dots q_{n+1}) = \text{true}$ if $\text{firstf}(\mathcal{P}(q_0 a_0 \dots q_{n+1})) = \text{firstf}(\mathcal{P}(q_0 a_0 \dots q_n)) < \infty$. Every time this path formula is false, we increased the size of the greatest prefix that we are sure is correct.

As shown by the path formula $\mathfrak{A}$ for example, path formulae are extremely strong as they may depend on the global structure of the system, here by depending on the other existing runs with the same observation. This is far stronger than atomic propositions used in PLTL for example that only depend on the current state of the run.

Formally, a path formula is either generated by a context sensitive grammar or equivalently its acceptance is decided by a linear bounded automaton [Kur64]. In other words, one has to be able to determine the truth of a path formula in linear space.

**Example 3.7.** Among the examples of path formulae given in Example 3.6, the most difficult one is $\mathfrak{W}$. Let us show how one can compute the truth of this path formula in linear space. We first define for $\sigma \in \Sigma_o^*$ and $q \in Q$, the restriction of $\text{firstf}$ to $q$: $m(\sigma, q) = \min\{k \mid \exists \rho \in \text{SR}, \text{last}(\rho) = q \wedge \mathcal{P}(\rho) = \sigma \wedge \rho_{\downarrow k} \text{ is faulty}\}$ with the convention that $\min(\emptyset) = \infty$.

Let $\rho$ be a finite run, $\sigma$ its observed sequence. If $\sigma = \varepsilon$, $\mathfrak{W}(\rho) = \text{false}$. Else $\sigma = \sigma_1 \dots \sigma_n$. For every $q \in Q$, we compute the values $m(\sigma, q)$ and $m(\sigma_1 \dots \sigma_{n-1}, q)$ with the following algorithm:

<table><caption>**Algorithm 1** Computing the values of $m$</caption><tr><td>1:</td><td>Input: pLTS A, σ ∈ Σ<sup>*</sup><sub>o</sub></td></tr><tr><td>2:</td><td>Output: (m(σ<sub>≤k</sub>, q))<sub>k≤|σ|,q∈Q</sub></td></tr><tr><td>3:</td><td>for q ∈ Q do</td></tr><tr><td>4:</td><td>m(ε, q) ← ∞</td></tr><tr><td>5:</td><td>for i = 1 to n do</td></tr><tr><td>6:</td><td>for q, q' ∈ Q do</td></tr><tr><td>7:</td><td>m(σ<sub>1</sub> ... σ<sub>i</sub>, q) ← ∞</td></tr><tr><td>8:</td><td>if q ⇒<sup>σ<sub>i</sub></sup><sub>f</sub> q' then</td></tr><tr><td>9:</td><td>m(σ<sub>1</sub> ... σ<sub>i</sub>, q') → min(m(σ<sub>1</sub> ... σ<sub>i-1</sub>, q'), i)</td></tr><tr><td>10:</td><td>if q ⇒<sup>σ<sub>i</sub></sup><sub>f</sub> q' then</td></tr><tr><td>11:</td><td>m(σ<sub>1</sub> ... σ<sub>i</sub>, q') → min(m(σ<sub>1</sub> ... σ<sub>i-1</sub>, q'), m(σ<sub>1</sub> ... σ<sub>i-1</sub>, q))</td></tr></table>
This algorithm uses linear space in n. Moreover, we have an equivalence between $\mathfrak{W}(\rho) = \text{true}$ and $\max_{q \in Q}\{m(\sigma_1 \dots \sigma_{n-1}, q)\} < \max_{q \in Q}\{m(\sigma, q)\} < \infty$. Thus the truth of $\mathfrak{W}$ can be decided by a linear bounded automaton. It is therefore a path formula.

We now define the syntax of pathL.

**Definition 3.7.** The syntax of a pathL formula is:

$$ \phi ::= \mathfrak{p} \mid \neg\phi \mid \phi_1 \wedge \phi_2 \mid \diamond\phi $$

where $\mathfrak{p}$ is a path formula. In the sequel we use the standard shortcut $\Box\phi \equiv \neg\diamond\neg\phi$.

A formula is evaluated at some position $k$ of a run $\rho = q_0 a_0 q_1 \dots$. The prefix $\rho_{\le k}$ of $\rho$ is defined by $\rho_{\le k} = q_0 a_0 q_1 \dots q_k$. The semantics of pathL is inductively defined by:

* $\rho, k \models \alpha$ if $\alpha(\rho_{\le k})$, note that only the past of $\rho$ is used;

* $\rho, k \models \neg\phi$ if $\rho, k \not\models \phi$;

* $\rho, k \models \phi_1 \wedge \phi_2$ if $\rho, k \models \phi_1$ and $\rho, k \models \phi_2$;

* $\rho, k \models \diamond\phi$ if there exists $k' \ge k$ such that $\rho, k' \models \phi$.

Finally $\rho \models \phi$ if $\rho, 0 \models \phi$. Due to the presence of path formulae (with no restriction) this language subsumes LTL and more generally any $\omega$-regular specification language, i.e. any language that can be recognized by an $\omega$-automaton such as a Rabin automaton.

**Proposition 3.6.** The language generated by pathL subsumes $\omega$-regular languages.

*Proof.* The language of a deterministic Rabin automaton is determined by a finite family of pair of sets $(E_i, F_i)$. It consists of the set of runs $\rho$ for which there exists $i \in \mathbb{N}$ such that $\rho$ visits finitely often the states of $E_i$ and infinitely often the states of $F_i$. We define the path formulae $\mathfrak{E}_i$ and $\mathfrak{F}_i$ such that $\mathfrak{E}_i(\rho) = \text{true}$ iff $\text{last}(\rho) \in E_i$ and $\mathfrak{F}_i(\rho) = \text{true}$ iff $\text{last}(\rho) \in F_i$. The runs accepted by the Rabin automaton equivalently satisfy the formula $\bigvee_i(\diamond\Box(\neg\mathfrak{E}_i) \wedge (\Box\diamond\mathfrak{F}_i))$. The language accepted by the Rabin automaton is thus generated by pathL. $\square$

In order to reason about the probabilistic behaviour of a pLTS, we introduce the notion of qualitative probabilistic formulae:

**Definition 3.8.** The syntax of a qualitative probabilistic formula of pathL is: $\mathbb{P}^{\boxtimes p}(\phi)$ with $\boxtimes \in \{<, >, =\}$, $p \in \{0, 1\}$ and $\phi \in \text{pathL}$.

The semantics is obvious: $\mathcal{A} \models \mathbb{P}^{\boxtimes p}(\phi)$ if and only if $\mathbb{P}(\{\rho \in \Omega \mid \rho \models \phi\}) \boxtimes p$.

The set of Borel sets defined by pathL is closed by complementation since the complement of the set of runs generated by a formula $\phi$ is generated by the formula $\neg\phi$. Therefore given a pLTS $\mathcal{A}$ and a formula $\phi$, $\mathcal{A} \models \mathbb{P}^0(\phi)$ iff $\mathcal{A} \models \mathbb{P}^0(\neg\phi)$ and $\mathcal{A} \models \mathbb{P}^1(\phi)$ iff $\mathcal{A} \models \mathbb{P}^0(\neg\phi)$. The qualitative probabilistic formulae can thus be restricted to $\mathbb{P}^0(\phi)$ and $\mathbb{P}^0(\phi)$.
## 3.2 Logical characterisation of diagnosability

We now exhibit qualitative probabilistic formulae $\psi$ such that a pLTS $\mathcal{A}$ is diagnosable iff $\mathcal{A} \models \psi$.

**FF-diagnosability.** We start with FF-diagnosability. This notion seems to be the easiest one as it focuses on faulty runs and its definition already uses a family of Borel sets. Indeed, we can prove a simple characterisation of FF-diagnosability using the path formulae $f$ and $\mathfrak{U}$ that we defined in Example 3.6.

**Proposition 3.7.** Let $\mathcal{A}$ be a pLTS. Then $\mathcal{A}$ is FF-diagnosable iff $\mathcal{A} \models \mathbb{P}^0(\diamond\Box(f \wedge \mathfrak{U}))$.

Once a run becomes surely faulty, it cannot become ambiguous. Thus, informally, this formula means that a pLTS is FF-diagnosable if the measure of runs that are infinitely often faulty and ambiguous is equal to 0. These runs are the faulty runs for which the fault can never be claimed by the FF-diagnoser. It is thus natural to require their probability to be equal to 0.

*Proof.* We write $E = \{\rho \in \Omega \mid \diamond\Box(f \wedge \mathfrak{U})\}$ for the set of runs we are interested in. We further define, for every $\rho \in \min F$, $E_\rho = \{\rho' \in \Omega \mid \rho \preceq \rho' \wedge \rho' \models \Box\mathfrak{U}\}$ and for every $n \in \mathbb{N}$, $E_\rho^n = \{\rho' \in \Omega \mid \rho \preceq \rho' \wedge \rho' \models \Box^n\mathfrak{U}\}$ where $\rho \models \Box^n\phi$ if for every $k \le n$, $\rho, k \models \phi$. As $\rho \in \min F$ and $\rho', n \models f \wedge \mathfrak{U}$ implies $\rho'[0, n]$ is faulty and ambiguous, we have for all $n \ge 0$ $E_\rho^n \subseteq \text{FAmb}_{n+|\rho|}$. Observe that $E = \bigcup_{\rho \in \min F} E_\rho$ and that $E_\rho = \cap_{n \in \mathbb{N}} E_\rho^n$. Thus $\mathbb{P}(E) = \sum_{\rho \in \min F} \mathbb{P}(E_\rho)$ and $\lim_{n \to \infty} \mathbb{P}(E_\rho^n) = \mathbb{P}(E_\rho)$.

* Assume first that $\mathbb{P}(E) > 0$. Then, there exists $\rho \in \min F$ such that $\mathbb{P}(E_\rho) > 0$. By definition, for every $n > |\rho|_o$, $\mathbb{P}(\text{FAmb}_n) \ge \mathbb{P}(E_\rho)$. Thus, $\mathcal{A}$ is not FF-diagnosable.

* Assume now that $\mathbb{P}(E) = 0$. So, for every $\rho \in \min F$, $\mathbb{P}(E_\rho) = 0$. Let us pick some $\varepsilon > 0$. Since $F = \bigcup_{n \in \mathbb{N}} F_n$, there exists $n_0$ such that for every $n \ge n_0$, $\mathbb{P}(F \setminus F_n) \le \frac{\varepsilon}{3}$. Let $R = \{\rho \in \min F \mid |\rho|_o < n_0\}$. Pick a finite subset $R'$ of $R$ such that $\sum_{\rho \in R \setminus R'} \mathbb{P}(\rho) \le \frac{\varepsilon}{3}$. Define $K = |R'|$. Let $n_1$ be such that for every $n \ge n_1$ and every $\rho \in R'$, $\mathbb{P}(E_\rho^n) \le \frac{\varepsilon}{3K}$. Observe now that for every $n \ge n_0$, $\text{FAmb}_n \subseteq (F \setminus F_n) \cup \bigcup_{\rho \in R \setminus R'} C(\rho) \cup \bigcup_{\rho \in R'} E_\rho^n$. Thus, for every $n \ge n_1$, $\mathbb{P}(\text{FAmb}_n) \le \frac{\varepsilon}{3} + \frac{\varepsilon}{3} + K \frac{\varepsilon}{3K} = \varepsilon$. Since $\varepsilon$ is arbitrary, $\mathcal{A}$ is FF-diagnosable. $\square$

**IF-diagnosability.** IF-diagnosability focuses on infinite runs and $\text{FAmb}_\infty$ is not per se a Borel set. Obtaining a characterisation is thus more difficult. Thanks to Theorem 3.1 however, in finitely-branching pLTS the above characterisation also holds for IF-diagnosability.

**Corollary 3.2.** Let $\mathcal{A}$ be a finitely-branching pLTS. Then $\mathcal{A}$ is IF-diagnosable iff $\mathcal{A} \models \mathbb{P}^0(\diamond\Box(f \wedge \mathfrak{U}))$.

**IA-diagnosability.** The assumption of finitely-branching pLTS is also needed in order to characterise IA-diagnosability. In addition to the path formula $\mathfrak{U}$ we also use the path formula $\mathfrak{W}$ defined in Example 3.6, page 78.
**Proposition 3.8.** Let $\mathcal{A}$ be a finitely-branching pLTS. Then $\mathcal{A}$ is IA-diagnosable iff
$\mathcal{A} \models \mathbb{P}^= (\diamond \square (\mathfrak{U} \wedge \mathfrak{W})).$

Intuitively, as a faulty run cannot become correct, if a run does not satisfy $\mathfrak{U}$ once,
then $\rho \models \diamond \square (\neg \mathfrak{U})$. Thus, $\rho \not\models \diamond \square (\mathfrak{U} \wedge \mathfrak{W})$ if either (1) it does not satisfy $\mathfrak{U}$ at least
once, meaning $\rho$ is surely faulty, or (2) does not satisfy $\mathfrak{W}$ infinitely often. In the latter
case, the intuition is the following. Infinitely often firstf has increased. If there exists
a faulty run $\rho_f$ with $\mathcal{P}(\rho) = \rho_f$, then firstf is bounded, on the prefixes of $\mathcal{P}(\rho)$, by the
length at which $\rho_f$ becomes faulty. Thus no faulty run exists with observation $\mathcal{P}(\rho)$
and $\rho$ is surely correct.

*Proof.* In order to prove formally the adequacy of the formula, it is enough to show that $\rho \in \Omega$ is ambiguous if and only if $\rho \models \diamond \square (\mathfrak{U} \wedge \mathfrak{W})$. We focus below on correct runs; the case of faulty runs can be treated in a similar, and even simpler, way.

* Let $\rho \in \mathcal{C}\mathit{Amb}_{\infty}$. Since $\rho$ is ambiguous, there exists a faulty run $\rho'$ such that $\mathcal{P}(\rho') = \mathcal{P}(\rho)$. Let $k_0$ be such that $\rho'_{\downarrow k_0}$ is faulty. Thus for all $k \ge k_0$, firstf($\mathcal{P}(\rho_{\downarrow k})$) $\le k_0$ and in addition it is non-decreasing. So there exists some $k_1 \ge k_0$ such that for all $k \ge k_1$, firstf($\mathcal{P}(\rho_{\downarrow k})$) is constant. We thus obtain $\rho \models \diamond \square \mathfrak{W}$. Moreover, since $\rho \models \square \mathfrak{U}$, we conclude that $\rho \models \diamond \square (\mathfrak{U} \wedge \mathfrak{W})$.

* Conversely, let $\rho$ be a correct run such that $\rho \models \diamond \square (\mathfrak{U} \wedge \mathfrak{W})$. Thus there is a position $k_0$ such that for all $k \ge k_0$, $\rho, k \models \mathfrak{W}$. In particular, by definition of $\mathfrak{W}$, for all $k \ge k_0$, there is a finite signalling run $\rho'^{(k)}$ such that $\mathcal{P}(\rho'^{(k)}) = \mathcal{P}(\rho_{\downarrow k})$ and $\rho'_{\downarrow k_0}^{(k)}$ is faulty. Consider the tree of these runs $\rho'^{(k)}$ by merging the common prefixes. This tree is finitely branching and infinite. By König's lemma, it must admit an infinite branch, corresponding to a run $\rho'$ with $\mathcal{P}(\rho') = \mathcal{P}(\rho)$ and $\rho'_{\downarrow k_0}$ faulty. We deduce that $\rho$ is ambiguous. $\square$

<figure><img src="image_44.png" /><figcaption>Figure 3.16: An infinitely-branching IA-diagnosable pLTS which does not satisfy $\mathbb{P}^= (\diamond \square (\mathfrak{U} \wedge \mathfrak{W}))$.</figcaption></figure>

The pLTS of Figure 3.16 illustrates the need for the finitely-branching assumption
in Proposition 3.8. The set of unobservable events is {$u, f$}. Observation $b$ occurs in
every infinite correct run, while the observed sequence of the single infinite faulty run
is $a^\omega$. This pLTS is thus IA-diagnosable. However, it does not satisfy $\mathbb{P}^= (\diamond \square (\mathfrak{U} \wedge \mathfrak{W}))$
since the unique infinite faulty run has probability $\frac{1}{2}$ and satisfies at the same time
□W, by unicity, and □U. Indeed for every $n \in \mathbb{N}$, there is a correct signalling run with observed sequence $a^n$.

Observe that the sets of runs specified by the characterisations of FF-diagnosability (◇□(f ∧ U)) and IA-diagnosability (◇□(U ∧ W)) are $F_\sigma$ sets, i.e. countable unions of closed sets.

### 3.3 Non-expressivity results

We chose to use a logic where the structural and probabilistic aspects are separated. This brought some advantages, but also weakens the expressibility. As a consequence, approximate notions of diagnosability for which the probabilities are important to define the ambiguity cannot be characterised. We prove this formally by showing that there is no Borel set $E$ and $F$ such that neither $\mathcal{A} \models \mathbb{P}^0(E)$ nor $\mathcal{A} \models \mathbb{P}^0(F)$ characterises 1/2FF-diagnosability.

**Proposition 3.9.** There exists a finitely-branching LTS $\mathcal{A}$ such that for every Borel sets $E$ and $F$ of runs, there exists a pLTS $\mathcal{A} = (\mathcal{A}, \mathbf{P})$ such that:

* either $\mathcal{A}$ is 1/2FF-diagnosable and $\mathbb{P}_{\mathcal{A}}(E) > 0$;

* or $\mathcal{A}$ is not 1/2FF-diagnosable and $\mathbb{P}_{\mathcal{A}}(E) = 0$.

and

* either $\mathcal{A}$ is 1/2FF-diagnosable and $\mathbb{P}_{\mathcal{A}}(F) = 0$;

* or $\mathcal{A}$ is not 1/2FF-diagnosable and $\mathbb{P}_{\mathcal{A}}(F) > 0$.

This proposition is proved by constructing a family of pLTS whose underlying LTS is the same, thus the Borel set we construct is the same for every member of this family. However the probabilities can be appropriately chosen in order for the pLTS to model or not the formula in contradiction with its diagnosability.

*Proof.* Consider the LTS $\mathcal{A} = (\langle Q, q_0, \Sigma, T \rangle)$ defined as follows and let the set of unobservable events be $\Sigma_u = \{\mathbf{f}, u\}$:

* $Q = \{q_0, q_f, q_c\}$,

* $\Sigma = \{a, b, \mathbf{f}, u\}$,

* $T = \{(q_0, u, q_c), (q_0, \mathbf{f}, q_f), (q_c, a, q_c), (q_c, b, q_c), (q_f, a, q_f), (q_f, b, q_f)\}$.

We consider a family of pLTS, represented in Figure 3.17 with underlying LTS $\mathcal{A}$. Given a pair of probabilities $(p_1, p_2)$, we define the pLTS $\mathcal{A}_{(p_1, p_2)} = (\mathcal{A}, \mathbf{P}_{(p_1, p_2)})$ in which $\mathbf{P}_{(p_1, p_2)}(q_0, \mathbf{f}, q_f) = \mathbf{P}_{(p_1, p_2)}(q_0, u, q_c) = 1/2$, $\mathbf{P}_{(p_1, p_2)}(q_c, a, q_c) = p_1$, $\mathbf{P}_{(p_1, p_2)}(q_c, b, q_c) = 1 - p_1$, $\mathbf{P}_{(p_1, p_2)}(q_f, a, q_f) = p_2$ and $\mathbf{P}_{(p_1, p_2)}(q_f, b, q_f) = 1 - p_2$.

First note that $\mathcal{A}_{(p_1, p_2)}$ is 1/2FF-diagnosable iff $p_1 \neq p_2$. This can be established similarly to what was done in Example 3.5, page 68. In fact one can show that $\mathcal{A}_{(p_1, p_2)}$ is AFF-diagnosable iff $p_1 \neq p_2$.
<figure><img src="image_45.png" /><figcaption>Figure 3.17: A family of pLTS whose underlying LTS has no appropriate characterisation for 1/2FF-diagnosability.</figcaption></figure>

Let $E$ be an arbitrary Borel set over the set of runs of $\mathcal{A}$. If there exists a probability value $p$ such that $\mathcal{A}_{(p,p)} \models \mathbb{P}^0(E)$ we have the first part of the result. Else, let $p$ and $p'$ be two probabilities with $p \neq p'$. As the probabilities of the runs of $E$ in $\mathcal{A}_{(p,p')}$ do not depend simultaneously on $p$ and on $p'$, $\mathbb{P}_{\mathcal{A}_{(p,p')}}(E) + \mathbb{P}_{\mathcal{A}_{(p',p)}}(E) = \mathbb{P}_{\mathcal{A}_{(p,p)}}(E) + \mathbb{P}_{\mathcal{A}_{(p',p')}}(E)$. Moreover, for every probability $p''$, $\mathcal{A}_{(p'',p'')} \not\models \mathbb{P}^0(E)$, thus either $\mathbb{P}_{\mathcal{A}_{(p,p')}}(E) > 0$ or $\mathbb{P}_{\mathcal{A}_{(p',p)}}(E) > 0$ which concludes the first part of the proof.

Let $F$ be an arbitrary Borel set. If there exists a probability $p$ such that $\mathcal{A}_{(p,p)} \models \mathbb{P}^0(E)$ we have the first part of the result. Else, let $p$ and $p'$ be two probabilities with $p \neq p'$. As before, $\mathbb{P}_{\mathcal{A}_{(p,p')}}(F) + \mathbb{P}_{\mathcal{A}_{(p',p)}}(F) = \mathbb{P}_{\mathcal{A}_{(p,p)}}(F) + \mathbb{P}_{\mathcal{A}_{(p',p')}}(F) = 0$. Thus both $\mathcal{A}_{(p,p')} \models \mathbb{P}^0(F)$ and $\mathcal{A}_{(p',p)} \models \mathbb{P}^0(E)$ which concludes the second part of the proof. $\square$

For exact notions of diagnosability, intuitively, FA-diagnosability would be in between FF-diagnosability and IA-diagnosability in terms of complexity. Surprisingly we showed that FA-diagnosability does not admit such a characterisation: there is no $F_\sigma$ set $E$ such that a pLTS $\mathcal{A}$ is FA-diagnosable if and only if $\mathcal{A} \models \mathbb{P}^0(E)$.

**Proposition 3.10.** There exists a finitely-branching infinite LTS $\mathcal{A}$ such that for every $F_\sigma$ set $E$ of runs, there exists a pLTS $\mathcal{A} = (\mathcal{A}, \mathbf{P})$ such that:

* either $\mathcal{A}$ is FA-diagnosable and $\mathbb{P}_{\mathcal{A}}(E) > 0$;

* or $\mathcal{A}$ is not FA-diagnosable and $\mathbb{P}_{\mathcal{A}}(E) = 0$.

This proposition is proved in a similar fashion as Proposition 3.9, it is only more involved. The family of pLTS we construct has infinitely many states and infinitely many parametric probabilities. These probabilities can be chosen in order to give a positive value to either the limit of the probability of $\mathcal{C}_{\text{Amb}}_n$ or to the given $F_\sigma$ set.

*Proof.* Consider the LTS $\mathcal{A} = (\langle Q, q_0, \Sigma, T \rangle)$ defined as follows:

* $Q = \{f_1, q_f\} \cup \{q_i \mid i \in \mathbb{N}\}$;

* $\Sigma = \{a, b, c, u, \mathbf{f}\}$;

* $T = \{(q_0, u, q_f), (q_0, u, q_1), (q_f, a, q_f), (q_f, b, q_f), (q_f, \mathbf{f}, f_1), (f_1, b, f_1), (f_1, c, f_1) \cup \{(q_i, a, q_{i+1}), (q_i, b, q_{i+1})\}_{i \ge 1}$;
$$ \bullet \Sigma_u = \{\mathbf{f}, u\}. $$

<figure><img src="image_46.png" /><figcaption>Figure 3.18: A family of pLTS whose underlying LTS has no appropriate characterization of FA-diagnosability.</figcaption></figure>

We consider a family of pLTS, represented in Figure 3.18, with underlying LTS $\mathcal{A}$. For $\mathbf{p} = (p_n)_{n \ge 1}$ a sequence of probabilities, we define the pLTS $\mathcal{A}_{\mathbf{p}} = (\mathcal{A}, \mathbf{P}_{\mathbf{p}})$ in which for every $n \ge 1$ the probability that ‘b’ occurs from state $q_n$ is $\mathbf{P}_{\mathbf{p}}(q_n, b, q_{n+1}) = p_n$, the probability that ‘a’ occurs from state $q_n$ is $\mathbf{P}_{\mathbf{p}}(q_n, a, q_{n+1}) = 1 - p_n$ and all other probabilities are independent of $\mathbf{p}$: $\mathbf{P}_{\mathbf{p}}(q_0, u, q_f) = \mathbf{P}_{\mathbf{p}}(q_0, u, q_1) = \mathbf{P}_{\mathbf{p}}(f_1, b, f_1) = \mathbf{P}_{\mathbf{p}}(f_1, c, f_1) = \frac{1}{2}$, $\mathbf{P}_{\mathbf{p}}(q_f, a, q_f) = \mathbf{P}_{\mathbf{p}}(q_f, b, q_f) = \mathbf{P}_{\mathbf{p}}(q_f, \mathbf{f}, f_1) = \frac{1}{3}$.

Observe that a faulty run almost surely produces a ‘c’, so that $\lim_{n \to \infty} \mathbb{P}(\mathcal{F}\text{Amb}_n) = 0$. Moreover, as the ambiguous runs are the ones ending by a ‘b’, the probability to be ambiguous after $n$ observations on the leftmost part is $\frac{1}{2} \frac{2^{n-1}}{3^n}$ and on the rightmost part is $\frac{1}{2} p_n \mathbb{P}(\mathcal{C}\text{Amb}_n) = p_n + \frac{2^{n-1}}{3^n}$. Therefore, $\mathcal{A}_{\mathbf{p}}$ is FA-diagnosable iff $\lim_{n \to \infty} p_n = 0$.

Let $E$ be an arbitrary $F_\sigma$ set. We pick some FA-diagnosable $\mathcal{A}_{\mathbf{p}}$ i.e. such that $\lim_{n \to \infty} p_n = 0$ and write $\mathbb{P}_{\mathbf{p}}$ for the probability measure it induces. If $\mathbb{P}_{\mathbf{p}}(E) > 0$ we are done. Assume thus that $\mathbb{P}_{\mathbf{p}}(E) = 0$. In order to define a second pLTS, via $\mathbf{p}'$, consider an infinite increasing sequence $\{n_j\}_{j \le 1}$ and let for $n \notin \{n_j\}_{j \le 1}$, $p'_n = p_n$ and for $n \in \{n_j\}_{j \ge 1}$, $p'_n = \frac{1}{2}$. Due to the sub-sequence $p'_{n_j} = \frac{1}{2}$, $\mathcal{A}_{\mathbf{p}'}$ is not FA-diagnosable. The sequence $\{n_j\}_{j \le 1}$ depends on $\mathbb{P}_{\mathbf{p}}$ and will be defined after some preliminary observations.

Let $F = \{\rho \mid q_0 u q_1 \le \rho\}$. Denoting $\mathbb{P}_{\mathbf{p}'}$ the probability measure of the second pLTS, observe that $\mathbb{P}_{\mathbf{p}'}(E \setminus F) = \mathbb{P}_{\mathbf{p}}(E \setminus F) = 0$. Using the above discussion, the $F_\sigma$ set $E \cap F = \bigcup_{m \in \mathbb{N}} \bigcap_{n \in \mathbb{N}} O_{m,n}$ where for all $m, n$, $O_{m,n}$ is a disjoint union of cylinders $C(\rho)$ with $|\rho| = n$, $O_{m,n+1} \subseteq O_{m,n}$ and $O_{m,n} \subseteq O_{m+1,n}$. Denote $F_m = \bigcap_{n \in \mathbb{N}} O_{m,n}$. For all $m$, $\lim_{n \to \infty} \mathbb{P}_{\mathbf{p}}(O_{m,n}) = \mathbb{P}_{\mathbf{p}}(E \cap F_m) \le \mathbb{P}_{\mathbf{p}}(E \cap F) = 0$.

* $n_1$ is chosen such that for all $n \ge n_1$, $p_n \le \frac{1}{2}$. Observe now that for all $n_j$,

$$ p'_{n_j} = \frac{1}{2} = \frac{1}{2p_{n_j}} p_{n_j} \text{ and } 1 - p'_{n_j} = \frac{1}{2} \le 1 - p_{n_j} \le \frac{1}{2p_{n_j}} (1 - p_{n_j}). $$

By definition of $\mathbb{P}_{\mathbf{p}'}$, since $O_{m,n}$ is a disjoint union of cylinders $C(\rho)$ with $|\rho| = n$, applying inductively the previous inequalities, for all $n$ such that $n_k < n \le n_{k+1}$ (denoting $n_0 = 0$):

$$ \mathbb{P}_{\mathbf{p}'}(O_{m,n}) \le \frac{\mathbb{P}_{\mathbf{p}}(O_{m,n})}{2^k \prod_{1 \le j < k} p_{n_j}}. \qquad (3.1) $$
• Assume that we have chosen $n_1, \dots, n_k$. Since $\lim_{n \to \infty} \mathbb{P}_p(O_{k,n}) = 0$, there exists $n_{k+1} > n_k$ such that $\mathbb{P}_p(O_{k,n_{k+1}}) \le \prod_{1 \le j \le k} p_{n_j}$. We choose such an index.
Equation (3.1) now implies that for all $m \le k$,

$$ \mathbb{P}_{\mathbf{p}'}(O_{m,n_{k+1}}) \le \mathbb{P}_{\mathbf{p}'}(O_{k,n_{k+1}}) \le \frac{1}{2^k}. $$

Thus for all $m$,

$$ \mathbb{P}_{\mathbf{p}'}(F_m) = \lim_{k \to \infty} \mathbb{P}_{\mathbf{p}'}(O_{m,n_{k+1}}) = 0. $$

Since $E \cap F = \bigcup_{m \in \mathbb{N}} F_m$, $\mathbb{P}_{\mathbf{p}'}(E \cap F) = 0$ and so $\mathbb{P}_{\mathbf{p}'}(E) = 0$. $\square$

Beyond Proposition 3.10, we conjecture that the impossibility also holds for arbitrary Borel sets.

Proposition 3.10 only shows the non-existence for characterisations that requires a null probability of the given set. There could thus still exists a characterisation asking for a positive probability. In fact, such a characterisation does not exist. This impossibility is even stronger than the one of Proposition 3.10 as we show that a positive probability characterization cannot exist whatever the Borel set (and not only $F_\sigma$).

**Proposition 3.11.** There exists a finitely-branching LTS $\mathcal{A}$ such that for every Borel set $E$ of runs, there exists a pLTS $\mathcal{A} = ((\mathcal{A}, \mathbf{P}), \Sigma_o, \mathcal{P})$ such that:

* either $\mathcal{A}$ is FA-diagnosable and $\mathbb{P}_{\mathcal{A}}(E) = 0$;

* or $\mathcal{A}$ is not FA-diagnosable and $\mathbb{P}_{\mathcal{A}}(E) > 0$.

This proof is similar to the previous one, albeit with an even more complex family of pLTS. Indeed, here, instead of having a parametric probability $p_i$ for every $i \in \mathbb{N}$ we have one for every word $w \in \{a, b\}^*$.

*Proof.* Consider the LTS $\mathcal{A} = (\langle Q, q_0, \Sigma, T \rangle)$ defined as follows:

* $Q = \{f_1, q_f, q_0\} \cup \{q_w | w \in (a+b)^*\}$;

* $\Sigma = \{a, b, c, u, \mathbf{f}\}$;

* $T = \{(q_0, u, q_f), (q_0, u, q_1), (q_f, a, q_f), (q_f, b, q_f), (q_f, \mathbf{f}, f_1), (f_1, b, f_1), (f_1, c, f_1)\} \cup \{(q_w, a, q_{wa}), (q_w, b, q_{wb})\}_{w \in (a+b)^*}$;

* $\Sigma_u = \{\mathbf{f}, u\}$.

We consider a family of pLTS, represented in Figure 3.19, with underlying LTS $\mathcal{A}$, parametrised by a mapping $\mathbf{p} : (a+b)^* \to (0,1)$. Let $\mathcal{A}_{\mathbf{p}} = ((\mathcal{A}, \mathbf{P}_{\mathbf{p}}), \Sigma_o, \mathcal{P})$ be the pLTS such that the probability that 'b' occurs from state $q_w$ is $\mathbf{P}(q_w, b, q_{wb}) = \mathbf{p}(w)$, the probability that 'a' occurs from state $q_w$ is $\mathbf{P}(q_w, b, q_{wa}) = 1 - \mathbf{p}(w)$ and all other probabilities are independent from $\mathbf{p}$: $\mathbf{P}_{\mathbf{p}}(q_0, u, q_f) = \mathbf{P}_{\mathbf{p}}(q_0, u, q_1) = \mathbf{P}_{\mathbf{p}}(f_1, b, f_1) = \mathbf{P}_{\mathbf{p}}(f_1, c, f_1) = \frac{1}{2}$, $\mathbf{P}_{\mathbf{p}}(q_f, a, q_f) = \mathbf{P}_{\mathbf{p}}(q_f, b, q_f) = \mathbf{P}_{\mathbf{p}}(q_f, \mathbf{f}, f_1) = \frac{1}{3}$. In the sequel, for
<figure><img src="image_47.png" /><figcaption>Figure 3.19: Another family of pLTS whose underlying LTS has no appropriate characterisation of FA-diagnosability.</figcaption></figure>

convenience, we also write $\mathbf{p}(w, b)$ for $\mathbf{p}(w)$, and define $\mathbf{p}(w, a) = 1 - \mathbf{p}(w)$, so that $\mathbf{P}(q_w, a, q_{wa}) = \mathbf{p}(w, a)$.

Word $w$ can be decomposed into letters $w = w[1] \dots w[n]$, and we give notations for factors: $w[1, k] = w[1] \dots w[k]$ with the convention that $w[1, 0] = \varepsilon$. Finally we define $\mathbf{p}_{\mathbf{p}}(w) = \prod_{1 \le k \le n} \mathbf{p}(w[1, k-1], w[k])$, as the probability to read $w$ from $q_{\varepsilon}$. Since $\lim_{n \to \infty} \mathbf{P}(\text{FAmb}_n) = 0$ and $\mathbf{P}(\text{CAmb}_{n-1}) = \sum_{w||w|=n-1} \mathbf{p}(w, b) + \frac{2^{n-1}}{3^n}$, we deduce that $\mathcal{A}_{\mathbf{p}}$ is FA-diagnosable iff $\lim_{n \to \infty} \sum_{|w|=n-1} \mathbf{p}(w, b) = 0$.

Let $E$ be an arbitrary measurable set. Pick some pLTS $\mathcal{A}_{\mathbf{p}}$ which is FA-diagnosable, i.e. with $\lim_{n \to \infty} \sum_{|w|=n-1} \mathbf{p}(w, b) = 0$. If $\mathbb{P}_{\mathbf{p}}(E) = 0$ where $\mathbb{P}_{\mathbf{p}}$ is the probability of this pLTS, we are done. Assume therefore that $\mathbb{P}_{\mathbf{p}}(E) > 0$. Let $F = \{\rho \mid q_0 u q_{\varepsilon} \subseteq \rho\}$ be the set of runs starting with a $u$-transition to $q_{\varepsilon}$. Denoting $\mathbb{P}_{\mathbf{p}'}$ the probability measure of any other pLTS $\mathcal{A}_{\mathbf{p}'}$, observe that $\mathbb{P}_{\mathbf{p}'}(E \setminus F) = \mathbb{P}_{\mathbf{p}}(E \setminus F)$. So, if $\mathbb{P}_{\mathbf{p}}(E \setminus F) > 0$, then by picking any non FA-diagnosable $(\mathcal{A}, \mathbf{P}_{\mathbf{p}'})$, we are done. So assume $\mathbb{P}_{\mathbf{p}}(E \setminus F) = 0$ which implies $\mathbb{P}_{\mathbf{p}}(E \cap F) > 0$. The probability being an inner regular measure (recall Definition 2.4, page 37), there exists a closed set $G \subseteq E \cap F$ with $\mathbb{P}_{\mathbf{p}}(G) > 0$.

If $G = F$ then $\mathbb{P}_{\mathbf{p}'}(G) = \mathbb{P}_{\mathbf{p}}(G) = \frac{1}{2}$. In this case, we can therefore conclude by picking any non FA-diagnosable pLTS $\mathcal{A}_{\mathbf{p}'}$.

Assuming $G \subsetneq F$, since $G$ is closed, there is some cylinder $C(\rho)$ with $\rho = q_0 u q_{\varepsilon} \dots q_w$ such that $G \cap C(\rho) = \emptyset$. Then we define the pLTS $\mathcal{A}_{\mathbf{p}'}$ as the pLTS $\mathcal{A}_{\mathbf{p}}$ except that for every $w \le w'$ and every $x \in \{a, b\}$, $\mathbf{p}'(w', x) = \frac{1}{2}$. Thus for every $n \ge |w|$, $\sum_{|w'|=n} \mathbf{p}'(w', b) \ge \frac{\mathbb{P}_{\mathbf{p}}(\rho)}{2}$. So $\mathcal{A}_{\mathbf{p}'}$ is not FA-diagnosable. On the other hand, $\mathbb{P}_{\mathbf{p}'}(E \cap F) \ge \mathbb{P}_{\mathbf{p}'}(G) = \mathbb{P}_{\mathbf{p}}(G) > 0$. $\square$

With Proposition 3.10 and Proposition 3.11 FA-diagnosability appears to be the most complicated of the exact diagnosability notions. Indeed, it cannot be characterised by any set of at least the first two level of the Borel hierarchy contrary to the other notions. This confirms the intuition that was raised when defining the diagnosers associated with each notion of diagnosability. For approximate notions of diagnosability, the non-expressibility result of Proposition 3.9 clearly shows that studying these notions requires a characterisation that intertwines structural and probabilistic elements.
# 4 Conclusion

In Section 1, appropriate diagnosers were associated with notions of diagnosability. This gave another point of view on the notions of diagnosability and raised the question of the memory that is necessary for a diagnoster. We showed that for approximate notions of diagnosability, unbounded memory may be necessary even for finite systems. However for exact notions of diagnosability, every example we gave used finite memory. In Chapter 4, we study diagnosability of finite pLTS and establish what memory is needed for each notion of exact diagnosability.

In Section 2, the links between the various diagnosability notions were established. This showed multiple interesting facts. In non-probabilistic systems, diagnosability only focuses on faulty runs as, for finitely-branching systems, if there is an infinite faulty ambiguous run, there also exists an infinite correct ambiguous run. However, when probabilistic models are considered, this symmetry is broken. Caring about both faulty and correct runs make for an entirely new notion. Moreover, probabilities do not affect correct and faulty runs in the same way concerning ambiguity: while IF- and FF-diagnosability are equivalent for finitely-branching systems, IA- and FA-diagnosability are not equivalent even for finite systems. Another interesting point, the uniformity requirement is not as important for exact notions of diagnosis than for approximate ones. Last, while AFF-diagnosability could appear to be close to FF-diagnosability as it forces an arbitrary high accuracy, the two notions are still very different.

In Section 3, characterisations composed of a probabilistic requirement on a set of paths defined by a *pathL* formula were established, when possible, for the notions of diagnosability. The notions which could not be characterised where the approximate notions of diagnosability (this is due to the sort of characterisation we were looking for) and FA-diagnosability. The latter is quite surprising as the definition of FA-diagnosability seems to be in between the ones of FF- and IA-diagnosability. Using model-checking techniques, one could derive an algorithm to decide a notion characterised by a logical formula. The absence of characterisation for approximate diagnosability and FA-diagnosability does not however mean that there is no algorithm for these problems. Indeed, we show in Chapter 4 that for finite pLTS, one can give a more specific characterisation of the exact diagnosability notions, including the FA-diagnosability. These characterisations have the same descriptive complexity and are used to obtain an algorithm. In Chapter 5, we study diagnosability for infinite-state systems and base our approach on the characterisations proved in the current section.
# Chapter 4

## Algorithmic analysis of the diagnosability of finite pLTS

In Chapter 3, we studied the notions of diagnosability in a general setting. More precisely, we showed that a diagnoser could be associated with each notion of diagnosability, we established the links between the different diagnosability definitions and gave a logical characterisation of multiple versions of exact diagnosability. With additional assumptions, stronger results can be established: characterisations can be refined and efficient algorithms can be designed. One of the usual restriction is the finiteness of systems. Many real systems can be represented with finitely many states (a vending machine, a Pac-Man game, ...). In fact, most of the systems which interaction with the environment only requires to keep in memory a finite number of events would fit in such a framework. For example, let us consider a server that receives and processes requests. If the server uses a finite memory, then after memorising a fixed number of yet unprocessed requests, the next request might be discarded without being processed due to a stack overflow. Such servers can be represented with finitely many states. Servers able to memorise an unbounded number of requests is dealt with in Chapter 5. When considering finite systems, we immediately get some results as consequences of the ones of Chapter 3. For example, any finite system being finitely branching, according to Theorem 3.1, page 73, IF-diagnosability and FF-diagnosability, two diagnosability notions focused only on faulty runs, are equivalent. As another example, every logical characterisation given in Section 3 of Chapter 3 applies.

The first step is to establish what additional results can be obtained for diagnosability when we only study systems with finitely many states. These systems can easily be represented and have important properties that do not hold in the general case. For example, there is a finite number of probability values in the system since there is a finite number of transitions. This is not true in the general case as can be seen in the example of Figure 3.11, page 72. Using these additional properties, we establish new characterisations of the diagnosability notions in Section 1. These characterisations are not given as probabilistic logical formulae but as conditions on the structure or on the probabilities of the language observed in the system. More precisely, the characterisa-
tions of the exact diagnosability notions are purely structural (i.e the probability values do not matter): they rely on a variant of the determinisation of the system. For the approximate diagnosability notions, the probabilities matter, and cannot be removed from the characterisation. The given characterisation relies on the comparisons of the probability of sets of observed sequences that can be observed from pairs of states.

Once the characterisations are established, we apply them to get as many algorithmic and complexity results as possible. One such application, is to provide an algorithm to decide the diagnosability of a system. Indeed, given a “simple” characterisation, one can easily check if it holds on a given system. Checking a characterisation can be done with many different algorithms, some being more efficient than others. The efficiency of an algorithm is described by the complexity class the problem belongs to, in computational complexity theory. When possible we provide algorithms that are optimal with respect to the standard computational classes. For the other diagnosability problems, we establish that the associated decision problem is undecidable. This is done in Section 2.

When a system is diagnosable, there exists a diagnoser for this system. The possible diagnosers use different amount of memory, give their verdict more or less quickly, etc. In Section 3, we show how to automatically construct a diagnoser for systems that are exactly diagnosable. The diagnosers we build have optimal memory and give their verdict as soon as possible. The constructions of the exact diagnosers are based on the characterisations given in Section 1. This strengthens the importance of these characterisations.

This chapter develops and extends some of the results from [BHL14, BHL16a].

# 1 Characterisations of diagnosability

In this section, we establish characterisations for the different notions of exact diagnosability and for one notion of approximate diagnosability. These characterisations strongly rely on the restriction to finite state systems. Therefore they are easier to express and check, but in general cannot be adapted to more general cases as will be seen in Chapter 5. As a direct consequence of the finite-state restriction and of Theorem 3.1, page 73, FF-diagnosability and IF-diagnosability coincide. So we only consider FF-diagnosability in the rest of this chapter.

For all the exact diagnosability notions, the methodology is similar. We first construct an *ad hoc* deterministic automaton which gathers all the information needed for the diagnosis, by tracking possible correct and faulty executions. Secondly, we build the product of the original pLTS with this deterministic automaton<fnref n="1" />. Diagnosability can then be characterised on the product by graph-based properties.

For approximate diagnosability, we show that the diagnosability notions can be characterised relying on the distance 1 problem for labelled Markov chains (LMC). This problem, recalled in Chapter 2, receives as input two LMC and asks for the existence

<footnote n="1">¹Using such a product to enrich the initial model was mentioned as an usual technique page 29. There, the deterministic automaton was called belief automaton.</footnote>
of an event, that is almost sure in one LMC, and has null measure in the other. It was shown to be decidable in PTIME [CK14].

## 1.1 Exact diagnosis

The deterministic automata we build are variants of the deterministic Büchi automaton introduced in [HHMS13], that accepts the infinite unambiguous observed sequences. The latter tracks the subsets of possible states reached by signalling runs associated with an observed sequence. It looks like the on-the-fly determinisation of $\mathcal{A}$ viewing unobserved events as silent transitions. However, in view of the forthcoming characterisations, the subsets of correct and faulty states are divided in three sets: $U$, $V$ and $W$. The intuitive meaning of these sets is the following one:

* A state $q$ belongs to $U$, if there is a correct signalling run with the current observed sequence ending in $q$;

* A state $q$ belongs to $V \cup W$ if there is a faulty signalling run with the current observed sequence ending in $q$.

* The partition between $V$ and $W$ ensures that for all $q \in V$, $q' \in W$ and $\rho$ a faulty run ending in $q$, there exists a faulty run $\rho'$ ending in $q'$ with an earlier fault than the fault of $\rho$. In other words, $V$ and $W$ contain the states reached by faulty runs, while $W$ keeps track of the runs that have been faulty for the longest time.

$W$ corresponds to the set of faulty states for which the ambiguity with the correct states of $U$ has to be resolved (when both are not empty), while $V$ corresponds to a waiting room of states reached by faulty runs that will be examined when the current ambiguity is resolved.

Before giving the definition of the deterministic automaton associated with a pLTS and for sake of readability, we define for two sets of states $U$ and $V$ and an observation $a \in \Sigma_o$ the set of states

$$ \text{updatefaulty}(U, V, a) = \{q \mid \exists q' \in U, q' \Rightarrow_f^a q\} \\ \cup \{q \mid \exists q' \in V, q' \Rightarrow^a q\}. $$

This set contains the states reached from $U$ by a faulty signalling run of observation $a$ and the ones reached from $V$ by a signalling run of observation $a$.

**Definition 4.1.** Given a pLTS $\mathcal{A}$, the deterministic automaton associated with $\mathcal{A}$ is $\text{Obs}(\mathcal{A}) = \{S, s_0, \Delta, F\}$ where

* $s_0 = (\{q_0\}, \emptyset, \emptyset)$ is the initial state of $\text{Obs}(\mathcal{A})$;

* the states and transitions of the deterministic Büchi automaton $\text{Obs}(\mathcal{A})$ are inductively defined by:

Given $(U, V, W)$ a state of $\text{Obs}(\mathcal{A})$ and $a \in \Sigma_o$, there exists a state $(U', V', W') \in S$ and a transition $(U, V, W) \stackrel{a}{\rightarrow} (U', V', W')$ in $\Delta$ as soon as:
1. $\{q \in U \cup V \cup W \mid q \Rightarrow^a \emptyset\} \neq \emptyset$,

2. $U' = \{q \mid \exists q' \in U, q' \Rightarrow_c^a q\}$,

3. If $W = \emptyset$ then $V' = \emptyset$ and $W' = \text{updatefaulty}(U, V, a)$,

4. If $W \neq \emptyset$ then $W' = \text{updatefaulty}(\emptyset, W, a)$ and $V' = \text{updatefaulty}(U, V, a) \setminus W'$;

• the set $F$ of accepting states consists of all triples $(U, V, W)$ with $U = \emptyset$ or $W = \emptyset$.

When $U = \emptyset$, the current signalling run is surely faulty, since $U$ tracks the possible states after a correct run. When $W = \emptyset$ the current signalling run may be ambiguous (if $V \neq \emptyset$) but the “oldest” possible faulty runs under scrutiny have been discarded. Hence, any infinite observed sequence of $\mathcal{A}$ passing infinitely often through $F$ is not ambiguous (either it is surely faulty, or ambiguities are resolved one after another).

**Example 4.1.** Let $\mathcal{A}$ be the pLTS of Figure 4.1. We represent the associated deterministic automaton $\text{Obs}(\mathcal{A})$ in Figure 4.2, where accepting states for the Büchi condition are doubly framed.

<figure><img src="image_48.png" /><figcaption>Figure 4.1: An IA and FF-diagnosable pLTS which is not FA-diagnosable.</figcaption></figure>

Let us consider the observed sequence $a^\omega$ which has probability $1/2$ in the pLTS. The initial state of $\text{Obs}(\mathcal{A})$ is $(\{q_0\}, \emptyset, \emptyset)$ meaning that the initial state of the pLTS is $q_0$ and no fault occurred so far. Then, observing ‘a’ we reach $(\{q_1, q_2\}, \emptyset, \{f_2\})$ meaning that from $q_0$, we can reach $q_1$ and $q_2$ with correct signalling run of observation ‘a’ and $f_2$ with a faulty signalling run of observation ‘a’. As this faulty run is the oldest one, it is added to $W$. The second observed ‘a’ leads to the state $(\{q_1, q_2\}, \{f_2\}, \emptyset)$. The run that ended in $f_2$ previously cannot be extended by observing an ‘a’, thus the set $W$ which tracked this run (as the only oldest faulty run) is empty. However a new fault can be created ending in state $f_2$, this fault being made while $W$ was tracking other faults, it is not considered “old” and thus is added to $V$. This state is therefore an accepting state. Observing yet another ‘a’ leads back to $(\{q_1, q_2\}, \emptyset, \{f_2\})$. The run tracked by $V$ disappeared, a new fault was created and as $W$ was empty it is considered a “old” fault and $f_2$ is put in $W$. As the path of $\text{Obs}(\mathcal{A})$ corresponding to the observed sequence $a^\omega$ alternates between these two states infinitely often, it visits infinitely often a state where $W = \emptyset$, thus $a^\omega$ is accepted.

For the other observed sequences, a ‘b’ can only be observed in a faulty state, therefore any observed sequence containing a ‘b’ is surely faulty. This can be seen in $\text{Obs}(\mathcal{A})$ as any path containing a ‘b’ ends in one of the five rightmost states, all of which have an empty set $U$ (the first component corresponding to the correct reachable states). As
<figure><img src="image_49.png" /><figcaption>Figure 4.2: The deterministic automaton associated with the pLTS of Figure 4.1. The states that are framed twice are accepting for the Büchi condition.</figcaption></figure>

any state with $U = \emptyset$ is accepting, every infinite observed sequence containing a 'b' is accepted.

The next proposition recalls the main property of this automaton.

**Proposition 4.1 ([HHMS13])**. Let $\mathcal{A}$ be a finite pLTS. Then the deterministic Büchi automaton $\text{Obs}(\mathcal{A})$ accepts exactly the infinite unambiguous observed sequences of $\mathcal{A}$.

**Example 4.2.** As seen in Example 4.1, every observed sequence of the pLTS of Figure 4.1 is accepted by the associated deterministic automaton. According to Proposition 4.1, this means that there is no infinite ambiguous sequence in this pLTS, thus it is FF- and FA-diagnosable.

### 1.1.1 FF-diagnosability

As explained earlier, for each diagnosability notion, we consider a variant of $\text{Obs}(\mathcal{A})$. For FF-diagnosability, we only need to remove the ambiguity for faulty runs. So we can omit the faulty sets of states $V$ and $W$. We write $\text{FF}(\mathcal{A})$ for the resulting simplified automaton, called FF-automaton, obtained from $\text{Obs}(\mathcal{A})$ by only considering the $U$-component of states.

**Example 4.3.** Figure 4.3 illustrates this construction on the pLTS of Figure 4.1. This automaton reflects that once b happens, the current signalling run is surely faulty. Thus the set of possible correct states is empty (state $s_2$).

To recover the stochastic behaviour of $\mathcal{A}$ which is not reflected in $\text{FF}(\mathcal{A})$, we now define the pLTS $\mathcal{A}_{\text{FF}} = \mathcal{A} \times \text{FF}(\mathcal{A})$ as the product of $\mathcal{A}$ and $\text{FF}(\mathcal{A})$ synchronised over observed events.

**Definition 4.2.** Given a pLTS $\mathcal{A} = (Q, q_0, \Sigma, T)$ associated with the FF-automaton $\text{FF}(\mathcal{A}) = \{S, s_0, \Delta, F\}$, we define $\mathcal{A}_{\text{FF}} = (Q', (q_0, \{q_0\}), \Sigma, T')$ where:
<figure><img src="image_50.png" /><figcaption>Figure 4.3: The FF-automaton of pLTS of Figure 4.1.</figcaption></figure>

* $Q' = Q \times S$;

* $((q, B), a, (q', B)) \in T' \text{ iff } (q, a, q') \in T$ and

- either $a \in \Sigma_u$ and $B = B'$,

- or $a \in \Sigma_o$ and there exists a transition $B \xrightarrow{a} B'$ in $\Delta$.

Since FF($\mathcal{A}$) is deterministic and complete, $\mathcal{A}_{FF}$ is still a pLTS, with the same stochastic behaviour as $\mathcal{A}$. More precisely, there is a bijection between the runs of $\mathcal{A}$ and the runs of FF($\mathcal{A}$). A run and its image by the bijection have the same observation and the same probability. In addition, the $U$-component of a state $(q, U)$ of $\mathcal{A}_{FF}$ stores the relevant information w.r.t FF-diagnosability of the observed sequence so far.

**Example 4.4.** *Carrying on with the example pLTS of Figure 4.1, Figure 4.4 shows the resulting product pLTS. Observe that it has two bottom strongly connected components (BSCC), consisting of the absorbing states $(q_1, s_1)$ and $(f_2, s_2)$.*

<figure><img src="image_51.png" /><figcaption>Figure 4.4: The synchronised product of the pLTS of Figure 4.1 and its FF-automaton.</figcaption></figure>

In a finite pLTS almost all runs end in a BSCC [BK08], and FF-diagnosability is a property of runs expressed as an almost sure event. So, the characterisation of FF-diagnosability can be stated on the BSCC of $\mathcal{A}_{FF}$.

**Proposition 4.2.** Let $\mathcal{A}$ be a finite pLTS. Then $\mathcal{A}$ is FF-diagnosable if and only if $\mathcal{A}_{FF}$ has no BSCC containing a state $(q, U)$ with $q \in Q_f$ and $U \neq \emptyset$.
The proof relies on two elements. First, a run will almost surely reach a BSCC of the pLTS. Second, for a faulty run to be ambiguous, the set $U$ contained in the state in which the run ends must not be empty. Therefore if every BSCC corresponds to either correct runs (i.e. $q \in Q_c$) or faulty unambiguous runs (i.e. $U = \emptyset$), the pLTS is FF-diagnosable.

*Proof.* Suppose first that there exists a reachable BSCC $C$ of $\mathcal{A}_{\text{FF}}$ and a state $s = (q, U)$ in $C$ such that $q \in Q_f$ and $U \neq \emptyset$. Let $\rho$ be a signalling run leading from the initial state $s_0$ of $\mathcal{A}_{\text{FF}}$ to $s$. Now, for every state $s' = (q', U') \in C$, necessarily $q' \in Q_f$ and $U' \neq \emptyset$, because $C$ is strongly connected$^2$. So for every signalling run $\rho'$ that extends $\rho$, writing $s' = (q', U')$ for the state $\rho'$ leads to, there exists a correct signalling run $\rho''$ such that $\mathcal{P}(\rho'') = \mathcal{P}(\rho')$ and $q_0 \xrightarrow{\rho''} q''$ with $q'' \in U'$. As a consequence the observed sequence $\mathcal{P}(\rho'')$ is ambiguous in $\mathcal{A}_{\text{FF}}$, and for every $n \ge |\rho|_o$, $\mathbb{P}(\text{FAmb}_n) \ge \mathbb{P}(\rho)$. As $\mathcal{A}$ and $\mathcal{A}_{\text{FF}}$ have the same ambiguous observed sequences and the associated runs have the same probabilities, $\mathcal{A}$ is not FF-diagnosable.

Suppose now that for every state $s = (q, U)$ of a BSCC $C$, either $q \in Q_c$, or $U = \emptyset$. This property is in fact uniform by BSCC: for every BSCC $C$, either for every state $(q, U) \in C$, $q \in Q_c$, or, for every state $(q, U) \in C$, $U = \emptyset$. This is a straightforward consequence of $C$ being strongly connected. Moreover, if a run $\rho$ reaches a pair $(q, U)$ then $q \in Q_c$ implies $U \neq \emptyset$. Indeed, let $\rho'$ be the greatest signalling run prefix of $\rho$. $\rho'$ ends in a pair $(q', U')$ where $U' = U$ as $\mathcal{P}(\rho) = \mathcal{P}(\rho')$. Moreover if $q \in Q_c$, then $q' \in Q_c$, therefore $q' \in U$ implying that $U \neq \emptyset$. Therefore in $\mathcal{A}_{\text{FF}}$ the BSCC are partitioned in correct ones, in case all $q$-components of states in $C$ are correct, and faulty ones, in case all $U$-components of states in $C$ are empty ensuring unambiguity of faulty runs ending in a BSCC. Since runs almost surely leave the transient states and reach a BSCC, this implies that $\lim_{n \to \infty} \mathbb{P}(\text{FAmb}_n) = 0$. $\square$

As a consequence of this characterisation, we establish the equivalence between FF- and uniform FF-diagnosability for finite pLTS, claimed in Theorem 3.1.

**Proposition 4.3.** Let $\mathcal{A}$ be a finite pLTS. If $\mathcal{A}$ is FF-diagnosable, then it is uniformly FF-diagnosable.

In a finite FF-diagnosable pLTS, thanks to the characterisation given in Proposition 4.2, we know that faults can be detected at worst when the run reaches a BSCC. The proof consists in showing and using that the speed at which a BSCC is reached is uniform from any state.

*Proof.* Let $\mathcal{A}$ be an FF-diagnosable pLTS. Given a run $\rho$ of $\mathcal{A}$, let $\rho_{\text{FF}}$ be the corresponding run in $\mathcal{A}_{\text{FF}}$: the states in $\rho_{\text{FF}}$ extend the states appearing along $\rho$ by subsets of possible correct states after the corresponding prefix of the observed sequence $\mathcal{P}(\rho)$. Let $S_{\text{BSCC}}$ denotes the set of states of $\mathcal{A}_{\text{FF}}$ that belong to a BSCC. Last, for every state $(q, U)$ of $\mathcal{A}_{\text{FF}}$ and every $n \in \mathbb{N}$, denote by $\text{SR}_n^{q,U}$ the set of signalling runs in $\mathcal{A}_{\text{FF}}$ of length $n$ starting at $(q, U)$.

<footnote>$^2$Recall that the set $Q_f$ is absorbing</footnote>
Let $\alpha > 0$. Our objective is to get $n_\alpha$ such that for every $n \ge n_\alpha$ and every minimal faulty run $\rho \in \min \mathcal{F}$:

$$ \mathbb{P}_{\mathcal{A}}(\{\rho' \in \mathrm{SR}_{n+|\rho|_o} \mid \rho \preceq \rho' \wedge \mathrm{CorP}(\mathcal{P}(\rho)) > 0\}) \le \alpha \cdot \mathbb{P}(\rho). $$

We first exploit the almost sure convergence towards BSCC in $\mathcal{A}_{FF}$. For every state $(q, U)$ of $\mathcal{A}_{FF}$, the measure of runs starting in $(q, U)$ and avoiding all BSCC during $n$ steps tends to 0, when $n$ goes to infinity. Thus, given $\alpha$, for every reachable $(q, U)$, there exists $n_{q,U} \in \mathbb{N}$ such that for every $n \ge n_{q,U}$,

$$ \mathbb{P}_{\mathcal{A}_{FF}}(\{\rho'_{FF} \in \mathrm{SR}_{n}^{q,U} \mid \mathrm{last}(\rho'_{FF}) \notin S_{\mathrm{BSCC}}\}) \le \alpha. $$

We define $n_\alpha$ as the maximum of $n_{q,U}$ over all states $(q, U)$.

Now let $\rho$ be a minimal faulty run of $\mathcal{A}$, and define $(q, U) = \mathrm{last}(\rho_{FF})$. Since $n_\alpha \ge n_{q,U}$, $\mathbb{P}_{\mathcal{A}_{FF}}(\{\rho'_{FF} \in \mathrm{SR}_{n_\alpha}^{q,U} \mid \mathrm{last}(\rho'_{FF}) \notin S_{\mathrm{BSCC}}\}) \le \alpha$. Therefore, as $\mathcal{A}$ and $\mathcal{A}_{FF}$ have the same probabilistic behaviour,

$$ \mathbb{P}_{\mathcal{A}}(\{\rho' \in \mathrm{SR}_{n_\alpha+|\rho|_o} \mid \rho \preceq \rho' \wedge \mathrm{last}(\rho'_{FF}) \notin S_{\mathrm{BSCC}}\}) \le \alpha \cdot \mathbb{P}(\rho). $$

Thanks to the characterisation of Proposition 4.2, all states in BSCC reachable from $(q, U)$ in $\mathcal{A}_{FF}$ necessarily are of the form $(q', \emptyset)$. Therefore, if a finite run $\rho'_{FF}$ reaches such a BSCC, $\rho'_{FF}$ admits no correct run with same observed sequence, and hence $\mathrm{CorP}(\mathcal{P}(\rho'_{FF})) = 0$. Equivalently, $\mathrm{CorP}(\mathcal{P}(\rho')) > 0$ implies $\mathrm{last}(\rho'_{FF}) \notin S_{\mathrm{BSCC}}$. Thus

$$ \mathbb{P}_{\mathcal{A}}(\{\rho' \in \mathrm{SR}_{n_\alpha+|\rho|_o} \mid \rho \preceq \rho' \wedge \mathrm{CorP}(\mathcal{P}(\rho')) > 0\}) \le \alpha \cdot \mathbb{P}(\rho) $$

which shows that $\mathcal{A}$ is uniformly FF-diagnosable. $\square$

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

### 1.1.2 FA-diagnosability

<figure><img src="image_53.png" /><figcaption>Figure 4.5: The FA-automaton of the pLTS of Figure 4.1.</figcaption></figure>

For FA-diagnosability, we again start from $\mathrm{Obs}(\mathcal{A})$. Here, we need information about the ambiguity of both faulty and correct runs. Yet, we still do not need to keep all the information given by $\mathrm{Obs}(\mathcal{A})$. Indeed, we can gather the $V$ and $W$ components into a unique set, that we again call $V$. In other words we keep the information on which faulty states could be reached, but not the distinction between “old” and “new” faulty runs. The resulting simplified automaton is denoted by $\mathrm{FA}(\mathcal{A})$.
**Example 4.5.** Figure 4.5 illustrates this construction on the pLTS of Figure 4.1. As expected, the FA-automaton is a refinement of the FF-automaton: the U-component of a state in $\mathcal{F}\mathcal{A}$ corresponds to a state in $\mathcal{FF}(\mathcal{A})$. For instance, state $s_2$ of Figure 4.3 is split here into $s_2$, $s_3$ and $s_4$.

As we did for the FF case, we now define the pLTS $\mathcal{A}_{\text{FA}} = \mathcal{A} \times \mathcal{F}\mathcal{A}(\mathcal{A})$ as the product of $\mathcal{A}$ and $\mathcal{F}\mathcal{A}(\mathcal{A})$ synchronised over observed events (the definition has the same structure as the one of Definition 4.2, only using $\mathcal{F}\mathcal{A}(\mathcal{A})$ instead of $\mathcal{FF}(\mathcal{A})$). $\mathcal{A}_{\text{FA}}$ is still a pLTS with same stochastic behaviour as $\mathcal{A}$ augmented with the relevant information of the observed sequence w.r.t FA-diagnosability.

**Example 4.6.** Figure 4.6 continues Example 4.5 and shows the synchronised product for the pLTS of Figure 4.1.

<figure><img src="image_54.png" /><figcaption>Figure 4.6: The synchronised product of pLTS of Figure 4.1 and its FA-automaton.</figcaption></figure>

Again, FA-diagnosability is characterised through the BSCC of $\mathcal{A}_{\text{FA}}$.

**Proposition 4.4.** Let $\mathcal{A}$ be a finite pLTS. $\mathcal{A}$ is FA-diagnosable if and only if $\mathcal{A}_{\text{FA}}$ has no BSCC that:

* either contains a state $(q, U, V)$ with $q \in Q_f$ and $U \neq \emptyset$;

* or contains a state $(q, U, V)$ with $q \in Q_c$ and $V \neq \emptyset$.

Note that the characterisation of FA-diagnosability is symmetric for correct states and $V$-component (resp. faulty states and $U$-component). This reflects the symmetry of the definition of FA-diagnosability.

The main difference between this proof and the one of Proposition 4.2 is that the second item is not uniform inside a BSCC: there may exists a BSCC containing two states $(q_1, U_1, V_1)$ and $(q_2, U_2, V_2)$ with $q_1, q_2 \in Q_c$, $V_1 = \emptyset$ and $V_2 \neq \emptyset$. As a consequence it is harder to show that if a BSCC verifies the second item, then the pLTS is not FA-diagnosable. Instead of having every extension of the run to be correct ambiguous, the extensions only are ambiguous when they visit some particular states. However,
the probability that a run ends in such a state converges towards the steady state distribution of this state which is positive as the state belongs to a BSCC, contradicting the FA-diagnosability.

*Proof.* To prove the left-to-right implication, we proceed by contraposition. If one assumes the first item holds, the same argument as in the proof of Proposition 4.2 applies. Precisely, suppose that there exists a reachable BSCC $C$ of $\mathcal{A}_{\text{FA}}$ and a state $s = (q, U, V)$ in $C$ such that $q \in Q_f$ and $U \neq \emptyset$. Let $\rho$ be a signalling run leading from the initial state $s_0$ of $\mathcal{A}_{\text{FA}}$ to $s$. Now, for every state $s' = (q', U', V') \in C$, necessarily $q' \in Q_f$ and $U' \neq \emptyset$, because $C$ is strongly connected. So for every signalling run $\rho'$ that extends $\rho$, writing $s' = (q', U', V')$ for the state $\rho'$ leads to, there exists a correct signalling run $\rho''$ such that $\mathcal{P}(\rho'') = \mathcal{P}(\rho')$ and $q_0 \xrightarrow{\rho''} q''$ with $q'' \in U'$. As a consequence the observed sequence $\mathcal{P}(\rho'')$ is ambiguous, and for every $n \ge |\rho|_o$, $\mathbb{P}(\text{FAmb}_n) \ge \mathbb{P}(\rho)$, so that $\mathcal{A}$ is not FA-diagnosable.

Suppose now that there exists a reachable BSCC $C$ of $\mathcal{A}_{\text{FA}}$ and a state $s = (q, U, V)$ in $C$ such that $q \in Q_c$ and $V \neq \emptyset$. Since the pair $(U, V)$ is unchanged by unobservable transitions, w.l.o.g we assume that $s$ is the successor of some state of $C$ by an observable event and we denote $C'$ the set of such states. Observe that a signalling run that reaches $s$ is ambiguous. Denote $\pi_i(s')$ the probability that a random run of length $i$ ends in a state $s'$. In a finite DTMC, for every state $s'$ of a reachable BSCC the Cesaro-limit $\pi_{\infty}(s') = \lim_{n \to \infty} 1/(n+1) \sum_{i=0}^{n} \pi_i(s')$ exists and is greater than 0. For $s' \in C'$ denote by $p_{s',s}$ the probability of an observable transition from $s'$ to $s$. Then

$$0 < \sum_{s' \in C'} \pi_{\infty}(s') p_{s',s} \le \liminf_{n \to \infty} \frac{1}{n+1} \sum_{i=0}^{n} \alpha_i(s)$$

where $\alpha_i(s)$ is the probability that a random signalling run of length $i$ ends in $s$. $\alpha_i$ differs from $\pi_i$ by only considering signalling runs. From time 0 to time $n$, a run can be a signalling run at most $n+1$ times. Thus:

$$\frac{1}{n+1} \sum_{i=0}^{n} \alpha_i(s) \le \frac{1}{n+1} \sum_{i=0}^{n} \mathbb{P}(\text{CAmb}_i)$$

which implies that

$$0 < \liminf_{n \to \infty} \frac{1}{n+1} \sum_{i=0}^{n} \mathbb{P}(\text{CAmb}_i) \le \limsup_{n \to \infty} \mathbb{P}(\text{CAmb}_n).$$

In this case also, we conclude that $\mathcal{A}$ is not FA-diagnosable.

The proof of Proposition 4.2 has established that a signalling run reaching a BSCC $C$ where for every state $s = (q, U, V)$, $q$ is faulty and $U = \emptyset$, is surely faulty. Similarly a signalling run that reaches a BSCC where for every state $s = (q, U, V)$, $q$ is correct and $V = \emptyset$, is surely correct. Thus an ambiguous signalling run must only visit transient
states. Since runs almost surely leave the transient states and reach a BSCC, this implies that:

$$ \limsup_{n \to \infty} \mathbb{P}(\mathbf{FA}_{\mathbf{mb}_n}) + \mathbb{P}(\mathbf{CA}_{\mathbf{mb}_n}) = 0, $$

and therefore, the pLTS is FA-diagnosable. □

Let us emphasise that although there does not exist a simple logical characterisation of FA-diagnosability, in finite pLTS, it enjoys a characterisation that is similar to the one of FF-diagnosability.

### 1.1.3 IA-diagnosability

IA-diagnosability is the notion of exact diagnosability for which we need to use Obs($\mathcal{A}$) with no simplification. However, to stick to the presentation for the other diagnosability notions, we write here IA($\mathcal{A}$) for Obs($\mathcal{A}$). As before, to come up with a characterisation, one builds $\mathcal{A}_{IA} = \mathcal{A} \times IA(\mathcal{A})$, the product of $\mathcal{A}$ and IA($\mathcal{A}$) synchronised over observed events.

**Example 4.7.** Figure 4.7 shows the synchronised product corresponding to the pLTS depicted in Figure 4.1. Among the BSCC, all the faulty ones (i.e. the ones reached after a faulty event) have $U = \emptyset$, while $\{(q_1, s_1), (q_1, s'_1)\}$, the single one that is reached by a correct run, has a state $(q_1, s'_1)$ with $W = \emptyset$.

<figure><img src="image_55.png" /><figcaption>Figure 4.7: The synchronised product of the pLTS of Figure 4.1 and its IA-automaton.</figcaption></figure>
We now establish a characterisation of IA-diagnosability on $\mathcal{A}_{IA}$.

**Proposition 4.5.** Let $\mathcal{A}$ be a finite pLTS. $\mathcal{A}$ is IA-diagnosable if and only if $\mathcal{A}_{IA}$ has no BSCC such that:

* either, all its states $(q, U, V, W)$ fulfil $q \in Q_f$ and $U \neq \emptyset$;

* or all its states $(q, U, V, W)$ fulfil $q \in Q_c$ and $W \neq \emptyset$.

*Proof.* This proof relies on Proposition 4.1. An infinite run is not ambiguous if its observation satisfy the Büchi condition of $\text{Obs}(\mathcal{A})$, therefore $\mathcal{A}_{IA}$ will be IA-diagnosable if the pLTS almost surely satisfies the Büchi condition. As a run almost surely reaches a BSCC, every BSCC must contain a state that allows the diagnosis.

Assume first that $\mathcal{A}_{IA}$ has a BSCC with (at least) some state $(q, U, V, W)$ with $q \in Q_f$ and $U \neq \emptyset$. Using Proposition 4.2, $\mathcal{A}$ is not FF-diagnosable and thus not IA-diagnosable either, due to Theorem 3.1. Assume now some BSCC $C$ of $\mathcal{A}_{IA}$ has all its states $(q, U, V, W)$ with $q \in Q_c$ and $W \neq \emptyset$. In particular none of these states are accepting for the deterministic Büchi automaton $\text{IA}(\mathcal{A})$. Let $\rho$ be a finite signalling run that hits $C$. By Proposition 4.1, any infinite run $\rho'$ that extends $\rho$ is ambiguous. From $q \in Q_c$ we deduce that $\mathbb{P}(\text{CAMb}_{\infty}) \ge \mathbb{P}(\rho) > 0$. Therefore $\mathcal{A}$ is not IA-diagnosable.

Assume now $\mathcal{A}_{IA}$ has no BSCC such that either, all its states $(q, U, V, W)$ fulfil $q \in Q_f$ and $U \neq \emptyset$, or all its states $(q, U, V, W)$ fulfil $q \in Q_c$ and $W \neq \emptyset$. First observe that in case some BSCC of $\mathcal{A}_{IA}$ contains some state $(q, U, V, W)$ with $q \in Q_f$ and $U \neq \emptyset$, then all its states satisfy the same constraints. Moreover, if some state $(q, U, V, W)$ of a BSCC has $q \in Q_c$, then all states of this BSCC have their first component in $Q_c$. Therefore, the condition can be reformulated as follows: all BSCC $C$ of $\mathcal{A}_{IA}$ satisfy:

* either all states $(q, U, V, W)$ of $C$ fulfil $q \in Q_f$ and $U = \emptyset$;

* or all states $(q, U, V, W)$ of $C$ fulfil $q \in Q_c$ and some state $(q, U, V, W)$ of $C$ fulfils $W = \emptyset$.

Whatever the case, all BSCC contain (at least) an accepting state for the Büchi condition of $\text{IA}(\mathcal{A})$. Since all runs almost surely end in a BSCC and visit each of its states infinitely often, using Proposition 4.1, almost all runs of $\mathcal{A}_{IA}$ are unambiguous. This proves that $\mathcal{A}$ is IA-diagnosable. $\square$

Surprisingly, while in general FA-diagnosability could not be characterised by a logical formula contrary to IA-diagnosability, restricted to finite systems, the characterisation of IA-diagnosability is the more involved one.

## 1.2 Approximate diagnosis

We now turn to the characterisation of approximate diagnosis and particularly of AFF-diagnosability. The reason why we only consider AFF-diagnosability here will become clear in Subsection 2.2.1 where we show that all other approximate diagnosability notions are undecidable. Our characterisation of AFF-diagnosability relies on the notion of
distance between two Markov chains with labels on the transitions. A labelled Markov chain (LMC) is a pLTS where every event is observable: $\Sigma = \Sigma_o$. In order to exploit results of [CK14] on LMC in our context of pLTS, we introduce the mapping $\mathcal{M}$ that computes in polynomial time the probabilistic closure of a pLTS w.r.t. unobservable events and produces an LMC. Informally, the probabilities of all paths of $\mathcal{A}$ from state $q$ to state $q'$ with same observed sequence $a \in \Sigma_o$ are gathered to obtain the probability in $\mathcal{M}(\mathcal{A})$ to move from $q$ to $q'$ with label $a$. The transformation is formally defined below. For sake of simplicity, we denote by $\mathcal{A}_q$, the pLTS $\mathcal{A}$ where the initial state has been substituted by $q$.

**Definition 4.3.** Given a pLTS $\mathcal{A} = (Q, q_0, \Sigma, T, \mathbf{P})$ with $\Sigma = \Sigma_o \uplus \Sigma_u$, the labelled Markov chain $\mathcal{M}(\mathcal{A}) = (\dot{Q}, \dot{q}_0, \dot{\Sigma}, \dot{T}', \dot{\mathbf{P}}')$ is defined by:

* $T' = \{(q, a, q') \mid \exists \rho = q \cdots a q' \in \text{SR}_1(\mathcal{A}_q)\}$ (and so $a \in \Sigma_o$).

* for every $(q, a, q') \in T'$, $\mathbf{P}'(q, a, q') = \mathbb{P}(\{\rho \in \text{SR}_1(\mathcal{A}_q) \mid \rho = q \cdots a q'\})$.

**Example 4.8.** The LMC associated with the pLTS of Figure 4.1 is represented in Figure 4.8. The transition from $q_0$ to $q_1$ which was unobservable has been replaced by a transition labelled by 'a'. The new transition has probability 1/2 which is the product of the probability of the replaced unobservable transition (of value 1/2) and of the transition labelled by 'a' that followed (of value 1). A transition from $q_0$ to $f_2$ appeared, it replaces the run $q_0 u q_2 \mathbf{f} f_1 a f_2$ which has probability 1/8.

<figure><img src="image_56.png" /><figcaption>Figure 4.8: The LMC obtained from the pLTS of Figure 4.1.</figcaption></figure>

Let $E$ be a prospect<fnref n="3" /> of $\Sigma_o^\omega$ (i.e. a measurable subset of $\Sigma_o^\omega$ for the standard measure), we denote by $\mathbb{P}^{\mathcal{M}}(E)$ the probability that prospect $E$ occurs in the LMC $\mathcal{M}$. Given two LMC $\mathcal{M}_1$ and $\mathcal{M}_2$, the (probabilistic) distance between $\mathcal{M}_1$ and $\mathcal{M}_2$ generalises the concept of distance for distributions. Given a prospect $E$, $|\mathbb{P}^{\mathcal{M}_1}(E) - \mathbb{P}^{\mathcal{M}_2}(E)|$ expresses the absolute difference between the probabilities that $E$ occurs in $\mathcal{M}_1$ and in $\mathcal{M}_2$. The distance between $\mathcal{M}_1$ and $\mathcal{M}_2$ is defined as the supremum over the prospects:

<footnote n="3">³The term used in the literature is event. We differ here as we already use event for the letters labelling the transitions as established in Definition 2.5, page 38</footnote>
**Definition 4.4.** Let $\mathcal{M}_1$ and $\mathcal{M}_2$ be two LMC over the same alphabet $\Sigma_o$. Then $d(\mathcal{M}_1, \mathcal{M}_2)$ the distance between $\mathcal{M}_1$ and $\mathcal{M}_2$ is:

$$d(\mathcal{M}_1, \mathcal{M}_2) = \sup\{|\mathbb{P}^{\mathcal{M}_1}(E) - \mathbb{P}^{\mathcal{M}_2}(E)| \mid E \text{ prospect of } \Sigma_o^\omega\}.$$

**Example 4.9.** Consider the LMC of Figure 4.8, called $\mathcal{M}_1$, and the one of Figure 4.9, called $\mathcal{M}_2$. The prospect $E = \{a^\omega\}$ has probability $1/2$ in $\mathcal{M}_1$ and $0$ in $\mathcal{M}_2$. Thus $d(\mathcal{M}_1, \mathcal{M}_2) \ge 1/2$. Moreover, $\mathcal{M}_2$ can be obtained from $\mathcal{M}_1$ by deleting the state $q_1$ (and the associated transitions) and merging $q_0$ with $q_2$. As a consequence, for any prospect $E$ such that $a^\omega \notin E$, $\mathbb{P}^{\mathcal{M}_2}(E) = 2 \cdot \mathbb{P}^{\mathcal{M}_1}(E)$. We thus have $\mathbb{P}^{\mathcal{M}_1}(\{a^\omega\}) - \mathbb{P}^{\mathcal{M}_2}(\{a^\omega\}) = 1/2$, $\mathbb{P}^{\mathcal{M}_2}(\Sigma_o^\omega \setminus \{a^\omega\}) - \mathbb{P}^{\mathcal{M}_1}(\Sigma_o^\omega \setminus \{a^\omega\}) = 1/2$, and for any other prospect $E$, the difference is smaller or equal to $1/2$. Therefore $d(\mathcal{M}_1, \mathcal{M}_2) = 1/2$.

<figure><img src="image_57.png" /><figcaption>Figure 4.9: An example of LMC.</figcaption></figure>

The distance 1 problem asks, given two LMC $\mathcal{M}_1$ and $\mathcal{M}_2$, whether $d(\mathcal{M}_1, \mathcal{M}_2) = 1$. The next proposition summarises the results of Chen and Kiefer on LMC, that we use later.

**Proposition 4.6** ([CK14]).

* Given two LMC $\mathcal{M}_1, \mathcal{M}_2$, there exists a prospect $E$ such that:

$$d(\mathcal{M}_1, \mathcal{M}_2) = \mathbb{P}^{\mathcal{M}_1}(E) - \mathbb{P}^{\mathcal{M}_2}(E).$$

* The distance 1 problem for LMC is decidable in polynomial time.

The first item of this proposition states that the supremum is reached (and thus is a maximum). In fact, given two LMC $\mathcal{M}_1, \mathcal{M}_2$, the authors show that one prospect reaching the maximum is $E = \{w \in \Sigma_o^\omega \mid \lim_{n \to \infty} \frac{\mathbb{P}^{\mathcal{M}_1}(w \le n)}{\mathbb{P}^{\mathcal{M}_2}(w \le n)} \ge 1\}$.

We now use the notion of distance 1 to characterise AFF-diagnosability. Let us first consider a subclass of pLTS called initial-fault pLTS. Informally, an initial-fault pLTS $\mathcal{A}$ consists of two disjoint pLTS $\mathcal{A}^f$ and $\mathcal{A}^c$ and an initial state $q_0$ with an outgoing unobservable correct transition leading to $\mathcal{A}^c$ and a transition labelled by $f$ leading to $\mathcal{A}^f$ (see Figure 4.10). Moreover no faulty transitions occur in $\mathcal{A}^c$. In other words, if a fault occurs during a run of an initial-fault pLTS, it does so on the very first transition.

**Definition 4.5** (Initial-fault pLTS). A pLTS $\mathcal{A} = (Q, q_0, \Sigma, T, \mathbf{P})$ is an initial fault pLTS if there exist two disjoint pLTS $\mathcal{A}^f = (Q_f, q_f, \Sigma, T_f, \mathbf{P}_f)$ and $\mathcal{A}^c = (Q_c, q_c, \Sigma \setminus \{\mathbf{f}\}, T_c, \mathbf{P}_c)$ such that:
<figure><img src="image_58.png" /><figcaption>Figure 4.10: Schematic representation of an initial-fault pLTS.</figcaption></figure>

• $Q = \{q_0\} \uplus Q_f \uplus Q_c$;

• $T = T_f \uplus T_c \uplus \{(q_0, u, q_c), (q_0, \mathbf{f}, q_f)\}$ with $u \in \Sigma_u$;

• for every $t \in T_f$, we have $\mathbf{P}(t) = \mathbf{P}_f(t)$ and for every $t \in T_c$, we have $\mathbf{P}(t) = \mathbf{P}_c(t)$, and $\mathbf{P}((q_0, u, q_c)) = \mathbf{P}((q_0, \mathbf{f}, q_f)) = 1/2$.

We denote such a pLTS by $\mathcal{A} = \langle q_0, \mathcal{A}^f, \mathcal{A}^c \rangle$.

**Example 4.10.** The pLTS of Figure 4.11 is a simple initial-fault pLTS.

<figure><img src="image_59.png" /><figcaption>Figure 4.11: A uniformly AFF-diagnosable initial-fault pLTS.</figcaption></figure>

Under the initial-fault restriction, we can get a simple characterisation for AFF-diagnosability as established in the next lemma. The idea of this characterisation is then extended to every pLTS.

**Lemma 4.1.** Let $\mathcal{A} = \langle q_0, \mathcal{A}^f, \mathcal{A}^c \rangle$ be an initial-fault pLTS. Then $\mathcal{A}$ is AFF-diagnosable if and only if $d(\mathcal{M}(\mathcal{A}^f), \mathcal{M}(\mathcal{A}^c)) = 1$.

We write $\mathbb{P}$, $\mathbb{P}_f$ and $\mathbb{P}_c$ for the probability measures of pLTS $\mathcal{A}$, $\mathcal{A}^f$ and $\mathcal{A}^c$. By construction of $\mathcal{M}(\mathcal{A}^f)$ and $\mathcal{M}(\mathcal{A}^c)$, for every observed sequence $\sigma$, $\mathbb{P}^{\mathcal{M}(\mathcal{A}^f)}(\sigma) = \mathbb{P}_f(\sigma)$ and similarly $\mathbb{P}^{\mathcal{M}(\mathcal{A}^c)}(\sigma) = \mathbb{P}_c(\sigma)$. In words, the mapping $\mathcal{M}$ leaves unchanged the probability of occurrence of an observed sequence.

AFF-diagnosability is a property of identification (decide whether the run is faulty) of the finite runs that start by a fault with high probability, using the probability $\mathbb{P}$. The distance 1 between $\mathcal{M}(\mathcal{A}^f)$ and $\mathcal{M}(\mathcal{A}^c)$ is also a property of identification (decide which LMC the run that produces the infinite observed sequence belongs to) of infinite observed sequences, using the probabilities $\mathbb{P}_f$ and $\mathbb{P}_c$. As mentioned above, these three probability measures are probabilities of parts of the pLTS $\mathcal{A}$ and are thus related. The proof therefore mostly consists in understanding the links between the two identification
properties: how to translate the set of finite runs identified by AFF-diagnosability into a set of infinite sequences and reciprocally. The intuition to establish the relation is that the prefixes of an infinite faulty run reveals the fault with arbitrarily high accuracy if and only if the associated infinite observed sequence “reveals” that the run belongs to $M(\mathcal{A}^f)$.

*Proof.* Let us prove the equivalence, starting with the left-to-right implication.

* Assume $\mathcal{A}$ is AFF-diagnosable. Then, for every $\varepsilon > 0$ and every minimal faulty run $\rho$:

$$ \lim_{n \to \infty} \mathbb{P}(\{\rho' \in \mathbf{SR}_{n+|\rho|_o} \mid \rho \preceq \rho' \wedge \mathrm{CorP}(\mathcal{P}(\rho')) > \varepsilon\}) = 0. \quad (4.1) $$

Pick some $0 < \varepsilon < 1$. Applying Equation (4.1) on the minimal faulty run $\rho_f = q_0 \mathbf{f} q_f$ with $|\mathcal{P}(\rho_f)| = 0$, there exists some $n \in \mathbb{N}$ such that:

$$ \mathbb{P}(\{\rho \in \mathbf{SR}_n \mid \rho_f \preceq \rho \wedge \mathrm{CorP}(\mathcal{P}(\rho)) > \varepsilon\}) \le \varepsilon. $$

Let $\mathfrak{S}$ be the set of observed sequences of faulty runs with observable length $n$ and correctness proportion not exceeding threshold $\varepsilon$:

$$ \mathfrak{S} = \{\sigma \in \Sigma_o^n \mid \exists \rho \in \mathbf{SR}_n, \mathcal{P}(\rho) = \sigma \wedge \rho_f \preceq \rho \wedge \mathrm{CorP}(\sigma) \le \varepsilon\}. $$

We define $E = \mathrm{Cyl}(\mathfrak{S})$ to be the prospect consisting of the infinite suffixes of these sequences. Let us show that $\mathbb{P}_c(E) \le \varepsilon/(1 - \varepsilon)$ and $\mathbb{P}_f(E) \ge 1 - 2\varepsilon$. We have:

$$ \mathbb{P}_f(E) = 1 - 2 \mathbb{P}(\{\rho \in \mathbf{SR}_n \mid \rho_f \preceq \rho \wedge \mathrm{CorP}(\mathcal{P}(\rho)) > \varepsilon\}) \ge 1 - 2\varepsilon $$

where the factor 2 comes from the probability 1/2 in $\mathcal{A}$ to enter $\mathcal{A}^f$ that $\mathbb{P}_f$ does not take into account contrary to $\mathbb{P}$.

Moreover, for every observed sequence $\sigma \in \mathfrak{S}$, $\mathrm{CorP}(\sigma) \le \varepsilon$. Using the definition of $\mathrm{CorP}$:

$$ \mathrm{CorP}(\sigma) = \frac{\mathbb{P}(\{\rho \in \mathcal{C} \cap \mathbf{SR}_n \mid \mathcal{P}(\rho) = \sigma\})}{\mathbb{P}(\{\rho \in \mathbf{SR}_n \mid \mathcal{P}(\rho) = \sigma\})} = \frac{\mathbb{P}_c(\sigma)}{\mathbb{P}_c(\sigma) + \mathbb{P}_f(\sigma)} \le \varepsilon. $$

Thus, $\mathbb{P}_c(\sigma) \le \frac{\varepsilon}{1-\varepsilon} \mathbb{P}_f(\sigma)$. Hence:

$$ \mathbb{P}_c(E) = \sum_{\sigma \in \mathfrak{S}} \mathbb{P}_c(\sigma) \le \sum_{\sigma \in \mathfrak{S}} \frac{\varepsilon}{1-\varepsilon} \mathbb{P}_f(\sigma) = \frac{\varepsilon}{1-\varepsilon} \mathbb{P}_f(E) \le \frac{\varepsilon}{1-\varepsilon}. $$

Therefore $d(\mathcal{M}(\mathcal{A}^c), \mathcal{M}(\mathcal{A}^f)) \ge \mathbb{P}_f(E) - \mathbb{P}_c(E) \ge 1 - \varepsilon(2 + \frac{1}{1-\varepsilon})$. Since $\varepsilon$ was arbitrary, taking the limit when $\varepsilon$ goes to 0, we obtain the desired result: $d(\mathcal{M}(\mathcal{A}^c), \mathcal{M}(\mathcal{A}^f)) = 1$. Note that we did not exhibit the prospect that reaches the maximum but only a prospect $\varepsilon$-close to it. The proof could be modified to use this maximum prospect, but it makes the proof unnecessarily more complicated.

* Conversely assume that $d(\mathcal{M}(\mathcal{A}^f), \mathcal{M}(\mathcal{A}^c)) = 1$. Thanks to Proposition 4.6, there exists a prospect $E \subseteq \Sigma_o^\omega$ such that $\mathbb{P}_f(E) = 1$ and $\mathbb{P}_c(E) = 0$.

For every $n \in \mathbb{N}$, let $\mathfrak{S}_n$ be the set of prefixes of length $n$ of the observed sequences of $E$: $\mathfrak{S}_n = \{\sigma \in \Sigma_o^n \mid \exists \sigma' \in E, \sigma \preceq \sigma'\}$. For every $\varepsilon > 0$, we also define $\mathfrak{S}_n^\varepsilon$ as the
subset of $\mathfrak{S}_n$ consisting of sequences whose correctness proportion exceeds threshold $\varepsilon$: $\mathfrak{S}_n^\varepsilon = \{\sigma \in \mathfrak{S}_n | \text{CorP}(\sigma) > \varepsilon\}$.

From $\bigcap_{n \in \mathbb{N}} \text{Cyl}(\mathfrak{S}_n) = E$, we derive that $\lim_{n \to \infty} \mathbb{P}_c(\mathfrak{S}_n) = \mathbb{P}_c(E) = 0$. Thus $\lim_{n \to \infty} \mathbb{P}_c(\mathfrak{S}_n^\varepsilon) = 0$.

On the other hand, for every $n \in \mathbb{N}$,

$$ \mathbb{P}_c(\mathfrak{S}_n^\varepsilon) = \sum_{\sigma \in \mathfrak{S}_n^\varepsilon} \mathbb{P}_c(\sigma) > \sum_{\sigma \in \mathfrak{S}_n^\varepsilon} \frac{\varepsilon}{1-\varepsilon} \mathbb{P}_f(\sigma) = \frac{\varepsilon}{1-\varepsilon} \mathbb{P}_f(\mathfrak{S}_n^\varepsilon). $$

Since $\varepsilon$ is fixed, we have $\mathbb{P}_f(\mathfrak{S}_n^\varepsilon) < \frac{1-\varepsilon}{\varepsilon} \mathbb{P}_c(\mathfrak{S}_n^\varepsilon)$, thus $\lim_{n \to \infty} \mathbb{P}_c(\mathfrak{S}_n^\varepsilon) = 0$ implies that $\lim_{n \to \infty} \mathbb{P}_f(\mathfrak{S}_n^\varepsilon) = 0$.

Let $\rho$ be a minimal faulty run and $\alpha > 0$. There exists $n_\alpha \ge |\rho|_o = 1$ such that for all $n \ge n_\alpha$, $\mathbb{P}_f(\mathfrak{S}_n^\varepsilon) \le \alpha$. Let $n \ge n_\alpha$, and $\tilde{\mathfrak{S}}_n$ be the set of observed sequences of length $n$ triggered by a run with prefix $\rho$ and whose correctness proportion exceeds $\varepsilon$:

$$ \tilde{\mathfrak{S}}_n = \{\sigma \in \Sigma_o^n | \exists \rho' \in \mathbf{SR}_n, \rho \preceq \rho' \wedge \mathcal{P}(\rho') = \sigma \wedge \text{CorP}(\sigma) > \varepsilon\}. $$

Let us prove that $\mathbb{P}(\tilde{\mathfrak{S}}_n) \le \alpha$. On the one hand, since $\mathbb{P}_f(\mathfrak{S}_n) \ge \mathbb{P}_f(E) = 1$, $\mathbb{P}_f(\tilde{\mathfrak{S}}_n \cap (\Sigma_o^n \setminus \mathfrak{S}_n)) = 0$. On the other hand, since $\mathbb{P}_f(\mathfrak{S}_n^\varepsilon) \le \alpha$, $\mathbb{P}_f(\tilde{\mathfrak{S}}_n \cap \mathfrak{S}_n) \le \mathbb{P}_f(\mathfrak{S}_n^\varepsilon) \le \alpha$. Thus, $\mathbb{P}_f(\tilde{\mathfrak{S}}_n) = \mathbb{P}_f(\tilde{\mathfrak{S}}_n \cap \mathfrak{S}_n) + \mathbb{P}_f(\tilde{\mathfrak{S}}_n \cap (\Sigma_o^n \setminus \mathfrak{S}_n)) \le \alpha$. Because $\alpha$ was taken arbitrary, we obtain that $\lim_{n \to \infty} \mathbb{P}_f(\tilde{\mathfrak{S}}_n) = 0$. Observe now that

$$ \mathbb{P}(\{\rho' \in \mathbf{SR}_n | \rho \preceq \rho' \wedge \text{CorP}(\mathcal{P}(\rho')) > \varepsilon\}) = \frac{1}{2} \mathbb{P}_f(\tilde{\mathfrak{S}}_n). $$

Therefore, $\lim_{n \to \infty} \mathbb{P}(\{\rho' \in \mathbf{SR}_n | \rho \preceq \rho' \wedge \text{CorP}(\mathcal{P}(\rho')) > \varepsilon\}) = 0$. In conclusion $\mathcal{A}$ is AFF-diagnosable. $\square$

This characterisation shows that, for initial-fault pLTS, AFF-diagnosability can be reduced to the distance 1 problem. As one can perform the closure w.r.t. unobservable events and check the distance 1 in polynomial time, AFF-diagnosability for initial-fault pLTS belongs to PTIME.

**Example 4.11.** Consider the initial-fault pLTS of Figure 4.11 $\langle q_0, \mathcal{A}^f, \mathcal{A}^c \rangle$ and the prospect $E = \{\sigma \in \Sigma_o^\omega | \limsup_{n \in \mathbb{N}} \frac{|\sigma_{<n}|_b}{n} \ge \frac{1}{2}\}$. As a 'b' has a probability 3/4 to be observed at each step in $\mathcal{A}^f$ and 1/4 in $\mathcal{A}^c$, $\mathbb{P}_f(E) = 1$ and $\mathbb{P}_c(E) = 0$ where $\mathbb{P}_f$ and $\mathbb{P}_c$ are the probability measures of $\mathcal{A}^f$ and $\mathcal{A}^c$. Therefore this initial-fault pLTS is AFF-diagnosable. In fact, as this pLTS has a single minimal faulty run, it is even uniformly AFF-diagnosable.

**Remark 4.1.** There exists a single minimal faulty run in every initial-fault pLTS. As a consequence, AFF-diagnosability and uniform AFF-diagnosability are equivalent for initial-fault pLTS.

In order to understand why characterising AFF-diagnosability for general pLTS is more involved, consider the pLTS $\mathcal{A}$ presented in Figure 4.12. Recall that $\mathcal{A}$ is AFF-diagnosable as shown in the proof of Theorem 3.1, page 73.
<figure><img src="image_60.png" /><figcaption>Figure 4.12: An AFF-diagnosable pLTS where the distance 1 characterisation cannot be applied in a simple way.</figcaption></figure>

Let us look at the distance between pairs of a correct and a faulty states of $\mathcal{A}$ that can be reached by runs with the same observed sequence. On the one hand, we have $d(\mathcal{M}(\mathcal{A}_{q_1}), \mathcal{M}(\mathcal{A}_{q_f})) \le 3/16$ since for any prospect $E$ either (1) $b^\omega \in E$ implying $\mathbb{P}^{\mathcal{M}(\mathcal{A}_{q_f})}(E) = 1$ and $\mathbb{P}^{\mathcal{M}(\mathcal{A}_{q_0})}(E) \ge 13/16$ or (2) $b^\omega \notin E$ implying $\mathbb{P}^{\mathcal{M}(\mathcal{A}_{q_f})}(E) = 0$ and $\mathbb{P}^{\mathcal{M}(\mathcal{A}_{q_0})}(E) \le 3/16$. On the other hand, $d(\mathcal{M}(\mathcal{A}_{q_c}), \mathcal{M}(\mathcal{A}_{q_f})) = 1$ since $\mathbb{P}^{\mathcal{M}(\mathcal{A}_{q_f})}(b^\omega) = 1$ and $\mathbb{P}^{\mathcal{M}(\mathcal{A}_{q_c})}(b^\omega) = 0$.

Intuitively, the pair $(q_1, q_f)$ is irrelevant, since the correct state $q_1$ does not belong to a BSCC of the pLTS, while $(q_c, q_f)$ is relevant since $q_c$ belongs to a BSCC triggering a “recurrent” ambiguity. The next theorem characterises AFF-diagnosability for general pLTS, establishing the soundness of this intuition.

**Theorem 4.1.** Let $\mathcal{A}$ be a pLTS. Then, $\mathcal{A}$ is AFF-diagnosable if and only if for every correct state $q_c$ belonging to a BSCC and every faulty state $q_f$ reachable by a faulty run $\rho_f$ such that $q_c$ is reachable by a run with same observed sequence, $d(\mathcal{M}(\mathcal{A}_{q_c}), \mathcal{M}(\mathcal{A}_{q_f})) = 1$.

The proof of Theorem 4.1, due to its complexity and length, is divided into two lemmas, Lemma 4.2 and Lemma 4.3 given below, each of them stating one implication of the equivalence.

**Lemma 4.2.** Let $\mathcal{A}$ be a pLTS. If there exists $q_c \in Q_c$ belonging to a BSCC, $q_f \in Q_f$ such that $d(\mathcal{M}(\mathcal{A}_{q_f}), \mathcal{M}(\mathcal{A}_{q_c})) < 1$ and runs $q_0 \stackrel{\rho_c}{\Rightarrow} q_c$ and $q_0 \stackrel{\rho_f}{\Rightarrow} q_f$ such that $\mathcal{P}(\rho_c) = \mathcal{P}(\rho_f)$, then $\mathcal{A}$ is not AFF-diagnosable.

This lemma is the easiest of the two. It is proved by contraposition. Assume there exist two states in $\mathcal{A}$, $q_c \in Q_c$ belonging to a BSCC and $q_f \in Q_f$ reachable resp. by $\rho_c$ and $\rho_f$ with $\mathcal{P}(\rho_c) = \mathcal{P}(\rho_f)$, and with $d(\mathcal{M}(\mathcal{A}_{q_c}), \mathcal{M}(\mathcal{A}_{q_f})) < 1$. Applying Lemma 4.1 to the initial-fault pLTS $\mathcal{A}' = \langle q'_0, \mathcal{A}_{q_f}, \mathcal{A}_{q_c} \rangle$ where $q'_0$ is a new state, one deduces that $\mathcal{A}'$ is not AFF-diagnosable. First we relate the probabilities of runs in $\mathcal{A}$ and $\mathcal{A}'$. Then we show that considering the additional faulty runs with same observed sequence as $\rho_f$ does not make $\mathcal{A}$ AFF-diagnosable.

*Proof.* Let $\mathcal{A}$ be a pLTS, assume there exists $q_c \in Q_c$ belonging to a BSCC, $q_f \in Q_f$ such that $d(\mathcal{M}(\mathcal{A}_{q_f}), \mathcal{M}(\mathcal{A}_{q_c})) < 1$ and runs $q_0 \stackrel{\rho_c}{\Rightarrow} q_c$ and $q_0 \stackrel{\rho_f}{\Rightarrow} q_f$ such that $\mathcal{P}(\rho_c) = \mathcal{P}(\rho_f)$. Let us introduce some notations:

$$ \sigma_0 := \mathcal{P}(\rho_f) = \mathcal{P}(\rho_c), \quad p_f := \mathbb{P}_{\mathcal{A}}(\rho_f), \quad p_c := \mathbb{P}_{\mathcal{A}}(\rho_c). $$
Let $p_g (\ge p_f)$ be the probability of the faulty runs with observed sequence $\sigma_0$:

$$p_g = \mathbb{P}_A(\{\rho \in \mathbf{SR}_{|\sigma|} | \mathcal{P}(\rho) = \sigma_0, \text{ and } \rho \text{ is faulty}\}).$$

For all $n \ge |\sigma|$, let $\mathfrak{S}_n$ be the set of observed sequences of length $n$ “extending” $\rho_f$:

$$\mathfrak{S}_n = \{\sigma \in \Sigma_o^n | \exists \rho \in \mathbf{SR}_n, \rho_f \preceq \rho \wedge \mathcal{P}(\rho) = \sigma\}.$$

Given $\sigma \in \mathfrak{S}_n$, we refine $p_f, p_c$ and $p_g$ as follows.

* $p_f^\sigma = \mathbb{P}_A(\{\rho \in \mathbf{SR}_n | \rho_f \preceq \rho \wedge \mathcal{P}(\rho) = \sigma\})$;

* $p_c^\sigma = \mathbb{P}_A(\{\rho \in \mathbf{SR}_n | \rho_c \preceq \rho \wedge \mathcal{P}(\rho) = \sigma\})$;

* $p_g^\sigma = \mathbb{P}_A(\{\rho \in \mathbf{SR}_n | \rho \text{ is faulty and } \mathcal{P}(\rho) = \sigma\})$.

We introduce the initial-fault pLTS $\mathcal{A}' = \langle q'_0, \mathcal{A}_{q_f}, \mathcal{A}_{q_c} \rangle$ for some new state $q'_0$. It is well-defined since $q_c$ belongs to a BSCC so that $\mathcal{A}_{q_c}$ does not trigger faults. We write $\mathcal{P}'$ for the probability measure in $\mathcal{A}'$. Since $d(\mathcal{M}(\mathcal{A}_{q_f}), \mathcal{M}(\mathcal{A}_{q_c})) < 1$, due to Lemma 4.1, there exist positive reals $\alpha', \varepsilon' \le 1$ such that for all $n_0 \in \mathbb{N}$ there exists $n \ge n_0$:

$$\mathbb{P}_{\mathcal{A}'}\{\rho \in \mathbf{SR}_n | q'_0 \mathbf{f} q_f \preceq \rho \wedge \mathrm{CorP}(\mathcal{P}(\rho)) > \varepsilon\} > \alpha' .$$

This entails the following inequality for $\mathcal{A}$:

$$\mathbb{P}(\{\rho \in \mathbf{SR}_n | \rho_f \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + \frac{p_c}{p_f} p_f^{\mathcal{P}(\rho)}} > \varepsilon'\}) > 2p_f \alpha' .$$

Indeed in $\mathcal{A}'$, the probability of the set of faulty (resp. correct) run with observed sequence $\mathcal{P}(\rho)$ is $\frac{p_f^{\mathcal{P}(\rho)}}{2p_f}$ (resp. $\frac{p_c^{\mathcal{P}(\rho)}}{2p_c}$): the probability in $\mathcal{A}'$ to go in $q_f$ (resp. $q_c$) initially, 1/2, times the probability in $\mathcal{A}$ of the runs extending $\rho_f$ (resp. $\rho_c$) with observation $\mathcal{P}(\rho)$, $p_f^{\mathcal{P}(\rho)}$ (resp. $p_c^{\mathcal{P}(\rho)}$), divided by the probability of $\rho_f$ (resp. $\rho_c$), $p_f$ (resp. $p_c$). Finally the $2p_f$ factor of the lower bound takes into account the fact that the probability of reaching $q_f$ in $\mathcal{A}'$ is 1/2 while the probability of $\rho$ in $\mathcal{A}$ is $p_f$.

Observe that $\frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)}+\frac{p_c}{p_f}p_f^{\mathcal{P}(\rho)}} > \varepsilon'$ is equivalent to $\frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)}+p_f^{\mathcal{P}(\rho)}} > \frac{\varepsilon'p_c}{\varepsilon'p_c+(1-\varepsilon')p_f}$. So defining $\tilde{\varepsilon} = \frac{\varepsilon'p_c}{\varepsilon'p_c+(1-\varepsilon')p_f} \le 1$ and $\tilde{\alpha} = 2p_f\alpha' \le 2$, the previous inequality can be rewritten:

$$\mathbb{P}(\{\rho \in \mathbf{SR}_n | \rho_f \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} > \tilde{\varepsilon}\}) > \tilde{\alpha}.$$

Let $\mathfrak{S}'_n$ be the subset of observed sequences of $\mathfrak{S}_n$ whose correctness proportion is greater than $\tilde{\varepsilon}$ when only considering extensions of $\rho_f$, but smaller than $\varepsilon^* = \frac{\tilde{\alpha}\tilde{\varepsilon}}{4}$ when considering all faulty runs:

$$\mathfrak{S}'_n = \{\sigma \in \mathfrak{S}_n | \frac{p_c^\sigma}{p_c^\sigma + p_f^\sigma} > \tilde{\varepsilon} \wedge \frac{p_c^\sigma}{p_c^\sigma + p_g^\sigma} \le \varepsilon^*\}.$$
Let $\sigma \in \mathfrak{S}'_n$, $p_f^\sigma < \frac{1-\tilde{\epsilon}}{\tilde{\epsilon}} p_c^\sigma$ and $p_c^\sigma \le \frac{\epsilon^*}{1-\epsilon^*} p_g^\sigma$. Therefore $p_f^\sigma < \frac{(1-\tilde{\epsilon})\epsilon^*}{(1-\epsilon^*)\tilde{\epsilon}} p_g^\sigma$.

Summing over all sequences of $\mathfrak{S}'_n$: $\sum_{\sigma \in \mathfrak{S}'_n} p_f^\sigma < \frac{(1-\tilde{\epsilon})\epsilon^*}{(1-\epsilon^*)\tilde{\epsilon}} p_g$.

Since $p_g \le 1$: $\sum_{\sigma \in \mathfrak{S}'_n} p_f^\sigma \le \frac{(1-\tilde{\epsilon})\tilde{\alpha}}{4(1-\frac{\tilde{\alpha}\tilde{\epsilon}}{4})} \le \frac{\tilde{\alpha}}{2}$.

Thus,

$$ \mathbb{P}(\{\rho \in \mathbf{SR}_n | \rho_f \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_g^{\mathcal{P}(\rho)}} > \epsilon^*\}) \ge \frac{p_f^\sigma}{p_c^\sigma + p_g^\sigma} $$

$$ \mathbb{P}(\{\rho \in \mathbf{SR}_n | \rho_f \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} > \tilde{\epsilon}\}) - \sum_{\sigma' \in \mathfrak{S}'_n} p_f^{\sigma'} > \tilde{\alpha} - \frac{\tilde{\alpha}}{2} = \frac{\tilde{\alpha}}{2}. $$

Observe that given $\sigma \in \mathfrak{S}_n$, $\text{CorP}(\sigma) \ge \frac{p_c^\sigma}{p_c^\sigma + p_g^\sigma}$, since we ignore correct runs $\rho$ with $\mathcal{P}(\rho) = \sigma$ that do not extend $\rho_c$. So defining $\epsilon = \epsilon^*$ and $\alpha = \tilde{\alpha}/2$, for all $n_0 \in \mathbb{N}$ there exists $n \ge n_0$:

$$ \mathbb{P}(\{\rho \in \mathbf{SR}_n | \rho_f \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_g^{\mathcal{P}(\rho)}} > \epsilon\}) > \alpha. $$

Let $\rho_0$ be the minimal faulty run such that $\rho_0 \preceq \rho_f$. We observe that $\text{Cyl}(\rho_f) \subseteq \text{Cyl}(\rho_0)$, so that

$$ \mathbb{P}(\{\rho \in \mathbf{SR}_n | \rho_0 \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_g^{\mathcal{P}(\rho)}} > \epsilon\}) > \alpha $$

which establishes that $\mathcal{A}$ is not AFF-diagnosable. $\square$

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

**Lemma 4.3.** Let $\mathcal{A}$ be a pLTS. If for all $q_0 \stackrel{\rho_c}{\Rightarrow} q_c$ and $q_0 \stackrel{\rho_f}{\Rightarrow} q_f$ with $\mathcal{P}(\rho_c) = \mathcal{P}(\rho_f)$, $q_f \in Q_f$ and $q_c \in Q_c$ belonging to a BSCC, $d(\mathcal{M}(A_{q_c}), \mathcal{M}(A_{q_f})) = 1$, then $\mathcal{A}$ is AFF-diagnosable.

Let $\rho_0$ be a minimal faulty run, $\alpha > 0, \epsilon > 0$, $\sigma_0 = \mathcal{P}(\rho_0)$ and $n_0 = |\sigma_0|$. Before developing the proof, we sketch its structure and illustrate it in Figure 4.13. First, we extend the runs with observed sequence $\sigma_0$ by $n_b$ observable events where $n_b$ is chosen in order to get a high probability that the runs end in a BSCC.

Let $\sigma \in \Sigma_\sigma^{n_b}$ be such an observed sequence. We partition the possible runs with observed sequence $\sigma_0\sigma$ into three sets $\mathfrak{R}_\sigma^F$, $\mathfrak{R}_\sigma^C$ and $\mathfrak{R}_\sigma^T$. $\mathfrak{R}_\sigma^F$ is the subset of faulty runs while $\mathfrak{R}_\sigma^C$ (resp. $\mathfrak{R}_\sigma^T$) is the set of correct runs ending (resp. not ending) in a BSCC. At first, we do not take into account the transient runs in $\mathfrak{R}_\sigma^T$. We apply Lemma 4.1 to obtain an integer $n_\sigma$ such that from $\mathfrak{R}_\sigma^F$ and $\mathfrak{R}_\sigma^C$, we can diagnose with (appropriate) high probability and low correctness proportion after $n_\sigma$ observations. Among the runs that trigger diagnosable observed sequences, some will exceed the correctness proportion, $\epsilon$, when taking into account the runs from $\mathfrak{R}_\sigma^T$. Yet we show that the probability of such runs is small when cumulated over all extensions $\sigma$ leading to the required upper bound $\alpha$.
<figure><img src="image_62.png" /><figcaption>Figure 4.13: Illustration of the proof of Lemma 4.3.</figcaption></figure>

Proof. Let $\rho_0$ be a minimal faulty run, $\alpha > 0, \varepsilon > 0$, $\sigma_0 = \mathcal{P}(\rho_0)$ and $n_0 = |\sigma_0|$. Since almost surely a random run ends in a BSCC, there exists $n_b$ such that for $\eta = \frac{\alpha\varepsilon}{4}$

$$ \mathbb{P}\{\rho \in \mathbb{SR}_{n_0+n_b} | \sigma_0 \le \mathcal{P}(\rho) \wedge \mathit{last}(\rho) \text{ does not belong to a BSCC}\} < \eta. $$

Let $\mathcal{G} = \{\sigma \in \Sigma_{\sigma}^{n_b} | \exists \rho \in \mathbb{SR}_{n_0+n_b} \rho_0 \le \rho \wedge \mathcal{P}(\rho) = \sigma_0\sigma\}$. Pick some $\sigma \in \mathcal{G}$ and define:

* $\mathfrak{R}_{\sigma}^{F} = \{\rho \in \mathbb{SR}_{n_0+n_b} | \mathcal{P}(\rho) = \sigma_0\sigma \wedge \mathit{last}(\rho) \in Q_f\}$;

* $\mathfrak{R}_{\sigma}^{C} = \{\rho \in \mathbb{SR}_{n_0+n_b} | \mathcal{P}(\rho) = \sigma_0\sigma \wedge \mathit{last}(\rho) \in Q_c \text{ and belongs to a BSCC}\}$;

* $\mathfrak{R}_{\sigma}^{T} = \{\rho \in \mathbb{SR}_{n_0+n_b} | \mathcal{P}(\rho) = \sigma_0\sigma \wedge \mathit{last}(\rho) \in Q_c \text{ and does not belong to a BSCC}\}$.

Temporarily, we ignore the runs of $\mathfrak{R}_{\sigma}^{T}$. Let $Q_c^{\sigma} = \{\mathit{last}(\rho) | \rho \in \mathfrak{R}_{\sigma}^{C}\}$ and $Q_f^{\sigma} = \{\mathit{last}(\rho) | \rho \in \mathfrak{R}_{\sigma}^{F}\}$. For every pair $(q_f, q_c) \in Q_f^{\sigma} \times Q_c^{\sigma}$, consider the initial-fault pLTS $\mathcal{A}' = \langle q'_0, \mathcal{A}_{q_f}, \mathcal{A}_{q_c} \rangle$ for some new state $q'_0$, and denote $\mathbb{P}'$ its associated probability measure. Due to Lemma 4.1, for all $\alpha' > 0, \varepsilon' > 0$, there exists $n_{q_f, q_c}$ such that for all $n \ge n_{q_f, q_c}$:

$$ \mathbb{P}'\{\rho \in \mathbb{SR}_n | q'_0 \mathbf{f} q_f \le \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} > \varepsilon'\} \le \alpha' $$

where $p_c^{\mathcal{P}(\rho)}$ (resp. $p_f^{\mathcal{P}(\rho)}$) is the probability in $\mathcal{A}'$ of a correct (resp. faulty) run with observed sequence $\mathcal{P}(\rho)$.
Define in $\mathcal{A}$, $p_c^{\mathcal{P}(\rho)}$ (resp. $p_f^{\mathcal{P}(\rho)}$) to be the probability of a correct (resp. faulty) run with observed sequence $\mathcal{P}(\rho)$, $p_f = \min(\mathcal{P}(\rho) | \rho \in \mathfrak{R}_{\sigma}^{F})$ and $p_c = \sum_{\rho \in \mathfrak{R}_{\sigma}^{C}} \mathcal{P}(\rho)$. By a worst-case reasoning, one gets $p_c^{\mathcal{P}(\rho)} \ge \frac{2}{p_c} p_c^{\sigma_0 \sigma \mathcal{P}(\rho)}$ and $p_f^{\mathcal{P}(\rho)} \le \frac{2}{p_f} p_f^{\sigma_0 \sigma \mathcal{P}(\rho)}$. Thus for all $n \ge n_0 + n_b + \max(n_{q_f, q_c})$:

$$ \mathbb{P}\{\rho \in \mathbf{SR}_n \mid \exists \rho' \in R_{\sigma}^{F} \wedge \rho' \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + \frac{p_c}{p_f} p_f^{\mathcal{P}(\rho)}} > \varepsilon'\} \le 2\alpha' $$

where the factor 2 takes into account the first transition in $\mathcal{A}'$.

Choosing $\varepsilon' = \frac{\varepsilon p_f}{\varepsilon p_f + (2-\varepsilon)p_c}$ and $\alpha' = \frac{\alpha}{4|\mathfrak{G}|}$, after algebraic operations the previous inequality can be rewritten:

$$ \mathbb{P}\{\rho \in \mathbf{SR}_n \mid \exists \rho' \in R_{\sigma}^{F} \wedge \rho' \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} > \frac{\varepsilon}{2}\} \le \frac{\alpha}{2|\mathfrak{G}|} . $$

Let $n_{\sigma} = n_0 + n_b + \max(n_{q_f, q_c} \mid (q_f, q_c) \in Q_f^{\sigma} \times Q_c^{\sigma})$ and $n_1 = \max(n_{\sigma} \mid \sigma \in \mathfrak{G})$ and consider $n \ge n_1$. Ignoring the runs of $\mathfrak{R}_{\sigma}^{T}$, one could detect the fault done in $\rho_0$ with good accuracy and high probability $n_1$ steps after it occurred.

We now take into account the runs of $\mathfrak{R}_{\sigma}^{T}$. Let $\rho \in \{\rho \in \mathbf{SR}_n \mid \exists \rho' \in \mathfrak{R}_{\sigma}^{F} \wedge \rho' \preceq \rho\}$. Define $p_t^{\mathcal{P}(\rho)}$ to be the probability of runs (1) with observed sequence $\mathcal{P}(\rho)$ and (2) extending runs of $\mathfrak{R}_{\sigma}^{T}$. Since a correct run with observed sequence $\mathcal{P}(\rho)$ must have a prefix in $\mathfrak{R}_{\sigma}^{T}$ or in $\mathfrak{R}_{\sigma}^{C}$:

$$ \mathrm{CorP}(\mathcal{P}(\rho)) \le \frac{p_c^{\mathcal{P}(\rho)} + p_t^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_t^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} . $$

Consider the following set of runs:

$$ \tilde{\mathfrak{R}}_{\sigma}^{n} = \{ \rho \in \mathbf{SR}_n \mid \exists \rho' \in \mathfrak{R}_{\sigma}^{F} \wedge \rho' \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)} + p_t^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_t^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} > \varepsilon \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_t^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} \le \frac{\varepsilon}{2} \} . $$

For $\rho \in \tilde{\mathfrak{R}}_{\sigma}^{n}$, one gets by algebraic operations, $\frac{2p_t^{\mathcal{P}(\rho)}}{\varepsilon} > p_f^{\mathcal{P}(\rho)}$.

Thus $\mathbb{P}(\tilde{\mathfrak{R}}_{\sigma}^{n}) < \frac{2\mathbb{P}(\mathfrak{R}_{\sigma}^{T})}{\varepsilon}$ and $\sum_{\sigma \in \mathfrak{G}} \mathbb{P}(\tilde{\mathfrak{R}}_{\sigma}^{n}) < \frac{2\sum_{\sigma \in \mathfrak{G}} \mathbb{P}(\mathfrak{R}_{\sigma}^{T})}{\varepsilon}$.

Due to the choice of $n_b$, $\sum_{\sigma \in \mathfrak{G}} \mathbb{P}(\mathfrak{R}_{\sigma}^{T}) < \eta$, and we derive $\sum_{\sigma \in \mathfrak{G}} \mathbb{P}(\tilde{\mathfrak{R}}_{\sigma}^{n}) < \frac{2\eta}{\varepsilon} = \frac{\alpha}{2}$.
Summarising for all $n \ge n_1$:

$$ 
\begin{align*}
& \mathbb{P}\{\rho \in \mathrm{SR}_n \mid \rho_0 \preceq \rho \wedge \mathrm{CorP}(\mathcal{P}(\rho)) > \varepsilon\} \\
&= \sum_{\sigma \in \mathcal{S}} \mathbb{P}\{\rho \in \mathrm{SR}_n \mid \rho_0 \preceq \rho \wedge \sigma_0 \sigma \preceq \mathcal{P}(\rho) \wedge \mathrm{CorP}(\mathcal{P}(\rho)) > \varepsilon\} \\
&\le \sum_{\sigma \in \mathcal{S}} \mathbb{P}\{\rho \in \mathrm{SR}_n \mid \exists \rho' \in \mathfrak{R}_{\sigma}^F \wedge \rho' \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} > \frac{\varepsilon}{2}\} \\
&\quad + \mathbb{P}\{\rho \in \mathrm{SR}_n \mid \exists \rho' \in \mathfrak{R}_{\sigma}^F \wedge \rho' \preceq \rho \wedge \frac{p_c^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} \le \frac{\varepsilon}{2} \wedge \frac{p_c^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}}{p_c^{\mathcal{P}(\rho)} + p_t^{\mathcal{P}(\rho)} + p_f^{\mathcal{P}(\rho)}} > \varepsilon\} \\
&\le |\mathcal{G}| \frac{\alpha}{2|\mathcal{G}|} + \frac{\alpha}{2} = \alpha
\end{align*}
$$

which establishes the AFF-diagnosability of $\mathcal{A}$.

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

As an alternative to the proof of Theorem 4.1, one could mimic the approach by Kiefer and Sistla [KS16] for monitorability. The idea would be, from a pLTS $\mathcal{A}$ to derive two hidden Markov chains, say $\mathcal{H}_c$ and $\mathcal{H}_f$ representing respectively the observed sequences for correct and faulty runs of $\mathcal{A}$. However, to establish that distinguishability of $\mathcal{H}_c$ and $\mathcal{H}_f$ corresponds to AFF-diagnosability essentially relies on the same arguments we used in the above proof (and so this alternative approach would not simplify it). The difficulty lies in that the properties one conditions by to obtain $\mathcal{H}_c$ and $\mathcal{H}_f$, namely always correct or eventually faulty, anticipate on the future behaviour of the system; in contrast, the correctness proportion appearing in the definition of AFF-diagnosability only reasons about the possible behaviours up to the last observation.

# 2 Verification of the diagnosability

We now study the decidability of the different diagnosability notions for finite pLTS and in the positive case provide the complexity. The characterisations given in Section 1 play an important role in this study. Indeed, when a simple characterisation exists, the diagnosability problem is decidable (an algorithm consists in checking this characterisation). Conversely, when we did not exhibit a characterisation, we show that the problem is undecidable.

## 2.1 Decidability results and upper bounds

We start by showing how to check the characterisations defined in Section 1, therefore providing upper bounds to some of the diagnosability problems. We first consider exact diagnosability notions, and establish that they can all be solved in PSPACE. In all cases, to obtain the PSPACE upper-bound, we avoid building explicitly the exponential size product pLTS (that is used in the characterisations) and only explore it on-the-fly.

The three results have similar proofs. As a consequence we first develop the case of FF-diagnosability then we simultaneously deal with both FA and IA-diagnosability.
**Proposition 4.7.** The FF-diagnosability problem is decidable in PSPACE.

The proof consists in designing a PSPACE algorithm to check the characterisation given in Proposition 4.2. This algorithm exploits Savitch's Theorem [Sav70] which establishes that PSPACE = NPSPACE. This theorem allows us to use non-determinism in our decision procedure.

*Proof.* To obtain a PSPACE algorithm, we cannot build explicitly the product pLTS $\mathcal{A}_{\text{FF}}$, which is exponential in the size of $\mathcal{A}$. Given two states $s, s'$ of $\mathcal{A}_{\text{FF}}$, one can check in polynomial space in the size of $\mathcal{A}$ whether $s'$ can be reached from $s$. Indeed, reachability of a state is known to be in non-deterministic logarithmic space in the size of the system, thus here NPSPACE, which is equal to PSPACE thanks to Savitch's Theorem. Using this procedure, we can check whether a state $s$ is not in a BSCC by guessing another state $s'$ such that $s'$ is reachable from $s$ but $s$ is not reachable from $s'$. Here again we apply Savitch's Theorem.

Thus the procedure that decides whether $\mathcal{A}$ is not FF-diagnosable consists in guessing a state $s = (q, U)$ with $q \in Q_f$ and $U \neq \emptyset$, checking that it is reachable from $s_0$ and whether $s$ belongs to a BSCC. $\square$

We state below similar results for FA and IA-diagnosability problems.

**Proposition 4.8.** The FA- and IA-diagnosability problems are decidable in PSPACE.

The two proofs are similar to the proof of Proposition 4.7: we design a decision procedure which uses non-determinism to check the characterisation given in the previous section and the non-determinism is removed using Savitch's Theorem.

*Proof.* We first check the characterisation of FA-diagnosability given in Proposition 4.4 without explicitly building the product pLTS $\mathcal{A}_{\text{FA}}$. First given a state $(q, U, V)$ of $\mathcal{A}_{\text{FA}}$ we can check in polynomial space whether it belongs to a BSCC (as in the proof of Proposition 4.7). We can also check in polynomial space whether some state $(q', U', V')$ with $U' = \emptyset$ or $V' = \emptyset$ can be reached from $(q, U, V)$ by guessing such a state and then checking the reachability condition. Combining the two, this provides a polynomial space algorithm to check whether $(q, U, V)$ belongs to a BSCC in which no state $(q', U', V')$ fulfils $U' \neq \emptyset$ and $V' \neq \emptyset$. Thus the procedure that decides whether $\mathcal{A}$ is not FA-diagnosable consists in guessing a state $s = (q, U, V)$, checking that it is reachable from $s_0$ and belongs to a BSCC where all states $(q', U', V')$ fulfil $U' \neq \emptyset$ and $V' \neq \emptyset$.

We use the characterisation of IA-diagnosability given in Proposition 4.5 without building explicitly the product pLTS $\mathcal{A}_{\text{IA}}$. First, given a state $(q, U, V, W)$ of $\mathcal{A}_{\text{IA}}$, we can check in polynomial space that it belongs to a BSCC (as in the proof of Proposition 4.7). We can also check in polynomial space whether it is coreachable from a state $(q', U', V', W')$ that fulfils $U' = \emptyset$ or $W' = \emptyset$ by guessing such a state. Combining the two procedures, we can check in polynomial space whether $(q, U, V, W)$ belongs to a BSCC where all states $(q', U', V', W')$ of the BSCC fulfil $U' \neq \emptyset$ and $W' \neq \emptyset$. Thus the procedure that decides whether $\mathcal{A}$ is not IA-diagnosable consists in guessing a state $s = (q, U, V, W)$, checking that it is reachable from the initial state $s_0$ and belongs to a BSCC where all states $(q', U', V', W')$ fulfil $U' \neq \emptyset$ and $W' \neq \emptyset$. $\square$
For approximate diagnosability, we focus on AFF-diagnosability and establish a com-
plexity upper-bound, relying on the characterisation from the previous section.

**Theorem 4.2.** *The AFF-diagnosability problem is decidable in PTIME for pLTS.*

*Proof.* The decidability and complexity results rely on the characterisation of AFF-diagnosability showed in Theorem 4.1. Reachability of a pair of states with the same observed sequence is decidable in NLOGSPACE by an appropriate "self-synchronised product" of the pLTS that we detail below. Since there are at most a quadratic number of pairs to check, and given that the distance 1 problem can be decided in polynomial time due to [CK14] (as recalled in Proposition 4.6), the decidability and PTIME upper-bound follow.

We now define the appropriate “self-synchronised product” of the pLTS mentioned
above. Given a pLTS $\mathcal{A} = \langle Q, q_0, \Sigma, T, \mathbf{P} \rangle$ we build the product LTS $\mathcal{A} \otimes \mathcal{A} = \langle Q \times Q, \{q_0, q_0\}, \Sigma, T' \rangle$ where $((q_1, q_2), a, (q'_1, q'_2)) \in T'$ if

- if $a \in \Sigma_u$ then either $(q_1, a, q'_1) \in T$ and $q'_2 = q_2$ or $(q_2, a, q'_2) \in T$ and $q'_1 = q_1$;

- else $(a \in \Sigma_o), (q_1, a, q'_1) \in T$ and $(q_2, a, q'_2) \in T$.

A pair of state $(q, q')$ is reachable in $\mathcal{A} \otimes \mathcal{A}$ from $(q_0, q_0)$ if and only if there exist two
runs $\rho$ and $\rho'$ of $\mathcal{A}$ such that $\text{last}(\rho) = q$, $\text{last}(\rho') = q'$ and $\mathcal{P}(\rho) = \mathcal{P}(\rho')$. Therefore, $\mathcal{A}$
is AFF-diagnosable if for any pair of states reachable in $\mathcal{A} \otimes \mathcal{A}$, $(q, q')$, with $q$ correct,
belonging to a BSCC of $\mathcal{A}$, and $q'$ faulty, then $d(\mathcal{M}(\mathcal{A}_q), \mathcal{M}(\mathcal{A}_{q'})) = 1$. All tests can
be checked in PTIME. $\square$

We thus have decidability of every notions of exact diagnosability and of one notion
of approximate diagnosability, AFF-diagnosability. Surprisingly, AFF-diagnosability,
which definition seems more complicated as it depends on the exact probabilistic values
of the transitions contrary to the definitions of the exact notions of diagnosability, has
a lower upper bound.

**2.2 Hardness of Diagnosability**

We gave upper bounds on the complexity of diagnosability in Subsection 2.1. We
now provide tight lower bounds: on the one hand we establish undecidability of the
approximate diagnosability notions that were not characterised, and on the other hand
we provide a PSPACE lower bound for the exact diagnosis.

**2.2.1 Undecidability results**

After having previously proved that AFF-diagnosability can be solved in polynomial time, we now establish that all other specifications of approximate diagnosability are undecidable. This result could be expected for εFF-diagnosability and uniform εFF-diagnosability since it is often the case for problems mixing probabilities, partial ob-
servation and quantitative requirement (here represented by $\varepsilon)^4$. On the contrary, the undecidability of the uniform AFF-diagnosability problem is at first sight surprising since it is a slight variation of the AFF-diagnosability problem. In fact the reduction for the latter problem is more intricate than the one for the $\varepsilon$FF- and uniform $\varepsilon$FF-diagnosability. We reduce the emptiness problem for probabilistic automata [Paz71] to both problems. Let us first details this problem. A probabilistic automaton is an automaton enhanced with probabilities on the transitions so that given a state and a letter, the sum of the probabilities of the transition exiting each state and labelled by the given letter is 1.

**Example 4.12.** Figure 4.14 represents a probabilistic automaton which initial state is $q_0$ and set of accepting states is $\{q_2\}$. The sum of the probability of the transitions exiting $q_0$ is 2 as there is a transition labelled by a ‘a’ and a transition labelled by a ‘b’. The word bab has probability 1/2 to end in $q_2$ and 1/2 to end in $q_1$.

<figure><img src="image_64.png" /><figcaption>Figure 4.14: An example of probabilistic automaton.</figcaption></figure>

**Definition 4.6.** A probabilistic automaton is a tuple $A = (Q, \delta_0, \Sigma, (P_a)_{a \in \Sigma}, F)$ where

* $Q$ is a set of states with $F \subseteq Q$, the set of final states;

* $\delta_0 \in \text{Dist}(Q)$ is the initial distribution;

* $\Sigma$ is an alphabet;

* For every $a \in \Sigma$, $P_a$ is a stochastic $Q \times Q$ matrix.

When $P_a[q, q'] > 0$, there is a transition from $q$ to $q'$ labelled by $a$ and $P_a[q, q']$. Given a word $w = a_1...a_n \in \Sigma^*$, the acceptance probability of $w$, $P_A(w)$ is defined by $P_A(w) = \sum_{q_0 \in Q} \delta_0(q_0) \sum_{q \in F} P_w[q_0, q]$ where $P_w = P_{a_1} \cdots P_{a_n}$. Given a rational threshold $0 < \varepsilon < 1$, the language $L_{A,\varepsilon}$ is defined by $L_{A,\varepsilon} = \{w \in \Sigma^* | P_A(w) > \varepsilon\}$. For a probabilistic automaton $A$ and a threshold $\varepsilon$, the emptiness problem asks whether

<footnote n="4">⁴one of the most famous example is the undecidability of the emptiness problem for probabilistic automaton [Paz71] that we detail below, see also [MHC03] for some examples of undecidable problems for partially observable Markov decision process, a formalism which also contains a form of control of the system</footnote>
$\mathcal{L}_{A,\varepsilon} = \emptyset$. This problem is undecidable even for a fixed $0 < \varepsilon < 1$ [Paz71]. The problem is also undecidable for the language defined by $\{w \in \Sigma^* | \mathbf{P}_A(w) \geq \varepsilon\}$, i.e. when the inequality is not strict. One can also restrict oneself to automata such that every word $w$ satisfies $1/4 \leq \mathbf{P}_A(w) \leq 3/4$. This can be ensured by a simple construction. Given a probabilistic automaton $A$ with initial distribution $\delta_0$ and a threshold $0 < \lambda < 1$, we build the probabilistic automaton $A'$ that contains the states of $A$ and two additional states $q_a$ and $q_r$. The new initial distribution goes in $q_a$ and $q_r$ with probability $1/4$ and with probability $1/2$ it uses the initial distribution of $A$. In the last case, the behaviour is the one of $A$, from $q_r$ and $q_a$ everything can be observed with a self-loop and $q_a$ is a final state. For every word $w$, we have

$$ \mathbf{P}_{A'}(w) = \frac{\mathbf{P}_A(w)}{2} + \frac{1}{4}. $$

This is the sum of the probability to be accepted after starting initially in the $A$ component of $A'$ plus the probability to go in $q_a$. As a consequence, every word is accepted in $A'$ with probability between $1/4$ and $3/4$ and a word is above the $\lambda$ threshold in $A$ iff it is above $1/4 + \lambda/2$ in $A'$. Thus the emptiness is also undecidable with this restriction. Note that this assumption relies on the use of an initial distribution $\delta_0$ instead of an initial state $q_0$. Indeed, with an initial state, the word $\varepsilon$ would have probability 0 or 1. When this assumption is not needed, we use an initial state instead of an initial distribution. Another important undecidable problem that is used in a latter chapter is the value 1 problem. It asks for a probabilistic automaton $A$ if for all $\varepsilon > 0$ $\mathcal{L}_{A,1-\varepsilon} \neq \emptyset$. In other words, does there exist words of arbitrarily high probability? This problem is known to be undecidable [GO10].

**Theorem 4.3.** For any rational $0 < \varepsilon < 1$, the $\varepsilon$FF-diagnosability and uniform $\varepsilon$FF-diagnosability problems are undecidable for pLTS.

We make a reduction from the emptiness problem of probabilistic automata. From a given probabilistic automaton $A = \langle Q, \delta_0, \Sigma, (\mathbf{P}_a)_{a \in \Sigma}, F \rangle$, we build a pLTS which produces with probability 1 runs whose observed sequence belongs to $\Sigma^{*\sharp w}$ (where $\sharp \notin \Sigma$) and for all $n \geq 2$, the correctness proportion CorP of $w^{\sharp n}$, with $w \in \Sigma^*$, satisfies CorP($w^{\sharp n}$) = $\mathbf{P}_A(w)$. In other words, if a word $w$ is accepted with probability greater than $\varepsilon$, then the ambiguity of the word $w^{\sharp 2}$ is greater than $\varepsilon$ and every faulty run with this observation will remain ambiguous.

*Proof.* Let $A = \langle Q, \delta_0, \Sigma, (\mathbf{P}_a)_{a \in \Sigma}, F \rangle$ be a probabilistic automaton. W.l.o.g we assume $1/4 \leq \mathbf{P}_A(w) \leq 3/4$ for every $w \in \Sigma^*$. Define the pLTS $\mathcal{A} = \langle Q', q_0, \Sigma', T', \mathbf{P}' \rangle$ as follows:

* $\Sigma' = \Sigma \uplus \{\sharp, \mathbf{f}, u\}, \Sigma'_u = \{\mathbf{f}, u\}$;

* $Q' = Q \cup \{q_0, q_c^\sharp, q_f^\sharp, f^\sharp\}$;

* $T' = \{(q_0, u, q) \mid q \in Q, \delta_0(q) > 0\} \cup \{(q, a, q) \mid q, q' \in Q, a \in \Sigma, \mathbf{P}_a[q, q'] > 0\} \cup \{(q, \sharp, q_c^\sharp | q \in F\} \cup \{(q, \sharp, q_f^\sharp | q \in Q \setminus F\} \cup \{q_c^\sharp, \sharp, q_c^\sharp\} \cup \{q_f^\sharp, \mathbf{f}, f^\sharp\} \cup \{f^\sharp, \sharp, f^\sharp\}$
• $\mathbf{P}'$ is defined by:

- For all $q \in Q$ such that $\delta_0(q) > 0$, $\mathbf{P}'(q_0, u, q) = \delta_0(q)$;

- For all $q \in Q$ and $a \in \Sigma$, $\mathbf{P}'(q, a, q') = \frac{\mathbf{P}_a[q, q']}{1+|\Sigma|}$;

- For all $q \in F$, $\mathbf{P}'(q, \sharp, q_c^\sharp) = \frac{1}{1+|\Sigma|}$;

- For all $q \in Q \setminus F$, $\mathbf{P}'(q, \sharp, q_f^\sharp) = \frac{1}{1+|\Sigma|}$;

- $\mathbf{P}'(q_f^\sharp, \mathbf{f}, f^\sharp) = \mathbf{P}'(f^\sharp, \sharp, f^\sharp) = \mathbf{P}'(q_c^\sharp, \sharp, q_c^\sharp) = 1$.

This reduction is illustrated in Figure 4.15. In each state, the sum of the probabilities of the existing transitions correctly sum to 1. For instance, let $q \in F$ and $a \in \Sigma$, then $\sum_{q' \in Q} \mathbf{P}_a[q, q'] = 1$, thus:

$$ \sum_{(q,a,q') \in T'} \mathbf{P}'(q, a, q') = \sum_{a \in \Sigma} \sum_{q' \in Q} \frac{\mathbf{P}_a[q, q']}{1 + |\Sigma|} + \mathbf{P}'(q, \sharp, q_c^\sharp) = \frac{|\Sigma|}{1 + |\Sigma|} + \frac{1}{1 + |\Sigma|} = 1. $$

<figure><img src="image_65.png" /><figcaption>Figure 4.15: From probabilistic automata to pLTS.</figcaption></figure>

We claim that the following three assertions are equivalent:

1. $\mathcal{A}$ is $\varepsilon$FF-diagnosable;

2. $\mathcal{A}$ is uniformly $\varepsilon$FF-diagnosable;

3. $\mathcal{L}_{A,\varepsilon} = \emptyset$.

Given that uniform $\varepsilon$FF-diagnosability entails $\varepsilon$FF-diagnosability, we only show that item 1 implies item 3, and item 3 implies item 2. The first implication is proved by contraposition.

1 implies 3 Assume that there exists a word $w \in \Sigma^*$ such that $\mathbf{P}_A(w) > \varepsilon$. Consider the set of signalling correct runs with observed sequence $w^{\sharp^{n+2}}$. By construction, its probability is $\frac{\mathbf{P}_A(w)}{(1+|\Sigma|)^{|w|+1}}$. Similarly, the set of signalling faulty runs with observed sequence $w^{\sharp^{n+2}}$ has probability $\frac{1-\mathbf{P}_A(w)}{(1+|\Sigma|)^{|w|+1}}$. Thus $\text{CorP}(w^{\sharp^{n+2}}) = \mathbf{P}_A(w) > \varepsilon$. By assumption on $\mathcal{A}$, $\mathbf{P}_A(w) \le 3/4 < 1$, so that the set of faulty runs with
observed sequence $w^{\#n+2}$ is non-empty. Pick $\rho$ a minimal faulty run with observed sequence $w^{\#\#}$. Using the above probability values, for every $n \ge 0$:

$$ \mathbb{P}(\{\rho' \in \mathbf{SR}_{n+|\rho|_o} \mid \rho \preceq \rho' \wedge \mathrm{CorP}(\mathcal{P}(\rho')) > \varepsilon\}) = \mathbb{P}(\rho) . $$

Thus $\mathcal{A}$ is not $\varepsilon$FF-diagnosable.

**3 implies 2** Assume that for every word $w \in \Sigma^*$, $\mathrm{Pr}_A(w) \le \varepsilon$. Let $\rho$ be a minimal faulty run of $\mathcal{A}$. By construction, its observed sequence is of the form $w^{\#2}$ with $w \in \Sigma^*$. Using the same reasoning as above, for every $\rho \preceq \rho'$: $\mathrm{CorP}(\mathcal{P}(\rho')) = \mathrm{Pr}_A(w)$, and thus $\mathrm{CorP}(\mathcal{P}(\rho')) \le \varepsilon$. Therefore, for any $\alpha > 0$, choosing $n_\alpha = 0$, one gets:

$$ \mathbb{P}(\{\rho' \in \mathbf{SR}_{n_\alpha+|\rho|} \mid \rho \preceq \rho' \wedge \mathrm{CorP}(\mathcal{P}(\rho')) > \varepsilon\}) = 0 . $$

So $\mathcal{A}$ is uniformly $\varepsilon$FF-diagnosable.

This completes the proof that $\varepsilon$FF-diagnosability and uniform $\varepsilon$FF-diagnosability are undecidable. $\square$

Uniform AFF-diagnosability is also shown to be undecidable by a reduction from the emptiness problem for probabilistic automata.

**Theorem 4.4.** *The uniform AFF-diagnosability problem is undecidable for pLTS.*

As this reduction is more involved, we start by a developed sketch of proof and then give the full proof. We proceed by a reduction from the emptiness problem for probabilistic automata where w.l.o.g. one assumes that the acceptance probability of any word lies between 1/4 and 3/4. Given such a probabilistic automaton one builds a pLTS as follows.

* With probability 1/2 one enters one of the two copies of the automaton whose probabilities are modified in a similar way as in the previous proof.

* In a non-final (resp. final) state of the first (resp. second) copy, one may exit the copy of the automaton by taking a transition labelled by $b$ (resp. $f$) and enter a terminating state. In a final state (resp. non-final) state of the first (resp. second) copy, one may “restart” the copy of the automaton by taking a transition labelled by $\#$ which lead to the initial state of the copy.

* The terminating state of the first copy iteratively outputs with probability 1/2 $\#b$ or $b$ while the terminating block of the second copy endlessly outputs $b$.

Due to the behaviour of the terminating blocks, the correctness proportion of a faulty run goes to 0 as its length increases. Thus the pLTS is AFF-diagnosable. The element that will depend on the probabilistic automaton is the uniformity of the convergence.

Observe that the language of the observed sequences of minimal faulty runs extended by one transition is $(\Sigma^*\#)^*\Sigma^*b$.
Assume there exists a word $w$ with acceptance probability strictly greater than $1/2$. Then in $\mathcal{A}$, the correctness proportion of $(w^{\#})^{n_b}$ fulfils: $\lim_{n \to \infty} \text{CorP}((w^{\#})^{n_b}) = 1$. Due to this property (and the behaviours of the terminating blocks), the pLTS is not uniformly AFF-diagnosable. If no such word exists, then for any $w = w_1\#w_2\#\dots w_k\#$, $\text{CorP}(w) \le 3/4$. Due to this property (and the behaviours of the terminating blocks), the pLTS is uniformly AFF-diagnosable.

We now develop the full proof.

*Proof.* Let $A = \langle Q, \delta_0, \Sigma, (\mathbf{P}_a)_{a \in \Sigma}, F \rangle$ be a probabilistic automaton such that the acceptance probability of any word lies between $1/4$ and $3/4$. Define the pLTS $\mathcal{A} = \langle Q', q'_0, \Sigma', T', \mathbf{P}' \rangle$ as follows.

* $\Sigma' = \Sigma \uplus \{\#^b, u, \mathbf{f}\}, \Sigma'_{uo} = \{u, \mathbf{f}\}$;

* $Q' = \{q^u, q^f \mid q \in Q\} \cup \{q'_0, b^u, b^f\}$;

*

$$
\begin{align*}
T' = & \{(q'_0, u, q^u) \mid \delta_0(q) > 0\} \cup \{(q'_0, u, q^f) \mid \delta_0(q) > 0\} \cup \{(q^u, \#^b, q_0^u) \mid q \in F, \delta_0(q) > 0\} \\
& \cup \{(q^f, \#^b, q^f) \mid q \in Q \setminus F, \delta_0(q) > 0\} \cup \{(q^u, \#^b, b^u) \mid q \in Q \setminus F\} \\
& \cup \{b^u, \#^b, b^u\} \cup \{b^u, \#^b, b^u\} \cup \{b^f, \#^b, b^f\} \cup \{(q^f, \mathbf{f}^b, b^f) \mid q \in F\} \\
& \cup \{(q^u, a, q'^u), (q^f, a, q'^f) \mid q, q' \in Q, a \in \Sigma, \mathbf{P}_a[q, q'] > 0\}
\end{align*}
$$

* $\mathbf{P}'$ is defined by:

- For all $q \in Q$ with $\delta_0(q) > 0$), $\mathbf{P}'(q'_0, u, q^u) = \mathbf{P}'(q'_0, u, q^f) = \frac{\delta_0(q)}{2}$;

- For all $(q^u, a, q'^u) \in T'$, $\mathbf{P}'(q^u, a, q'^u) = \frac{\mathbf{P}_a[q, q']}{1+|\Sigma|}$;

- For all $(q^f, a, q'^f) \in T'$, $\mathbf{P}'(q^f, a, q'^f) = \frac{\mathbf{P}_a[q, q']}{1+|\Sigma|}$;

- For all $(q^u, \#^b, q_0^u) \in T'$, $\mathbf{P}'(q^u, \#^b, q_0^u) = \frac{\delta_0(q_0)}{1+|\Sigma|}$;

- For all $(q^f, \#^b, q_0^f) \in T'$, $\mathbf{P}'(q^f, \#^b, q_0^f) = \frac{\delta_0(q_0)}{1+|\Sigma|}$;

- For all $(q^u, \#^b, b^u) \in T'$, $\mathbf{P}'(q^u, \#^b, b^u) = \frac{1}{1+|\Sigma|}$;

- For all $(q^f, \mathbf{f}^b, b^f) \in T'$, $\mathbf{P}'(q^f, \mathbf{f}^b, b^f) = \frac{1}{1+|\Sigma|}$;

- $\mathbf{P}'(b^u, \#^b, b^u) = \mathbf{P}'(b^u, \#^b, b^u) = \frac{1}{2}$;

- $\mathbf{P}'(b^f, \#^b, b^f) = 1$.

This reduction is illustrated in Figure 4.16. In each state, the sum of the probabilities of the exiting transitions correctly sum to 1. For instance, let $q \in Q$,

$$ \sum_{(q^f, a, q') \in T'} \mathbf{P}'(q^f, a, q') = \sum_{a \in \Sigma} \sum_{q' \in Q} \frac{\mathbf{P}_a[q, q']}{1 + |\Sigma|} + \frac{1}{1 + |\Sigma|} = \frac{|\Sigma|}{1 + |\Sigma|} + \frac{1}{1 + |\Sigma|} = 1. $$
<figure><img src="image_66.png" /><figcaption>Figure 4.16: From probabilistic automata to pLTS: rectangles surround the two copies of the state space of the probabilistic automaton.</figcaption></figure>

We claim that $\mathcal{A}$ is uniformly AFF-diagnosable if and only if $\mathcal{L}_{A,1/2} = \emptyset$.
Observe first that for all $q \in Q$, $\mathcal{L}^\omega(\mathcal{A}_{qf}) \subseteq \mathcal{L}^\omega(\mathcal{A}_{qu})$ so that all faulty runs are ambiguous.

• Assume that there exists a word $w \in \Sigma^*$ such that $\mathbf{P}_A(w) > 1/2$. We prove that $\mathcal{A}$ is not uniformly $\frac{1}{2}$FF-diagnosable. So we pick arbitrary $0 < \alpha < 1$ and $n_\alpha$.

Consider the observed sequence $\sigma_n = (w^\sharp)^{n\flat}$ for some $n$ to be fixed later. As every word is accepted with positive probability by $\mathcal{A}$, it is ambiguous. Let

$$ \gamma_n = \frac{\mathbb{P}(\{\rho' \in \mathbf{C} \mid \mathcal{P}(\rho') = \sigma_n\})}{\mathbb{P}(\{\rho' \in \mathbf{F} \mid \mathcal{P}(\rho') = \sigma_n\})}. $$

Since $\mathbf{P}_A(w) > 1/2$, $\gamma_n$ fulfils $\lim_{n \to \infty} \gamma_n = \infty$.

Let $\rho_n$ be a minimal faulty run with $\mathcal{P}(\rho_n) = \sigma_n$. Let $\rho$ be a signalling run extending $\rho_n$ with $|\rho|_o = |\rho_n|_o + n_\alpha$. Then $\mathcal{P}(\rho) = \sigma_n b^{n_\alpha}$. By a straightforward examination of $\mathcal{A}$ one gets:

$$ \frac{\mathbb{P}(\{\rho' \in \mathbf{C} \mid \mathcal{P}(\rho') = \sigma_n b^{n_\alpha}\})}{\mathbb{P}(\{\rho' \in \mathbf{F} \mid \mathcal{P}(\rho') = \sigma_n b^{n_\alpha}\})} = \frac{\gamma_n 2^{-n_\alpha}}{1 + \gamma_n 2^{-n_\alpha}}. $$

Choosing $n$ such that $\gamma_n 2^{-n_\alpha} > 1$, one gets: $\text{CorP}(\rho) > 1/2$. So:

$$ \mathbb{P}(\{\rho \in \text{SR}_{n_\alpha + |\rho_n|_o} \mid \rho_n \preceq \rho \wedge \text{CorP}(\mathcal{P}(\rho)) > \frac{1}{2}\}) = \mathbb{P}(\rho) > \alpha \mathbb{P}(\rho). $$

Thus $\mathcal{A}$ is not uniformly $\frac{1}{2}$FF-diagnosable.
• Conversely assume that for every word $w \in \Sigma^*$, $\mathbf{P}_A(w) \le 1/2$. Combining this assumption with the hypothesis that $\mathbf{P}_A(w) \ge 1/4$, one deduces that for every observed sequence $\sigma \in (\Sigma \cup \{\#\})^{\mathbf{b}}$, $\text{CorP}(\sigma) \le 3/4$. On the other hand, for every minimal faulty run $\rho$, $\mathcal{P}(\rho) \in (\Sigma \cup \{\#\})^{\mathbf{b}}$.

Pick any positive $\varepsilon, \alpha$ and consider an arbitrary minimal faulty run $\rho$. The observed sequence $\sigma'$ of a faulty run $\rho'$ that extends $\rho$ fulfils $\sigma' = \mathcal{P}(\rho)^{\mathbf{b}n}$ for some $n$. After a new occurrence of $\mathbf{b}$ the fraction between the probability of correct runs with observed sequence $\sigma'\mathbf{b}$ over the probability of faulty runs with observed sequence $\sigma'\mathbf{b}$ is halved. Thus choosing $n_\alpha$ such that $\frac{3 \cdot 2^{-n_\alpha}}{1+3 \cdot 2^{-n_\alpha}} \le \varepsilon$, for all $n \ge n_\alpha$:

$$ \mathbb{P}(\{\rho' \in \mathbf{SR}_{n+|\rho|_o} \mid \rho \preceq \rho' \wedge \text{CorP}(\mathcal{P}(\rho)) \le \varepsilon\} = \mathbb{P}(\rho) \ge (1-\alpha)\mathbb{P}(\rho). $$

Thus $\mathcal{A}$ is uniformly $\varepsilon$FF-diagnosable and since $\varepsilon$ was chosen arbitrarily, $\mathcal{A}$ is uniformly AFF-diagnosable. $\square$

The undecidability of (uniform) $\varepsilon$FF- and of uniform AFF-diagnosability are due to different reasons. For (uniform) $\varepsilon$FF-diagnosability, it is mainly caused by the use of a quantitative requirement (shown through the use of $\varepsilon$). For the uniform AFF-diagnosability, the problem arises as the detection speed of the fault strongly depends on the behaviour of the system before the occurrence of the fault. Limiting the behaviour of the system before the occurrence of a fault can raise decidability results (as in initial-fault pLTS where uniform AFF-diagnosability is diagnosable as it is equivalent to AFF-diagnosability).

Thanks to Proposition 3.5, page 70, and the definition of AFF-diagnosability, we know that a system is AFF-diagnosable iff for all $\varepsilon > 0$ there exists an $\varepsilon$FF-diagnoser of the system. Limiting oneself to finite memory can sometimes bring better decidability or complexity results (in $[\text{BFH}^+14]$ for example). It is therefore natural to question if such a restriction would make uniform AFF-diagnosability decidable. There is several ways to add the finite-memory restriction to AFF-diagnosability:

1. a system is AFF-diagnosable with finite memory if for all $\varepsilon > 0$ there exists a finite-memory $\varepsilon$FF-diagnosers;

2. a system is AFF-diagnosable with finite memory if there exists $\lambda > 0$, such that for all $0 < \varepsilon < \lambda$ there exists a finite-memory $\varepsilon$FF-diagnosers;

3. a system is AFF-diagnosable with finite memory if there exists a sequence $(\varepsilon_n)_{n \in \mathbb{N}}$ such that $\forall n, \varepsilon_n > 0$, $\varepsilon_n \xrightarrow{n \to \infty} 0$ and for all $n \in \mathbb{N}$ there exists a finite-memory $\varepsilon_n$-diagnosers;

These three notions are however equivalent since if $D$ is a finite-memory $\varepsilon$FF-diagnosers for some $\varepsilon > 0$, then $D$ is a finite-memory $\varepsilon'$-diagnoser for all $\varepsilon' > \varepsilon$. Surprisingly, this restriction complexifies the problem as stated in the following proposition.

**Proposition 4.9.** *The AFF-diagnosability with finite memory problem is undecidable for pLTS.*
The proof is obtained thanks to the reduction made in the proof of Theorem 4.4. Indeed, in this particular case, we can show that the uniform property is equivalent to the finite-memory restriction.

*Proof.* Given a probabilistic automaton $\mathcal{A}$, let $\mathcal{A}$ be the pLTS built in the reduction of the proof of Theorem 4.4. We know that $\mathcal{A}$ is uniformly AFF-diagnosable if and only if $\mathcal{L}_{\mathcal{A},1/2} = \emptyset$. We show that $\mathcal{A}$ is uniformly AFF-diagnosable iff for every $\varepsilon > 0$ there exists a finite-memory $\varepsilon$FF-diagnoser of $\mathcal{A}$, which establishes the undecidability.

Assume that $\mathcal{A}$ is uniformly AFF-diagnosable. Let $\varepsilon > 0$. By definition of uniform AFF-diagnosability, there exists $n_0 \in \mathbb{N}$ such that for all minimal faulty run $\rho \in \min\mathbf{F}$ and all $n \ge n_0$, $\mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^{\varepsilon}) \le \frac{\mathbb{P}(\rho)}{2}$. As Cyl$(\rho)$ is a single infinite run, this means that $\mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^{\varepsilon}) = 0$. Let $D$ be the diagnoser that counts how many $b$ were observed and outputs $\top$ iff this number is above $n_0$ and no $\#b$ was observed after the first $b$. This diagnoser can be represented with finite memory as it only needs to count up to a fixed value $n_0$. Moreover it is an $\varepsilon$FF-diagnoser:

* correctness. if $D(w) = \top$ for some $w \in \Sigma_o \cup \{b, \#\}\*$, then there exists $w' \in \Sigma_o \cup \{\#\}\*$ such that $w = w'b^{n'}$ with $n' \ge n_0$. As in $\mathcal{A}$, every word is accepted with positive probability, there exists a minimal faulty run $\rho$ with observation $w'$. Let $\rho_f$ be the infinite run of $\text{Cyl}(\rho)$. By uniformity, $\rho_f \notin \text{FAmb}_{n'+|\rho|_o}^{\varepsilon}$. Moreover, the prefix of length $n' + |\rho|_o$ of $\rho_f$ has observation $w$. Thus $\text{CorP}(w) \le \varepsilon$.

* reactivity. The $n$ observations following a fault are $b$, and no $\#b$ can be observed after the first $b$ in a faulty run. Thus, for all $m \ge n$, $\mathbb{P}(\rho' \in \mathbf{F} \cap \text{SR}_m | D(\mathcal{P}(\rho)) =?) = 0$ which implies reactivity.

Conversely, assume that $\mathcal{A}$ is not uniformly AFF-diagnosable. There thus exists $\varepsilon > 0$ such that $\mathcal{A}$ is not uniformly $\varepsilon$FF-diagnosable. Suppose there exists a finite-memory $\varepsilon$FF-diagnoser with $m$ memory states. As $\mathcal{A}$ is not uniformly $\varepsilon$FF-diagnosable, there exists a minimal faulty run $\rho$ such that for all $n \le m + 1$, $\mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^{\varepsilon}) > 0$. Since there exists only one infinite run $\rho_f$ extending $\rho$, this means $\rho_f \in \text{FAmb}_{n+|\rho|_o}^{\varepsilon}$. Consider the observation $\mathcal{P}(\rho)^{b^{m+1}}$. The last $m+1$ memory states visited in the finite-memory diagnoser while reading this observation are denoted $s_1, \dots, s_{m+1}$. None of these memory state can claim a fault by correctness of the diagnoser and as $\rho_f \in \text{FAmb}_{n+|\rho|_o}^{\varepsilon}$ for $n \le m + 1$. Moreover, as the finite-memory diagnoser has $m$ states, there exists $i, j \le m + 1$ such that $s_i = s_j$. there thus exists a cycle labelled by a number of $b$ in the finite-memory diagnoser. By determinism of the diagnoser, it means that for all $n \in \mathbb{N}$, $D(\mathcal{P}(\rho)^{b^{m+1}}) =? $ which contradict the reactivity requirement. There thus does not exists a finite-memory $\varepsilon$FF-diagnoser. $\square$

### 2.2.2 PSPACE-hardness of exact diagnosability

In order to establish a lower bound for the complexity of exact diagnosability, we introduce a variant of language universality.
**Definition 4.7.** A language $\mathcal{L}$ over an alphabet $\Sigma$ is said eventually universal if there exists a word $v \in \Sigma^*$ such that $v^{-1}\mathcal{L} = \Sigma^*$.

Several variants of the universality problem were shown to be PSPACE-complete in [RSX12] but, to the best of our knowledge, eventual universality has not been considered.

Because of our diagnosis framework, we focus on live non-deterministic finite automata (NFA). Similarly to pLTS, an NFA is *live* if from every state there is at least one outgoing transition. The language of an NFA $A$, denoted $\mathcal{L}(A)$, is defined as the set of finite words that are accepted by $A$.

**Proposition 4.10.** Let $A$ be a *live* NFA where all states are terminal. Then deciding whether $\mathcal{L}(A)$ is eventually universal is PSPACE-hard.

*Proof.* We reduce the universality problem for NFA, which is known to be PSPACE-complete [MS72] to the eventual universality problem. Let $A = (Q, q_0, \Sigma, T, F)$ be an NFA. Starting from $A$, one builds in polynomial time the NFA $A' = (Q', q_0, \Sigma', T', Q')$ where $\Sigma' = \Sigma \uplus \{\sharp\}$, $Q' = Q \uplus \{s\}$, and

$$T' = T \cup \{(q, \sharp, q_0) \mid q \in F\} \cup \{(s, a, s) \mid a \in \Sigma\} \cup \{(q, a, s) \mid a \in \Sigma, q \not\to_A \}$$

with $q \not\to_A$ meaning that there is no transition exiting $q$ in $A$. The additional state $s$ and the associated transitions are added to ensure that $A'$ is *live*, they do not alter the accepted language.

* Assume that $\mathcal{L}(A) = \Sigma^*$. Any word $w$ over the alphabet $\Sigma'$ can be decomposed into $w = w_1\sharp w_2\sharp \dots \sharp w_n$ with $w_i \in \Sigma^*$. For each factor $w_i$, since $A$ is universal, there exists a run $\rho_i$ on $w_i$ ending in some terminal state $q_i \in F$. Therefore $w$ is accepted in $A'$ by the run $\rho_1\sharp\rho_2\sharp \dots \sharp\rho_n$. Hence $A'$ is universal, and thus eventually universal: $\varepsilon^{-1}\mathcal{L}(A') = \Sigma'^*$.

* Conversely assume that $A'$ is eventually universal and let $v \in \Sigma'^*$ be such that $v^{-1}\mathcal{L}(A') = \Sigma'^*$. Given $w \in \Sigma^*$, we consider the word $w' = v\sharp w\sharp$. Since $A'$ is eventually universal with witness $v$, $w' \in \mathcal{L}(A')$ and there exists an accepting run that can be decomposed as: $\rho\sharp\rho'\sharp q_0$. As a $\sharp$ can only be read in a final state and leads to $q_0$, the run $\rho'$, which corresponds to the word $w$, has $q_0$ as initial state, ends in a final state of $A$, and by construction of $A'$ only uses transitions of $A$. So $\rho'$ is a run of $A$ that accepts $w$. Therefore $w \in \mathcal{L}(A)$, and $A$ is universal. $\square$

Now that we established that universal eventuality is PSPACE-hard, we can use it to establish a complexity lower bound for the different exact diagnosability problems.

**Proposition 4.11.** The FF-diagnosability, FA-diagnosability and IA-diagnosability problems are PSPACE-hard.

*Proof.* The proof is by reduction from the eventual universality problem. Let $A$ be a *live* NFA over $\Sigma$, in which all states are final. One builds in polynomial time the initial-fault pLTS $\mathcal{A} = \langle q'_0, \mathcal{A}^f, \mathcal{A}^c \rangle$ depicted in Figure 4.17 where $\Sigma_o = \Sigma \uplus \{\sharp\}$, $\Sigma_u = \{u, f\}$ and all transitions outgoing a state have the same probability. $\mathcal{A}^f$ consists of a single state on
which any letter of $\Sigma$ can be read with a self loop. $\mathcal{A}^c$ is a copy of $A$ to which we add a new state $q_{\#}$ to which one can access by a transition labelled by $\#^c$ from any state of the copy of $A$.

We establish the following two implications (note that they do not use the same diagnosability notion):

* $\mathcal{A}$ is not FA-diagnosable implies $\mathcal{A}$ is eventually universal;

* $\mathcal{A}$ is eventually universal implies $\mathcal{A}$ is not FF-diagnosable.

Since FA-diagnosability implies IA-diagnosability, which implies IF-diagnosability which is equivalent to FF-diagnosability according to Theorem 3.1, page 73, this proves that all three notions are at least as hard as eventual universality.

<figure><img src="image_67.png" /><figcaption>Figure 4.17: A reduction for PSPACE-hardness of IF-, FA- and IA-diagnosability.</figcaption></figure>

* Assume that $\mathcal{A}$ is not FA-diagnosable. By Proposition 4.4, either $\mathcal{A}_{\text{FA}}$ contains a reachable BSCC $\mathcal{C}$ with some state $s = (q, U, V) \in \mathcal{C}$ such that $q \in Q_f$ and $U \neq \emptyset$ or $\mathcal{A}_{\text{FA}}$ contains a reachable BSCC $\mathcal{C}$ with some state $s = (q, U, V) \in \mathcal{C}$ such that $q \in Q_c$ and $V \neq \emptyset$. The latter case is excluded since the only correct state belonging to a BSCC of $\mathcal{A}_{\text{FA}}$ contains $q_{\#}$ as first component and $q_{\#}^c$ is only reachable by a transition labelled by $\#^c$. As this observation cannot occur in a faulty run, $q = q_{\#}^c$ implies $V = \emptyset$. Consider the former case: obviously $q = f_0$. Since $\mathcal{C}$ is a BSCC and $f_0$ is a sink state in $\mathcal{A}$, for every state $s' = (q', U', V') \in \mathcal{C}$, one has $q' = f_0$ and $U' \neq \emptyset$. Since in $f_0$ all events of $\Sigma$ are enabled, this implies that for all $w \in \Sigma^*$, there is a correct run $\rho_1$ in $\mathcal{A}$ starting from some state of $q \in U$ with observed sequence $w$. Consider an observed sequence $v \in \Sigma^*$ labelling a run in $\mathcal{A}_{\text{FA}}$ from the initial state to $s$. Then there is correct run in $\mathcal{A}$ from $q'_0$ to $q$ with observed sequence $v$. So the run $\rho = \rho_0\rho_1$ has $vw$ as observed sequence. Since $\rho = q'_0u\rho'$ with $\rho'$ a run of $\mathcal{A}$ starting from $q_0$, $vw \in \mathcal{L}(\mathcal{A})$. This holds for any word $w$, thus $v^{-1}\mathcal{L}(\mathcal{A}) = \Sigma^*$ and $\mathcal{A}$ is eventually universal.

* Assume that there exists a word $v \in \Sigma^*$ such that $v^{-1}\mathcal{L}(\mathcal{A}) = \Sigma^*$. Of course, any word extending $v$ is also a witness that $\mathcal{A}$ is eventually universal. Let $v' \in \Sigma^*$ be such that some faulty run with observed sequence $vv'$ ends in a BSCC $\mathcal{C}$ of $\mathcal{A}_{\text{FF}}$. Since $(vv')^{-1}\mathcal{L}(\mathcal{A}) = \Sigma^*$, all states of $\mathcal{C}$ are of the form $(f_0, U)$ with $U \neq \emptyset$. Therefore, by Proposition 4.2, $\mathcal{A}$ is not FF-diagnosable. $\square$

Since the lower bounds match the upper bounds, the different notions of exact diagnosability are PSPACE-complete for finite pLTS.
# 3 Diagnoser construction

When a system is shown to be diagnosable, the next step is to build a diagnoser. A diagnoser that works in every case would keep track of every run compatible with the observed sequence and give a verdict depending on the nature of this set of runs. This diagnoser, by nature, uses unbounded memory. For implementation purpose, we are rather interested in finite-memory diagnosers as defined in Section 1 of Chapter 3. We explain how to automatically build a finite-memory diagnoser for a diagnosable system. This is not possible for every notion of diagnosability however. Indeed, we showed in Proposition 3.4, page 69, that $\varepsilon$FF-diagnosers may need infinite memory. Therefore we do not develop approximate diagnosability here, and focus on exact diagnosability.

## 3.1 FF-diagnoser

We start with FF-diagnosers. These diagnosers only provide information about faulty runs. In the sequel we fix $\mathcal{A}$ a finite pLTS.

**Proposition 4.12.** If $\mathcal{A}$ is an FF-diagnosable pLTS with $n$ correct states, one can build an FF-diagnoser for $\mathcal{A}$ with at most $2^n$ memory states.

*Proof.* The idea of this proof and of all the following proofs for constructing a finite-memory diagnoser is to use the characterisation given in Section 1. For example, in order to construct the FF-diagnoser, we first build the FF-automaton of $\mathcal{A}$. Then we define the finite-memory diagnoser on its structure. Finally we show that the constructed diagnoser is indeed an FF-diagnoser thanks to the FF-diagnosability of the system.

For an FF-diagnosable pLTS $\mathcal{A}$ with $\text{FF}(\mathcal{A}) = (S, s_0, \Delta, F)$, its deterministic and complete FF-automaton, we define the finite memory diagnoser $(S, \Sigma_o, \text{up}, s_0, D_{fm})$ with $\text{up}(s, a) = s'$ if $(s, a, s') \in \Delta$ and $D_{fm}(U) = \top$ iff $U = \emptyset$. Let us show that the induced diagnoser $D$ is indeed an FF-diagnoser, and that it has at most $2^n$ memory states, where $n$ is the number of correct states of $\mathcal{A}$.

**commitment** When $U$ is empty, it remains empty forever which implies commitment.

**correctness** When $D$ outputs the verdict $\top$, $\text{FF}(\mathcal{A})$ is in the state associated with $\emptyset$. As $U$ contains the set of correct states reachable with the current observed sequence, the observed sequence is surely faulty.

**reactivity** If an infinite faulty run $\rho$ is such that $D(\mathcal{P}(\rho)) =? \ $ then, by construction of $\text{FF}(\mathcal{A})$ and definition of $D$, for every length $n \in \mathbb{N}$, there exists a finite correct signalling run $\rho_n \in \text{SR}_n$ such that $\mathcal{P}(\rho_n) = \mathcal{P}(\rho_{\downarrow n})$. Using König's lemma, since $\mathcal{A}$ is finitely branching, one can extract an infinite correct run $\rho_\infty$ such that $\mathcal{P}(\rho_\infty) = \mathcal{P}(\rho)$, so that $\rho \in \text{FAmb}_\infty$. Moreover $\mathbb{P}(\text{FAmb}_\infty) = 0$ as $\mathcal{A}$ is FF-diagnosable. Putting everything together, for every minimal faulty run $\rho$, $\mathbb{P}(\{\rho' \in \Omega \mid \rho \preceq \rho' \wedge D(\mathcal{P}(\rho')) =? \}) = 0$.

**size** The memory states are states of $\text{FF}(\mathcal{A})$, which are themselves subsets of correct states of $\mathcal{A}$. Therefore, $D$ uses at most $2^n$ memory states, with $n = |Q_c|$.
☐

We now show that the size order of the previous FF-diagnoser is optimal.

**Proposition 4.13.** *There is a family ${\mathcal{A}_n}_{n\in\mathbb{N}}$ of FF-diagnosable pLTS such that $\mathcal{A}_n$ has $2n + 2$ correct states and it admits no FF-diagnoser with less than $2^n$ states.*

<figure><img src="image_68.png" /><figcaption>Figure 4.18: An FF-diagnosable pLTS requiring an FF-diagnoser with exponential size.</figcaption></figure>

*Proof.* This proof is inspired by a similar result of lower bounds on controllers established in [HHMS13]. Consider the example of Figure 4.18 where $\Sigma_o = \{a, b, c\}$ and the initial state is $q_0$. Consider a finite faulty run including a *c* event. Its observed sequence belongs to $\mathcal{L} = \{a, b\}^* a\{a, b\}^{n-1}c^+$. Since any finite correct run has an observed sequence belonging to $\mathcal{L}' = \{a, b\}^* \cup \{a, b\}^* b\{a, b\}^{n-1}c^+$ and $\mathcal{L} \cap \mathcal{L}' = \emptyset$, $\text{FAmb}_n \uplus \text{CAmb}_n \subseteq \{\rho \mid \mathcal{P}(\rho) \in \{a, b\}^n\}$. Since $\lim_{n\to\infty} \mathcal{P}(\{\rho \mid \mathcal{P}(\rho) \in \{a, b\}^n\}) = 0$, the pLTS is FA-diagnosable and so IA-diagnosable and FF-diagnosable.

Intuitively, when a *c* is observed, any FF-diagnoser must have remembered the observable event that happened *n* steps earlier to know if the run is faulty or not. Thus, it must remember the last *n* observed events, in case a *c* event occurs.

More formally, assume there exists a diagnoser $D = (M, \Sigma, m_0, \mathbf{up}, D_{fm})$ with less than $2^n$ memory states. Then there exist two distinct words $w_1 \in \{a, b\}^n$ and $w_2 \in \{a, b\}^n$ leading to the same memory state: $\mathbf{up}(m_0, w_1) = \mathbf{up}(m_0, w_2)$. The words $w_1$ and $w_2$ differ at least from one letter say $w_1[i] = b$ and $w_2[i] = a$. Consider for $k \ge 1$, the signalling correct run $\rho_{1,k}$ corresponding to observed sequence $w_1 a^{i-1} c^k$ whose sequence of visited states is $q_0^i r_1 \dots r_n^{k+1}$ and the signalling faulty run $\rho_{2,k}$ corresponding to observed sequence $w_2 a^{i-1} c^k$ whose sequence of visited states is $q_0^i l_0 l_1 \dots l_n^{k+1}$. They also lead to the same memory state. By correctness, $D(w_1 a^{i-1} c^k) =?$. Thus for all suffixes $\rho$ of $\rho_{2,1}$, $D(\rho) =?$ contradicting the reactivity of $D$. ☐

## 3.2 FA-diagnoser

We now turn to FA-diagnosability which not only considers the diagnosis of faults but also of correct runs. We build the FA-diagnoser from the FA-automaton similarly to what was done in Proposition 4.12.
**Proposition 4.14.** A pLTS $\mathcal{A}$ is FA-diagnosable if it admits an FA-diagnoser. Moreover, if $\mathcal{A}$ is a FA-diagnosable pLTS with $n$ states, one can build an FA-diagnoser with at most $2^n$ memory states.

*Proof.* Let $\mathcal{A}$ be a pLTS. Assume first that there exists an FA-diagnoser $D$ for $\mathcal{A}$. For every $n \in \mathbb{N}$, we define $\mathrm{FD}_n = \{\rho \in \Omega \mid D(\mathcal{P}(\rho_{\downarrow n})) = \top\}$ the set of runs that are diagnosed faulty after $n$ observed events, and symmetrically $\mathrm{CD}_n = \{\rho \in \Omega \mid \forall m \ge n, D(\mathcal{P}(\rho_{\downarrow m})) = \bot\}$ the set of runs that are persistently diagnosed correct after $n$ observed events. The sequences $(\mathrm{CD}_n)_{n \in \mathbb{N}}$ and $(\mathrm{FD}_n)_{n \in \mathbb{N}}$ are non-decreasing. As $? \prec \bot$ and $? \prec \top$, for every run $\rho \in \Omega$, $D_{\inf}(\mathcal{P}(\rho)) = ?$ is equivalent to $\rho \notin \bigcup_n (\mathrm{FD}_n \cup \mathrm{CD}_n)$. Thus we have $\bigcup_{n \in \mathbb{N}} (\mathrm{FD}_n \cup \mathrm{CD}_n) = \{\rho \in \Omega \mid D_{\inf}(\mathcal{P}(\rho)) \neq ?\}$. Since $D$ is reactive, $\mathbb{P}(\{\rho \in \Omega \mid D_{\inf}(\mathcal{P}(\rho)) \neq ?\}) = 1$. Moreover, since $D$ is correct, for every $n \in \mathbb{N}$, $\mathrm{FD}_n \subseteq \mathrm{Sf}_n$ and $\mathrm{CD}_n \subseteq \mathrm{Sc}_n$. Thus for every $n \in \mathbb{N}$, $\mathbb{P}(\mathrm{FAmb}_n \cup \mathrm{CAmb}_n) = 1 - \mathbb{P}(\mathrm{Sf}_n \cup \mathrm{Sc}_n) \le 1 - \mathbb{P}(\mathrm{FD}_n \cup \mathrm{CD}_n)$ and $\lim_{n \to \infty} \mathbb{P}(\mathrm{FAmb}_n \cup \mathrm{CAmb}_n) \le 1 - \liminf_{n \to \infty} \mathbb{P}(\{\rho \in \mathrm{SR}_n \mid D(\mathcal{P}(\rho)) \neq ?\}) = 0$. This shows that $\mathcal{A}$ is FA-diagnosable.

Assume now that $\mathcal{A}$ is FA-diagnosable and has $n$ states. From $\mathrm{FA}(\mathcal{A}) = (S, s_0, \Delta, F)$ the FA-automaton of $\mathcal{A}$, we define $D = (S, \Sigma_o, s_0, \mathrm{up}, D_{fm})$ the finite-memory diagnoser where $\mathrm{up}(s, a) = s'$ if $(s, a, s') \in \Delta$, $D_{fm}((U, V)) = \top$ iff $U = \emptyset$ and $D_{fm}((U, V)) = \bot$ iff $V = \emptyset$. Let us check that $D$ is an FA-diagnoser, and that its size is at most $2^n$ if $n$ denotes the number of states of $\mathcal{A}$.

**commitment** When $U$ is empty, it remains empty forever which implies commitment.

**correctness** Let $w \in \Sigma_o^*$ be an observed sequence. If $(U, V)$ is the state in $\mathrm{FA}(\mathcal{A})$ reached after reading $w$, then recall that $U$ (resp. $V$) is the set of states in $\mathcal{A}$ that can be reached by correct (resp. faulty) signalling runs labelled by $w$. By construction, if $D(w) = \top$ then $w$ is surely faulty, and if $D(w) = \bot$ then $w$ is surely correct.

**reactivity** Let $\rho$ be a signalling run such that $D(\mathcal{P}(\rho)) = ?$. Due to the characterisation of Proposition 4.4, the strictly connected component of $\mathcal{A}_{\mathrm{FA}}$ that $\rho$ has reached cannot be a BSCC. So given some $n \in \mathbb{N}$,

$$ \mathbb{P}(\{\rho \in \Omega \mid \exists m \ge n \ D(\mathcal{P}(\rho_{\downarrow m})) = ?\}) \le \mathbb{P}(\{\rho \in \Omega \mid \rho_{\downarrow n} \text{ does not reach a BSCC}\}). $$

Thus

$$ \begin{align*} \mathbb{P}(\{\rho \in \Omega \mid D_{\inf}(\mathcal{P}(\rho)) = ?\}) &= \lim_{n \to \infty} \mathbb{P}(\{\rho \in \Omega \mid \exists m \ge n \ D(\mathcal{P}(\rho_{\downarrow m})) = ?\}) \\ &\le \limsup_{n \to \infty} \mathbb{P}(\{\rho \in \Omega \mid \rho_{\downarrow n} \text{ does not reach a BSCC}\}) \\ &= 0. \end{align*} $$

**size** $D$ has at most $2^n$ memory states because every state of $\mathrm{FA}(\mathcal{A})$ consists of a pair $(U, V)$ with $U \subseteq Q_c$ and $V \subseteq Q_f$.

□
As the pLTS of Figure 4.18 is FA-diagnosable, and since any FA-diagnoser is also an FF-diagnoser, using Proposition 4.13 we obtain the following lower bound for the size of FA-diagnosers.

**Proposition 4.15.** There is a family $\{A_n\}_{n \in \mathbb{N}}$ of FA-diagnosable pLTS such that $A_n$ has $2n + 2$ states and it admits no FA-diagnoser with less than $2^n$ memory states.

## 3.3 IA-diagnoser

We end with IA-diagnosability and build an IA-diagnoser similarly as to what was done in Proposition 4.12.

**Proposition 4.16.** If $\mathcal{A}$ is a IA-diagnosable pLTS with $n_c$ correct states and $n_f$ faulty states, one can build an IA-diagnoser with at most $2^{n_c}3^{n_f}$ states.

*Proof.* Let $\mathcal{A}$ be an IA-diagnosable pLTS. From $\mathrm{IA}(\mathcal{A}) = (S, s_0, \Delta, F)$ the IA-automaton of $\mathcal{A}$, we define $D = (S, \Sigma_o, s_0, \mathrm{up}, D_{fm})$ the finite-memory diagnoser where $\mathrm{up}(s, a) = s'$ if $(s, a, s') \in \Delta$, $D_{fm}((U, V, W)) = \top$ iff $U = \emptyset$ and $D_{fm}((U, V, W)) = \bot$ iff $W = \emptyset$. Let us prove that $D$ is indeed an IA-diagnoser for $\mathcal{A}$.

**commitment.** When $U$ is empty, it remains empty forever which implies commitment.

**correctness.** For any word $w \in \Sigma_o^*$, we denote by $(U_w, V_w, W_w)$ the state in $\mathrm{IA}(\mathcal{A})$ reached after reading $w$. For any word $w$, if $U_w = \emptyset$, by construction of $\mathrm{IA}(\mathcal{A})$, $w$ is surely faulty. Assume now that $W_w = \emptyset$ and $U_w \neq \emptyset$. Let $w'$ be the longest proper prefix of $w$ such that $W_{w'} = \emptyset$. Let $\rho$ be any signalling run with $\mathcal{P}(\rho) = w$. Assume that $\rho_{\downarrow|w'|}$ is faulty. Thus the states visited by $\rho_{\downarrow n}$ for $|w'| < n \le |w|$ were always in $W_{\rho_{\downarrow n}}$. Since $W_w = \emptyset$, this is not possible and so $\rho_{\downarrow|w'|}$ is correct. Thus every time a state with $W = \emptyset$ is visited, the length of the greatest prefix, for which all signalling subruns corresponding to this prefix are correct, is increased. This establishes correctness.

**reactivity.** Let $\rho$ be an infinite run such that $D_{sup}(\mathcal{P}(\rho)) =?$. Due to the characterisation of Proposition 4.5, either (1) the strongly connected component of $\mathcal{A}_{IA}$ that $\rho$ infinitely often visits is not a BSCC or (2) $\rho$ does not visit infinitely often all the states of this strongly connected component. The probability of such runs is null which establishes the reactivity.

**size D** has at most $2^{n_c}3^{n_f}$ memory states because every state of $\mathrm{IA}(\mathcal{A})$ consists of a triple $(U, V, W)$ with $U \subseteq Q_c$ and $V \cup W \subseteq Q_f$. Moreover, one does not keep in $V$ the states that are tracked in $W$, ensuring $V \cap W = \emptyset$. $\square$

The following lower bound can be derived from the proof of Proposition 4.13, since the pLTS of Figure 4.18 is IA-diagnosable, and because any IA-diagnoser is also an FF-diagnoser.
**Proposition 4.17.** There is a family ${\mathcal{A}_n}_{n \in \mathbb{N}}$ of IA-diagnosable pLTS such that $\mathcal{A}_n$ has $2n + 2$ states and it admits no IA-diagnoser with less than $2^n$ memory states.

The construction of an exact diagnoser can thus require exponential time, which is one class above the verification of exact diagnosability. This exponential time is only necessary if we want to build the full diagnoser though. Another possibility would be to update the state of the diagnoser on-the-fly during a run. One would only need to keep the current memory state (which has linear space), but the update process would take a polynomial time, instead of the constant time obtained when using a fully-built diagnoser.

# 4 Conclusion

In Section 1, we gave characterisations of the different notions of exact diagnosability and of one notion of approximate diagnosability for finite systems. The characterisations of the notions of exact diagnosability are of the same descriptive complexity, something that is impossible in the general case as shown in Section 3 of Chapter 3, page 77. The characterisation of the notion of approximate diagnosability has two important differences compared to the ones of exact diagnosability: (1) it depends on the exact probabilities of the system and (2) it only requires a comparison between pairs of states.

In Section 2, we gave matching upper and lower bounds for the various diagnosability problems for finite systems. These results heavily relied on the characterisations given in Section 1. Thus, as the characterisations of every notion of exact diagnosability have the same descriptive complexity, it is not surprising that they end up having the same complexity. The results on the approximate diagnosability notions are more surprising. AFF-diagnosability, the notion for which a characterisation was obtained, is decidable in polynomial time, a better complexity than what is needed for the exact diagnosability notions. This gain in complexity is obtained as, contrary to exact diagnosability where one needs to follow sets of states, for AFF-diagnosability, only pairs of states have to be compared. The comparison however depends on the exact values of the probabilities of the system, which brings a different kind of difficulty to the analysis. While this difficulty could be solved for AFF-diagnosability, it is the main reason of the undecidability of all the other notions of approximate diagnosability: (uniform) $\varepsilon$FF- and uniform AFF-diagnosability. On this point, uniform AFF-diagnosability is equivalent to the notion of AA-diagnosability introduced in [TT05] which decidability was left open (only necessary conditions were given). Our undecidability result thus answers negatively to this question.

In Section 3, we gave automatic methods to construct finite-memory diagnosers for systems that are exactly diagnosable. We also showed that the sizes of the generated diagnosers are asymptotically optimal. For approximate notions of diagnosability, there does not necessarily exist finite-memory diagnosers and deciding the existence of such a diagnoser is undecidable. When such a diagnoser does not exist, one may need unbounded memory. Depending on the form of the unbounded memory required, it can be more or less manageable (for example a counter can easily be implemented).
# Chapter 5

## Algorithmic analysis of the diagnosability of infinite pLTS

In Chapter 4, we showed how to solve diagnosability for systems that can be represented by a pLTS with finitely many states. While this encompasses many kinds of systems, this is far from being exhaustive. Often, in order to satisfy its specification, a system will require unbounded memory: for example, when the system receives and records information or requests from the environment. Observe that an infinite number of states does not mean an infinite memory *per se*, but only an unbounded one. Stacks and queues are instances of such dynamic data structures.

While allowing an infinite amount of states increases the expressive power of the model, it increases the difficulty of its study. First, the studied systems must possess a finite representation. This can be done by assuming only a finite part of the system needs to be studied (e.g. infinite systems with finite attractors [BBS06]) or by using a higher level model whose semantics is an infinite-state system (Petri nets [Mur89, Dia09, CGS14], well structured transition systems [FS01], pushdown automata [AM04, KEM06, MP09, HS10, EY12]). We study such a formalism in this chapter.

Diagnosability has already been studied for infinite-state non-stochastic systems: represented by pushdown automata [MP09] or by Petri nets [CGLS12, BHSS18]. Partially observable visibly pushdown automata is a subclass of partially observable pushdown automata for which diagnosability was studied in [MP09]; for such models, diagnosability is decidable (using the determinisation procedure of [AM04]). With a restriction on the unobservable subnet akin to our convergence assumption, [CGLS12] gives a decidable characterisation of a non-stochastic notion of diagnosability for partially observable Petri nets. However the algorithm is non-primitive recursive. The authors of [BHSS18] extend this work by considering different classes of Petri nets and reducing the complexity (EXPSPACE for the general case). However to the best of our knowledge diagnosis of probabilistic infinite-state systems has not yet been studied.

So we extend these works by considering the probabilistic variants of diagnosability. In Section 1, we study the stochastic diagnosability of partially observable probabilistic pushdown automata (POpPDA). As diagnosability is already undecidable for
non-stochastic systems [MP09], the decidability of the stochastic variants is unlikely. However the notations introduced here will be used in Section 2 where we consider a restriction of POpPDA called partially observable probabilistic visibly pushdown automata (POpVPA). This restricted class has many advantages. It naturally benefits from the numerous results which are known for POpPDA [BEKK13], especially the ones on model-checking algorithms [KEM06, EY12]. Moreover, the authors of [AM04] gave an algorithm for the determinisation of a POpVPA. PopVPA generates an infinite-state pLTS and the efficient characterisations given in Chapter 4 strongly rely on the finiteness of the models. They thus cannot be used any more. So, we use the characterisations from the Section 3 of Chapter 3 based on the *pathL* logic. However the model-checking algorithm cannot be directly applied to the formulae of the *pathL* logic. Some tricky machinery will be required to "encode" the path formulae of the *pathL* logic in the system in order to use the results of [EY12]. Finally, in Section 3, we study the diagnosability of partially observable stochastic Petri nets (POSPN), we mimic the restriction used on POpPDA in Section 2, and discuss the case of partially observable stochastic visible Petri nets (VSPN).

This chapter develops and extends some of the results from [BHL16b, LGS18].

# 1 Diagnosability of probabilistic pushdown automata

In this section we study infinite-state pLTS generated by probabilistic pushdown automata (pPDA). First, we define pPDA and the infinite-state pLTS generated by a pPDA. The pPDA model being very expressive, we show that diagnosability of pPDA is undecidable.

## 1.1 Probabilistic pushdown automata

A pPDA randomly generates infinite behaviours using a stack. This stack contains letters of a stack alphabet with the most recently added letter put at the top. Transitions of the pPDA can be conditioned by the top of the stack. Moreover, a transition can push a new element onto the stack, pop one element off it or modify the top of the stack. Let us first see an example of an infinite state pLTS, that we will be able to represent by a pPDA.

**Example 5.1.** The pLTS of Figure 5.1 represents a server that accepts jobs (event in) until it randomly decides to serve the jobs (event serve). When a job is done the result is delivered (event out). When all jobs are done, the server waits for a new batch of jobs. However randomly, the server may trigger a fault (event f) and then abort all remaining jobs (event abort). Afterwards, the server is reset (event reset).

The infinite number of states in this system comes from the unbounded number of jobs the server can receive before he starts serving them. To see this system using a stack, one could use a stack letter to represent a job and add one such letter to the stack every time a new job comes in. Dealing with a job (event out) or aborting it (event abort) removes an element of the stack.
<figure><img src="image_69.png" /><figcaption>Figure 5.1: An infinite-state pLTS that can be represented by a pPDA.</figcaption></figure>

We now define pPDA similarly to what can be found in [KEM06].

**Definition 5.1.** A probabilistic pushdown automaton (pPDA) is defined by a tuple $V = (Q, q_0, \Sigma, \Gamma, \delta, \mathbf{P})$ where:

* $Q$ is a finite set of states with $q_0$ the initial state;

* $\Sigma$ is a finite alphabet of events;

* $\Gamma$ is a finite alphabet of stack symbols including a set of bottom stack symbols $\Gamma_{\perp}$ with initial symbol $\perp_0 \in \Gamma_{\perp}$;

* $\delta \subseteq Q \times \Gamma \times \Sigma \times Q \times \Gamma^*$ is the set of transitions such that for every $(q, \gamma, a, q, w) \in \delta$, $|w| \le 2$, $\gamma \in \Gamma_{\perp}$ implies $w \in \Gamma_{\perp}(\Gamma \setminus \Gamma_{\perp})^*$ and $\gamma \notin \Gamma_{\perp}$ implies $w \in (\Gamma \setminus \Gamma_{\perp})^*$;

* $\mathbf{P}$ is the transition probability function fulfilling for every $q \in Q$ and $\gamma \in \Gamma$:

$$ \sum_{(q, \gamma, a, q', w) \in \delta} \mathbf{P}[(q, \gamma, a, q', w)] = 1. $$

A pPDA may be viewed as a pLTS equipped with a stack. The transitions of the pPDA can depend on the top symbol of the stack and modify it. The definition ensures that the stack is never empty: the bottom stack symbols $\Gamma_{\perp}$ are never removed. Moreover symbols of $\Gamma_{\perp}$ never occurs elsewhere in the stack. Let $T = (q, \gamma, a, q', w) \in \delta$ be a transition of a pPDA. If $|w| = 1$ (resp. $|w| = 2$, $|w| = 0$) then $T$ is said to be a *local* (resp. *push*, *pop*) transition. A local transition can update the top symbol and a push transition can modify the top symbol and add another symbol on top of it. Notions such as runs are defined on pPDA analogously to what was done for pLTS. We call *configuration* the pair composed by a state and a stack.

The semantics of a pPDA is the (potentially infinite) pLTS representing its behaviour. The states of this pLTS are pairs consisting of a state and a stack contents. They therefore contains all the information that are necessary in the pPDA to determine the available transitions and their probabilities.
**Definition 5.2.** A probabilistic pushdown automaton pPDA $\mathcal{V} = (Q, q_0, \Sigma, \Gamma, \delta, \mathbf{P})$ defines a pLTS $\mathcal{A}_\mathcal{V} = (Q_\mathcal{V}, (q_0, \perp), \Sigma, T_\mathcal{V}, \mathbf{P}_\mathcal{V})$ where:

* $Q_\mathcal{V} = \{(q, z) \mid q \in Q \wedge z \in \perp\Gamma^*\}$;

* $T_\mathcal{V} = \{((q, z\gamma), a, (q', zw)) \mid z\gamma \in \perp\Gamma^* \wedge (q, \gamma, a, q', w) \in \delta\}$;

* For every $((q, z\gamma), a, (q', zw)) \in T_\mathcal{V}$, $\mathbf{P}_\mathcal{V}[((q, z\gamma), a, (q', zw))] = \mathbf{P}[(q, \gamma, a, q', w)]$.

As a pPDA has a finite number of states, the associated pLTS is finitely branching.

**Example 5.2.** Figure 5.2 gives an example of a pPDA whose semantics is the pLTS from Figure 5.1. Indeed, the stack alphabet has only one letter. We could thus replace it by a counter giving the number of element in the stack. The pLTS of Figure 5.1 does exactly that by representing the configuration $(q_1, \gamma^n)$ of the semantics of the pPDA by the state $q_{1n}$ and similarly for the other configurations. A transition $t = (q, \gamma, a, q', w)$ is represented by an edge from state $q$ to state $q'$ and labelled by $\mathbf{P}[t] \cdot \gamma, a, w$.

Observe that in this example the set of states is not partitioned between faulty and correct states as from the state $f_1$ reached by a faulty run, one can go back to the initial state with the reset event (event $r$).

<figure><img src="image_70.png" /><figcaption>Figure 5.2: A pPDA generating the pLTS from Figure 5.1 and two finite of its runs.</figcaption></figure>

As for pLTS, we enlarge pPDA with partial observation features. As discussed in Section 1.3 of Chapter 2, this can be done either by partitioning the alphabet of events into observable and unobservable events or by providing a mask function associating
with every event an observation. In the previous chapters we used the partition of the
alphabet of events. Here, we use the mask function which is more appropriate for our
needs.

**Definition 5.3.** A partially observable pPDA (POpPDA) is a tuple $\langle V, \Sigma_o, \mathcal{P} \rangle$ consisting of a pPDA $V$ equipped with a mapping $\mathcal{P} : \Sigma \to \Sigma_o \cup \{\varepsilon\}$ where $\Sigma_o$ is the set of observations.

A POpPDA is diagnosable according to a notion of diagnosability if the pLTS it generates is diagnosable. As the generated pLTS are finitely branching, thanks to Theorem 3.1 a POpPDA is FF-diagnosable iff it is IF-diagnosable.

**Example 5.3.** Consider the pPDA $V$ of Figure 5.2, we define $\Sigma_o = \{\text{in}, \text{out}, \text{loc}, \text{reset}\}$ and two observation masks $P_1$ and $P_2$ with $P_1(\text{in}) = \text{in}, P_1(\text{serve}) = P_1(\text{empty}) = P_1(\text{reset}) = \text{loc}, P_1(\text{abort}) = P_1(\text{out}) = \text{out}$ and $P_1(\text{f}) = \varepsilon, P_2(\text{reset}) = \text{reset}$ and for every event $t \neq \text{reset}, P_2(t) = P_1(t)$. $\langle V, \Sigma_o, P_1 \rangle$ and $\langle V, \Sigma_o, P_2 \rangle$ are two POpPDA differentiated only by the observation of the event reset. As a faulty run will inevitably contain a reset and a correct run that leaves $q_0$ will contain a serve, the POpPDA $\langle V, \Sigma_o, P_2 \rangle$ which distinguishes these two events is diagnosable for every non-uniform exact notion of diagnosability. However, the POpPDA $\langle V, \Sigma_o, P_1 \rangle$ is not diagnosable as serving the requests and going back to $q_0$ has the same observation as making a fault, aborting the requests and going back to $q_0$.

## 1.2 Undecidability of diagnosability for POpPDA

Unfortunately, for every notion of diagnosability, the diagnosability problem for POpPDA is undecidable. The undecidability can be obtained by adapting the proof for diagnosability of *non-probabilistic* pushdown automata [MP09]. However, in order to show how robust the result is, we rather reduce from the Post Correspondence Problem (PCP). An instance of PCP is given by an integer $n \in \mathbb{N}$ and two families of non-empty words $\{v_i\}_{i \le n}$ and $\{w_i\}_{i \le n}$ on the alphabet $\{a, b\}$. The following question is undecidable [Pos46]: does there exist $k > 0$ and $i_1, \dots, i_k \in \{1, \dots, n\}$ such that $w_{i_1} \dots w_{i_k} = v_{i_1} \dots v_{i_k}$?

We show in Theorems 5.1 and 5.2 that undecidability already holds for two (incomparable) subclasses of POpPDA with restriction on what is observable and on the number of phases of any run. A *phase* is a portion of a run in which the stack either never decreases or never increases.

**Theorem 5.1.** The diagnosability problems are undecidable for POpPDA even when (1) a local transition does not update the top of the stack, (2) every event labelling a push transition is fully observable and corresponds to the pushed symbol, and (3) every run has at most two phases.

The use of the stack is obviously central to the proof of the undecidability. Moreover
conditions (1) and (2) limit the ability of push and local transitions to silently manip-
ulate the stack. There is no such limitation for pop transitions however as the proof of
undecidability heavily rely on hiding when the pop transitions are performed.
Let us sketch the proof. We reduce the PCP problem to the diagnosability problem. To do so, the POpPDA we build, from a PCP instance $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$, is divided in three parts. In the first one, it will select and push onto its stack a sequence of numbers, $i_1...i_k$, with $\forall j \le k, i_j \le n$. Then it goes randomly to one of the two other parts of the POpPDA, one part being accessed by a faulty transition. Each of these two parts is associated with a family of words of the PCP instance. Once it reached one of these parts, say the one associated with the $w_i$, the run will read the words of $w_i$ induced by the numbers pushed on the stack. The resulting observation is $w = w_{i_1}...w_{i_k}$. On the other part, the observation is similarly $v = v_{i_1}...v_{i_k}$. The fault can be detected if and only if $v \ne w$. Having the pop transition undetected is fundamental as it allows to hide when the word $w_{i_j}$ starts being read.

*Proof.* Let $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$ be a PCP instance In this proof, we let $\ell_i$ (resp. $m_i$) be the length of $v_i$ (resp. $w_i$). Also, given a word $w$ and $k \le |w|$ we use $w[k]$ to denote the $k^{th}$-letter of $w$.

We build a pPDA $\mathcal{V} = (Q, \Sigma, \Gamma, \delta, \mathbf{P})$ as follows:

* $Q = \{q_0, q_c, q_s, f_s\} \cup \{q_i^k | 1 \le i \le n, 1 \le k \le \ell_i\} \cup \{f_i^k | 1 \le i \le n, 1 \le k \le m_i\}$;

* $\Sigma = \{1, ..., n, \mathfrak{h}, u, r, \mathbf{f}, a, b\}$;

* $\Gamma = \{1, ..., n, \perp_0\}$ with $\Gamma_{\perp} = \{\perp_0\}$;

* $\delta$ consists of the following transitions:

$$ \begin{aligned} & \{(q_0, \perp_0, x, \perp_0 x, q_c) \mid 1 \le x \le n\} \cup \{(q_c, x, y, xy, q_c) \mid 1 \le x, y \le n\} \\ & \cup \{(q_i^k, z, v_i[k], z, q_i^{k+1}) \mid 1 \le i \le n, 1 \le k < \ell_i, z \in \{\perp_0, 1, \dots, n\}\} \\ & \cup \{(f_i^k, z, w_i[k], z, f_i^{k+1}) \mid 1 \le i \le n, 1 \le k < m_i, z \in \{\perp_0, 1, \dots, n\}\} \\ & \cup \{(q_i^{\ell_i}, z, v_i[\ell_i], z, q_s) \mid 1 \le i \le n, z \in \{\perp_0, 1, \dots, n\}\} \cup \{(q_s, x, r, \varepsilon, q_x^1) \mid 1 \le x \le n\} \\ & \cup \{(f_i^{m_i}, z, w_i[m_i], z, f_s) \mid 1 \le i \le n, z \in \{\perp_0, 1, \dots, n\}\} \cup \{(f_s, x, r, \varepsilon, f_x^1) \mid 1 \le x \le n\} \\ & \cup \{(q_c, x, u, x, q_s), (q_c, x, \mathbf{f}, x, f_s) \mid 1 \le x \le n\} \cup \{(q_s, \perp_0, \mathfrak{h}, \perp_0, q_s), (f_s, \perp_0, \mathfrak{h}, \perp_0, f_s)\}. \end{aligned} $$

* $\mathbf{P}$ assigns arbitrary positive probabilities to transitions in $\delta$:

$$ \mathbf{P}(q, \gamma, a, q', w) > 0 \Leftrightarrow (q, \gamma, a, q', w) \in \delta \text{ and } \sum_{(q, \gamma, a, q', w) \in \delta} \mathbf{P}[(q, \gamma, a, q', w)] = 1. $$

We further consider the POpPDA $\langle \mathcal{V}, \Sigma_o, \mathcal{P} \rangle$ with $\Sigma_o = \Sigma \setminus \{r, u, \mathbf{f}\}$, and the masking function satisfies $\mathcal{P}(u) = \mathcal{P}(r) = \mathcal{P}(\mathbf{f}) = \varepsilon$ and $\mathcal{P}(x) = x$ for any other event $x$. This POpPDA is represented in Figure 5.3.

Let us prove that the instance of the PCP is positive if and only if the POpPDA is IF-, IA-, FA- and AFF-diagnosable.

First, observe that $\mathfrak{h}$ almost surely occurs in an infinite run of the pPDA $\mathcal{V}$. Thus, for any $\varepsilon > 0$, there exists $N_{\varepsilon} \in \mathbb{N}$ such that the measure of signalling runs with observable length $N_{\varepsilon}$ that reach configurations $(q_s, \perp_0)$ or $(f_s, \perp_0)$ by an event $\mathfrak{h}$ is at least $1 - \varepsilon$.
• Assume that there exists a solution $i_1, \dots, i_k$ to the PCP instance $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$. Consider in the POpPDA the faulty run:

$$ \rho_f = q_0(i_j q_c)_{j \le k} \mathbf{f}(f_s r(f_{ij}^p w_{ij}[p])_{p \le m_{ij}})_{j \le k} (f_s \mathfrak{h})^\omega, $$

and the correct run:

$$ \rho_c = q_0(i_j q_c)_{j \le k} u(q_s r(q_{ij}^p v_{ij}[p])_{p \le l_{ij}})_{j \le k} (q_s \mathfrak{h})^\omega. $$

<figure><img src="image_71.png" /><figcaption>Figure 5.3: A POpPDA for the proof of Theorem 5.1.</figcaption></figure>

These two runs have the same observed sequence: $\mathcal{P}(\rho_f) = \mathcal{P}(\rho_c) = i_1 \dots i_k w \mathfrak{h}^\omega$ with $w = w_{i_1} \dots w_{i_k} = v_{i_1} \dots v_{i_k}$. Therefore, $\rho_f$ is an infinite ambiguous faulty run. Given that $\mathcal{P}(\rho_f) > 0$, we deduce that the POpPDA $(\mathcal{V}, \Sigma_o, \mathcal{P})$ is not IF-diagnosable. From Theorem 3.1, it is also neither IA-diagnosable nor FA-diagnosable. Moreover, after the occurrence of a fault, there is no probabilistic choice. As a consequence the correctness proportion is either 0 or 1/2. As the correctness proportion of the faulty prefixes of $\rho_f$ is never 0 as seen above, the POpPDA is not AFF-diagnosable.
• Conversely, assume that the PCP instance $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$ has no solution. Let $\varepsilon > 0$, let $N_\varepsilon \in \mathbb{N}$ be the integer obtained with our earlier observation. Consider a correct run $\rho_c$ with observable length $N_\varepsilon$, ending in $(q_s, \perp_0)$ and containing at least an occurrence of $\mathfrak{h}$. Its observed sequence is of the form $\mathcal{P}(\rho_c) = i_1 \dots i_k v_{i_1} \dots v_{i_k} \mathfrak{h}^m$ for some $i_1, \dots, i_k, m$. Due to the fact that $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$ has no solution, no faulty run can have the same observed sequence. Therefore, $\rho_c$ is surely correct. Symmetrically, any faulty run ending in $(f_s, \perp_0)$ after an occurrence of $\mathfrak{h}$ is surely faulty. We thus conclude that, for any $\varepsilon > 0$, there exists $N_\varepsilon \in \mathbb{N}$ such that $\mathbb{P}(\mathsf{FAmb}_{N_\varepsilon} \uplus \mathsf{CAmb}_{N_\varepsilon}) \le \varepsilon$. As a consequence, the POpPDA $\langle \mathcal{V}, \Sigma_o, \mathcal{P} \rangle$ is FA-diagnosable. By Theorem 3.1 it is also IA-diagnosable, IF-diagnosable and AFF-diagnosable. $\square$

A similar undecidability result holds for a class of POpPDA in which pop events are fully observable, and the number of phases is constant:

**Theorem 5.2.** The diagnosability problems are undecidable for POpPDA even when (1) a local transition does not update the top of the stack, (2) every event labelling a pop transition is fully observable and corresponds to the popped symbol, and (3) every run has at most two phases.

*Proof.* The proof follows the same line as the one for Theorem 5.1. The difference is that instead of choosing first the words that will be read by pushing them on the stack and later popping them off discreetly, the pPDA reads the words and silently push on the stack which words were read and at the end pop them off and verify if the same sequence could indeed be used for both family of words.

From an instance $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$ of PCP, let us define a pPDA $\mathcal{V} = (Q, \Sigma, \Gamma, \delta, \mathbf{P})$ where:

• $Q = \{q_0, q_s, f_s, q_e, f_e\} \cup \{q_i^k \mid 1 \le i \le n, 1 \le k \le \ell_i\} \cup \{f_i^k \mid 1 \le i \le n, 1 \le k \le m_i\}$;

• $\Sigma = \{1, \dots, n, \mathfrak{h}, u, c, \mathbf{f}, a, b\}$;

• $\Gamma = \{1, \dots, n, \perp_0\}$ with $\Gamma_\perp = \{\perp_0\}$;

• $\delta$ consists of the following transitions:

$$ \begin{aligned} & \{(q_0, \perp, u, \perp, q_s), (q_0, \perp, \mathbf{f}, \perp, f_s), (q_e, \perp, \mathfrak{h}, \perp, q_e), (f_e, \perp, \mathfrak{h}, \perp, f_e)\} \\ & \cup \{(q_i^k, z, v_i[k], z, q_i^{k+1}) \mid 1 \le i \le n, 1 \le k < \ell_i, z \in \{\perp, 1, \dots, n\}\} \\ & \cup \{(f_i^k, z, w_i[k], z, f_i^{k+1}) \mid 1 \le i \le n, 1 \le k < m_i, z \in \{\perp, 1, \dots, n\}\} \\ & \cup \{(q_i^{\ell_i}, z, v_i[\ell_i], z, q_s) \mid 1 \le i \le n, z \in \{\perp, 1, \dots, n\}\} \\ & \cup \{(f_i^{m_i}, z, w_i[m_i], z, f_s) \mid 1 \le i \le n, z \in \{\perp, 1, \dots, n\}\} \\ & \cup \{(q_s, z, c, zx, q_x^1) \mid z \in \{\perp, 1, \dots, n\}, x \in \{1, \dots, n\}\} \\ & \cup \{(f_s, z, c, zx, f_x^1) \mid z \in \{\perp, 1, \dots, n\}, x \in \{1, \dots, n\}\} \\ & \cup \{(q_s, x, x, \varepsilon, q_e) \mid x \in \{1, \dots, n\}\} \cup \{(f_s, x, x, \varepsilon, f_e) \mid x \in \{1, \dots, n\}\} \\ & \cup \{(q_e, x, x, \varepsilon, q_e) \mid x \in \{1, \dots, n\}\} \cup \{(f_e, x, x, \varepsilon, f_e) \mid x \in \{1, \dots, n\}\}. \end{aligned} $$
• P assigns arbitrary positive probabilities to transitions in $\delta$.

We further consider the POpPDA $(\mathcal{V}, \Sigma_o, \mathcal{P})$ with $\Sigma_o = \Sigma \setminus \{c, u, \mathbf{f}\}$, and the masking function satisfies $\mathcal{P}(u) = \mathcal{P}(c) = \mathcal{P}(\mathbf{f}) = \varepsilon$ and $\mathcal{P}(x) = x$ for any other event $x$. This POpPDA is represented in Figure 5.4.

<figure><img src="image_72.png" /><figcaption>Figure 5.4: A POpPDA for the proof of Theorem 5.2.</figcaption></figure>

Let us prove that the instance of the PCP is positive if and only if the POpPDA is IF-, IA-, FA- and AFF-diagnosable.

First, observe that $\mathfrak{h}$ almost surely occurs in an infinite run of the pPDA $\mathcal{V}$. Thus, for any $\varepsilon > 0$, there exists $N_\varepsilon \in \mathbb{N}$ such that the measure of signalling runs with observable length $N_\varepsilon$ that reach configurations $(q_e, \perp_0)$ or $(f_e, \perp_0)$ by an event $\mathfrak{h}$ is at least $1 - \varepsilon$.

• Assume that there exists a solution $i_1, \dots, i_k$ to the PCP instance $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$. Consider the faulty run:

$$ \rho_f = q_0 \mathbf{f} f_s (c(f_{ij}^p w_{ij}[p])_{p \le m_{ij}} f_s)_{j \le k} (i_j f_e)_{j \le k} (\mathfrak{h} f_e)^\omega , $$

and the correct run:

$$ \rho_c = q_0 u q_s (c(q_{ij}^p v_{ij}[p])_{p \le l_{ij}} q_s)_{j \le k} (i_j q_e)_{j \le k} (\mathfrak{h} q_e)^\omega . $$
These two runs have the same observed sequence: $\mathcal{P}(\rho_f) = \mathcal{P}(\rho_c) = w_1 \dots i_k \mathcal{h}^\omega$ with $w = w_{i_1} \dots w_{i_k} = v_{i_1} \dots v_{i_k}$. Therefore, $\rho_f$ is an infinite ambiguous faulty run. Given that $\mathbb{P}(\rho_f) > 0$, we deduce that the POpPDA $\langle \mathcal{A}, \Sigma_o, \mathcal{P} \rangle$ is not IF-diagnosable. From Theorem 3.1, it is also neither IA-diagnosable nor FA-diagnosable. Moreover, after reaching the state $f_e$ or $q_e$, there is no probabilistic choice. As a consequence the sequence of the correctness proportion of the faulty prefixes of $\rho_f$ is stationary. As it is never 0 as seen above, the POpPDA is not AFF-diagnosable.

* Conversely, assume that the PCP instance $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$ has no solution. Let $\varepsilon > 0$, let $N_\varepsilon \in \mathbb{N}$ be the integer obtained with our earlier observation. Consider a correct run $\rho_c$ with observable length $N_\varepsilon$ ending in $(q_e, \perp_0)$ and with an occurrence of $\mathcal{h}$. Its observed sequence is of the form $v_{i_1} \dots v_{i_k} i_1 \dots i_k \mathcal{h}^m$ for some $i_1, \dots, i_k, m$. Due to the fact that $(n, \{v_i\}_{i \le n}, \{w_i\}_{i \le n})$ has no solution, no faulty run can have the same observed sequence. Therefore, $\rho_c$ is surely correct. Symmetrically, any faulty run ending in $(f_e, \perp_0)$ by an occurrence of $\mathcal{h}$ is surely faulty. We thus conclude that, for any $\varepsilon > 0$, there exists $N_\varepsilon \in \mathbb{N}$ such that $\mathbb{P}(\mathsf{FAmb}_{N_\varepsilon} \uplus \mathsf{CAmb}_{N_\varepsilon}) \le \varepsilon$. As a consequence, the POpPDA $\langle \mathcal{V}, \Sigma_o, \mathcal{P} \rangle$ is FA-diagnosable. By Theorem 3.1 it is also IA-diagnosable, IF-diagnosable and AFF-diagnosable. $\square$

# 2 Diagnosability of probabilistic visibly pushdown automata

As diagnosability is undecidable for pPDA, we now turn to a more restrictive model: probabilistic visibly pushdown automata (pVPA) [AM04]. While keeping a significant expressive power, pVPA is a natural subclass of pushdown automata that is more tractable than the general model and which language has many of the desirable properties that regular languages have. In particular, there exists a method for the determinisation of a non-deterministic visibly pushdown automaton [AM04].

We formally define pVPA and describe how to build a diagnosis-oriented determinisation of a pVPA. Then, we give a decision procedure for diagnosability and study the hardness of the diagnosability problems.

## 2.1 Probabilistic visibly pushdown automata and diagnosis-oriented determinisation

A pVPA is a pPDA where events are partitioned into three sets depending on if they correspond to push, pop, or local transitions.

**Definition 5.4.** A probabilistic visibly pushdown automaton (pVPA) is a pPDA $\mathcal{V} = (Q, q_0, \Sigma, \Gamma, \delta, \mathbf{P})$ whose event alphabet is partitioned into local, push and pop events $\Sigma = \Sigma_{\mathcal{h}} \uplus \Sigma_{\mathcal{h}'} \uplus \Sigma_{\mathcal{b}}$ and such that for every transition $T = (q, \gamma, a, q', w) \in \delta$, $T$ is a local (resp. push, pop) transition iff a is a local (resp. push, pop) event.

A pVPA without the transition probability function $\mathbf{P}$ is called a visibly pushdown automata (VPA).

The definitions of pPDA carry on to pVPA in particular the semantics of a pVPA is an infinite-state finitely-branching pLTS.
**Example 5.4.** Consider the pPDA of Figure 5.2. This pPDA is a pVPA as shown by the partition of events given by $\Sigma_{\#} = \{in\}$, $\Sigma_{\flat} = \{out, abort\}$ and $\Sigma_{\natural} = \{serve, empty, reset, f\}$.

To define partially observable pVPA, we equip a pVPA with a mask function and require that only local events may be unobservable, and that pushes and pops can still be distinguished. As a consequence, given the observed sequence of one run, one can deduce the height of the stack as the difference between pushes and pops, plus one (the bottom symbol).

**Definition 5.5.** A partially observable pVPA (POpVPA) is a tuple $(\mathcal{V}, \Sigma_o, \mathcal{P})$ consisting of a pVPA $\mathcal{V}$ equipped with a mapping $\mathcal{P}: \Sigma \to \Sigma_o \cup \{\varepsilon\}$ such that:

* $\Sigma_o = \Sigma_{o,\#} \uplus \Sigma_{o,\flat} \uplus \Sigma_{o,\flat}$ is the set of observations;

* $\mathcal{P}(\Sigma_{\#}) \subseteq \Sigma_{o,\#} \cup \{\varepsilon\}$, $\mathcal{P}(\Sigma_{\flat}) \subseteq \Sigma_{o,\flat}$ and $\mathcal{P}(\Sigma_{\flat}) \subseteq \Sigma_{o,\flat}$.

When we aimed to verify the diagnosability of finite pLTS in Chapter 4, one of the first step was to build a diagnosis-oriented determinisation of the pLTS (see Definition 4.1, page 91). While this could not be done for pPDA, a determinisation for pVPA was established by Alur and Madhusudan [AM04]. Following the same approach, we now explain how to adapt the determinisation of [AM04] for diagnosability. For a pVPA $\mathcal{V}$, its determinisation is called the estimate VPA of $\mathcal{V}$ and is denoted $\mathcal{A}(\mathcal{V})$. As in the finite case, we need tags that reflect the category of runs (faulty or correct) given an observed sequence with a distinction between “old” and “young” faulty runs. Due to its technicality, we postpone the formal definition of $\mathcal{A}(\mathcal{V})$: we first explain some features of the construction and illustrate them on an example (represented in Figure 5.5).

**States and stack symbols.** The VPA $\mathcal{A}(\mathcal{V})$ tracks all runs with same observation in parallel memorising their status w.r.t. faults. More precisely to the current set of runs corresponds the symbol on the top of the stack which is a set of tuples where each tuple is written as a fraction $\frac{\gamma, X, q}{\gamma, \neg, X, \neg, q, \neg}$. Let us describe the meaning of this tuple:

* $q$ is the current state of the run and $\gamma$ is the symbol on the top of its stack;

* $X \in \mathrm{Tg} = \{U, V, W\}$ is the status of the run: $U$ for a correct run, $V$ for a young faulty run and $W$ for an old faulty run;

* The denominator $(\gamma^{-}, X^{-}, q^{-})$, is related to the configuration just after the last push event of the run: $\gamma^{-}$ is the stack symbol under the top symbol, while $X^{-}$ is the status of the run reaching this configuration and $q^{-}$ the state of this configuration.

A priori, a single state *run* would be enough. However the simulation of a pop event in the original VPA is performed in two steps requiring some additional states that we explain later.

**Example 5.5.** The initial configuration of the VPA $\mathcal{A}(\mathcal{V})$ of Figure 5.5 ($\mathrm{run}, |\{\substack{\perp_0, U, q_0 \\ \perp_0, U, q_0}\}|)$ corresponds to the empty run represented by a singleton. The denominator of bottom stack symbols is by convention $(\perp_0, U, q_0)$ and is irrelevant for specifying the transitions of $\mathcal{A}(\mathcal{V})$.
$$ 
\begin{aligned}
a_0^X &= \{\underline{\perp, X, q_0}\}, a_1^X = \{\gamma, \underline{X, q_0}\}, a_\infty^X = \{\gamma, \underline{X, q_0}\}, b_1^X = \{\gamma, \underline{X, q_1}\}, b_\infty^X = \{\gamma, \underline{X, q_1}\} \\
c_0^X &= \{\underline{\perp, X, q_1}, \underline{\perp, X, f_1}\}, c_1^X = \{\gamma, \underline{X, q_1}, \gamma, \underline{X, f_1}\}, c_\infty^X = \{\gamma, \underline{X, q_1}, \gamma, \underline{X, f_1}\}, \quad X \in \{U, W\}
\end{aligned}
$$

<figure><img src="image_73.png" /><figcaption>Figure 5.5: The VPA $\mathcal{A}(V)$ associated with the POpVPA $\langle V, \Sigma_o, \mathcal{P}_2 \rangle$ of Example 5.3 with two runs. The tag V was ignored to remove redundancy and simplify the figure.</figcaption></figure>
**Tag updates.** Let us explain how the tag X of an item $\frac{\gamma, X, q}{\gamma^-, X^-, q^-}$ of the current stack symbol is determined. If this item corresponds to a correct run then X = U. When after a transition of $\mathcal{A}(\mathcal{V})$ a (tracked) correct run becomes faulty, there are two cases. Either there was no tag W in (the numerators of items of) the top stack symbol of the stack then the run is tagged by W. Otherwise it is tagged by V meaning that it is a young faulty run. The tag V (young) becomes W (old) when, in the previous state, there was no tag W in the top stack symbol. A tag W is unchanged along the run.

**Local transitions.** Given an observed local event $o \in \Sigma_{o,\#}$, from the state *run* with top stack symbol *bel*, there is a local transition (*run*, *bel*, *o*, *run*, *bel'*') in $\mathcal{A}(\mathcal{V})$ looping over *run* that encodes the possible signalling runs with observation *o* in $\mathcal{V}$. More precisely for every transition sequence $(q, \alpha) \stackrel{o}{\Rightarrow} (r, \beta)$ in $\mathcal{V}$ (i.e. a sequence of unobservable local events ended by an event *e* with $\mathcal{P}(e) = o$) and $\frac{\alpha, X, q}{\alpha^-, X^-, q^-} \in bel$ one inserts $\frac{\beta, Y, r}{\alpha^-, X^-, q^-}$ in *bel'*. The value of Y follows the rules of tag updates.

**Example 5.6.** In the VPA $\mathcal{A}(\mathcal{V})$ of Figure 5.5 there are several transitions corresponding to the transition $(q_0, \gamma, \text{serve}, q_1, \gamma)$ of $\mathcal{V}$ including $(\text{run}, \{\frac{\gamma, U, q_0}{\gamma, U, q_0}\}, \text{loc}, \text{run}, \{\frac{\gamma, U, q_1}{\gamma, U, q_0}\})$. For example, the runs represented in Figure 5.5 use this transition.

**Push transitions.** Given an observed push event $o \in \Sigma_{o,\#}$, from the state *run* with top stack symbol *bel*, there is a push transition (*run*, *bel*, *o*, *run*, *bel'*'bel''') in $\mathcal{A}(\mathcal{V})$ looping over *run* that encodes the possible signalling runs with observation *o* in $\mathcal{V}$. More precisely for every transition sequence $(q, \alpha) \stackrel{o}{\Rightarrow} (r, \beta^{-} \beta)$ in $\mathcal{V}$ and $\frac{\alpha, X, q}{\alpha^-, X^-, q^-} \in bel$ one inserts $\frac{\beta^{-}, Y, r}{\alpha^-, X^-, q^-}$ in *bel'* and $\frac{\beta, Y, r}{\beta^{-}, Y, r}$ in *bel''*. The value of Y follows the rules of tag updates.

**Example 5.7.** In Figure 5.5 several transitions of $\mathcal{A}(\mathcal{V})$ correspond to the transition $(q_0, \perp_0, \text{in}, q_0, \perp_0 \gamma)$ of $\mathcal{V}$, including $(\text{run}, \{\frac{\perp_0, U, q_0}{\perp_0, U, q_0}\}, \text{in}, \text{run}, \{\frac{\perp_0, U, q_0}{\perp_0, U, q_0}\}\{\frac{\gamma, U, q_0}{\perp_0, U, q_0}\})$ and several transitions of $\mathcal{A}(\mathcal{V})$ correspond to the transition $(q_0, \gamma, \text{in}, q_0, \gamma \gamma)$ of $\mathcal{V}$, including $(\text{run}, \{\frac{\gamma, U, q_0}{\perp_0, U, q_0}\}, \text{in}, \text{run}, \{\frac{\gamma, U, q_0}{\perp_0, U, q_0}\}\{\frac{\gamma, U, q_0}{\gamma, U, q_0}\})$. Here, the specification of the tag updates is straightforward since it does not involve faulty runs. The runs represented in Figure 5.5 use these two transitions from the initial state.

**Pop transitions.** Given an observed pop event $o \in \Sigma_{o,b}$, from the state *run* with top stack symbol *bel*, the “pop operation” is performed by a sequence of two transitions: a pop transition labelled by *o* reaching another state that contains some information. This information is then used by the next (local) transition labelled by $\varepsilon$ to move back to state *run* with a consistent stack symbol. Given an intermediate stack symbol, there is exactly one possible such transition. Thus despite these transitions, $\mathcal{A}(\mathcal{V})$ is still deterministic. The first transition (*run*, *bel*, *o*, $\ell, \varepsilon$) in $\mathcal{A}(\mathcal{V})$ is specified as follows. The next state $\ell$ is a set of items of the following shape $\frac{X, q}{\alpha^-, X^-, q^-}$. More precisely for every transition sequence $(q, \alpha) \stackrel{o}{\Rightarrow} (r, \varepsilon)$ in $\mathcal{V}$ (i.e. a sequence of unobservable local events ended by an event *e* with $\mathcal{P}(e) = o$) and $\frac{\alpha, X, q}{\alpha^-, X^-, q^-} \in bel$ one inserts $\frac{Y, r}{\alpha^-, X^-, q^-}$ in $\ell$. The value of Y follows the rules of tag updates. A transition $(\ell, bel, \varepsilon, \text{run}, bel')$ is specified as follows. For every $\frac{X', q'}{\gamma, X, q'}$ in $\ell$ and $\frac{\gamma, X, q}{\gamma^-, X^-, q^-}$ in *bel* (i.e. the denominator of the first fraction and the numerator of the second fraction match), one inserts $\frac{\gamma, X', q'}{\gamma^-, X^-, q^-}$ in *bel'*.
**Example 5.8.** Let us describe how the pop is performed by two transitions in the runs of the VPA of Figure 5.5 from the state reached after event serve. From $q_1$ with $\gamma$ as top of the stack there are two transitions whose observation is pop: $(q_1, \gamma, \text{out}, q_1, \varepsilon)$ and $(q_1, \gamma, \text{abort}, f_1, \varepsilon)$. Thus starting from run with top stack symbol $\{\frac{\gamma, U, q_1}{\gamma, U, q_0}\}$, one reaches state $\ell = \{\frac{U, q_1}{\gamma, U, q_0}, \frac{W, f_1}{\gamma, U, q_0}\}$. The faulty run is tagged with W as there was no tag W in the former top stack symbol. In the next configuration, the top stack symbol is $\{\frac{\gamma, U, q_0}{\perp_0, U, q_0}\}$. So the transition labelled by $\varepsilon$ moves back to state run with updated top stack symbol $\{\frac{\gamma, U, q_1}{\perp_0, U, q_0}, \frac{\gamma, W, f_1}{\perp_0, U, q_0}\}$.

We now give the definition of the estimate VPA $\mathcal{A}(\mathcal{V})$ associated with a given POpVPA $\mathcal{V}$. Let $\mu \in \{g, c, f\}$ we write $(q, \gamma) \stackrel{\circ}{\Rightarrow}_{\mu} (q', w)$ with $o \in \Sigma_o$ if when $\mu = g$ (resp. $c, f$), there exists a (resp. correct, faulty) run of transitions starting from $(q, \gamma)$ to $(q', w)$ such that all transitions are unobservable except the last one labelled by $e$ with $\mathcal{P}(e) = o$. Let $\rho$ be such a run then we also write $(q, \gamma) \stackrel{\rho}{\Rightarrow}_{\mu} (q', w)$ All transitions of such runs are local except the last one whose type depends on the type of $o$.

**Definition 5.6.** Given $\langle \mathcal{V}, \mathcal{P}, \Sigma_o \rangle$ a POpVPA with $\mathcal{V} = (Q, \Sigma, \Gamma, \delta, \mathbf{P})$, its estimate VPA is the deterministic VPA $\mathcal{A}(\mathcal{V}) = (Q^e, \Sigma_o, \Gamma^e, \delta^e)$ defined by:

* $Q^e = \{\text{run}\} \uplus (2^{\Gamma \times (\mathcal{T}\mathbf{g} \times Q^2)} \setminus \emptyset)$ is the set of states with initial state $q_0^e = \text{run}$;

* $\Gamma^e = 2^{(\Gamma \times \mathcal{T}\mathbf{g} \times Q^2)} \setminus \emptyset$ is the stack alphabet with set of bottom stack symbols $\Gamma_{\perp}^e = 2^{\text{Init}} \setminus \emptyset$ where $\text{Init} = \{\underset{\perp_0, U, q_0}{\alpha, X, q} \mid (X, q) \in \mathcal{T}\mathbf{g} \times Q\}$ and initial stack symbol $\perp_0^e = \{\underset{q_0, U, \perp_0}{\alpha, U, \perp_0}\}$;

* The transition relation $\delta^e$ is defined as follows.

**local transitions** $(\text{run}, \text{bel}, o, \text{run}, \text{bel}') \in \delta^e$ if:

* $\frac{\beta, U, r}{\alpha^-, U, q^-} \in \text{bel}'$ iff there exists $\frac{\alpha, U, q}{\alpha^-, U, q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_c (r, \beta)$.

* If W occurs in bel, $\frac{\beta, W, r}{\alpha^-, X, q^-} \in \text{bel}'$ iff there exists $\frac{\alpha, W, q}{\alpha^-, X, q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_g (r, \beta)$.

* If W occurs in bel, $\frac{\beta, V, r}{\alpha^-, X, q^-} \in \text{bel}'$ iff

(1) there exists $\frac{\alpha, U, q}{\alpha^-, U, q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_f (r, \beta)$ or

(2) there exists $\frac{\alpha, V, q}{\alpha^-, X, q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_g (r, \beta)$.

* If W does not occur in bel, $\frac{\beta, W, r}{\alpha^-, X, q^-} \in \text{bel}'$ iff

(1) there exists $\frac{\alpha, U, q}{\alpha^-, X, q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_f (r, \beta)$ or

(2) there exists $\frac{\alpha, V, q}{\alpha^-, X, q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_g (r, \beta)$.

**push transitions** $(\text{run}, \text{bel}, o, \text{run}, \text{bel}'\text{bel}'') \in \delta^e$ if:

* $\frac{\beta^-, U, r}{\alpha^-, U, q^-} \in \text{bel}'$ and $\frac{\beta, U, r}{\beta^-, U, r} \in \text{bel}''$ iff there exists $\frac{\alpha, U, q}{\alpha^-, U, q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_c (r, \beta^-, \beta)$.