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

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

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

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

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

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

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

**pop transitions** $(\text{run}, \text{bel}, o, \ell, \varepsilon) \in \delta^e$ with $\ell \in Q^e \setminus \{\text{run}\}$ if:

* $\frac{\tilde{U},r}{\alpha^-,\tilde{U},q^-} \in \ell$ iff $\frac{\alpha,\tilde{U},q}{\alpha^-,\tilde{U},q^-} \in \text{bel}$ and $(q, \alpha) \stackrel{\alpha}{\Rightarrow}_c (r, \varepsilon)$.

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

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

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

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

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

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

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

**$\varepsilon$-transitions** $(\ell, \text{bel}, \varepsilon, \text{run}, \text{bel}') \in \delta^e$ if:

$$ \frac{\alpha,\tilde{X}',r}{\alpha^-,\tilde{X}^-,q^-} \in \text{bel}' \text{ iff there exists } \frac{\alpha,\tilde{X},q}{\alpha^-,\tilde{X}^-,q^-} \in \text{bel} \text{ and } \frac{\tilde{X}',r}{\alpha^-,\tilde{X}},q \in \ell. $$

We say that a configuration is *stable* if its associated state is *run*.

**Example 5.9.** Let us explain the runs given in the Figure 5.5. It starts in the initial configuration $(\text{run}, \left| \left\{ \frac{\perp_0,\tilde{U},q_0}{\perp_0,\tilde{U},q_0} \right\} \right|)$ which represents the empty run.

From $q_0$ there exists only one path of observation in the POpVPA. As this path is correct, by reading in on the estimate VPA we reach $(\text{run}, \left| \left\{ \frac{\gamma,\tilde{U},q_0}{\perp_0,\tilde{U},q_0} \right\} \right| \right)$. The new element of the stack $\{ \frac{\gamma,\tilde{U},q_0}{\perp_0,\tilde{U},q_0} \}$ means that the stack of the possible run has head $\gamma$ and its current state is $q_0$ after a correct run, moreover the run entered $q_0$ when it pushed this $\gamma$ and it does not have a second non-terminal element in our stack. Reading a second in is

still doable by a single run, we reach $(\text{run}, \left| \left\{ \frac{\gamma,\tilde{U},q_0}{\gamma,\tilde{U},q_0} \right\} \right| \right)$ which modifies one information compared to before: we know from the bottom part of the head stack that the stack has at least a second $\gamma$.
Reading a serve then is possible as there exists a correct signalling run from $q_0$ to $q_1$ with observation serve. The estimate VPA modifies the head stack so as to represent that the run we follow is now in $q_1$ but without modifying anything else.

Reading a pop event is more involved: from $q_1$ with head of stack $\gamma$, triggering a pop can be done by a correct run staying in $q_1$ or by a faulty run going in $f_1$. To represent this and the popping of the stack, we go in two steps. In the first step, we go to the state $\{\frac{U,q_1}{\gamma,U,q_0}, \frac{W,f_1}{\gamma,U,q_0}\}$ which keeps the information of the two possibilities of current configuration and we pop the stack. In the second step, we deterministically take an $\epsilon$ transition that transfer this information from the state to the stack. In order to transfer the information, the estimate VPA checks which of the current possible runs (represented by $\frac{U,q_1}{\gamma,U,q_0}$ and $\frac{W,f_1}{\gamma,U,q_0}$) corresponds to each of the new head of stack. This is done by comparing the bottom part of the run with the top part of the head of stack, here $\gamma, U, q_0$ in every cases. Reading a second pop realises a similar process reaching (run, $|\{\frac{U,q_1}{\gamma,U,q_0}, \frac{W,f_1}{\gamma,U,q_0}\}|$). An empty would lead to (run, $|\{\frac{U,q_0}{\gamma,U,q_0}\}|$) as there is a correct run from $q_1$ to $q_0$ labelled by empty but no run from $f_1$ with such label. Similarly a reset cannot be taken from $q_1$ but it can be read from $f_1$, thus we reach (run, $|\{\frac{W,q_0}{\gamma,U,q_0}\}|$).

The following proposition links runs of $V$ and observed sequences of $A(V)$.

**Proposition 5.1.** Let $\sigma$ be an observed sequence of $A(V)$ and $\rho^*$ be its corresponding finite run with successive stable configurations (run, $w_0$)...(run, $w_n$). Let $w_n = bel_1...bel_h$ and for $i < n$, $bel^{(i)}$ be the top stack symbol of $w_i$. Then:

* For all $\frac{\gamma_h, X_h, q_h}{\gamma_{h-1}, X_{h-1}, q_{h-1}} \in bel_h$, there exists a sequence $(\frac{\gamma_i, X_i, q_i}{\gamma_{i-1}, X_{i-1}, q_{i-1}})_{0<i<h}$ such that for all $i$, $\frac{\gamma_i, X_i, q_i}{\gamma_{i-1}, X_{i-1}, q_{i-1}} \in bel_i$ and a signalling run $\rho$ of $V$ such that $\mathcal{P}(\rho) = \sigma$ that reaches configuration $(q_h, \gamma_1...\gamma_h)$. In addition:

* if $X_h = U$ then $\rho$ may be chosen correct;

* if $X_h \neq U$ then $\rho$ may be chosen faulty;

* if $X_h = W$ then there exists $0 < k \leq n$, such that $\rho_{\downarrow k}$ is faulty and $W$ does not occur in $bel^{(k-1)}$.

* Conversely, let $\rho$ be a signalling run of $V$ such that $\mathcal{P}(\rho) = \sigma$ reaching configuration $(q_h, \gamma_1...\gamma_h)$, there exists a sequence $(\frac{\gamma_i, X_i, q_i}{\gamma_{i-1}, X_{i-1}, q_{i-1}})_{0<i\leq h}$ such that for all $i$, $\frac{\gamma_i, X_i, q_i}{\gamma_{i-1}, X_{i-1}, q_{i-1}} \in bel_i$. In addition:

* if $\rho$ is correct then $X_h = U$;

* if $\rho$ is faulty then $X_h \neq U$;

* if there exists $0 < k \leq n$, such that $\rho_{\downarrow k}$ is faulty and $W$ does not occur in $bel^{(k-1)}$ then $X_h = W$.

The difficulty of this proof is the number of cases that have to be studied: what is the tag and which kind of transition (local, push or pop) is considered. As a consequence,
we only detail the most involved case (when the event is a pop and the tag is W. The result is obtained by induction on the size of the observed sequence and mostly consists in understanding the definitions of $\mathcal{A}(\mathcal{V})$ and especially of the tag updates.

*Proof.* We prove the result by induction on $|\sigma|$. The basis case is straightforward. For the inductive step, we only detail the most involved case: $\sigma[n] \in \Sigma_{o,b}$. For the properties related to tags, we only detail the ones related to W. Denote $\sigma' = \sigma[1]\dots\sigma[n-1]$ and $w_{n-1} = bel'_1 \dots bel'_h bel'_{h+1}$.

* Let $\frac{\gamma_h, X_h, q_h}{\gamma_{h-1}, X_{h-1}, q_{h-1}} \in bel_h$. By construction, there exists $\frac{\gamma'_{h+1}, X'_{h+1}, q'_{h+1}}{\gamma'_h, X'_h, q'_h} \in bel'_{h+1}$ with $\gamma'_h = \gamma_h$, a signalling run $(q'_{h+1}, \gamma'_{h+1}) \stackrel{\rho''}{\implies} (q_h, \varepsilon)$ with $\text{proj}(\rho'') = \sigma[n]$, $\frac{\gamma'_h, X'_h, q'_h}{\gamma'_{h-1}, X'_{h-1}, q'_{h-1}} \in bel'_h$ where $(\gamma'_{h-1}, X'_{h-1}, q'_{h-1}) = (\gamma_{h-1}, X_{h-1}, q_{h-1})$ and $X_h$ is obtained by updating $X'_{h+1}$ w.r.t. $bel'_{h+1}$ and $\rho''$. In particular if $X_h = W$ then:

(1) $X'_{h+1} = W$, or

(2) W does not occurs in $bel'_{h+1}$ and (a) $X'_{h+1} = V$ or (b) $X'_{h+1} = U$ and $\rho''$ is faulty.

By inductive hypothesis, there exists a sequence $(\frac{\gamma'_i, X'_i, q'_i}{\gamma'_{i-1}, X'_{i-1}, q'_{i-1}})_{0<i\le h}$ such that for all $i$, $\frac{\gamma'_i, X'_i, q'_i}{\gamma'_{i-1}, X'_{i-1}, q'_{i-1}} \in bel'_i$ and a signalling run $\rho'$ of $\mathcal{V}$ such that $\mathcal{P}(\rho') = \sigma'$ reaching configuration $(q'_{h+1}, \gamma'_1 \dots \gamma'_{h+1})$. Consider the signalling run $\rho = \rho'\rho''$; it reaches configuration $(q_h, \gamma'_1 \dots \gamma'_h)$. Since for all $i < h$, $bel'_i = bel_i$, the sequence $(\frac{\gamma'_i, X'_i, q'_i}{\gamma'_{i-1}, X'_{i-1}, q'_{i-1}})_{0<i<h}$ and the run $\rho$ are appropriate. The three additional properties follow from the rules of tag updates. In particular, if $X_h = W$, then:

◦ the assertion (1) holds and then the property comes from the inductive hypothesis, or

◦ the assertion (2) holds which implies that W does not occur in $bel'_{h+1}$ and $\rho$ is faulty.

* Let $\rho$ be a signalling run of $\mathcal{V}$ such that $\mathcal{P}(\rho) = \sigma$ which reaches configuration $(q_h, \gamma_1 \dots \gamma_h)$. Let us write $\rho = \rho_{\downarrow n-1} \rho''$ with $(q'_{h+1}, \gamma'_{h+1}) \stackrel{\rho''}{\implies} (q_h, \varepsilon)$. By the inductive hypothesis, there exists a sequence $(\frac{\gamma'_i, X'_i, q'_i}{\gamma'_{i-1}, X'_{i-1}, q'_{i-1}})_{0<i\le h+1}$ such that for all $i$, $\frac{\gamma'_i, X'_i, q'_i}{\gamma'_{i-1}, X'_{i-1}, q'_{i-1}} \in bel'_i$ and for all $i \le h$, $\gamma'_i = \gamma_i$. By construction, $\frac{\gamma_h, X_h, q_h}{\gamma'_{h-1}, X'_{h-1}, q'_{h-1}} \in bel_h$ for some $X_h$. Since $bel_i = bel'_i$ for all $i < h$, we obtain the required sequence of items.

The three additional properties follow from the rules of tag updates. In particular, assume there exists $0 < k \le n$, such that $\rho_{\downarrow k}$ is faulty and W does not occur in $bel^{k-1}$.

◦ If $\rho_{\downarrow n-1}$ is correct then, as $\rho$ is faulty, $\rho''$ is faulty and W does not occur in $bel^{n-1} = bel'_{h+1}$. So by construction $X_h = W$.

◦ If $\rho_{\downarrow n-1}$ is faulty then:

* either $X'_{h+1} = W$ and by construction $X_h = W$,

* or $X'_{h+1} = V$. By induction hypothesis there does not exist $0 < k \le n-1$, such that $\rho_{\downarrow k}$ is faulty and W does not occur in $bel^{k-1}$. So W does not occur in $bel^{n-1} = bel'_{h+1}$. Therefore $X_h = W$.

□
## 2.2 Decidability of diagnosability for POpVPA

Our goal in this subsection is to use the characterisations from the Section 3 of Chapter 3 to decide the diagnosability of POpLTS generated by POpVPA. To do so, we face the difficulty that the Borel sets that characterise IF-, IA- and FF-diagnosability are not a priori regular, even in the finitely-branching case. Yet, for POpVPA, we circumvent this problem, and manage to specify these sets by pLTL formula on a product of the POpVPA with its estimate VPA, the tags are used to define the atomic propositions. The decidability of the qualitative model checking for recursive probabilistic systems [EY12] then yields the decidability of the above three diagnosability notions for POpVPA.

The first step is to build the product of the POpVPA and its estimate VPA. From this point on, we assume that the set of states of the POpVPA is separated between correct and faulty states $Q = Q_c \cup Q_f$. This can be done without loss of generality: the transformation ensuring this is similar to the one shown for pLTS in Section 1.4 of Chapter 2. We build $V_{A(\mathcal{V})} = \mathcal{V} \times A(\mathcal{V})$ the product automaton of $\mathcal{V}$ and $A(\mathcal{V})$ synchronised on the alphabet of observed events $\Sigma_o$. The transitions of $\mathcal{V}$ labelled by unobservable events do not change the second component of the state and the transitions of $A(\mathcal{V})$ labelled by $\varepsilon$ do not change the first component of the state. Due to the determinism of $A(\mathcal{V})$, $V_{A(\mathcal{V})}$ has the same probabilistic behaviour as the one of $\mathcal{V}$ except that it memorises additional information along the run. More precisely, let $\rho$ be a run of $\mathcal{V}$, then $\bar{\rho}$, a run of $V_{A(\mathcal{V})}$, is obtained from $\rho$ by following the same transitions and adding the single $\ominus$ transition firable after any pop transition. One immediately gets $\mathbb{P}_{V_{A(\mathcal{V})}}(\bar{\rho}) = \mathbb{P}_{V}(\rho)$. Formally we have:

**Definition 5.7.** Given $\langle\mathcal{V}, \mathcal{P}, \Sigma_o\rangle$ a POpVPA $\mathcal{V} = (Q, \Sigma, \Gamma, \delta, \mathbf{P})$ and its estimate VPA $A(\mathcal{V}) = (Q^e, \text{run}, \Sigma_o, \Gamma^e, \delta^e)$, their synchronised product is the pVPA $V_{A(\mathcal{V})} = (Q^A, \Sigma \cup \{\ominus\}, \Gamma^A, \delta^A, \mathbf{P}^A)$ where:

* $Q^A = Q \times Q^e$ is the set of states with initial state $q_0^A = (q_{0,c}, \text{run})$;

* $\Gamma^A = \Gamma \times \Gamma^e$ is the stack alphabet with $\Gamma_{\perp} \times \Gamma_{\perp}^e$ the set of bottom stack symbols and $\perp_0^A = (\perp_0, \frac{\perp_0, \mathbf{U}, q_0}{\perp_0, \mathbf{U}, q_0})$ the initial symbol;

* The transition relation $\delta^A$ consists of:

**local transitions.**

* For all $(q, \gamma, a, q', \gamma') \in \delta$ with a unobservable and $bel \in \Gamma^e$, we have $((q, \text{run}), (\gamma, bel), a, (q', \text{run}), (\gamma', bel)) \in \delta^A$;

* For all $(q, \gamma, a, q', \gamma') \in \delta$ and $(\text{run}, bel, o, \text{run}, bel') \in \delta^e$ with $\mathcal{P}(a) = o$, we have $((q, \text{run}), (\gamma, bel), a, (q', \text{run}), (\gamma', bel')) \in \delta^A$;

* For all $(\ell, bel, \varepsilon, \text{run}, bel') \in \delta^e$, $q \in Q$ and $\gamma \in \Gamma$, we have

$$((q, \ell), (\gamma, bel), \ominus, (q, run), (\gamma, bel')) \in \delta^A;$$

**push transitions.**

* For all $(q, \gamma, a, q', \gamma'\gamma'') \in \delta$ and $(\text{run}, bel, o, \text{run}, bel' bel'') \in \delta^e$ with $\mathcal{P}(a) = o$, we have $((q, \text{run}), (\gamma, bel), a, (q', \text{run}), (\gamma', bel')(\gamma'', bel'')) \in \delta^A$;
**pop transitions.**

* For all $(q, \gamma, a, q', \varepsilon) \in \delta$ and $(run, bel, o, \ell, \varepsilon) \in \delta^e$ with $\mathcal{P}(a) = o$, we have $((q, run), (\gamma, bel), a, (q', \ell), \varepsilon) \in \delta^A$;

* The transition probability function $\mathbf{P}^A$ is defined by:

- $\mathbf{P}^A((q, run), (\gamma, bel), a, (q', run), (\gamma', bel')) = \mathbf{P}(q, \gamma, a, q', \gamma');$

- $\mathbf{P}^A((q, run), (\gamma, bel), a, (q', run), (\gamma', bel')(\gamma'', bel'')) = \mathbf{P}(q, \gamma, a, q', \gamma'\gamma'');$

- $\mathbf{P}^A((q, run), (\gamma, bel), a, (q', \ell), \varepsilon) = \mathbf{P}(q, \gamma, a, q', \varepsilon);$

- for $\ell \in Q^e \setminus \{\text{run}\}$, $\mathbf{P}^A((q, \ell), (\gamma, bel), \ominus, (q, run), (\gamma, bel')) = 1$.

**Example 5.10.** The product POpVPA contains the current run of the POpVPA and the information given by the estimate POpVPA. Let us consider the faulty run given as example in the Figure 5.2. This POpVPA does not follow the separation between correct and faulty states. Here we write $q_c$ (resp. $q_f$) if the state $q$ was reached by a correct (resp. faulty) run. After reading in, we are in state $(q_{0,c}, run)$ meaning that the state of the possible run is $q_0$, it was reached by a correct run and our estimate VPA is in state run, the head of stack is $(\gamma, \left|\left\{\frac{\gamma, U, q_{0,c}}{\perp_0, U, q_{0,c}}\right\}\right|)$, meaning our real head is $\gamma$ and the rest is the head of the estimate VPA. If we follow the faulty run until after the first pop, we reach the state $(f_{1,f}, \{\frac{U, q_1}{\gamma, U, q_{0,c}}, \frac{W, f_{1,f}}{\gamma, U, q_{0,c}}\})$, we are thus in $f_1$ with a faulty run and the estimate VPA is in one of the temporary states. In order to leave this state, we read $a \ominus$ which leads to the state $(f_{1,f}, run)$. $\ominus$ is an event only affecting the part of the POpVPA corresponding to the estimate VPA, allowing it to realise the $\varepsilon$ transition that follows the observation of a pop event.

Given a finite run $\rho$ of $\mathcal{V}$, we inductively define the run $\bar{\rho}$ of $\mathcal{V}_{\mathcal{A}(\mathcal{V})}$ as follows. First $(\overline{q_0}, \perp_0) = (q_0^A, \perp_0^A)$. Let $\rho$ of length $n \ge 1$, $a \in \Sigma$ and $q \in Q$ and $\gamma_1, \dots, \gamma_h \in \Gamma$ such that $\rho = \rho'a(q, \gamma_1 \dots \gamma_h)$. If $a \notin \Sigma_b$ then $\bar{\rho} = \bar{\rho}'a((q, run), (\gamma_1, bel_1) \dots (\gamma_h, bel_h))$ where $(run, bel_1 \dots bel_h)$ is the configuration reached by $\mathcal{P}(\rho)$ in $\mathcal{A}(\mathcal{V})$. If $a \in \Sigma_b$ then $\bar{\rho} = \bar{\rho}'a((q, \ell), (\gamma_1, bel_1) \dots (\gamma_h, bel_h)) \ominus ((q, run), (\gamma_1, bel_1) \dots (\gamma_{h-1}, bel_{h-1})(\gamma_h, bel_h'))$ where $(\ell, bel_1 \dots bel_h)$ is the configuration reached by $\mathcal{P}(\rho)$ in $\mathcal{A}(\mathcal{V})$ and $(run, bel_1 \dots bel_{h-1}, bel_h')$ is the single next configuration reached by an $\varepsilon$ transition. As previously observed, $\mathbb{P}(\rho) = \mathbb{P}(\bar{\rho})$.

In order to prove decidability of diagnosability for a POpVPA $\mathcal{V}$, one wants to check whether the formulae characterising diagnosability defined in Chapter 3 hold on $\mathcal{V}$. Let us first recall the relevant results of Chapter 3. We defined three path formulae:

* $f$: for every run $\rho$, $f(\rho) = \text{true}$ if $\rho$ is faulty;

* $\mathfrak{U}$: for every run $\rho$, $\mathfrak{U}(\rho) = \text{true}$ if there exists a correct signalling run $\rho'$ with $\mathcal{P}(\rho) = \mathcal{P}(\rho')$;

* $\mathfrak{W}$: $\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 $$
where $\mathbf{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$.

Using these path formulae, given a pLTS $\mathcal{A}$, we obtained the following results:

* $\mathcal{A}$ is FF-diagnosable iff $\mathcal{A} \models \mathbb{P}^0(\diamond\Box(\mathfrak{f} \wedge \mathfrak{U}))$;

* if $\mathcal{A}$ is finitely branching, $\mathcal{A}$ is IA-diagnosable iff $\mathcal{A} \models \mathbb{P}^0(\diamond\Box(\mathfrak{U} \wedge \mathfrak{W}))$.

The paths formulae $\mathfrak{f}$, $\mathfrak{U}$ and $\mathfrak{W}$ depends on the past of the run and not only on the current configuration. We therefore transform the pathL formulae into pLTL properties that are checked on $\mathcal{V}_{\mathcal{A}(\nu)}$. First, for each path formula we define an atomic propositions on the pairs $((q, run)(\gamma, bel))$ consisting of a state of $\mathcal{V}_{\mathcal{A}(\nu)}$ together with a top stack contents.

**Definition 5.8.** Let $\mathbf{bel} \subseteq 2^{(\Gamma \times \Gamma \times Q)^2}$, we say that the tag $\mathbf{X}$ occurs in $\mathbf{bel}$ if there exists $\frac{\gamma, \mathbf{X}, q}{\gamma, \mathbf{X}, q} \in \mathbf{bel}$.

The atomic propositions $\nu_f$, $\nu_u$ and $\nu_w$ corresponding to the path formulae $\mathfrak{f}$, $\mathfrak{U}$ and $\mathfrak{W}$ are defined by:

* $\nu_f((q, run)(\gamma, bel)) = \text{true}$ if and only if $q \in Q_f$;

* $\nu_u((q, run)(\gamma, bel)) = \text{true}$ if and only if $\mathfrak{U}$ occurs in $\mathbf{bel}$;

* $\nu_w((q, run)(\gamma, bel)) = \text{true}$ if and only if $\mathfrak{W}$ occurs in $\mathbf{bel}$.

We extend $\nu_f$, $\nu_u$ and $\nu_w$ over configurations $cf = ((q, \ell), w)$ with $\ell \neq \text{run by}$ $\nu_f(cf) = \nu_u(cf) = \nu_w(cf) = \text{true}$.

The atomic propositions $\nu_f$ and $\nu_u$ perfectly reflect the paths formula $\mathfrak{f}$ and $\mathfrak{U}$, and $\nu_w$ is eventually forever true if and only if $\mathfrak{W}$ is.

**Proposition 5.2.** Let $\rho$ be an infinite run of $\mathcal{V}$. Then:

* For all $k \in \mathbb{N}$, $\mathfrak{f}(\rho_{\downarrow k}) \Leftrightarrow \nu_f(\mathbf{last}(\bar{\rho}_{\downarrow k}))$ and $\mathfrak{U}(\rho_{\downarrow k}) \Leftrightarrow \nu_u(\mathbf{last}(\bar{\rho}_{\downarrow k}))$;

* $\rho \models \diamond\Box\mathfrak{W} \Leftrightarrow \exists K \forall k \geq K$. $\nu_w(\mathbf{last}(\bar{\rho}_{\downarrow k})) = \text{true}$.

The second component of $\mathcal{V}_{\mathcal{A}(\nu)}$ representing $\mathcal{A}(\mathcal{V})$, one can use the results of Proposition 5.1 to link the tags and the runs associated with the observed sequence. This is what we do here. The most complicated (and interesting) case being the link between $\mathfrak{W}$ and $\mathfrak{W}$. The idea is the following. When the tag $\mathfrak{W}$ disappears after following an observation in $\mathcal{A}(\mathcal{V})$, let $n$ be the observed length of the last time $\mathfrak{W}$ was not tagging any state, then the oldest fault in the current run occurred after the $n$'th observation. Thus every time $\mathfrak{W}$ is not present, the longest prefix of the run that is surely correct increased, ensuring that $\mathfrak{W}$ is false. Of course, $\mathfrak{W}$ can be false more often than the absences of $\mathfrak{W}$. However, if after the $n$'th observation, for $n \in \mathbb{N}$, $\mathfrak{W}$ always tag a state of the belief, it means that there exists a run consistent with the observation for which a fault occurred at most at the $n$'th step. Therefore $\mathbf{firstf}$ is bounded, which implies that $\mathfrak{W}$ will eventually become forever true.
*Proof.* First, note that $f$ and $\nu_f$ obviously coincide: they both express that a fault occurred.

To prove the second item, about $\mathfrak{U}$ and $\nu_u$, we use the link between observed sequences and the tag $U$ in $\mathcal{V}_{\mathcal{A}(\mathcal{V})}$. Let $\sigma$ be an observed sequence triggered by a run of $\mathcal{V}$. Then $\mathrm{bel}_{\sigma}$ is the top stack symbol of the stable configuration in $\mathcal{A}(\mathcal{V})$ reached by the run accepting $\sigma$ (so ending by an $\varepsilon$-transition if the last event is a pop event). Due to Proposition 5.1, $U$ occurs in $\mathrm{bel}_{\sigma}$ iff there is a correct signalling run of $\mathcal{V}$ with observed sequence $\sigma$. According to the definition of $\nu_u$, we thus deduce that for any finite signalling run $\rho$ of $\mathcal{V}$, $\nu_u(\mathrm{last}(\rho)) = \mathrm{true}$ iff $\mathfrak{U}(\rho) = \mathrm{true}$.

We now establish the link between $\mathfrak{W}$ and $\nu_W$. To show the left-to-right implication, let $\rho \in \Omega$ and $K_0 \in \mathbb{N}$ be such that $\rho, K_0 \models \Box\mathfrak{W}$. By definition of $\mathfrak{W}$, $\mathrm{firstf}(\mathcal{P}(\rho_{\downarrow k}))$ is constant and bounded by $K_0$ for $k \ge K_0$. For all $k \in \mathbb{N}$, let $\mathrm{bel}_k$ be the top stack symbol reached in $\mathcal{A}(\mathcal{V})$ after reading the observed sequence $\mathcal{P}(\rho_{\downarrow k})$. If for all $k \ge K_0$, $W$ occurs in $\mathrm{bel}_k$, then for all $k \ge K_0$, $\nu_w(\mathrm{last}(\bar{\rho}_{\downarrow k})) = \mathrm{true}$. Otherwise there exists $K_1 \ge K_0$ such that $W$ does not occur in $\mathrm{bel}_{K_1}$. Let $k > K_1$, as $\mathrm{firstf}(\mathcal{P}(\rho_{\downarrow k})) \le K_0$, there exists a faulty run $\rho'$ of $\mathcal{V}_{\mathcal{A}(\mathcal{V})}$ such that $\mathcal{P}(\rho') = \mathcal{P}(\bar{\rho}_{\downarrow n})$ and $\rho'_{\downarrow K_0}$ is faulty. $W$ does not occur in $\mathrm{bel}_{K_1}$ and $\rho'_{\downarrow K_1+1}$ is faulty. Thus by Proposition 5.1, $W$ occurs in $\mathrm{bel}_k$. Therefore for all $n > K_1$, $\nu_w(\mathrm{last}(\bar{\rho}_{\downarrow n})) = \mathrm{true}$.

Let us show the right-to-left implication. Let $\rho \in \Omega$ and $K \in \mathbb{N}$ be such that for all $k \ge K$, $\nu_w(\mathrm{last}(\bar{\rho}_{\downarrow k})) = \mathrm{true}$. By definition of $\nu_w$ for all $k \ge K$, $W$ occurs in $\mathrm{bel}_k$ (defined as above). Let $k \ge K$, by Proposition 5.1, there exists a run $\rho'$ of $\mathcal{V}_{\mathcal{A}(\mathcal{V})}$ such that $\mathcal{P}(\rho') = \mathcal{P}(\bar{\rho}_{\downarrow k})$ and there exists $n \le k$ such that $\rho'_{\downarrow n}$ is faulty and $W$ does not occur in $\mathrm{bel}_{n-1}$. Thus $n \le K$. Therefore for all $k \ge K$, $\mathrm{firstf}(\mathcal{P}(\rho_{\downarrow k})) \le K$. Since beyond $K$, $\mathrm{firstf}$ is bounded, it is non decreasing and then ultimately constant. Let $K'$ such that for all $k \ge K'$, $\mathrm{firstf}(\mathcal{P}(\rho_{\downarrow k})) = \mathrm{firstf}(\mathcal{P}(\rho_{\downarrow k-1}))$. So $\rho, K' \models \Box\mathfrak{W}$ and thus $\rho \models \Diamond\Box\mathfrak{W}$.

Thanks to the relationships between the path formulae, and the atomic propositions, and using the characterisations from Section 3 of Chapter 3, we reduce the FF-, IF- and IA-diagnosability to the model checking of a pLTL formula on the product VPA $\mathcal{V}_{\mathcal{A}(\mathcal{V})}$. Model checking qualitative pLTL for probabilistic pushdown automata is doable in polynomial space in the size of the model [EY12]. In our case, $\mathcal{V}_{\mathcal{A}(\mathcal{V})}$ is exponential in the size of $\mathcal{V}$. We thus obtain the decidability and a complexity upper-bound for the diagnosability problems for POpVPA.

**Theorem 5.3.** FF-diagnosability, IF-diagnosability and IA-diagnosability are decidable in EXPSPACE for POpVPA.

*Proof.* Thanks to the Propositions 5.2 and 5.1 and the characterisations of Propositions 3.7 (page 80) and 3.8 (page 81), we can derive pLTL characterisations of diagnosability for POpVPA. Namely, for $\mathcal{V}$ a POpVPA, as $\mathcal{V}$ and $\mathcal{V}_{\mathcal{A}(\mathcal{V})}$ have the same probabilistic behaviour,

* $\mathcal{V}$ is FF-diagnosable iff $\mathcal{V}_{\mathcal{A}(\mathcal{V})} \models \mathbb{P}^= (\diamond\Box (\nu_f \wedge \nu_u))$;

* $\mathcal{V}$ is IA-diagnosable iff $\mathcal{V}_{\mathcal{A}(\mathcal{V})} \models \mathbb{P}^= (\diamond\Box (\nu_u \wedge \nu_w))$.
Moreover, since POpPDA have finitely many states, the POpLTS they generate are finitely-branching. Therefore, IF-diagnosability coincides with FF-diagnosability according to Theorem 3.1. The two above qualitative pLTL formulae can be checked on probabilistic pushdown automata thanks to [EY09]. More precisely, one can transform $V_{A(\nu)}$ into a recursive Markov chain (the transformation is linear) [EY12]. Then, the model checking of qualitative pLTL on recursive Markov chains is doable in PSPACE in the size of the Recursive Markov Chain and EXPTIME in the size of the formulae [EY09]. In our case, the product VPA $V_{A(\nu)}$ is exponential in the size of $V$ and the size of the formulae is constant. This yields an EXPSPACE algorithm for checking diagnosability of POpVPA. □

## 2.3 EXPTIME-hardness of the diagnosability for POpVPA

While the notions of diagnosability we studied in the previous section are decidable in EXPSPACE (Theorem 5.3), this is not necessarily optimal. Here, we only show an EXPTIME lower bound on the complexity. This lower bound is obtained by reducing the universality problem for VPA, which is known to be EXPTIME-complete [AM04]. This reduction also applies to FA-diagnosability for which the decidability status is unknown.

**Theorem 5.4.** FF-, IF-, FA- and IA-diagnosability are EXPTIME-hard for POpVPA.

*Proof.* Let us start with FF-diagnosability. The proof is done by reduction from the universality problem for VPA, which is known to be EXPTIME-hard [AM04]. Recall the universality problem for VPA: given a VPA $A$ and a set of final states $Q_F$, do we have $P(\{\rho \in SR \mid \text{last}(\rho) \in Q_F\}) = \Sigma_o^\omega$?

Starting from a VPA $A$ we build a pVPA $V'$ (see Figure 5.6) with two components: one correct and one faulty, both reachable in one step from the initial state. The correct component is a copy of $A$ with a positive probability of making a reset (emptying its stack and going back to the initial state of $A$) in a final state. Every reset starts by a new observable event $\searrow$, followed by some pop event $\searrow$ and ends by a second $\searrow$. In the faulty component, one can read any observation of $\Sigma_o^*$ and also has the possibility to produce $\searrow$ and $\searrow$ in a way that mimics a reset. If a $\searrow$ is read, then the faulty component triggers some $\searrow$ and a $\searrow$ as would be done in the correct component. This way, the observation associated with a reset does not give any information on the correctness of a system. What matters is after which observed sequence can a reset occur. If an observed sequence cannot end in an accepting state of $A$, then in a faulty run, with probability 1 this observed sequence will be read in between two resets, revealing the fault. Reciprocally, if $A$ is universal, everything that can be observed on a faulty run can also be observed in the correct component establishing that $V'$ is not diagnosable.

Formally, from a VPA $A = (Q, \Sigma, \Gamma, \delta)$ and a subset of accepting states $Q_F \subseteq Q$, we build a pVPA $V' = (Q', \Sigma', \Gamma', \delta', \mathbf{P}')$ as follows:

* $Q' = Q \cup \{f_0, f_\searrow, q'_0, q_\searrow\}$ and $q'_0$ is the initial state;

* $\Sigma' = \Sigma \uplus \{\mathbf{f}, u, \searrow, \searrow\}$;
• $\Gamma' = \Gamma \uplus \{B\}$ and $\Gamma'_{\perp} = \Gamma_{\perp}$;

• Writing $\delta_{\sharp}$, resp. $\delta_{\sharp}$ and $\delta_{\flat}$ for the set of local resp. push and pop transitions of $\mathcal{V}$, $\delta'$ consists of the following transitions:

**local** $\delta_{\sharp} \cup \{(q'_0, \perp_0, u, \perp_0, q_0), (q'_0, \perp_0, \mathbf{f}, \perp_0, f_0), (f_0, \gamma, \flat, \gamma, f_\flat) \mid \gamma \in \Gamma \cup \{\perp_0\} \} \cup \{(q, \gamma, \flat, \gamma, q_\flat) \mid q \in Q_F, \gamma \in \Gamma \cup \{\perp_0\} \} \cup \{(f_0, \gamma, a, \gamma, f_0) \mid a \in \Sigma_{\sharp}, \gamma \in \{B, \perp_0\} \} \cup \{(q_\flat, \perp_0, \flat, \perp_0, q_0), (f_\flat, \perp_0, \flat, \perp_0, f_0)\}$;

**push** $\delta_{\sharp} \cup \{(f_0, \gamma, a, \gamma B, f_0) \mid a \in \Sigma_{\sharp}, \gamma \in \{B, \perp_0\}\}$;

**pop** $\delta_{\flat} \cup \{(f_0, B, a, \varepsilon, f_0) \mid a \in \Sigma_{\flat}\} \cup \{(f_\flat, B, b, \varepsilon, f_\flat) \} \cup \{(q_\flat, \gamma, b, \varepsilon, q_\flat) \mid \gamma \in \Gamma\}$;

• $\mathbf{P}'$ is such that for every $\gamma \in \Gamma$, $\mathbf{P}'(f_0, \gamma, \flat, \gamma, f_\flat) = \frac{1}{2}$, and assigns arbitrary positive probabilities to the other transitions in $\delta'$.

We further consider the POpVPA $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$ with $\Sigma_o = \Sigma \cup \{\flat, \perp\}$ and the masking function satisfies $\mathcal{P}(u) = \mathcal{P}(\mathbf{f}) = \varepsilon$ and $\mathcal{P}(x) = x$ for any other event $x \in \Sigma'$. This construction is illustrated in Figure 5.6. The figure uses the following shortcuts: $a_\flat \in \Sigma_\flat$, $a_\sharp \in \Sigma_\sharp$, $\gamma \in \Gamma$, $\gamma' \in \{B, \perp_0\}$ and $z \in \Gamma \setminus \{\perp_0\}$.

<figure><img src="image_74.png" /><figcaption>Figure 5.6: A POpVPA for the EXPTIME-hardness of FF-diagnosability.</figcaption></figure>

The observed sequences corresponding to correct runs in $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$ are either of the form $w_1\flat b^{k_1}\flat w_2 \dots \flat b^{k_{n-1}}\flat w_n$ or of the form $w_1\flat b^{k_1}\flat w_2 \dots \flat w_{n-1}\flat b^m$. In these compositions, $w_i$, for $i < n$, is a sequence corresponding to a run of $\mathcal{V}$ starting in $q_0$ and ending in some accepting state $q_f \in Q_F$, $k_i$ is the number of elements in the stack after reading $w_i$ in $\mathcal{V}$ and also in $\mathcal{V}'$ (apart from the bottom stack symbol $\perp_0$), $w_n$ is the sequence associated with a run of $\mathcal{V}$ starting in $q_0$, and $m$ is at most the number of elements in the stack after reading $w_{n-1}$ in $\mathcal{V}$. Note that $k_i$ only depends on $w_i$, and does not depend on the exact run over $w_i$, since $\mathcal{V}$ is a VPA.

The observed sequences corresponding to faulty runs in $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$ are less constrained. They are of one of the two forms presented above, however the words $w_i$ for $i \le n$ can be any word of $\Sigma^*$.

Let us show that $\mathcal{V}$ is not universal if and only if $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$ is FF-diagnosable. First assume that $\mathcal{V}$ is not universal. Then there exists a word $w \in \Sigma^*$ such that no run of $\mathcal{V}$ reading $w$ ends in an accepting state $q_f$. However, the observed sequence of
any faulty run almost-surely contains the factor $\mathfrak{h}w\mathfrak{h}$. Indeed, faulty runs almost surely visit infinitely often the configuration $(f_b, \perp_0)$, and from there, the probability $\lambda$ to read $\mathfrak{h}w\mathfrak{h}$ is positive. Let $\rho$ be an infinite faulty run. Its observed sequence is of the form $\mathcal{P}(\rho) = w_1\mathfrak{h}\mathfrak{b}^{k_1}\mathfrak{h}w_2\mathfrak{h}\mathfrak{b}^{k_2}\mathfrak{h}w_3 \dots$ with $k_i \le |w_i|$ for every $i$. If there exists $i \le n$ such that $w_i = w$ then $\rho$ is surely faulty, since it has no corresponding correct run. The latter statement can be refined. For $n \ge |w|$, if, for every $i \le n$, $|w_i| \le n$ and there exists $i \le n$ such that $w_i = w$ then $\rho_{\downarrow 2n^2+n}$ is surely faulty. Indeed, $|w_i\mathfrak{h}\mathfrak{b}^{k_i}| \le 2n+1$, $w$ occurs at the latest for $i=n$, and once it occurs the prefix is surely faulty. Let us therefore consider faulty runs that do not satisfy this property. We let $\text{Avoid}_n = \{\rho \in \mathbf{F} \mid \mathcal{P}(\rho) = w_1\mathfrak{h}\mathfrak{b}^{k_1}\mathfrak{h}w_2\mathfrak{h}\mathfrak{b}^{k_2}\mathfrak{h}w_3 \dots \wedge (\forall i \le n \ w_i \ne w \lor \exists i \le n \ |w_i| > n)\}$. By construction, $\text{FAmb}_{2n^2+n} \subseteq \text{Avoid}_n$. Moreover, using standard union-sum inequalities, $\mathbb{P}(\text{Avoid}_n) \le (1-\lambda)^n + \frac{n}{2^n}$ (recall that $\lambda$ is the probability to read $\mathfrak{h}w\mathfrak{h}$ from $(f_0, \perp_0)$). Thus $\lim_{n \to \infty} \mathbb{P}(\text{Avoid}_n) = 0$ and hence $\lim_{n \to \infty} \mathbb{P}(\text{FAmb}_n) = 0$ so that $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$ is FF-diagnosable.

Assume now that $\mathcal{V}$ is universal. Let $\rho$ be an infinite surely faulty run of $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$. We write $\rho'$ for the greatest ambiguous prefix of $\rho$ and $a \in \Sigma_o \cup \{\mathfrak{h}, \mathfrak{b}\}$ such that $\rho'a$ is again a prefix of $\rho$. Observe that $a$ cannot be $\mathfrak{b}$ since the number of $\mathfrak{b}$'s between two $\mathfrak{h}$'s, whether on the left or right-hand-side of $\mathcal{V}'$, is entirely determined by the word of $\Sigma_o^*$ read before the first $\mathfrak{h}$. For the same reason, if $a = \mathfrak{h}$, $\mathcal{P}(\rho')$ ends with a word of $\Sigma_o^*$ (i.e. the number of $\mathfrak{h}$'s in $\mathcal{P}(\rho')$ is even). Let $w$ be the greatest suffix of $\mathcal{P}(\rho')$ contained in $\Sigma_o^*$. If $a = \mathfrak{h}$, we deduce that there is no run starting in $q_0$ with observed sequence $w$ and ending in an accepting state of $\mathcal{V}$. Therefore, $\mathcal{V}$ is not universal. Similarly, if $a \in \Sigma_o$, then there is no run starting in $q_0$ and with observed sequence $wa$. In that case also, $\mathcal{V}$ is not universal. We hence conclude that there is no infinite surely faulty run in $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$. As the probability to generate faulty runs is positive, this implies that $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$ is not IF-diagnosable. Now, IF-diagnosability is equivalent to FF-diagnosability for finitely-branching POpLTS (see Theorem 3.1), and so $\langle \mathcal{V}', \Sigma_o, \mathcal{P} \rangle$ is not FF-diagnosable.

Let us now argue for the **EXPTIME**-hardness of **FA**-diagnosability and **IA**-diagnosability. The reduction is very similar to the previous one: it only requires an additional state in the correct component that ensures that almost surely any correct run will be identified as being correct. Therefore the problem may only come from the faulty runs which are dealt with exactly as above. From the VPA $\mathcal{V} = (Q, \Sigma, \Gamma, \delta)$ and pVPA $\mathcal{V}' = (Q', \Sigma', \Gamma', \delta')$ defined above, we construct a pVPA $\mathcal{V}'' = (Q'', \Sigma'', \Gamma'', \delta'', \mathbf{P}'')$ such that

* $Q'' = Q' \cup \{q_c\}$ and $q'_0$ is the initial state;

* $\Sigma'' = \Sigma \cup \{\mathbf{f}, u, \mathfrak{h}, \alpha\}$;

* $\Gamma'' = \Gamma$;

* $\delta'' = \delta' \cup \{(q, \alpha, \gamma, q_c) \mid \gamma \in \Gamma \cup \{\perp_0\}, q \in Q \cup \{q_c\}\}$;

* $\mathbf{P}''$ assigns arbitrary positive probabilities to transitions in $\delta''$.
We further consider the POpVPA $\langle V'', \Sigma_o, \mathcal{P} \rangle$ with $\Sigma_o = \Sigma'' \setminus \{\mathbf{f}, u\}$, and the masking function satisfies $\mathcal{P}(\mathbf{f}) = \mathcal{P}(u) = \varepsilon$ and $\mathcal{P}(x) = x$ for any other event $x$. The construction is illustrated in Figure 5.7, where we use the shortcuts: $a_b \in \Sigma_b$, $a_{\mathfrak{h}} \in \Sigma_{\mathfrak{h}}$, $a_{\mathfrak{h}'} \in \Sigma_{\mathfrak{h}'}$, $\gamma \in \Gamma$, $\gamma' \in \{B, \perp_0\}$ and $z \in \Gamma \setminus \{\perp_0\}$.

<figure><img src="image_75.png" /><figcaption>Figure 5.7: A POpVPA for EXPTIME-hardness of FA-diagnosability and IA-diagnosability.</figcaption></figure>

$V''$ is a slight modification of $V'$: from any state of $V$ (accepting or not), reading the new letter $\alpha$ leads to the sink state $q_c$. As a consequence, for any correct run of $\langle V'', \Sigma_o, \mathcal{P} \rangle$, there is a positive probability at each step to perform event $\alpha$ and become surely correct. This implies $\lim_{n \to \infty} \mathbb{P}(\mathcal{C}\text{Amb}_n)_{n \in \mathbb{N}} = 0$. Observe that the above proof for $V'$ also applies to $V''$: $V$ is not universal if and only if $\langle V'', \Sigma_o, \mathcal{P} \rangle$ is FF-diagnosable. Now, since $\lim_{n \to \infty} \mathbb{P}(\mathcal{C}\text{Amb}_n)_{n \in \mathbb{N}} = 0$, FF-diagnosability, FA-diagnosability and IA-diagnosability coincide for $\langle V'', \Sigma_o, \mathcal{P} \rangle$. We conclude that $V$ is not universal if and only if $\langle V'', \Sigma_o, \mathcal{P} \rangle$ is diagnosable (for any notion of diagnosability). $\square$

While diagnosability was undecidable for POpPDA, the situation is more complex with POpVPA. Some notions become decidable, although we may not have the exact complexity, while for others decidability remains open. The method used here requires a characterisation that can be translated in pLTL. This is not possible for FA-diagnosability or the approximate notions of diagnosability which cannot be expressed in pathL. Recall that pathL is more expressive than LTL according to Proposition 3.6, page 79.

## 3 Diagnosability of infinite pLTS represented by stochastic Petri nets

In this section we study infinite-state pLTS generated by stochastic Petri nets (SPN). This model is incomparable to pPDA and therefore generates different kinds of pLTS. In Subsection 3.1 we formally define SPN and the infinite-state pLTS generated by an SPN. We then show in Subsection 3.2 that, as for pPDA, diagnosability is undecidable
in SPN, and that a restriction similar to what pVPA are to pPDA is not enough to regain decidability.

**3.1 Stochastic Petri nets**

A Petri net contains places and transitions. In each place there are tokens and a transition consumes tokens from input places and produces tokens in output places. From a manufacturing point of view, these tokens can be seen as different items that are received, assembled with other items, processed and the final product can be exported. Due to the locality of transitions, Petri nets are appropriate for modelling concurrent systems. The infinite behaviour comes from the potentially unbounded number of tokens inside the net. The sets of infinite-state pLTS that can be generated by pushdown systems and Petri nets are incomparable.

**Definition 5.9.** A Petri net (PN) is a structure $N = (P, M_0, T, Pre, Post)$, where $P$ is a set of $m$ places; $M_0$ is the initial marking, i.e. a vector $M: P \to \mathbb{N}$ that assigns to each place of a PN a non-negative integer number of tokens; $T$ is a set of $n$ transitions; $Pre: P \times T \to \mathbb{N}$ and $Post: P \times T \to \mathbb{N}$ are the pre- and post- incidence functions that specify the arcs. We also define $C = Post - Pre$ as the incidence matrix of the net.

For $\mathbf{Mat} \in \{Pre, Post, C\}$ and $t \in T$, we write $\mathbf{Mat}(\cdot, t)$ for the column vector which, for every $i \in \mathbb{N}$, contains at the row $i$ the value $\mathbf{Mat}(i, t)$. A transition $t$ is enabled from $M$ iff $M \ge Pre(\cdot, t)$ and may fire yielding the marking $M' = M + C(\cdot, t)$. One writes $M[\sigma]$ to denote that the sequence of transitions $\sigma = t_{j_1} \cdots t_{j_k}$ is enabled from $M$, and $M[\sigma] M'$ to denote that the firing of $\sigma$ yields $M'$. One writes $t \in \sigma$ to denote that a transition $t$ is contained in $\sigma$. The length of the sequence $\sigma$ (denoted $|\sigma|$) is the number of transitions in the sequence, here $k$.

**Example 5.11.** Consider the PN of Figure 5.8. The initial marking is $M_0 = [2, 0, 0, 0, 0]$. Two tokens are needed to fire $t_2$, one in place $p_1$ and one in place $p_2$. In order to take the manufacturing analogy again, this means two items must be assembled here. In $p_1$ two items are already here, ready for assembling, however $p_2$ is empty. Firing $t_1$ delivers one item to $p_2$, enabling the transition $t_2$. Once $t_2$ was fired, one token in $p_1$ and one token in $p_2$ are consumed and one token (the assembled product) is produced in $p_3$. There two transitions can be fired. For example, the token can be consumed by $t_4$ producing a new token in $p_4$ which enables $t_6$. This last transition consumes a token without creating any new one, so it could correspond to the finished product being sent, and thus removed from consideration by this system. A sequence of transitions corresponding to the arrival of new products, their processing and removing from the system is $\sigma = t_0 t_1 t_2 t_4 t_6$. Firing this sequence uses exactly the tokens that are created inside it. Therefore it can be repeated: $\sigma^k$ is enabled from $M_0$ for all $k \in \mathbb{N}$.

The set of all sequences that are enabled at the initial marking $M_0$ is denoted $L(N)$, i.e., $L(N) = \{\sigma \in T^* | M_0[\sigma]\}$. A marking $M$ is reachable in $N$ iff there exists a firing sequence $\sigma$ such that $M_0[\sigma] M$. The set of all markings reachable from $M_0$ defines the reachability set of $N$ and is denoted $R(N)$. Given $k \in \mathbb{N}$, a place $p$ of a PN $N$ is
<figure><img src="image_76.png" /><figcaption>Figure 5.8: A Petri net. Circles are places and rectangles are transitions. In the initial marking, $p_1$ has two tokens represented by the two black dots.</figcaption></figure>

k-bounded if for all $M \in R(N)$, $M(p) \le k$. It is bounded if there exists $k \in \mathbb{N}$ such that $p$ is k-bounded. A PN is bounded (resp. k-bounded) iff all of its places are bounded (resp. k-bounded).

**Example 5.12.** Consider again the PN of Figure 5.8. Firing $t_1$ k times in $M_0$ leads to the marking $M_1 = [2, k, 0, 0, 0]$. Therefore the place $p_2$ is not bounded.

Probabilities are added to a PN by adding a fire rate to every transition in the following way.

**Definition 5.10.** A Stochastic Petri Net (SPN) is a pair $\mathcal{N} = (N, \mu)$ where $N$ is a PN and for all $t \in T$, $\mu(t) \in \mathbb{R}^+$ is the rate of firing of transition $t$.

The usual interpretation of rates is that, in a given marking, a delay is computed for every enabled transition $t$ with an exponential probability distribution function of parameter $\mu(t)$, i.e. the probability distribution function for the delay of transition $t$ is $f_t: x \in \mathbb{R}^+ \mapsto \mu(t)e^{-\mu(t)x}$. Multiple time semantics [HM09] can be chosen in an SPN to decide how these delays are used to determine which transition is fired. For instance, one could use (a) a *single server policy*: each transition can only be fired once by a given marking, (b) a *race policy*: the transition whose firing delay elapses first is assumed to be the one that will fire next and (c) a *resampling memory policy*: at the entrance in a marking, the remaining delays associated with all transitions are forgotten. Observe that as we use an exponential probability distribution, whether the delays are forgotten or not does not modify the probabilistic semantic. Using these choices, one could then define the semantics of the SPN as a continuous time Markov chain. However, as we only focus on discrete-time semantics here, we simplify the definition of the probabilistic behaviours of the SPN. We remove the time consideration from the semantics, and only keep the discrete time Markov chain induced by the continuous time Markov chain. This semantics keeps enough information to answer questions expressed for example by pLTL or pCTL formulae, but cannot address time-related issues such as mean reaction time.

Using the simplified interpretation of rates, as for pLTS, a probability measure can be defined on the sequences of transitions of a PN. Given a sequence $\sigma \in T^*$, we write $C(\sigma)$ for the set of infinite sequences prefixed by $\sigma$, $C(\sigma) = \{\sigma' \in T^\omega \mid \exists \sigma'' \in$
$T^\omega : \sigma' = \sigma\sigma''\}$. The set of infinite sequences is the support of a probability measure defined by Caratheodory's extension theorem from the probabilities of the cylinders: the probability of the cylinder starting by the empty sequence $\varepsilon$ is equal to 1 and, for $\sigma t$ a sequence, the probability of $C(\sigma t)$ in $M_0$, written $\mathbb{P}(\sigma t)$, satisfies

$$ \mathbb{P}(\sigma t) = \mathbb{P}(\sigma) \times \frac{\mu(t)}{\sum_{t' \in T, M_0[\sigma t']} \mu(t')} $$

As for pPDA, we enhance SPN with a mask function.

**Definition 5.11.** A partially observable SPN (POSPN) is a tuple $\langle \mathcal{N}, \Sigma_o, \mathcal{P} \rangle$ consisting of an SPN $\mathcal{N}$ equipped with a mapping $\mathcal{P} : T \to \Sigma_o \cup \{\varepsilon\}$ where $\Sigma_o$ is the set of observations.

From now on, we assume that there does not exist a marking $M$ reachable from $M_0$ and an infinite sequence $\sigma \in T^\omega$ such that $\mathcal{P}(\sigma) = \varepsilon$ and $M[\sigma]$. This assumption corresponds to the assumption of convergence that was made for pLTS. The observed sequence $w$ of observations associated with the sequence $\sigma$ is $w = \mathcal{P}(\sigma)$. Note that the length of a sequence $\sigma$ is always greater than or equal to the length of the corresponding observed sequence $w$ (denoted $|w|$). Given a word $w \in L^*$, we write $\mathbb{P}(w) = \sum_{\sigma \in P_e^{-1}(w)} \mathbb{P}(\sigma)$. Thanks to our earlier assumption, this sum is finite.

**Example 5.13.** Consider again the PN $\mathcal{N}$ of Figure 5.8. We define the POSPN $\langle (N, \mu), \{a, b, c\}, \mathcal{P} \rangle$ such that for all $t \in T$, $\mu(t) = 1$ and $\mathcal{P}(t_0) = \mathcal{P}(t_1) = b, \mathcal{P}(t_2) = a, \mathcal{P}(t_3) = \mathcal{P}(t_4) = \varepsilon$ and $\mathcal{P}(t_5) = \mathcal{P}(t_6) = c$. The observed sequence bac corresponds to the sequences $t_1t_2t_3t_5$ and $t_1t_2t_4t_6$, each of which has a probability $\frac{1}{72}$. Therefore $\mathbb{P}(bac) = \frac{1}{36}$.

The (potentially infinite) pLTS associated with a POSPN is based on the reachability graph of the PN: every state corresponds to a reachable marking.

**Definition 5.12.** A POSPN $\langle \mathcal{N}, \Sigma_o, \mathcal{P} \rangle$ defines a pLTS $\mathcal{A}_\mathcal{N} = (Q_\mathcal{N}, M_0, T, T_\mathcal{N}, \mathbf{P}_\mathcal{N})$ where:

* $Q_\mathcal{N} = R(M_0)$;

* $T_s pn = \{(M, t, M') | M[t]M'\}$;

* For every $(M, t, M') \in T_\mathcal{N}, \mathbf{P}_\mathcal{N}[(M, t, M')] = \frac{\mu(t)}{\sum_{t' \in T, M[t'] \mu(t')} \mu(t')}.

This pLTS is infinite when the reachability set is infinite. This happens iff the PN is not bounded. If the PN is $k$-bounded, for $k \in \mathbb{N}$, then the size of the generated pLTS is exponential in the size of the PN and in $k$. A POSPN is diagnosable according to a notion of diagnosability if the pLTS it generates is diagnosable.

In order to mirror the POpVPA restriction of POpPDA, we introduce the notion of visible POSPN.

**Definition 5.13.** A visible POSPN (VSPN) is a POSPN such that
* an unobservable transition does not modify the number of tokens in the system;

* for every pair of two transitions $t_1$ and $t_2$ with $\mathcal{P}(t_1) = \mathcal{P}(t_2) \text{ Post}(\cdot, t_1)1_v - \text{Pre}(\cdot, t_1)1_v = \text{Post}(\cdot, t_2)1_v - \text{Pre}(\cdot, t_2)1_v$ where $1_v$ is the vector with 1 in every position.

This second condition means that the number of tokens is modified similarly by $t_1$ and $t_2$. An observer of a VSPN thus knows at all time how many tokens are present in the system.

## 3.2 Undecidability of diagnosability for stochastic Petri nets

The exact diagnosability problems for $k$-bounded Petri nets are decidable as the generated pLTS is exponential and the exact diagnosability problems for finite pLTS are decidable. Moreover deciding if a Petri net is bounded is also decidable [Rac78]. For unbounded Petri nets however, while non-stochastic variants of diagnosability are known to be decidable on Petri nets, this is not the case for the stochastic notions of exact diagnosability. In order to show the undecidability, we reduce the problem of the language inclusion for Petri nets, namely: given two PN $N^1$ and $N^2$, an observation alphabet $\Sigma_o$ and a mask function $\mathcal{P}$ does $\mathcal{P}(L(N^1)) \subseteq \mathcal{P}(L(N^2))$ hold? This problem is known to be undecidable(see the survey [EN94]).

**Theorem 5.5.** *The FF-, IA- and FA-diagnosability problems of POSPN are undecidable.*

Given two PN $N^1$ and $N^2$, we build an SPN where the initial transition (which can be faulty), produces tokens in one among two components. This component corresponds to an enhanced copy of one of the two given PN. Then, a sequence of this PN is triggered. At any moment during this sequence, a transition starting a reset operation can be taken. This reset operation removes all the tokens from the PN then produces the tokens corresponding to the initial marking so that a new sequence can be read by the PN. The goal is that the fault is detected iff an observed sequence that can only be triggered from $N^1$ is observed in between two resets operation.

The difficulty of this reduction lies in the reset operation as one cannot test directly whether the places of the PN were correctly emptied. This information however, can be encoded in the observation. Let us now describe what happens in a reset. The reset starts and ends by an observable $\#}$ and, in between, produces a certain number of $\flat$. Each of these $\flat$ removes a token that was left inside the PN, so that at any moment, the observer knows precisely the number of tokens within the system. If there is still at least one token in the system when the second $\#}$ occurs, a gadget is used to allow the system to trigger any observed sequence so that no information is given to the observer. In other words, the observed sequence in between two reset operations give an information on the system iff the previous reset had correctly emptied the PN.

*Proof.* Let $N^1 = (P^1, M_0^1, T^1, Pre^1, Post^1)$ and $N^2 = (P^2, M_0^2, T^2, Pre^2, Post^2)$ be two PN, with the mask function $\mathcal{P}$ and the observation alphabet $\Sigma_o$.
Without loss of generality, we assume that the initial marking $M_0^i$ has a single token in a place $p_0^i$ for $i = 1, 2$, that every transition is observable and that there exists an integer $k \in \mathbb{N}$ such that the number of tokens in the system is equal to $k$ times the length of the sequence plus 1. This last assumption could be ensured by choosing $k$ as the maximum number of tokens added by a transition (this means number of tokens created minus number of tokens consumed) and adding an additional place where the unnecessary tokens are put (i.e. if a transition adds $k'$ tokens with $k' < k$, then this new place receives $k - k'$ tokens).

<figure><img src="image_77.png" /><figcaption>Figure 5.9: Reduction from language inclusion. The Figure 5.10 represents the content of the box $\mathbf{Box}^1$, it is similar for $\mathbf{Box}^2$. Transitions are labelled by their name and their observation.</figcaption></figure>

We build the POSPN $(P, M_0, T, Pre, Post, \mu, \Sigma_o \cup \{\# , \flat\}, \mathcal{P}')$ (represented in Figure 5.9) where:

* $P = P^1 \cup P^2 \cup \{p_0\} \cup \{p_{emp}^i, p_{run}^i, p_{err}^i \mid i = 1, 2\}$;

* $T = T^1 \cup T^2 \cup \{t_{in}^i, t_{\#}^i, t_{rese}^i, t_{resn}^i \mid i = 1, 2\} \cup \{t_a^i \mid a \in \Sigma, i = 1, 2\} \cup \{t_{emp}^p, t_{err}^p \mid p \in P^1 \cup P^2\}$;

* for $i \in \{1, 2\}, p \in P^i, t \in T^i, Pre(p,t) = Pre^i(p,t)$ and $Pre(p_{run}^i, t) = 1, Pre(p_0, t_{in}^i) = 1, Pre(p_{emp}^i, t_{\#}^i) = 1, Pre(p_{run}^i, t_{resn}^i) = 1, Pre(p_{err}^i, t_{rese}^i) = 1, Pre(p_{emp}^i, t_{emp}^p) = Pre(p_{emp}^i, t_{emp}^p) = 1, Pre(p, t_{err}^p) = Pre(p_{emp}^i, t_{err}^p) = 1$. When undefined, $Pre(p,t) = 0$;

* for $i \in \{1, 2\}, p \in P^i, t \in T^i, Post(p,t) = Post^i(p,t)$ and $Post(p_{run}^i, t) = 1, Post(p_0^i, t_{in}^i) = Post(p_{run}^i, t_{in}^i) = 1, Post(p_{run}^i, t_{\#}^i) = Post(p_0^i, t_{\#}^i) = 1$, for $a \in \Sigma, Post(p_{emp}^i, t_{emp}^i) = 1, Post(p_0^i, t_{emp}^i) = k, Post(p_{emp}^i, t_{resn}^i) = Post(p_{emp}^i, t_{rese}^i) = 1, Post(p_{emp}^i, t_{emp}^p) = 1, Post(p_0^i, t_{emp}^p) = 2, Post(p_{emp}^i, t_{emp}^p) = 1$. When undefined, $Post(p,t) = 0$;

* $\mathcal{P}'$ extends $\mathcal{P}$ on $N$ by, for $p \in P^1 \cup P^2, i \in \{1, 2\}, a \in \Sigma, \mathcal{P}'(t_{in}^i) = \# , \mathcal{P}'(t_{\#}^i) = \mathcal{P}'(t_{err}^p) = \mathcal{P}'(t_{rese}^i) = \mathcal{P}'(t_{resn}^i) = \# , \mathcal{P}'(t_a^i) = a, \mathcal{P}'(t_{emp}^p) = \flat$;

* for $i \in \{1, 2\}, p \in P_i, \mu(t_{rese}^i) = \mu(t_{resn}^i) = \mu(t_{emp}^p) = 2k(|\Sigma| + |T_1|)$ (assuming $|T_1| \ge 1$) and for every other transition $t, \mu(t) = 1$.
<figure><img src="image_78.png" /><figcaption>Figure 5.10: Content of the box Box¹.</figcaption></figure>

Moreover, $t_{in}^1 = f$ is the fault transition.

We show that the system is FF-diagnosable iff $\mathcal{P}(L(N^1)) \not\subseteq \mathcal{P}(L(N^2))$.

First note that the set of observed sequences associated with the infinite sequences starting by the transition $t_{in}^i$, denoted $L^i$, contains exactly the words of the form $\sharp w_1 \sharp^b n_1 \sharp \dots w_k \sharp^b n_k \sharp \dots$ where for all $1 \le j \le k$, (1) $w_j \in \Sigma_o^*$, (2) $\sum_{m=1}^j k|w_m| + 1 \ge \sum_{m=1}^j n_m$ and (3) $\sum_{m=1}^{j-1} k|w_m| + 1 = \sum_{m=1}^{j-1} n_m$ implies $w_j \in \mathcal{P}(L(N^i))$.

Suppose that $\mathcal{P}(L(N^1)) \subseteq \mathcal{P}(L(N^2))$. Let $\sigma$ be an infinite faulty sequence. As $\sigma$ is faulty, it initially fired $t_{in}^1$, thus $\mathcal{P}(\sigma) \in L^1$. Thanks to the above remark on the languages $L_i$, and as $\mathcal{P}(L(N^1)) \subseteq \mathcal{P}(L(N^2))$, $\mathcal{P}(\sigma) \in L^2$, therefore there exists a sequence $\sigma'$ starting by the transition $t_{in}^2$ with same observation as $\sigma$. Moreover this transition is not faulty as it did not fire $t_{in}^1$ initially and cannot fire it after the first transition. Therefore $\mathcal{P}(\sigma)$ is not surely faulty. As this is true for every faulty sequence, the system is not IF-diagnosable. The pLTS generated by this POSVN being finitely branching, according to Theorem 3.1, this implies that the POSPN is not FF-diagnosable.

Suppose now that $\mathcal{P}(L(N^1)) \not\subseteq \mathcal{P}(L(N^2))$. There thus exists a word $w$ such that $w \in \mathcal{P}(L(N^1)) \setminus \mathcal{P}(L(N^2))$. The observed sequences of $L_1$ such that there exists $i \in \mathbb{N}$ with $\sum_{m=1}^{i-1} k|w_m| + 1 = \sum_{m=1}^{i-1} n_m$ and $w_i = w$ are surely faulty as they do not belong to $L^2$. We denote $SL_1$ the set of these observed sequences. Let us show now that with probability 1 an infinite faulty sequence belongs to $SL_1$.

While a token is in $p_{err}^1$ or $p_{run}^1$, every transition taken with observation other than $\sharp$ produces $k$ tokens in the copy of $N_1$. Moreover, there are at most $|\Sigma| + |T_1|$ such transitions, each with rate 1. As the transition triggering $\sharp$ has rate $2k(|\Sigma| + |T_1|)$, the expectation of the number of tokens produced before a $\sharp$ is below $1+2k$. During a reset
operation, as for all places $p \in P_1$, $\mu(t_{emp}^p) = 2k(|\Sigma| + |T_1|)$ and the two transitions producing $\sharp$ have rates 1, the expectation of the number of token removed from the copy of $N_1$, assuming there are enough tokens within the system, is greater than $1 + k(|\Sigma| + |T_1|)^1$. Thus, with probability 1, a faulty sequence will infinitely often remove all the tokens from $P^1$. Therefore with probability 1, the observation of an infinite faulty sequence will be of the form $\sharp w_1 \sharp^b n_1 \sharp \dots \sharp w_k \sharp^b n_k \sharp \dots \in L^1$ with infinitely many $i \in \mathbb{N}$ such that $\sum_{m=1}^{i-1} k|w_m| + 1 = \sum_{m=1}^{i-1} n_m$. There is a probability $p > 0$ that for any such $i$, $w_i = w$ as $w \in \mathcal{P}(L(N^1))$. Therefore with probability 1, there exists $i \in \mathbb{N}$ such that $w_i = w$. Hence with an infinite faulty sequence almost surely belongs to $SL_1$. This implies that the POSPN is **IF-diagnosable** and thus **FF-diagnosable**.

In order to reduce the problem to FA-diagnosability and IA-diagnosability, we proceed similarly to the proof of Theorem 5.4: we add another place $p_c$ and a transition $t_c$ that takes a token from $p_{run}^2$ and puts it in $p_c$. This transition has firing rate 1 and observation $\sharp$. This is thus the only transition with this observation. As a consequence, taking this transition ensures the run is surely correct and remains that way. As a run entering Box$^2$ almost surely infinitely often contains a token in $p_{run}^2$, every run almost surely either becomes faulty or surely correct. Therefore $\lim_{n \to \infty} \mathcal{C}_{Amb}_n = 0$. This implies that in this POSVN, FF-diagnosability is equivalent to FA-diagnosability and IA-diagnosability. The rest of the proof above then applies. $\square$

An interesting feature of this proof is that the number of tokens in the POSPN used in the reduction can be deduced from the observation at all time. Therefore it is a VSPN. This gives the following result.

**Corollary 5.1.** *The FF-, IA- and FA-diagnosability problems of VSPN is undecidable.*

Thus, a restriction similar to what allowed us to regain decidability in POpPDA is not enough for POSPN.

# 4 Conclusion

The study of diagnosability for infinite-state pLTS depends heavily on the model used to finitely represent such a pLTS. Choosing a model that is too powerful leads quickly to undecidability. This has been shown with the undecidability proofs established for restricted classes of POpPDA and POSPN. These proof contains important differences. For instance, while undecidability is proven for every notion of stochastic (and in fact even non-stochastic) diagnosability in POpPDA, it is only proven for the exact notions of diagnosability in POSPN. Moreover, it is known that non-stochastic diagnosability is decidable in PN. In this sense, PN is a model for which there is still hope to get decidability results. We did not use the notion of coverability graph here, which gives a finite over-approximation of the reachability graph. Maybe an analysis of its language coupled with a study of the pathological behaviours (due to the over-approximation) may help in solving AFF-diagnosability. Moreover, the restriction that was used for

<footnote n="1">¹This value is obtained by analysing the case where only one place contains tokens.</footnote>
POSPN was chosen to mimic the one used on POpPDA, but is not necessarily the most
suited to the model.

Even if the POpPDA model has the strongest undecidability results, the appropriate restriction allows to regain decidability. For POpVPA, we could use model-checking methods to verify pLTL formula equivalent to the logical characterisation of Section 3 of Chapter 3. This only gave decidability of the notions for which a logical characterisation was known. Many questions are still left open partially as a consequence.

First, it would be interesting to find ways to close the complexity gap between our
upper and lower bound for the decidable diagnosability notions. The complexity of the
current decision procedure comes from an exponential determinisation and the use of a
PSPACE model-checking result. As we are interested in specific simple formula, there
may be a way to verify them in PTIME instead. The exponential of the determinisation
seems harder to remove.

Second, we would want to determine the decidability status of FA-diagnosability. If it is undecidable, it would confirm the difference in complexity with the other notions of exact diagnosability that the logical characterisations showed. However, this difference was shown for infinite-state pLTS in general, not for pLTS generated by POpVPA. It is possible that, as for finite systems, FA-diagnosability could be decided for POpVPA with the same complexity as the other exact diagnosability notions.

Finally, one may be interested in considering the case of the approximate diagnos-
ability notions. The method used here cannot be applied. Moreover, it is unclear now
what the POpVPA restriction simplifies for approximate notions of diagnosability. Re-
call that in the finite case, no determinisation were used to solve these notions, allowing
for a PTIME algorithm. We conjecture that this notion remains undecidable.
# Part III

## Controlling Information in Active Systems
<figure><img src="image_79.png" /></figure>
Chapter 6

Control of the degradation in
probabilistic systems

Embedded systems are often equipped with one (or more) controller(s) that can modify the behaviour of the system in reaction to the environment. Controllers can, for example, be used in order to maintain some vital functionalities of the system when facing a failure of a component. As controllers need to detect failures to react efficiently, it is tempting to add to controllers a diagnosis task. In other words, the system will contain some choices that can be made and which will alter the behaviour of the system while satisfying its specification. Controllers will then resolve these choices in order to render the system diagnosable. Controllers can be formalised in multiple different ways. For example, controllers could be within the system and thus have full knowledge of the behaviour of the system or they could rely on partial observation similarly to diagnosers. Since the goal is for controllers to deduce the existence of a fault, we cannot assume they know exactly the state of the system, and thus it must rely on partial observation. Formally, some of the observable events are controllable and, considering its current observation, the controller chooses which subset of events the system can trigger. A system is then said to be *actively diagnosable* if there exists a controller ensuring its diagnosability. In [SLT98], the authors showed that the active diagnosability problem is decidable in doubly exponential time for non-probabilistic systems. Then in [HHMS17], the authors designed a single exponential time algorithm and proved this complexity to be optimal. In the probabilistic case, the controllable system can be represented by a weighted transition system in the active case. This weighted transition system, coupled with a controller, produces a pLTS that can have infinitely many states (depending on the memory required by the controller). Thus, unsurprisingly, the active probabilistic diagnosability is more complicated than the corresponding passive problem: exact diagnosability is PSPACE-complete in pLTS (see Chapter 4) while it is EXPTIME-complete (see [BFH+14]) for controllable weighted LTS (a controllable variant of pLTS).

However the choices performed by the controller ensuring active diagnosis may have
a pernicious effect: to detect faults, controllers sometimes could favour the occurrence of
these faults! Forcing a fault in the system easily ensures diagnosability but contradicts
the initial goal of trying to maintain important functionalities of the system. Additional requirements can thus be made to controllers in order to manage the degradation of the system. Thus, a controller ensures *safe active diagnosability* if the controlled system is diagnosable and there is a positive probability that an infinite run is correct. In other words, the controller is allowed to increase the probability of a fault in order to ensure diagnosability, however it must maintain a positive probability of correct behaviours. A quantitative version of this requirement fixes a threshold $\varepsilon$ to the probability of correct runs that the controller must achieve. Unfortunately, safe active probabilistic diagnosability is undecidable [BFH$^+$14]. However, when limited to finite-memory controllers, the problem becomes decidable in NEXPTIME [BFH$^+$14]. Safe active diagnosability may be too strong a requirement for some real systems. Indeed, systems age and whatever control is applied, their components will eventually fail. Thus, in many cases, the fault can be considered unavoidable by the system. As a consequence, some systems are designed to behave correctly for a long period of time at the end of which they will be replaced by a new system. Instead of trying to force runs to stay correct, a controller could try to slow the speed at which the system fails. This expresses a different kind of requirements for the degradation control of a system. We formalise the framework and these requirements in Section 1, establishing a few semantical results along the way. Then, in Section 2.1 we present the algorithmic results.

This chapter develops and extends some of the results from [BHL17b].

# 1 Degradation of a probabilistic system

In this section, we give formal definitions of the degradation of a system. These degradation notions have to be satisfied by the system simultaneously to diagnosability, ensuring that any fault is detected and the system does not produce faults too often or too quickly. As this combination depends on the notion of diagnosability chosen and our focus here is more on degradation, we only use FF-diagnosability (which is the simplest notion of exact diagnosability that we introduced in Chapter 2).

In terms of observation, we use in this chapter a partition between observable and unobservable events (see discussion of Section 1.3 of Chapter 2).

In Subsection 1.1, we give the definitions of degradation for pLTS. Then, in Subsection 1.2, we show how to add a form of control and state the problems we are interested in.

## 1.1 Degradation in passive systems

When protecting a system from degradation, we want that it has a sufficient probability not to trigger a fault, or at least, that if a fault has to occur, it can be postponed as much as possible. We study different notions of the degradation of a system: safety, fault freeness and resiliency.

A pLTS is *safe* [BFH$^+$14] if it guarantees a positive probability of infinite correct runs. A pLTS that is not safe is thus doomed to trigger a fault with probability 1. The probability to stay correct could however be arbitrarily low. So we can quantify the
notion in order to refine it: for $\varepsilon > 0$, a pLTS is $\varepsilon$-safe if this probability is greater or equal to $\varepsilon$.

**Definition 6.1.** Let $\mathcal{A}$ be a pLTS, $\varepsilon > 0$. $\mathcal{A}$ is $\varepsilon$-safe if $\mathbb{P}(C_\infty) \ge \varepsilon$. It is safe if $\mathbb{P}(C_\infty) > 0$.

As pointed out in the introduction, in some cases, safety is a too strong requirement. We formalise now two alternatives: fault freeness and resiliency. Fault freeness aims at quantifying the period of time during which the pLTS is correct. We introduce a discount factor $\gamma \le 1$ on duration in order to vary the importance given to the length of the correct runs. When $\gamma$ is chosen small, only the beginning of the runs matter. This focus on the short-term is useful for systems that are regularly replaced for example. A greater $\gamma$ will on the opposite be chosen if one wants the system to be correctly performing for a longer time. The expectation of this discounted value is then compared to a threshold $v$.

**Definition 6.2.** Let $\mathcal{A}$ be a pLTS, $0 < \gamma \le 1$ and $v \in [0, \infty]$.

* $\mathcal{A}$ is $(\gamma, v)$-fault free if $\sum_{n \ge 1} \mathbb{P}(C_n) \gamma^n \ge v$.

* $\mathcal{A}$ is lasting fault free if it is $(1, \infty)$-fault free.

Clearly, for any fixed value of $\gamma$, the greater $v$ is, the better the system. Remark also that for $\gamma < 1$, the sum $\sum_{n \ge 1} \mathbb{P}(C_n)\gamma^n$ is finite and smaller than $\frac{1}{1-\gamma}$. For $\gamma = 1$, $\sum_{n \ge 1} \mathbb{P}(C_n)\gamma^n$ is the mean observable length of the maximal correct signalling prefix of a random run, which can be infinite. This justifies the name *lasting fault free* when the expectation is infinite.

The notion of resiliency is an alternative measure of degradation based on a factor of degradation ratio per time unit $\alpha < 1$. A pLTS is $\alpha$-resilient if the proportion of finite correct runs which stays correct on the next occurrence of an observable event is asymptotically greater than $\alpha$. This requirement has two qualitative variants: strong resiliency (resp. weak resiliency) requires $\alpha$-resiliency for every (resp. for at least one) $\alpha < 1$. In other words, a system is weakly resilient if asymptotically, the probability to be in a correct run of observable length $n$ is greater than an exponential $\alpha^n$. And a system is strongly resilient if this probability is asymptotically greater than all such exponential.

**Definition 6.3 (Resilient pLTS).** Let $\mathcal{A}$ be a pLTS.

* Let $0 < \alpha < 1$. $\mathcal{A}$ is $\alpha$-resilient if $\limsup_{n \to \infty} \frac{\alpha^n}{\mathbb{P}(C_n)} = 0$;

* $\mathcal{A}$ is strongly resilient if for all $0 < \alpha < 1$, $\mathcal{A}$ is $\alpha$-resilient;

* $\mathcal{A}$ is weakly resilient if there exists $0 < \alpha < 1$ such that $\mathcal{A}$ is $\alpha$-resilient.

**Example 6.1.** Let us consider the pLTS $\mathcal{A}$ of Figure 6.1. We give examples of the different notions of degradation by studying some choices of probabilities $(p_i)_{i \in \mathbb{N}}$.
<figure><img src="image_80.png" /><figcaption>Figure 6.1: An example of infinite pLTS with parametric probabilities $(p_i)_{i \in \mathbb{N}}$.</figcaption></figure>

A has a single correct run $\rho = q_0 a q_1 a q_2 \dots$, with observation $a^\omega$ while every faulty run contains an infinite number of $b'$. A is thus FF-diagnosable. Moreover, the probability of $\rho$ is $\prod_{n \ge 1} p_n$ and the probability of its prefix of length $n$ is $r_n = \prod_{i \le n} p_i$. Consequently, A is safe iff $\lim_{n \to \infty} r_n > 0$. This can be achieved by choosing $p_i = 1 - \frac{1}{2^i}$ for example.

Also, by direct application of the definition, A is lasting fault free iff $\sum_{n \ge 1} r_n = \infty$. Let us consider different values of $(p_i)_{i \in \mathbb{N}}$.

* Let $p_i = \frac{i}{i+1}$. Then $r_n = \frac{1}{n+1}$. Thus A is not safe but is lasting fault free. For every $\alpha < 1$, $\lim_{n \to \infty} (n+1)\alpha^n = 0$. Thus A is also strongly resilient.

* Let $p_i = \frac{i^2}{(i+1)^2}$. Then $r_n = \frac{1}{(n+1)^2}$. Thus A is neither safe nor lasting fault free. For every $\alpha < 1$, $\lim_{n \to \infty} (n+1)^2 \alpha^n = 0$. Thus A is strongly resilient.

* We inductively define two sequences $m_k$ and $n_k$ by:

$$n_k = 2^{\sum_{j<k} m_j} \text{ (hence } n_0 = 1) \text{ and } m_k = n_k + \sum_{j<k} m_j + n_j.$$

We also define the intervals:

$$\bullet I_k = [n_k + \sum_{j<k} m_j + n_j, \sum_{j \le k} m_j + n_j];$$

$$\bullet J_k = [\sum_{j \le k} m_j + n_j, n_{k+1} + \sum_{i \le k} m_j + n_j].$$

When $i \in I_k$, we choose $p_i = \frac{1}{2}$. When $i \in J_k$, we choose $p_i = 1$.

Observe that for all $n \in J_k$, $r_n = 2^{-\sum_{j \le k} m_j}$. Consequently

$$\sum_{n \ge 1} r_n \ge \sum_{k \ge 0} \sum_{n \in J_k} r_n = \sum_{k \ge 0} 2^{\sum_{j \le k} m_j} 2^{-\sum_{j \le k} m_j} = \infty.$$

Thus A is lasting fault free.

Let $k \in \mathbb{N}$ and $n = \sum_{j \le k} m_j + n_j$. Consequently, $r_n = 2^{-\sum_{j \le k} m_j}$. Fix $\alpha = \frac{1}{\sqrt{2}}$.

$$\frac{\alpha^n}{r_n} = 2^{\sum_{j \le k} m_j} (\sqrt{2})^{-\sum_{j \le k} m_j + n_j} \ge 2^{m_k} (\sqrt{2})^{-2m_k} = 1.$$

Therefore A is not $\alpha$-resilient.

The next theorem establishes the precise links between the qualitative versions of the three degradation notions for pLTS.
**Theorem 6.1.** Let $\mathcal{A}$ be a pLTS.

* If $\mathcal{A}$ is safe then $\mathcal{A}$ is lasting fault free and strongly resilient;

* If $\mathcal{A}$ is finite then:
  $\mathcal{A}$ is safe iff $\mathcal{A}$ is lasting fault free iff $\mathcal{A}$ is strongly resilient;

* There exists a lasting fault free pLTS that is not strongly resilient;

* There exists a strongly resilient pLTS that is not lasting fault free.

The first assertion is quickly obtained from the definitions and the last two come directly from the previous examples. The second one requires a bit more development. As the pLTS $\mathcal{A}$ is finite, one can use the notion of bottom strictly connected component used in Chapter 4 to characterise the diagnosability notions for finite pLTS. A notable difference is that, in Chapter 4, we had to consider the BSCC of an enriched pLTS. Here, we show that every notion of degradation is equivalent to the existence of a reachable correct BSCC of the pLTS $\mathcal{A}$.

*Proof.* Let $\mathcal{A}$ be a safe pLTS. There exists $\varepsilon > 0$ such that for all $n$, $\mathbb{P}(C_n) \ge \varepsilon$. Thus, $\sum_{n \ge 1} \mathbb{P}(C_n) \ge \sum_{n \ge 1} \varepsilon = \infty$. Moreover, for all $\alpha < 1$, $\lim_{n \to \infty} \frac{\alpha^n}{\mathbb{P}(C_n)} \le \lim_{n \to \infty} \frac{\alpha^n}{\varepsilon} = 0$. Thus $\mathcal{A}$ is both lasting fault free and strongly resilient.

Let $\mathcal{A}$ be a finite pLTS. Observe that every BSCC of $\mathcal{A}$ contains either only correct states or only faulty states. Accordingly we can speak of faulty BSCC or correct BSCC. As $\mathcal{A}$ is a finite pLTS, we know that almost surely an infinite run reaches a BSCC and that the mean time to reach a BSCC is finite (see e.g. [BK08]). Due to the first result, $\mathcal{A}$ is safe iff there exists a reachable correct BSCC.

Suppose that $\mathcal{A}$ is not safe.

* Every reachable BSCC are faulty which implies that the mean time to reach a faulty BSCC if finite. This mean time is an upper bound on the mean observable length of the maximal signalling prefix of a correct run. Thus $\mathcal{A}$ is not lasting fault free.

* We note $m = |Q|$. For all $q \in Q_c$, there exists $\rho_q$ a run starting in $q$ composed of an elementary run from $q$ to a faulty BSCC followed by an elementary run (or circuit) in the BSCC of which only the last event is observable (by convergence). This run has an observable length smaller or equal to $m$. We note $\mu_q$, the probability of that run and $\mu = \min_{q \in Q_c} \mu_q$. Consider a signalling run $\rho$ of observable length $n$ for an arbitrary $n$ and ending in $q \in Q_c$. From the existence of $\rho_q$, $\mathbb{P}(\rho' \in \mathbb{SR}_{n+m} \cap C \mid \rho \le \rho') \le (1-\mu)\mathbb{P}(\rho)$. Thus $\mathbb{P}(C_{n+m}) \le (1-\mu)\mathbb{P}(C_n)$. So, $\mathbb{P}(C_n) \in O((1-\mu)^{\frac{n}{m}})$. Choosing $\alpha = (1-\mu)^{\frac{1}{m}}$, $\mathcal{A}$ is not $\alpha$-resilient and thus not strongly resilient. $\square$

## 1.2 Controlled systems

Extending the pLTS formalism in order to express control requires to fix at least two features of this formalism: the nature of the control and the distribution of probabilities of the controlled system. Intuitively, we want the control and the diagnosis to be realised by the same device: from its observations, it restricts the system in order to
diagnose it and limit its degradation. The control is thus done with partial observation. So we recall the *Controllable Labelled Transition System* (CLTS) from [BFH$^+$14]. In this model, in order to specify the control, a subset of observable events is considered controllable. The controller forbids a subset of controllable events depending on the sequence of observations it has received. Thus the controller cannot modify its choice between two observations. The transitions of the system are no more labelled by (rational) probabilities but by (integer) weights which measure their relative possibility of occurrence. Given a state and a set of forbidden controllable actions, the weights of the transitions exiting this state and labelled by uncontrollable or allowed controllable actions are normalised to obtain a probability distribution. If the controller does not introduce any deadlock, the controlled system is a live pLTS.

**Definition 6.4.** A Controllable Labelled Transition System (CLTS) is a tuple $C = \langle Q, q_0, \Sigma, T \rangle$ where:

* $Q$ is a set of states with an initial state $q_0 \in Q$;

* $\Sigma = \Sigma_o \uplus \Sigma_u$ is a finite set of events partitioned into the set of observable events $\Sigma_o$ containing controllable events $\Sigma_c \subseteq \Sigma_o$ and the set of unobservable events $\Sigma_u$ containing the fault $f$;

* $T: Q \times \Sigma \times Q \to \mathbb{N}$ is the transition function that associates an integer weight with each transition.

A CLTS induces a labelled transition system which transition relation is defined by $q \xrightarrow{a} q'$ if $T(q, a, q') > 0$. The extended relation $\Rightarrow$ and the other usual definitions are defined as for pLTS. We assume that the CLTS is convergent and live.

<figure><img src="image_81.png" /><figcaption>Figure 6.2: An example of CLTS. Weights are all equal to 1 and omitted on the figure. The only controllable event is $b$.</figcaption></figure>

**Example 6.2.** A CLTS $C$ is represented in Figure 6.2. If the control enables every event, the run $q_0 u q_1 a q_1 b q_2$ has probability $1/8$. If the control always forbids 'b', this same run has probability 0. And if it only allows 'b' after observing one 'a', it has probability $1/4$.
We now formalise the ingredients necessary to define how to control CLTS. Let $\Sigma^{\bullet} \subseteq \Sigma$ and $q \in Q$, let us write $G^{\Sigma^{\bullet}}(q)$ for the sum of the weights of the transitions exiting $q$ and labelled by an event of $\Sigma^{\bullet}$. Using this sum, we define a normalisation of the transition relation restricted to the events of $\Sigma^{\bullet}$ by:

$$T^{\Sigma^{\bullet}}(q, a, q') = \begin{cases} \frac{T(q, a, q')}{G^{\Sigma^{\bullet}}(q)} & \text{if } a \in \Sigma^{\bullet} \text{ and } G^{\Sigma^{\bullet}}(q) > 0 \\ 0 & \text{otherwise.} \end{cases}$$

A strategy of a CLTS $C$ is a function $\pi : \Sigma_o^* \to \text{Dist}(2^\Sigma)$ such that for all $w \in \Sigma_o^*$ and all $\Sigma^\bullet \in \text{Supp}(\pi(w))$, $\Sigma \setminus \Sigma_c \subseteq \Sigma^\bullet$. In other words, given an observation, a strategy chooses (possibly with randomisation) a set of allowed events that contains the uncontrollable events. Let $C$ be a CLTS and $\pi$ be a strategy, we consider the configurations of the form $(w, q, \Sigma^\bullet) \in \Sigma_o^* \times Q \times 2^\Sigma$ with $w$ the observed sequence, $q$ the current state and $\Sigma^\bullet$ the set of allowed events by $\pi$ after observation of $w$. We inductively define the set $\text{Reach}_\pi(C)$ of the reachable configurations under $\pi$ by:

* for all $\Sigma^\bullet \in \text{Supp}(\pi(\varepsilon))$, we have $(\varepsilon, q_0, \Sigma^\bullet) \in \text{Reach}_\pi(C)$;

* for all $(w, q, \Sigma^\bullet) \in \text{Reach}_\pi(C)$ and all $a \in \Sigma_u$ such that $q \xrightarrow{a} q'$, we have $(w, q', \Sigma^\bullet) \in \text{Reach}_\pi(C)$, and the corresponding transition is denoted by $(w, q, \Sigma^\bullet) \xrightarrow{a} \pi(w, q', \Sigma^\bullet)$;

* for all $(w, q, \Sigma^\bullet) \in \text{Reach}_\pi(C)$, all $a \in \Sigma_o \cap \Sigma^\bullet$ such that $q \xrightarrow{a} q'$ and all $\Sigma^\bullet' \in \text{Supp}(\pi(wa))$, we have $(wa, q', \Sigma^\bullet') \in \text{Reach}_\pi(C)$, and the corresponding transition is denoted by $(w, q, \Sigma^\bullet) \xrightarrow{a} \pi(wa, q', \Sigma^\bullet')$.

A strategy $\pi$ is called *live* if for every configuration $(w, q, \Sigma^\bullet) \in \text{Reach}_\pi(C)$, we have $G^{\Sigma^\bullet}(q) \neq 0$. Only the live strategies are relevant as the other strategies create deadlocks. We are now in a position to introduce the semantics of a CLTS controlled by a live strategy $\pi$ in terms of a live pLTS. Its set of states is $\text{Reach}_\pi(C)$ augmented by an initial state to randomly choose the initial control according to $\pi(\varepsilon)$. The probability distributions are based on $T^{\Sigma^\bullet}$ if the current control is $\Sigma^\bullet$ combined with the random choice of $\pi$ in case of an observable event occurrence.

**Definition 6.5.** Let $C$ be a CLTS and $\pi$ be a live strategy, the pLTS $C_\pi$ induced by the strategy $\pi$ on $C$ is defined by $C_\pi = \langle Q_\pi, \Sigma, q_{0\pi}, T_\pi, \mathbf{P}_\pi \rangle$ where:

* $Q_\pi = \{q_{0\pi}\} \cup \text{Reach}_\pi(C)$;

* for every $(\varepsilon, q_0, \Sigma^\bullet) \in \text{Reach}_\pi(C)$, $(q_{0\pi}, u, (\varepsilon, q_0, \Sigma^\bullet)) \in T_\pi$;

* for every $(w, q, \Sigma^\bullet), (w', q', \Sigma^\bullet') \in \text{Reach}_\pi(C)$, $((w, q, \Sigma^\bullet), a, (w', q', \Sigma^\bullet')) \in T_\pi \text{ iff } (w, q, \Sigma^\bullet) \xrightarrow{a} \pi(w', q', \Sigma^\bullet')$;

* for every $(\varepsilon, q_0, \Sigma^\bullet) \in \text{Reach}_\pi(C)$, $\mathbf{P}_\pi(q_{0\pi}, u, (\varepsilon, q_0, \Sigma^\bullet)) = \pi(\varepsilon)(\Sigma^\bullet)$;

* for every $((w, q, \Sigma^\bullet), a, (w, q', \Sigma^\bullet)) \in T_\pi$ and every $a \in \Sigma_u$, $\mathbf{P}_\pi((w, q, \Sigma^\bullet), a, (w, q', \Sigma^\bullet)) = T^{\Sigma^\bullet}(q, a, q')$;
$$
\bullet \text{ for every } \left( (w, q, \Sigma^{\bullet}), a, (wa, q', \Sigma'^{\bullet}) \right) \in T_{\pi} \text{ and every } a \in \Sigma_o \cap \Sigma^{\bullet}, \\
\mathbf{P}_{\pi} \left( (w, q, \Sigma^{\bullet}), a, (wa, q', \Sigma'^{\bullet}) \right) = T^{\Sigma^{\bullet}}(q, a, q') \cdot \pi(w.a)(\Sigma'^{\bullet}).
$$

**Example 6.3.** Consider the CLTS *C* depicted in Figure 6.2. There are two possible enabled subsets: Σ and Σ \ {b} that we denote Σ⁻. Let us define the strategy π by π(aⁿ) = pⁿ · Σ⁻ + rⁿ · Σ with pⁿ + rⁿ = 1 for all n ∈ N and π(w) = **1**_Σ otherwise. The generated pLTS Cπ is infinite. A part of it is represented in Figure 6.3. Let us develop the distribution of probabilities exiting the configuration (ε, q₁, Σ). The two transitions exiting q₁ are enabled with equal probabilities, thus normalised to 0.5. Since ‘a’ and ‘b’ are observable, the new control is chosen, in the case where a ‘a’ is observed, by a probabilistic choice p₁ · Σ⁻ + r₁ · Σ while if a ‘b’ is observed, there is a deterministic choice **1**_Σ. This results in three transitions with probability 0.5p₁, 0.5r₁ and 0.5 respectively.

<figure><img src="image_82.png" /><figcaption>Figure 6.3: An example of controlled CLTS.</figcaption></figure>

In Definition 3.2, page 58, we introduced finite-memory diagnosers. Similarly, one
can formally define finite-memory strategies for CLTS using a set of memory states, a
memory update function indicating how observations modify the memory state and a
decision function mapping every memory state to a choice of the strategy. The size of
the memory is the number of memory states. If the size of the memory of a strategy π
of a CLTS C is finite, then C_π is also finite.
Let us define the problems of active diagnosis in the context of the degradation control. Roughly speaking, given a CLTS, one asks whether there exists a strategy such that the associated pLTS is FF-diagnosable and satisfies the required property related to degradation. We distinguish, as usually done, the quantitative problems and the qualitative ones (such as safety, lasting fault freeness and strong/weak resiliency).

**Definition 6.6 (Quantitative problems).** Given a CLTS $\mathcal{C}$, $0 < \varepsilon, \alpha < 1$, $0 < \gamma \le 1$ and $v \in [0, \infty]$:

* The $\varepsilon$-safe active diagnosis problem consists in deciding if there exists a strategy $\pi$ such that $C_\pi$ is FF-diagnosable and $\varepsilon$-safe;

* The $(\gamma, v)$-fault free active diagnosis problem consists in deciding if there exists a strategy $\pi$ such that $C_\pi$ is FF-diagnosable and $(\gamma, v)$-fault free;

* The $\alpha$-resilient active diagnosis problem consists in deciding if there exists a strategy $\pi$ such that $C_\pi$ is FF-diagnosable and $\alpha$-resilient.

**Definition 6.7 (Qualitative problems).** Given a CLTS $\mathcal{C}$:

* The safe active diagnosis problem consists in deciding if there exists a strategy $\pi$ such that $C_\pi$ is FF-diagnosable and safe;

* The lasting fault free active diagnosis problem consists in deciding if there exists a strategy $\pi$ such that $C_\pi$ is FF-diagnosable and lasting fault free;

* The strongly resilient active diagnosis problem consists in deciding if there exists a strategy $\pi$ such that $C_\pi$ is FF-diagnosable and strongly resilient;

* The weakly resilient active diagnosis problem consists in deciding if there exists a strategy $\pi$ such that $C_\pi$ is FF-diagnosable and weakly resilient.

When tackling problems on strategies, the first step is to wonder if one can restrict the strategies that are considered. For example, can we use strategies with finite memory. This cannot be done as shown in the following example.

**Example 6.4.** In order to illustrate the impact of taking into account infinite memory strategies, let us examine the CLTS $\mathcal{C}$ of Figure 6.2. The only ambiguous observed sequence is $a^\omega$. A strategy $\pi$ thus makes it FF-diagnosable iff the probability of faulty runs with this observed sequence in $C_\pi$ is 0. This is done by allowing ‘b’ often enough so that it occurs with probability 1. However, the only correct run is $\rho = q_0 u(q_1 a)^\omega$ with observation $a^\omega$. Thus, $\mathcal{C}$ is not actively safely diagnosable.

Let us denote, as in Example 6.3, by $p_n$ the probability to forbid ‘b’ after the observed sequence $a^n$ given by the strategy $\pi$. Then $\mathbb{P}_{C_\pi}(q_0 u(aq_1)^n) = \frac{1}{2} \prod_{i \le n} \frac{1+p_i}{2}$. Thus, by choosing $p_n = 1 - \frac{1}{n+1}$, $C_\pi$ is FF-diagnosable, lasting fault free and strongly resilient. On the other hand, no finite-memory strategy could achieve this goal since otherwise by Theorem 6.1, $\mathcal{C}$ would be actively safely diagnosable.

Restricting one-self to finite-memory strategies is thus a loss of generality. It can however be useful to regain decidability of difficult problems as we will see later.
## 2 Algorithmic analysis of degradation

In this section we answer the problems listed above by establishing if they are decidable and in the positive case by giving their exact complexities. We start in Subsection 2.1 by proving the undecidability of the quantitative problems. As a consequence, in Subsection 2.2, we focus on the qualitative problems and prove the EXPTIME-completeness of all of them except the safe active diagnosis problem. Lastly, in Subsection 2.3, we see that the safe active diagnosis problem is more difficult but can still be decided efficiently when restricted to finite-memory strategies.

### 2.1 Undecidability of the quantitative problems

The quantitative problems turn out to all be undecidable. The proofs of these results are obtained by reductions from the emptiness problem of probabilistic automata<fnref n="1" />.

We start by showing the result for the $\varepsilon$-safe diagnosis problem, with $\varepsilon > 0$.

**Proposition 6.1.** *The $\varepsilon$-safe active diagnosis problem is undecidable.*

The idea of this proof is the following. Given a probabilistic automaton $A$ with alphabet $\Sigma$, one builds a CLTS $C$ composed of two independent parts each one initially entered with probability $\frac{1}{2}$ by an unobservable transition. The unobservable event leading to the first part is the fault $f$ which can only be detected almost surely if the observable event $\# \notin \Sigma$ occurs with probability 1. The second part is constituted of a CLTS version of $A$ augmented by exiting transitions. One can exit $A$ by allowing a $\#$. When this happens, if the system was in a final state of $A$ it goes to a correct BSCC of the CLTS, ensuring the run will remain correct. Else a fault is triggered on the next step. This construction ensures the following properties. If there exists a word $w$ with an acceptance probability at least $2\varepsilon$, the strategy which consists in forcing the observed sequence $w\#$ ensures a probability of the set of infinite correct runs of at least $\varepsilon$. In the opposite case, we show that no strategy can achieve this threshold.

*Proof.* Let $0 < \varepsilon < 1/2$. We proceed here by reduction from the problem of the existence of a word $w$ such that $P_A(w) \ge 2\varepsilon$. We consider a probabilistic automaton $A = \langle Q, q_0, \Sigma, (P_a)_{a \in \Sigma}, F \rangle$ for which w.l.o.g. we assume that: (1) $\Sigma \cap \{u, f, \#\}, \#\} = \emptyset$ and (2) the probabilities are fractions $\frac{n}{d}$ with fixed denominator $d \in \mathbb{N}$. One builds the CLTS $C = \langle Q', q'_0, \Sigma', T \rangle$ described in Figure 6.4 and defined by:

* $Q' = Q \cup \{q'_0, q_c, q_f, f_1, f_2\}$;

* $\Sigma' = \Sigma \cup \{f, u, \#\}, \#\}$, $\Sigma_u = \{f, u\}$ and $\Sigma_c = \Sigma \cup \{\#\}$;

* the transition function $T$ is defined as follows.

1.

$$ 
\begin{aligned}
T(q'_0, f, f_1) &= T(q'_0, u, q_0) = T(q_c, \#\), q_c) = T(q_f, f, f_2) = T(f_2, \#\), f_2) \\
&= T(f_1, \#\), f_2) = 1;
\end{aligned}
$$

<footnote n="1">¹see page 115.</footnote>
2. for every $a \in \Sigma$, $T(f_1, a, f_1) = 1$;

3. for every $s, s' \in Q$ and every $a \in \Sigma$, $T(s, a, s') = d \cdot \mathbf{P}_a(s, s')$;

4. for every $s \in F$, $T(s, \sharp, q_c) = 1$ and for every $s \in S \setminus F$, $T(s, \sharp, q_f) = 1$;

5. for every other triplet, $T$ is equal to 0.

As detailed above, the probabilities in $A$ are all multiplied by their common denominator $d$, to obtain integer weights, and we write $d \cdot A$ in the figure to represent this scaling.

<figure><img src="image_83.png" /><figcaption>Figure 6.4: Reduction to $\varepsilon$-safe diagnosability.</figcaption></figure>

Let us show that there exists a strategy $\pi$ such that $C_\pi$ is $\varepsilon$-safe and FF-diagnosable iff there exists a word $w$ accepted in $A$ with probability at least $2\varepsilon$.

Remark first that, for $\pi$ an arbitrary strategy, $C_\pi$ is FF-diagnosable iff $\sharp$ occurs almost surely in a run. Indeed, an observed sequence $w \in \Sigma^*$ is ambiguous. On the other hand every faulty run $\rho$ triggering a $\sharp$ will produce a $\sharp$ removing the ambiguity.

* Assume there exists a word $w = a_1 \dots a_k \in \Sigma^*$ such that $\mathbf{P}_A(w) \ge 2\varepsilon$. We define the deterministic strategy $\pi$ by:

* $\pi(w) = \{\mathbf{f}, u, \sharp, \flat\}$;

* for all $0 \le i < k$, $\pi(a_1 \dots a_i) = \{\mathbf{f}, u, a_{i+1}, \flat\}$;

* $\pi(w') = \Sigma'$ for any other word $w'$.

Observe that after at most $k+1$ observable events, any run leaves $Q \cup \{f_1\}$ and thus $\flat$ occurs almost surely implying that $C_\pi$ is FF-diagnosable. Moreover, the probability of correct runs with observation $w\sharp\flat$ is equal to $\frac{\mathbf{P}_A(w)}{2}$: it is the probability to take $u$ initially times the probability to end the observation of $w$ in an accepting state of $A$. As $\mathbf{P}_A(w) \ge 2\varepsilon$, this ensures that $C_\pi$ is $\varepsilon$-safe.
• Assume now that for all $w \in \Sigma^*$, $\mathbf{P}_A(w) < 2\varepsilon$. Let $\pi$ be a strategy such that $C_\pi$ is FF-diagnosable, thus with probability 1 an infinite run contains a $\sharp$. Moreover, this run is correct iff the first $\sharp$ is followed by a second $\sharp$. Then we have:

$$ 
\begin{align*}
\mathbb{P}_{\pi}(C_{\infty}) &= \sum_{w \in \Sigma^*} \mathbb{P}_{\pi}(w_{\sharp}\sharp) \\
&= \sum_{w \in \Sigma^*} \frac{\mathbb{P}_{\pi}(w_{\sharp}) \cdot \mathbf{P}_A(w)}{2} \\
&< \varepsilon \sum_{w \in \Sigma^*} \mathbb{P}_{\pi}(w_{\sharp}) \\
&= \varepsilon.
\end{align*}
$$

Therefore, $C_\pi$ is not $\varepsilon$-safe, which concludes the reduction and proves undecidability of the $\varepsilon$-safe active diagnosis problem. $\square$

We now turn to the $(\gamma, v)$-fault free active diagnosis problem. It is done once again by reduction from the emptiness problem of PA. In fact, it has many similarities with the previous proof, but instead of reaching a state $q_c$ where the run will stay correct, being accepted by the PA only postpones the fault by one step.

**Proposition 6.2.** *The $(\gamma, v)$-fault free active diagnosis problem is undecidable.*

The idea of this proof is the following. Given a probabilistic automaton $A$ with alphabet $\Sigma$, one builds a CLTS $C$ composed of two independent parts each one initially entered with probability $\frac{1}{2}$ by an unobservable transition. The unobservable event leading to the first part is the fault $f$ which can only be detected almost surely if the observable event $\sharp \notin \Sigma$ occurs with probability 1. The second part is constituted of a CLTS version of $A$ augmented by exiting transitions. One exits $A$ with probability $\frac{1}{2}$ at every step towards a faulty sub-part except if the $\sharp$ event is triggered. In this case, if the system was in a final state of $A$ it leaves the states of $A$ and postpones the occurrence of a fault by one time step compared to if it stayed in $A$. This construction ensures the following properties. If there exists a word $w$ with an acceptance probability at least $\frac{1}{2}$, the strategy which consists in forcing the observed sequence $w_{\sharp}$ as long as the run stays in $A$ ensures an average observable length (without discount) of the maximal correct signalling prefix greater or equal to 1. In the opposite case, we show that no strategy can achieve this threshold.

*Proof.* We proceed here by reduction from the problem of the existence of a word $w$ such that $\mathbf{P}_A(w) \ge \frac{1}{2}$. We consider the probabilistic automaton $A = \langle Q, q_0, \Sigma, (\mathbf{P}_a)_{a \in \Sigma}, F \rangle$ for which w.l.o.g. we assume that: (1) $\Sigma \cap \{u, \mathbf{f}, \sharp, \sharp\} = \emptyset$ and (2) the probabilities are fractions $\frac{n}{d}$ with fixed denominator $d$. One builds the CLTS $C = \langle Q', q'_0, \Sigma', T \rangle$ described in Figure 6.5 and defined by:

* $Q' = Q \cup \{q'_0, q'_c, q_c^1, q_c^2, q_c^3, f_1, f_2\}$;

* $\Sigma' = \Sigma \cup \{\mathbf{f}, u, \sharp, \sharp\}$, $\Sigma_u = \{\mathbf{f}, u\}$ and $\Sigma_c = \Sigma \cup \{\sharp\}$;
• the transition function $T$ is defined as follows.

1.

$$ 
\begin{aligned}
T(q'_0, \mathbf{f}, f_1) &= T(q'_0, u, q_0) = T(q_c^1, \#_c, q_c^3) = T(q_c^3, \#_c, q_c^3) = T(q_c^3, \mathbf{f}, f_2) \\
&= T(q_c^2, \mathbf{f}, f_2) = T(f_2, \#_c, f_2) = T(f_1, \#_c, f_2) = 1;
\end{aligned}
$$

2. for every $a \in \Sigma$, $T(f_1, a, f_1) = 1$;

3. for every $s, s' \in Q$ and every $a \in \Sigma$, $T(s, a, s') = d \cdot \mathbf{P}_a(s, s')$ and $T(s, a, q_c^2) = d$;

4. for every $s \in F$, $T(s, \#_c, q_c^1) = 1$ and for every $s \in S \setminus F$, $T(s, \#_c, q_c^2) = 1$;

5. for every other triplet, $T$ is equal to 0.

Here again, the probabilities in $A$ are multiplied by the constant $d$, which we abbreviate in the figure by $d \cdot A$.

<figure><img src="image_84.png" /><figcaption>Figure 6.5: Reduction to $(\gamma, v)$-fault free active diagnosability.</figcaption></figure>

Let us show that there exists a strategy $\pi$ such that $C_\pi$ is (1, 1)-fault free and FF-diagnosable iff there exists a word $w$ accepted in $A$ with probability at least $\frac{1}{2}$.

Remark first that, for $\pi$ an arbitrary strategy, $C_\pi$ is FF-diagnosable iff $\#_c$ occurs almost surely in a run. Indeed an observed sequence $w \in \Sigma^*$ is ambiguous. On the other hand every run $\rho$ leaving $Q \cup \{f_1\}$ almost surely reaches $f_2$ where $\#_c$ occurs and, whatever $\rho$, a fault has occurred.

• Assume that there exists $w = w_1 \dots w_k \in \Sigma^*$ such that $\mathbf{P}_A(w) \ge \frac{1}{2}$. We define the deterministic strategy $\pi$ by:

• $\pi(w) = \{\mathbf{f}, u, \#_c, \#_c\}$;

• for all $0 \le i < k$, $\pi(w_1 \dots w_i) = \{\mathbf{f}, u, w_{i+1}, \#_c\}$;
• $\pi(w') = \Sigma'$ for any other word $w'$.

Observe that after at most $k+1$ observable events, any run leaves $S \cup \{f_1\}$ and thus $\sharp$ occurs almost surely implying that $C_\pi$ is diagnosable.

By definition of $C$ and $\pi$, a correct signalling run $\rho$ such that $\mathcal{P}(\rho) = w_1 \dots w_i$ for $i < k$ has probability $\frac{1}{2}$ of staying correct at the next step depending on if the current state is $q_c^2$ or belongs to $Q$. Similarly, a correct signalling run $\rho$ such that $\mathcal{P}(\rho) = w_1 \dots w_k$ has a probability $\mathbf{P}_A(w)$ of being at the next step in $q_c^1$ and $1 - \mathbf{P}_A(w)$ in $q_c^2$. Moreover, in state $q_c^3$, a correct signalling run has a probability $\frac{1}{2}$ of staying correct and in $q_c^3$ at the next step. Therefore for all $n \in \mathbb{N}$, we have $n \le k$ implies $\mathbb{P}(C_n) = (\frac{1}{2})^n$ and $n > k$ implies $\mathbb{P}(C_n) = (\frac{1}{2})^{n-1}\mathbf{P}_A(w) \ge (\frac{1}{2})^n$. Finally: $\sum_{n=1}^\infty \mathbb{P}(C_n) \ge \sum_{n=1}^\infty (\frac{1}{2})^n = 1$.

• Assume that for all $w \in \Sigma^*$, $\mathbf{P}_A(w) < \frac{1}{2}$. Let $\pi$ be a strategy such that $C_\pi$ is diagnosable. Observe that (using a slight and understandable abuse of language):

$$ \mathbb{P}_{\pi}(C_n) = \sum_{w \in \Sigma^n} \mathbb{P}_{\pi}(w \wedge C) + \sum_{w \in \Sigma^{n-1}} \mathbb{P}_{\pi}(w \sharp \wedge C) + \sum_{1 < k \le n} \sum_{w \in \Sigma^{n-k}} \mathbb{P}_{\pi}(w \sharp^k \wedge C). $$

Let us show that $\mathbb{P}_{\pi}(C_{n+1}) \le \frac{\mathbb{P}_{\pi}(C_n)}{2}$ with a strict inequality if there exists $w \in \Sigma^{n-1}$ with $\mathbb{P}_{\pi}(w\sharp) > 0$.

$$ \mathbb{P}_{\pi}(C_{n+1}) = \sum_{w \in \Sigma^n} \sum_{x \in \Sigma \cup \{\sharp\}} \mathbb{P}_{\pi}(wx \wedge C) + \sum_{w \in \Sigma^{n-1}} \mathbb{P}_{\pi}(w\sharp^2 \wedge C) + \\ \sum_{1 < k \le n} \sum_{w \in \Sigma^{n-k}} \mathbb{P}_{\pi}(w\sharp^{k+1} \wedge C) $$

Let us examine the three terms.

◦ A correct run $\rho$ with observed sequence $w$ has a conditional equiprobability that $\text{last}(\rho) \in Q$ or $\text{last}(\rho) = q_c^2$. Thus, $\sum_{w \in \Sigma^n} \sum_{x \in \Sigma \cup \{\sharp\}} \mathbb{P}_\pi wx = \frac{1}{2} \sum_{w \in \Sigma^n} \mathbb{P}_\pi w$.

◦ A correct run $\rho$ with observed sequence $w\sharp^k$ such that $k > 1$ verifies $\text{last}(\rho) = q_c^3$. Thus, $\sum_{1 < k \le n} \sum_{w \in \Sigma^{n-k}} \mathbb{P}_\pi(w\sharp^{k+1} \wedge C) = \frac{1}{2} \sum_{1 < k \le n} \sum_{w \in \Sigma^{n-k}} \mathbb{P}_\pi(w\sharp^k \wedge C)$

◦ A correct run $\rho$ of observed sequence $w\sharp$ has a conditional probability $\mathbf{P}_A(w)$ that $\text{last}(\rho) = q_c^1$ and $1 - \mathbf{P}_A(w)$ that $\text{last}(\rho) = q_c^2$. Thus:

$$ \sum_{w \in \Sigma^{n-1}} \mathbb{P}_{\pi}(w\sharp^2 \wedge C) = \sum_{w \in \Sigma^{n-1}} \mathbf{P}_{A}(w) \mathbb{P}_{\pi}(w\sharp \wedge C) \le \frac{1}{2} \sum_{w \in \Sigma^{n-1}} \mathbb{P}_{\pi}(w\sharp \wedge C) $$

with a strict inequality if there exists a word $w \in \Sigma^{n-1}$ with $\mathbb{P}_\pi(w\sharp) > 0$.

By assumption, $C_\pi$ is diagnosable. Thus, according to our characterisation of a strategy ensuring FF-diagnosability, there exists a word $w$ such that $\mathbb{P}_\pi(w\sharp) > 0$. As a consequence, $\sum_{n=1}^\infty \mathbb{P}(C_n) < \sum_{n=1}^\infty (\frac{1}{2})^n = 1$, thus $A$ is not (1, 1) fault free. $\square$

**Remark 6.1.** A straightforward adaptation of the proof shows that for every $0 < \gamma < 1$, $A$ is $(\gamma, \frac{\gamma}{2-\gamma})$ fault free iff there exists a word $w$ such that $\mathbf{P}_A(w) \ge \frac{1}{2}$.
We end with the $\alpha$-resilient active diagnosis problem. The construction of the reduction is a bit simpler. This is due to the fact that the system is FF-diagnosable for any arbitrary strategy. In other words, the reduction only relies on the $\alpha$-resilient property to establish undecidability.

**Proposition 6.3.** *The $\alpha$-resilient active diagnosis problem is undecidable.*

This time, given a probabilistic automaton $A$ with alphabet $\Sigma$, one transforms $A$ into a CLTS, augmented by two states and some transitions. This CLTS is called $\mathcal{C}$ and its initial state is the initial state of $A$. At each step, when reading an event of $\Sigma$, with probability $1/2$ we exit $A$ and will commit a fault in the next step. When a $\sharp$ is read after a word $w_1\sharp\dots\sharp w_k$ with for all $i \le k$ $w_i$ does not contain $\sharp$, either we go back to the initial state of $A$ or we will trigger a fault on the next turn depending on the probability to accept $w_k$. If a strategy can regularly trigger a word with acceptance probability greater than $1/2$, it can slow the speed at which the runs become faulty.

*Proof.* We proceed here by reduction from the problem of the existence of a word $w$ such that $\mathbf{P}_A(w) > \frac{1}{2}$. We consider a probabilistic automaton $A = (Q, q_0, \Sigma, (\mathbf{P}_a)_{a \in \Sigma}, F)$ for which we assume w.l.o.g. that: (1) $\Sigma \cap \{u, \mathbf{f}, \sharp, \mathfrak{h}\} = \emptyset$ and (2) the probabilities are fractions $\frac{n}{d}$ with $d \in \mathbb{N}$ fixed. One builds the CLTS $\mathcal{C} = (Q', q_0, \Sigma', T)$ represented in Figure 6.6 (with some shortcuts to ease readability) and defined by:

* $Q' = Q \cup \{q_1, f_1\}$;

* $\Sigma' = \Sigma \cup \{\mathbf{f}, \sharp, \mathfrak{h}\}$, $\Sigma_u = \{\mathbf{f}\}$ et $\Sigma_c = \Sigma \cup \{\sharp\}$;

* the transition function $T$ is defined by:

1. $T(q_1, \mathbf{f}, f_1) = T(f_1, \mathfrak{h}, f_1) = 1$;

2. for every $s, s' \in Q, a \in \Sigma$, $T(s, a, s') = d \cdot \mathbf{P}_a(s, s')$ and $T(s, a, q_1) = d$;

3. for every $s \in F$, $T(s, \sharp, s_0) = 1$ and for every $s \in S \setminus F$, $T(s, \sharp, q_1) = 1$;

4. for every other triplet, $T$ is equal to 0.

Once again, the probabilities in $A$ are multiplied by the constant $d$, which we abbreviate in the figure by $d \cdot A$.

As every fault is followed by a $\mathfrak{h}$, whatever the strategy $\pi$, $C_\pi$ is FF-diagnosable.

* Assume there exists $w = w_1 \dots w_k \in \Sigma^*$ such that $\mathbf{P}_A(w) > \frac{1}{2}$. We denote $v = \mathbf{P}_A(w)$. We define the deterministic strategy $\pi$ by:

* $\pi((w\sharp)^*w) = \{\mathbf{f}, \mathfrak{h}, \sharp\}$;

* for all $0 \le i < k$, $\pi((w\sharp)^*w_1 \dots w_i) = \{\mathbf{f}, \mathfrak{h}, w_{i+1}\}$;

* $\pi(w') = \Sigma'$ for any other word $w'$.
<figure><img src="image_85.png" /><figcaption>Figure 6.6: Reduction to α-resilient active diagnosability.</figcaption></figure>

Under strategy $\pi$, the observed sequence of a correct run $\rho$ is some $(w^{\sharp})^m w_1 \dots w_i$ with
$0 \le i \le k$.

◦ If $\mathcal{P}(\rho) = (w^{\sharp})^m w_1 \dots w_i$ with $0 < i$ then with conditional equiprobability, $\text{last}(\rho) \in Q$ or $\text{last}(\rho) = q_1$. Thus with probability $\frac{1}{2}$, the run will be correct after the next observation.

◦ If $\mathcal{P}(\rho) = (w^{\sharp})^m$ then with conditional probability $v$, $\text{last}(\rho) = q_0$ and with probability $1-v$, $\text{last}(\rho) = q_1$. Thus with probability $v$, the run will be correct after the next observation.

Consider an arbitrary $n$ and write the Euclidian division of $n-1$ by $k+1$ as $n-1 = m(k+1)+i$ with $i \le k$. One has $2^{-(n-1)}\mathbb{P}_{\pi}(C_n) = (2v)^m$. Hence $\frac{2^{(n-1)}}{\mathbb{P}_{\pi}(C_n)} = \left(\frac{1}{2v}\right)^{\lfloor \frac{n-1}{k+1} \rfloor}$ implying $\lim_{n \to \infty} \frac{2^{-n}}{\mathbb{P}_{\pi}(C_n)} = 0$. So $C_{\pi}$ is $\frac{1}{2}$-resilient.

• Assume now that for every word $w \in \Sigma^*$, $\mathbf{P}_A(w) \le \frac{1}{2}$. Let $\pi$ be an arbitrary strategy. The observed sequence of a correct run $\rho$ is some $u_1^{\sharp} \dots \sharp u_m$ such that for all $i$, $u_i \in \Sigma^*$.

◦ If $u_m \neq \varepsilon$ with $0 < i$ then with conditional equiprobability, $\text{last}(\rho) \in Q$ or $\text{last}(\rho) = q_1$. Thus with probability $\frac{1}{2}$, the run will be correct after the next observation.

◦ If $u_m = \varepsilon$ then with conditional probability $\mathbf{P}_A(u_{m-1})$, $\text{last}(\rho) = q_0$ and with probability $1 - \mathbf{P}_A(u_{m-1})$, $\text{last}(\rho) = q_1$. Thus with probability $\mathbf{P}_A(u_{m-1}) \le 1/2$, the run will be correct after the next observation.

Summarising, one has: $\mathbb{P}_{\pi}(C_n) \le 2^{-(n-1)}$ implying $\limsup_{n \to \infty} \frac{2^{-n}}{\mathbb{P}_{\pi}(C_n)} \ge \frac{1}{2}$. So $C_{\pi}$ is not $\frac{1}{2}$-resilient. $\square$

## 2.2 Decidability of the Qualitative Problems

In contrast to the quantitative notions, and to the notable exception of the safe active
diagnosis problem, all the qualitative problems of diagnosability under degradation
constraints we introduced are decidable and EXPTIME-complete. The simplest case
is the one of weak resilient active diagnosability. The proof idea is common to all
cases: starting from a construction that gives an efficient characterisation of active
diagnosability (inspired from [BFH$^+$14] and detailed below), we establish a necessary
and sufficient condition for the existence of a control strategy that ensures the given
notion of diagnosability under a degradation constraint.
Let us start by defining a construction inspired from [BFH$^{+}$14] $^2$. This construction is the adaptation to the active setting of the FF-automaton used in Subsection 1.1.1 of Chapter 4, page 93. This construction uses the notion of belief. The initial belief is {$q_0$}, and given a current belief B and an observed event b, the belief obtained after b has been observed is defined by:

$$ \Delta(B, b) = \{q \in Q \mid \exists q' \in B, \rho \in SR_1, q' \stackrel{\rho}{\Rightarrow} q \wedge \mathcal{P}(\rho) = b\} . $$

$\Delta(B, b)$ is thus the set of states a partially observable systems may be in, given that the previous belief was B and observation O occurred. Importantly, it does not depend on the strategy as every controllable event is observable. The set of beliefs of a CLTS $\mathcal{C}$ is denoted $Bl_{\mathcal{C}}$ and we drop the subscript when there is no risk of confusion. Beliefs are of importance since they formalize the discrete information an observer has on the current state of the system. Thus, to decide FF-diagnosability of a CLTS, the states of the CLTS are enriched with two sets U and V that correspond, respectively, to the subset of correct, or faulty, states, that are reachable by a signalling run corresponding to the current observed sequence, i.e. to the set of correct, or faulty, states of the current belief. Such a pair of sets $(U, V)$ is therefore called a separated belief. As we study FF-diagnosability here, one could wonder why we do not only use a set U as we did in Chapter 4. In fact, in some of the constructions that we make later, we need to know the full belief. For example, forgetting a faulty state could result in a controller making a choice that creates a deadlock in this faulty state. By using U and V, we have the information pertaining to FF-diagnosis $(U)$ and to the current belief $(U \cup V)$.

Formally, from a CLTS $\mathcal{C} = \langle Q, q_0, \Sigma, T \rangle$, we define its belief version on the same event alphabet $\mathcal{C}^B = \langle Q^B, q_0^B, \Sigma, T^B \rangle$ by:

* $Q^B = Q \times 2^Q \times 2^Q$ and $q_0^B = (q_0, \{q_0\}, \emptyset)$;

* for every $(q, U, V) \in Q \times 2^Q \times 2^Q$, for every $a \in \Sigma$, and every $q' \in Q$

- if $a \notin \Sigma_o$, $T^B((q, U, V), a, (q', U, V)) = T(q, a, q')$;

- if $a \in \Sigma_o$, letting $U' = \Delta(U, a) \cap Q_c$ and $V' = \Delta(U \cup V, a) \cap Q_f$, then $T^B((q, U, V), a, (q', U', V')) = T(q, a, q')$.

- for every other triplet $((q, U, V), a, (q', U', V'))$, $T$ is equal to 0.

The size of the belief CLTS $\mathcal{C}^B$ is exponential in the size of $\mathcal{C}$. For the properties we are interested in, they have the same behaviour. We introduce $\Theta$, a discrete version of $T^B$, extended to observed sequences. For $w \in \Sigma_o^*$, $(q', U', V') \in \Theta((q, U, V), w)$ as soon as there exists a run $\rho$ such that $\mathcal{P}(\rho) = w$ and $(q, U, V) \stackrel{\rho}{\Rightarrow} (q', U', V')$.

We now construct $\mathbf{Win}$ the set of all separated beliefs $(U, V)$ such that, starting from any $(q, U, V)$ with $q \in U \cup V$, $\mathcal{C}^B$ is actively diagnosable. This set is computed as a greatest fixpoint. We let $\mathbf{Win}_0 = 2^{Q_c} \times 2^{Q_f}$ and for $n \in \mathbb{N}$, $\mathbf{Win}_{n+1}$ is the set of the

<footnote>$^2$The difference with the construction of [BFH$^{+}$14] is that we focus here on FF-diagnosability rather than IA-diagnosability which simplifies the writing of the proofs. The results of this chapter and of [BFH$^{+}$14] however hold for both notions of diagnosability.</footnote>
separated beliefs $(U, V)$ of $\text{Win}_n$ such that for all state $q \in U \cup V$, there exists a sequence of sets of allowed events $(\Sigma_i^\bullet)_{1 \le i \le k}$ and an observed sequence $w = o_1 \dots o_k$ with $o_i \in \Sigma_i^\bullet$ verifying:

* there exists a run $\rho$ starting in $(q, U, V)$ with $\mathcal{P}(\rho) = w$ and reaching $(q^*, U^*, V^*)$ with $q^* \in Q_c$ (i.e. the current state is correct) or $U^* = 0$ (the fault is claimed);

* Consider a state $q_i$ reached from $q' \in U \cup V$ by a run with observed sequence $o_1 \dots o_i$ with $0 \le i < k$, i.e. $(q_i, U_i, V_i) \in \Theta((q', U, V), o_1 \dots o_i)$ for a separated belief $(U_i, V_i)$. then:

1. the control induced by $\Sigma_{i+1}^\bullet$ does not create any deadlock: $G^{\Sigma_{i+1}^\bullet}(q_i) \neq 0$;

2. Every new separated belief obtained by an observable step $o \in \Sigma_{i+1}^\bullet$ starting in $q_i$ belongs to $\text{Win}_n$: $\forall o \in \Sigma_{i+1}^\bullet, \forall (q_o, U_o, V_o) \in \Theta((q_i, U_i, V_i), o), (U_o, V_o) \in \text{Win}_n$.

The computation of $\text{Win}$ is in polynomial time in the size of $C^B$, given that in every non-terminal iteration at least one separated belief is removed. The correctness of $\text{Win}$ is established in the richer context of IA-diagnosability in $[\text{BFH}^{+14}]$, and $\pi^*$ a (deterministic finite-memory) strategy ensuring diagnosability consists in, given a separated belief $(U, V) \in \text{Win}$ choosing the greatest set $\Sigma^\bullet$ such that every possible separated belief reached on the next step still belongs to $\text{Win}$. Thus, $\pi^*$ is the most permissive strategy ensuring active diagnosability.

To decide weakly (resp. strongly) resilient active diagnosability, and lasting fault free active diagnosability, we build on the belief CLTS construction.

**Theorem 6.2.** *Weakly resilient active diagnosability is EXPTIME-complete.*

Analysing the set of separated beliefs $\text{Win}$ gave a condition for the active diagnosability and in the positive case a deterministic finite-memory strategy $\pi^*$ ensuring it. We show in this proof, that in order for a CLTS to be weakly resilient active diagnosable, it needs (1) to be actively diagnosable and (2) $C^B$ must contain a reachable cycle of correct states associated with separated beliefs of $\text{Win}$. The idea is that if such a cycle exists, playing a strategy permissive enough (for example $\pi^*$), there is a fixed probability to stay within this cycle and this probability can be used to establish a lower bound to the speed at which the system becomes faulty.

The lower bound is straightforward considering that active diagnosability was already proven to be EXPTIME-hard $[\text{BFH}^{+14}]$.

*Proof.* We first establish the membership in EXPTIME. Given a CLTS $C$, its belief CLTS $C^B$, and the strategy $\pi^*$, we derive a pLTS $\mathcal{A}$. It is obtained from $C^B$ by restricting it to the states with separated belief in $\text{Win}$ and controlled by $\pi^*$. We claim that $C$ is actively diagnosable with guarantee of weak resiliency iff there exists in $\mathcal{A}$ a reachable cycle such that the first component of every state along the cycle is a correct state of $C$.
* Suppose first that such a cycle exists in $\mathcal{A}$. We let $\alpha > 0$ be the probability of this cycle, $n_1$ its length, $n_0$ the observed length of the shortest run reaching a state of the
cycle and $\mu$ the probability of this run. For all $n \ge n_0$, $\mathbb{P}_A(C_n) \ge \mu\alpha^{\lfloor \frac{n-n_0}{n_1} \rfloor}$. As a consequence, $\mathcal{A}$ is $\alpha'$-resilient for all $\alpha' < \alpha$. $\mathcal{A}$ is thus weakly resilient. Therefore, $C_{\pi^*}$, which has the same probabilistic behaviour as $\mathcal{A}$ is weakly resilient too.

* Conversely, suppose that there is no such cycle in $\mathcal{A}$. Let $\pi'$ be a (live) strategy such that $C_{\pi'}$ is FF-diagnosable. This strategy can be mimicked in $C^B$, ignoring the separated belief information. The reachable states of $C_{\pi'}^B$ are associated with separated beliefs of Win (due to the characterisation recalled above). As $\pi^*$ is the most permissive strategy ensuring to stay in Win, there does not exist any such cycle in $C_{\pi'}^B$ either. Consequently, there exists $n_f \in \mathbb{N}$ such that every run $\rho$ in $C_{\pi'}^B$ with $|\rho| \ge n_f$ ends in a state which first component is faulty. Thus $\mathbb{P}_{C_{\pi'}(C_{n_f})} = \mathbb{P}_{C_{\pi'}^B(C_{n_f})} = 0$, which means that $C_{\pi'}$ is not weakly resilient.

The complexity lower-bound is obtained by reduction from the active diagnos-
ability problem for CLTS, which is known to be EXPTIME-hard [BFH$^{+14}$]. From
$\mathcal{C} = \langle Q, q_0, \Sigma, T \rangle$ a CLTS, we define the CLTS $\mathcal{C}' = \langle Q \cup \{q'_0, q_s\}, q'_0, \Sigma \cup \{\#\}, T' \rangle$ with
$\#^{}$ a fresh observable event, and such that $T'(q'_0, \#^{}, q_0) = T'(q'_0, \#^{}, q_s) = T'(q_s, \#^{}, q_s) = 1$, for every $q, q' \in Q$ and $a \in \Sigma$, $T'(q, a, q') = T(q, a, q')$ and for every other triplet
$T'(q, a, q') = 0$. Clearly enough, $\mathcal{C}'$ is actively diagnosable iff $\mathcal{C}$ is actively diagnos-
able. Moreover, $\mathcal{C}'$ is safe by construction, and thanks to Theorem 6.1(a), it is strongly
resilient, and thus weakly resilient.
$\square$

The proof of the next theorem also relies on the set of separated beliefs Win. We build a subset of Win, called WinK. A separated belief (U, V) of Win belongs to WinK if there exists a strategy π such that from every distribution with support U ∪ V, π guarantees to stay in Win, and to give a positive probability to the set of infinite correct runs. The CLTS is actively diagnosable with guarantee of strong resiliency iff from the initial belief one can reach a belief of WinK while staying in Win. The strategy π defined with the construction of WinK does not necessarily allows to diagnose the system. So the winning strategy consists in cleverly combining the strategy used to make the system FF-diagnosable and π.

**Theorem 6.3.** *Strongly resilient active diagnosability is EXPTIME-complete.*

*Proof.* Let $\mathcal{C}$ be a CLTS. As in the construction preliminary to Theorem 6.2, we build $\mathcal{C}^B$, Win and $\pi^*$. We then define $\text{WinK}_U \subseteq 2^Q \times \text{Win}$ by a greatest fix point computation. For $(U', (U, V)) \in \text{WinK}_U$, $(U, V)$ is a separated belief for which there exists a strategy allowing to a set of runs starting in $U \cup V$ to stay in the states of $\mathcal{C}^B$ associated with a belief of Win, and if the run started in $U'$, it stayed correct. $\text{WinK}_U$ is obtained as the limit of a non-increasing sequence $(\text{WinK}_n)_{n \in \mathbb{N}}$ defined inductively by: $\text{WinK}_0 = \{(U', (U, V)) \mid (U, V) \in \text{Win} \wedge \emptyset \neq U' \subseteq U\}$ and for $n \in \mathbb{N}$, $\text{WinK}_{n+1}$ is the set of elements $(U', (U, V))$ of $\text{WinK}_n$ such that there exist a set of allowed events $\Sigma^\bullet$ verifying:

* $\Sigma^\bullet$ does not create a deadlock: $\forall q \in U \cup V, G^{\Sigma^\bullet}(q) \neq 0$;

* under the control $\Sigma^\bullet$ no run starting in a state of $U'$ will make a fault before the next observation: $\forall q_c \in U', \forall \rho \in \text{SR}_1, q_c \stackrel{\rho}{\Rightarrow} q \wedge \mathcal{P}(\rho) \in \Sigma^\bullet \Rightarrow q \in Q_c;$
• every triplet reached by an observable step $o \in \Sigma^\bullet$ belongs to $\text{WinK}_n$:
($\tilde{U}', (\tilde{U}, \tilde{V}) \in \text{WinK}_n$ with:

1. $\tilde{U}' = \{q'_c \in Q_c \mid \exists q_c \in U'_1, \exists \rho \in \text{SR}_1, q_c \stackrel{\rho}{\Rightarrow} q'_c \wedge \mathcal{P}(\rho) = a\}$;

2. $\tilde{U} = \Delta(U, o) \cap Q_c$ and $\tilde{V} = \Delta(U \cup V, o) \cap Q_f$.

From $\text{WinK}_U$, we define the set $\text{WinK} \subseteq \text{Win}$ by keeping only the second component of $\text{WinK}_U$: $\text{WinK} = \{(U, V) \in \text{Win} \mid \exists U', (U', (U, V)) \in \text{WinK}_U\}$. Let us state some of the properties of this construction.

• By induction, if $(U', (U, V)) \notin \text{WinK}_n$ then for every (live) strategy and $q \in U$, there exists a faulty run starting in $q$ of observable length $n$;

• If $\emptyset \neq U'' \subseteq U'$ then $(U', (U, V)) \in \text{WinK}_U$ implies $(U'', (U, V)) \in \text{WinK}_U$. Thus, if $(U, V) \notin \text{WinK}$, for all $q \in U$, $(\{q\}, (U, V)) \notin \text{WinK}_U$.

We also define PreWin the set of states of $C^B$ of the form $Q \times \text{Win}$ from which a state $(q, U, V)$ with $(U, V) \in \text{WinK}$ is reachable. Let us show that $C$ is diagnosable and strongly resilient iff the initial state of $C^B$ belongs to PreWin.

• Suppose that the initial state belongs to PreWin. Let $(U', (U, V))$ be an element of $\text{WinK}_U$. We define $\pi_{(U', (U, V))}$ the strategy that ensures to stay in $\text{WinK}_U$. This strategy immediately derives from the fixpoint definition of $\text{WinK}_U$. For $(U, V) \in \text{WinK}$, we also define $\pi_{(U, V)} = \pi_{(U', (U, V))}$ for an arbitrary $U'$ such that $(U', (U, V)) \in \text{WinK}_U$. Finally, we let $\pi_0$ be the following strategy working in three successive phases which may not all be triggered.

1. First $\pi_0$ mimics $\pi^*$ until a separated belief $(U, V) \in \text{WinK}$ is reached;

2. Then, at every observed sequence $w$, $\pi_0$ chooses to apply $\pi_{(U,V)}$ with probability $p_w = \frac{|w|}{|w|+1}$, and to switch to the third phase with probability $1 - p_w$;

3. Finally, $\pi_0$ behaves forever as $\pi^*$.

We observe that $C_{\pi_0}$ is FF-diagnosable. Indeed, on the one hand, the events allowed by $\pi_0$ are included in those allowed by the maximally permissive strategy $\pi^*$, and on the other hand almost-surely, $\pi^*$ is applied from some moment on. Therefore every fault will almost surely be detected.

Moreover, let us prove that it is strongly resilient. Indeed, by definition of PreWin, there exists a run $\rho$ starting in the initial state and reaching a state $(q, U, V)$ such that $(U, V)$ belongs to $\text{WinK}$. Let $U' \subseteq U$ the one chosen arbitrarily when defining $\pi_{(U,V)}$. Without loss of generality, we suppose that $\rho$ reaches a state of $U'$. As a fault can only be created after $\rho$ if $\pi_0$ switches to its third phase, for $n \ge |\rho|_o$ we have

$$ \mathbb{P}_{\pi_0}(\tilde{\rho} \in C_n \mid \rho \preceq \tilde{\rho}) \ge \mathbb{P}_{\pi_0}(\rho) \prod_{i=|\rho|}^{n} \frac{i}{i+1} = \mathbb{P}_{\pi_0}(\rho) \frac{|\rho|}{n+1}. $$
Thus, for every $0 < \alpha < 1$, similarly to $n\alpha^n$, $\frac{\alpha^n}{\mathbb{P}_{\pi_0}(C_n)}$ converges to 0.

• Conversely, suppose that the initial state does not belong to PreWin. Let $\pi$ be a strategy ensuring diagnosability. For every state $(q, U, V)$ with $q \in U$ reachable by a run $\rho_0$ with $\pi, (U, V) \notin \text{WinK}$ and due to one of our observations $(\{q\}, (U, V)) \notin \text{WinK}_U$. Let $K$ be the number of iterations in the fixpoint computation of WinK. Then, for every sequence of $K$ random choices under $\pi$, there exists a faulty run $\rho \in \mathbb{F}$, compatible with these choices, starting in $(q, U, V)$ and of observable length smaller than $K$. Adding up the probabilities of runs corresponding to every sequence of choices of $\pi$ we obtain

$$ \mathbb{P}_{\pi}(\rho \in \mathbb{F}_{|\rho_0|_o+K} | \rho_0 \preceq \rho) \geq \lambda^{K|Q|} \mathbb{P}_{\pi}(\rho_0) $$

where $\lambda = \min_{q' \in Q} \frac{1}{G^{\sum(q')}}$. Thus, for every $n \in \mathbb{N}$, $\mathbb{P}_{\pi}(C_{n+K}) \leq \mathbb{P}_{\pi}(C_n)(1 - \lambda^{K|Q|})$. Letting $\alpha = (1 - \lambda^{K|Q|})^{\frac{1}{K}}$, we obtain $\lim_{n \to \infty} \frac{\alpha^n}{\mathbb{P}_{\pi}(C_n)} > 0$, so that $C_{\pi_0}$ is not strongly resilient.

To conclude the proof, we observe that the EXPTIME-hardness derives from the same reduction as in the proof of Theorem 6.2. □

It turns out that this same combination of strategies can be used to ensure lasting fault freeness and FF-diagnosability. In fact, the following theorem establishes that the characterisation of the strongly resilient active diagnosability also applies to the lasting fault free active diagnosability.

**Theorem 6.4.** *Lasting fault free active diagnosability is equivalent to strongly resilient active diagnosability.*

We show here that the characterisation given in the proof of Theorem 6.3 for a CLTS to be actively diagnosable with guarantee of strong resiliency also characterises the fact that the CLTS is actively diagnosable with guarantee of lasting fault freeness. This shows the equivalence of the two notions in the active case.

*Proof.* We reuse the definitions from the proof of Theorem 6.3. Let us show that $C$ is actively diagnosable with guarantee of lasting fault freeness iff the initial state of $C^B$ belongs to PreWin.

• Suppose that the initial state belongs to PreWin. Then, as discussed in the proof of Theorem 6.3, $C_{\pi_0}$ is diagnosable and there exists a finite run $\rho$ such that $\mathbb{P}(\tilde{\rho} \in C_n | \rho \preceq \tilde{\rho}) \geq \mathbb{P}(\rho) \frac{|\rho|}{n+1}$. Thus:

$$ \sum_{n=1}^{\infty} \mathbb{P}(C_n) \geq \sum_{n=|\rho|}^{\infty} \mathbb{P}(\tilde{\rho} \in C_n | \rho \preceq \tilde{\rho}) \geq \mathbb{P}(\rho) |\rho| \sum_{n=|\rho|}^{\infty} \frac{1}{n+1} = \infty. $$

• Conversely, if the initial state does not belong to PreWin. Let $\pi$ be a strategy ensuring diagnosability. For every $n \in \mathbb{N}$, $\mathbb{P}(C_{n+K}) \leq \mathbb{P}(C_n)(1 - \lambda^{K|Q|})$. Thus:

$$ \sum_{n=1}^{\infty} \mathbb{P}(C_n) \leq K \sum_{n=1}^{\infty} (1 - \lambda^{K \cdot |Q|})^n \leq K \cdot |Q_B| \cdot \frac{1}{\lambda^{K \cdot |Q|}} < \infty. $$

□
Given the equivalence of strong resiliency and lasting fault freeness, from Theorem 6.3 we derive:

**Corollary 6.1.** *Lasting fault free active diagnosability is EXPTIME-complete.*

## 2.3 Safe active diagnosis problem under finite-memory strategies

Contrary to the other qualitative problems, safe active diagnosability is known to be undecidable [BFH$^+$14]. In order to regain decidability, one can restrict the strategies so that they only use finite memory. Note first that decidability is not immediate even if the strategies are assumed to be finite-memory, since no *a priori* bound on the memory is known$^3$. This restriction was studied in [BFH$^+$14] where the authors give an NEXPTIME algorithm. However, the known lower bound is only EXPTIME, leaving a gap. We refine here this complexity result by proving that safe active diagnosis can be solved in EXPTIME when restricting to finite-memory strategies.

To do so, we prove a more general result in the context of a well-known model, quite popular in artificial intelligence and more recently in formal methods, that combines partial observation, probabilities and control, namely *Partially Observable Markov Decision Processes* (POMDP) [Å65, KLC98]. We establish that the existence of finite-memory schedulers that ensure a Büchi objective with probability 1 and a safety objective with positive probability in a POMDP is decidable in EXPTIME. We then reduce the safe active diagnosis of a CLTS $C$ restricted to finite-memory strategies to the existence of a finite-memory scheduler in a POMDP $M_C$ ensuring at the same time a Büchi objective with probability 1 and a safety objective with positive probability.

**Definition 6.8.** A partially observable Markov decision process (POMDP) is a tuple $M = (Q, q_0, \mathbf{Obs}, \mathbf{Act}, T)$ where

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

* $\mathbf{Obs}: Q \to \mathcal{O} \cup \{\epsilon\}$ assigns an observation $\mathcal{O} \in \mathcal{O}$ to each state.

* $\mathbf{Act}$ is a finite set of actions;

* $T: Q \times \mathbf{Act} \to \text{Dist}(Q)$ is a partial transition function. Letting $\text{Ena}(q) = \{a \in \mathbf{Act} | T(q, a) \text{ is defined}\}$ the set of enabled actions in state $q$, we assume that:

- for all $q \in Q$, $\text{Ena}(q) \neq \emptyset$, and

- whenever $\text{Obs}(q) = \text{Obs}(q')$, then $\text{Ena}(q) = \text{Ena}(q')$ and slightly abusing our notation, we denote by $\text{Ena}(\mathcal{O})$ the set of events enabled in every state with observation $\mathcal{O}$.

A *decision rule* of a POMDP is a distribution from $\text{Dist}(\mathbf{Act})$ that resolves one non-determinism choice by randomization. A *scheduler* for a POMDP maps histories of observations to decision rules. Formally, a scheduler is a function $\tau: \mathcal{O}^+ \to \text{Dist}(\mathbf{Act})$

<footnote>$^3$In the case of Proposition 4.9, page 120, the restriction in fact made the problem more difficult.</footnote>
such that for every $O_1 \cdots O_i$, $\text{Supp}(\tau(O_1 \cdots O_i)) \subseteq \text{Ena}(O_i)$. Given a scheduler $\tau$, a POMDP $M$ yields a stochastic process. This stochastic process can be represented by an infinite state pLTS, denoted $M(\tau)$ in which states are histories of observations. One denotes by $\mathbb{P}_{\tau}^{M}(\text{Ev})$ the probability that an infinite observed sequence of $\text{Ev}$ is realized in this pLTS.

Similarly to what was said for strategies, one can define finite-memory schedulers for POMDP. The notion of *belief* can be adapted to POMDP. As for CLTS, it is a non-empty set of states that represents the current state estimate, i.e. the set of states the system may be in, given the actions (which affect the reachable set of states contrary to what is done for CLTS) and observations so far. The initial belief is $\{q_0\}$, and given a current belief $B$, a decision rule $\delta$ and an observation $O$, the belief obtained after $\delta$ has been applied and $O$ has been observed is defined by:

$$ \Delta(B, (\delta, O)) = \bigcup_{q \in B, a \in \text{Supp}(\delta)} \text{Supp}(T(q, a)) \cap \text{Obs}^{-1}(O). $$

Aiming at providing a POMDP $M_C$ for the safe active diagnosis problems of a CLTS $C$, we face several difficulties. First, in a CLTS the observations are related to events while in a POMDP they are related to states. As a consequence, we need to label the states by the latest observation made by the system. Secondly, our objectives are not based on states but on observed sequences. Fortunately, the relevant information pertaining to the observations, namely the information about ambiguity of observed sequences, is available in the belief. Thus (with two exceptions) the states are triples formed of a state $q$, an event ‘$a$’ and a belief $B$ of the CLTS. A third adaptation concerns the control mechanism. In $C$, the control is performed by choosing (possibly randomly) a subset of allowed controllable events. Thus actions of $M_C$ are subsets of events that include the uncontrollable events. Given some control decision $\Sigma^\bullet$, to define the transition probability of $M_C$ from $(q, a, B)$ to $(q', a', B')$, one must consider all runs in $C$ labelled by events of $\Sigma^\bullet$ from $q$ to $q'$ such that the last event, labelled by ‘$a$’, is the only observable one. The probability of any such run is obtained by the product of the individual step probabilities. The latter are then defined by the normalization of weights w.r.t. $\Sigma^\bullet$. Finally, there cannot be infinite runs of unobservable events due to the convergence of $C$. However some runs can reach, via unobservable events, a state from which no event of $\Sigma^\bullet$ is enabled. In other words, the control $\Sigma^\bullet$ applied in $(q, a, B)$ may have a positive probability to reach a deadlock (i.e. the chosen decision rule leads to a strategy for the CLTS which is not live). In order to capture this behaviour and to obtain a non defective probability distribution, we add an additional state *lost*, that corresponds to such deadlocks. The next definition formalizes our approach.

**Definition 6.9.** The POMDP $M_C = \langle Q^{Mc}, q_0^{Mc}, \text{Obs}, \text{Act}, T^{Mc} \rangle$ derived from a CLTS $C = \langle Q, q_0, \Sigma, T \rangle$ is defined by:

* $Q^{Mc} = Q \times \Sigma_o \times Bl_C \uplus \{(q_0, \varepsilon, \{q_0\}), \text{lost}\}$ with $q_0^{Mc} = (q_0, \varepsilon, \{q_0\})$;

* the set of observations is $O = \Sigma_o \cup \{\text{lost}\}$, with $\text{Obs}(\text{lost}) = \text{lost}$ and for $(q, a, B) \in Q^{Mc}, \text{Obs}((q, a, B)) = a$;
• $\mathbf{Act} = \{\Sigma^{\bullet} \subseteq \Sigma \mid \Sigma^{\bullet} \supseteq \Sigma \setminus \Sigma_c\}$;

• for every $(q_1, a, B) \in Q^{Mc}$ and $\Sigma^{\bullet} \in \mathbf{Act}$, $T^{Mc}((q_1, a, B), \Sigma^{\bullet}) = \mu \in \mathrm{Dist}(Q^{Mc})$ where for $b \in \Sigma^{\bullet} \cap \Sigma_o$:

$$- \mu((q', b, \Delta(B, b))) =$$

$$\sum_{\substack{q_1 \xrightarrow{a_1} q_2 \cdots \xrightarrow{a_n} q_{n+1} \\ a_1 \cdots a_n \in \Sigma^{\bullet} \cap \Sigma_u}} \left( \prod_{i=1}^{n} T^{\Sigma^{\bullet}}(q_i, a_i, q_{i+1}) \right) \cdot T^{\Sigma^{\bullet}}(q_{n+1}, b, q');$$

$$- \mu(\mathbf{lost}) = \sum_{\substack{q_1 \xrightarrow{a_1} q_2 \cdots \xrightarrow{a_n} q_{n+1} \\ a_1 \cdots a_n \in \Sigma^{\bullet} \cap \Sigma_u \\ G^{\Sigma^{\bullet}}(q_{n+1}) = 0}} \prod_{i=1}^{n} T^{\Sigma^{\bullet}}(q_i, a_i, q_{i+1});$$

• for every $\Sigma^{\bullet} \in \mathbf{Act}$, $T^{Mc}(\mathbf{lost}, \Sigma^{\bullet}) = \mathbf{1}_{\mathbf{lost}}$.

Given $C$, the construction of $M_C$, which is of size in $2^{O(|Q|+|\Sigma|)}$, can be done in exponential time. Also, the probability distributions over next states ($\mu$ in Definition 6.9) are presented as sums over runs of $C$, but they can be computed in polynomial time by matrix operations.

A CLTS $C$ and its associated POMDP $M_C$ are closely related. In particular, strategies in $C$ and schedulers in $M_C$ are in a one-to-one correspondence. First, let us explain how to naturally derive a strategy $\pi$ for $C$ from a scheduler $\tau$ in $M_C$. For an observed sequence $a_1 \cdots a_n \in \Sigma_o^*$, we set $\pi(a_1 \cdots a_n) = \tau(a_1 \cdots a_n)$. Notice that the strategy $\pi$ obtained that way is not necessarily live: for example, if after $a_1 \cdots a_n$ the choice of $\tau$ leads with positive probability to lost, then $\pi$ is not live. However, as soon as $\tau$ ensures to avoid state lost, then the corresponding strategy $\pi$ is live. Similarly, to a live strategy $\pi$ for $C$, we can associate a scheduler $\tau$ in $M_C$ that always avoids lost: given a sequence of observations that does not contain lost, thus of the form $a_1 \cdots a_n$, with $a_i \in \Sigma_o$ for all $i$, we set $\tau(a_1 \cdots a_n) = \pi(a_1 \cdots a_n)$.

Moreover, if $(\pi, \tau)$ is a pair of live strategy and corresponding scheduler (that always avoids lost), the probability measures $\mathbb{P}_{C_\pi}$ and $\mathbb{P}_{\tau}^{Mc}$ are essentially equivalent. More precisely, the product in $M_C$ with the observation and the belief does not change the probability measure defined by $C_\pi$.

We now show how to decide for POMDP the existence of a finite-memory scheduler that ensures a Büchi objective with probability one and a safety objective with positive probability. We use LTL notations to denote sets of runs in a POMDP, such as $\diamond$, $\square$ and $\square\diamond$ for eventually, always and infinitely often respectively (given a state $q$, $\square\diamond q$ thus represents the set of runs containing $q$ infinitely often).

**Theorem 6.5.** The problem whether, given a POMDP M with subsets of states F and I, there exists a finite-memory scheduler $\tau$ such that $\mathbb{P}_{\tau}^{M}(\square\diamond F) = 1$ and $\mathbb{P}_{\tau}^{M}(\square I) > 0$ is EXPTIME-complete.
Theorem 6.5 derives from Propositions 6.4 and 6.5 below, that state, respectively, the upper bound in the general case, and the lower bound in a particular case, namely for the safe active diagnosability under finite-memory strategies.

**Proposition 6.4.** Given a POMDP M with subsets of states F and I, one can decide in EXPTIME whether there exists a finite-memory scheduler $\tau$ such that $\mathbb{P}_{\tau}^{M}(\square\diamond F) = 1$ and $\mathbb{P}_{\tau}^{M}(\square I) > 0$.

Due to the complexity of this proof, we decompose it using two lemmas. The idea is the following. We first define a set $Win_{=1}$ of pairs of beliefs $(B, B')$ with $B \subseteq B'$ such that there exists a scheduler that ensures with probability 1 to stay in I from any state of B and to reach F from any state of $B'$. As $B \subseteq B'$, this implies that if one starts with a distribution which support is $B'$, there is a scheduler satisfying both the Büchi objective with probability one and the safety objective with positive probability. Such a belief $B'$ is a “winning” belief. However, there are “winning” beliefs that cannot be obtained directly from $Win_{=1}$. In Lemma 6.1, we show how to compute efficiently $Win_{=1}$ through a greatest fixed point algorithm. Using $Win_{=1}$, we then build a set of beliefs $Win$, which contains intuitively the beliefs from which there exists a scheduler that can reach a belief that corresponds to the second component of a pair in $Win_{=1}$ with positive probability while never reaching a “losing” belief (a belief from which we cannot satisfy the Büchi requirement). Finally, in Lemma 6.2 we show that $Win$ contains exactly the set of “winning” beliefs. Thus, there exists a scheduler satisfying the two objectives iff the initial belief $\{q_0\}$ belongs to $Win$.

*Proof.* In this proof, the POMDP M = $\langle Q, q_0, \text{Obs}, \text{Act}, T \rangle$ is fixed, and we use notation $\mathbb{P}_{\tau}^{\delta_0}(\text{Ev})$ to denote the probability of Ev under scheduler $\tau$ assuming that instead of $q_0$, the initial state in M is given by the distribution $\delta_0 \in \text{Dist}(Q)$.

Let us first explain how to compute the following set of pairs of beliefs:

$$ \begin{align*} \text{Win}_{=1} &= \{(B', B) \mid B' \subseteq I, B' \subseteq B \text{ s.t. } \exists \tau \text{ s.t.} \\ & \phantom{=} \quad \forall \delta_0 \text{ with } \text{Supp}(\delta_0) = B, \mathbb{P}_{\tau}^{\delta_0}(\square\diamond F) = 1, \text{ and} \\ & \phantom{=} \quad \forall \delta'_0 \text{ with } \text{Supp}(\delta'_0) = B', \mathbb{P}_{\tau}^{\delta'_0}(\square I) = 1\}. \end{align*} $$

Intuitively, $Win_{=1}$ denotes pairs of beliefs such that there exists a scheduler that ensures a Büchi objective almost-surely from the larger belief, and a safety objective almost-surely from the smaller one. Note that, (1) in the definition of $Win_{=1}$, we do not require the scheduler $\tau$ to be finite-memory and (2) as schedulers associate a decision rule to every sequence of observation, the same choices are taken after the same sequence of observations for the Büchi and the safety objective although the initial distribution differs. Given that we consider pairs of beliefs, we introduce the following notation: $\Delta((B', B), O_1) = (\Delta(B', O_1), \Delta(B, O_1))$, and similarly for sequences of actions and observations. Also, for $X \subseteq Q$ a subset of states, we denote by $Bl_{\subseteq X} = \{B \in Bl \mid B \subseteq X\}$ the set of beliefs contained in $X$.

We now show how to efficiently compute $Win_{=1}$.
**Lemma 6.1.** Let $\text{Win}_\infty$ be the greatest fixed point starting from $\{(q, B', B) \in Q \times \mathcal{B}l \times \mathcal{B}l \mid q \in B, B' \subseteq B, B' \subseteq I\}$ of the following operator:

$$
\begin{align*}
W &\mapsto \{(q, B'_1, B_1) \mid \exists n \ge 1, \exists q_0 \dots q_n \in Q, \exists \alpha_1, \dots \alpha_n \exists \mathbf{O}_1 \dots \mathbf{O}_n, \\
  &\phantom{\mapsto \{(q, B'_1, B_1) \mid \exists n \ge 1, \exists q_0 \dots q_n \in Q, \} } (B'_2, B_2) = \Delta((B'_1, B_1), (\alpha_1, \mathbf{O}_1) \dots (\alpha_n, \mathbf{O}_n)), \forall q' \in B_2, (q', B'_2, B_2) \in W, \\
  &\phantom{\mapsto \{(q, B'_1, B_1) \mid \exists n \ge 1, \exists q_0 \dots q_n \in Q, \} } q_0 = q, q_n \in F, \forall i < n, T(q_i, \alpha_{i+1})(q_{i+1}) > 0, \forall 1 \le j \le n, \text{Obs}(q_j) = \mathbf{O}_j, \\
  &\phantom{\mapsto \{(q, B'_1, B_1) \mid \exists n \ge 1, \exists q_0 \dots q_n \in Q, \} } \forall i \le n, \forall \mathbf{O}'_i, \text{ for } (B'_3, B_3) = \Delta((B', B), (\alpha_1, \mathbf{O}_1) \dots (\alpha_{i-1}, \mathbf{O}_{i-1}) (\alpha_i, \mathbf{O}'_i)) \\
  &\phantom{\mapsto \{(q, B'_1, B_1) \mid \exists n \ge 1, \exists q_0 \dots q_n \in Q, \} } \text{ we have } \forall q' \in B_3, (q, B'_3, B_3) \subseteq W \cap Q \times \mathcal{B}l_{\subseteq I} \times \mathcal{B}l \} .
\end{align*}
$$

$$
We have $\text{Win}_{=1} = \{(B', B) \mid \forall q \in B, (q, B', B) \in \text{Win}_{\infty}\}$.
$$

**Proof of Lemma 6.1.** To establish that $\text{Win}_{=1}$ corresponds to the projection on the pair of beliefs of $\text{Win}_\infty$, we first assume that for all $q \in B$, $(q, B', B)$ belongs to $\text{Win}_\infty$, and exhibit a scheduler $\tau$ that witnesses $(B', B) \in \text{Win}_{=1}$. Let us define $\tau$ as follows. The scheduler $\tau$ has finite memory $\mathcal{B}l \times \mathcal{B}l$. From memory state $(B', B)$, $\tau$ dictates to play uniformly all actions $\alpha$ such that for every observation $\mathcal{O}$ and every $q \in \Delta(B, \alpha, \mathcal{O})$, we have $(q, \Delta((B', B), \alpha, \mathcal{O})) \in \text{Win}_\infty$. Note that this set of “safe” actions is necessarily non empty because $(q, B', B) \in \text{Win}_\infty$. If $\alpha$ is played, and $\mathcal{O}$ is observed, the memory state of $\tau$ is updated to $\Delta((B', B), \alpha, \mathcal{O})$, which is still in $\text{Win}_\infty$, by assumption on $\alpha$. The scheduler $\tau$ then continues similarly with memory state $\Delta((B', B), \alpha, \mathcal{O})$. So defined, let us show that $\tau$ witnesses $(B', B) \in \text{Win}_{=1}$. First, let $\delta_0$ be a distribution with support $B$. The scheduler $\tau$ ensures to stay (surely) in $\text{Win}_\infty$. Moreover, for every $q \in B$, with a positive probability, say $p_{(q,B',B)} > 0$, the sequence $(\alpha_1, \mathbf{O}_1) \cdots (\alpha_n, \mathbf{O}_n)$ of actions and observations leading to $F$ that derives from the fixpoint definition, happens from $q$. There are finitely many $p_{(q,B',B)}$, all are positive, so they are lower bounded by some positive value $p$. Playing $\tau$ forever thus ensures visiting $F$ almost surely, and iterating this reasoning, even visiting $F$ infinitely often with probability 1. Now, assuming $B' \ne \emptyset$ let $\delta'_0$ be a distribution with support $B'$. Any action picked by $\tau$ ensures that, whatever the observation, the first belief-component remains in $I$. Therefore, surely, from distribution $\delta'_0$ the plays stay in the invariant $I$.

Let us now assume that the triplet $(q, B', B)$ is removed during the iterative computation of the fixed point $W_\infty$. We prove, by induction on $k$, that if $(q, B', B)$ is removed at iteration $k$, then, $(B', B) \notin \text{Win}_=1$. If $k=0$, the pair is removed at initialization, hence $B' \not\subseteq I$ or $B' \not\subseteq B$, and obviously $(B', B) \notin \text{Win}_=1$. Otherwise it happens at the $k$-th iteration, for some $k \ge 1$. Assume, towards a contradiction, that there exists a scheduler $\tau$, witnessing that $(B', B) \in \text{Win}_=1$. In particular, there exists a sequence of pairs of actions and observations allowed by the scheduler $(\alpha_1, \mathbf{O}_1) \cdots (\alpha_n, \mathbf{O}_n)$ so that there exists $q_0 \dots q_n \in Q$ with $q_0 = q$, $q_n \in F$, $\forall i < n, T(q_i, \alpha_{i+1})(q_{i+1}) > 0, \forall 1 \le j \le n$ and $\text{Obs}(q_j) = \mathbf{O}_j$. Because the triple $(q, B', B)$ was removed at iteration $k$, it must be that, either (1) for $(B'_2, B_2) = \Delta((B', B), (\alpha_1, \mathbf{O}_1) \cdots (\alpha_n, \mathbf{O}_n))$, there exists $q_2 \in B_2$ such that $(q_2, B', B) \notin W_{k-1}$, (2) no run corresponding to a sequence $(\alpha_1, \mathbf{O}_1) \cdots (\alpha_n, \mathbf{O}_n)$ satisfying (1) and starting in $q$ ends in $F$ or (3) there exists an index $i$ and an observation $\mathbf{O}'_i$ such that for $(B'_3, B_3) = \Delta((B', B), (\alpha_1, \mathbf{O}_1) \cdots (\alpha_{i-1}, \mathbf{O}_{i-1}) (\alpha_i, \mathbf{O}'_i))$ there exists $q \in B_3$, $(q, B'_3, B_3) \notin W_{k-1} \cap Q \times \mathcal{B}l_{\subseteq I} \times \mathcal{B}l$. In the first case, it means that
there is a positive probability, under $\tau$ to reach a pair of beliefs out of $W_{k-1}$, and thus out of $Win_{=1}$ by induction hypothesis. As the sequence of action and observations was chosen so that one can reach $F$ from $q$, the second case implies that the first case holds with our selected sequence of actions and observations. For the third case, let $(B'_3, B_3) = \Delta((B', B), (\alpha_1, O_1) \cdots (\alpha_{i-1}, O_{i-1})(\alpha_i, O'_i))$. Either there exists $q' \in B_3$ such that $(q, B'_3, B_3) \notin W_{k-1}$, then it is treated similarly to the first case. Else $B'_3 \notin Bl_{\subseteq I}$. Observe that, in this case, the second requirement on $\tau$ is not satisfied since $\mathbb{P}_{\tau}^{\delta_0}(\square I) < 1$. $\square$

Thanks to Lemma 6.1, $Win_{=1}$ can be computed in EXPTIME. Let us now define Lose as the set of beliefs that are clearly losing:

$$ \text{Lose} = \{B \in Bl | \neg\exists\tau \forall \delta_0 \text{ with } \text{Supp}(\delta_0) = B, \mathbb{P}_{\tau}^{\delta_0}(\square\diamond F) = 1\}. $$

As established e.g. in [BGG09] in the more general framework of 2-player stochastic games with signals, Lose can also be computed in EXPTIME.

Informally, we now consider the set of beliefs from which one can reach, while staying in $I$, and not risking to fall in Lose, some belief $B$ such that there exists $B' \neq \emptyset$ with $(B', B) \in Win_{=1}$. In order to easily represent what staying in $I$ means, we assume without loss of generality that the set of states $Q \setminus I$ is absorbing$^4$. Formally, let Win be the following set of beliefs:

$$ \text{Win} = \{B_0 \in Bl | \exists(B', B) \in \text{Win}_{=1} \text{ s.t. } B' \neq \emptyset \text{ and} \\ \exists \alpha_1 \cdots \alpha_n, \exists O_1 \cdots O_n, \Delta(B_0, (\alpha_1, O_1) \cdots (\alpha_n, O_n)) = B \\ \forall i \le n, \forall O'_i, \Delta(B_0, (\alpha_1, O_1) \cdots (\alpha_{i-1}, O_{i-1})(\alpha_i, O'_i)) \notin \text{Lose}\}. $$

The set Win characterizes winning beliefs, that is, beliefs from which there exists a finite-memory scheduler (called a winning scheduler) ensuring at the same time, the Büchi objective $\square\diamond F$ almost-surely, and the safety objective $\square I$ with positive probability. Formally:

**Lemma 6.2.** $B_0 \in Win$ if and only if for every $\delta_0$ with $\text{Supp}(\delta_0) = B_0$, there exists a finite-memory scheduler $\tau$ such that $\mathbb{P}_{\tau}^{\delta_0}(\square\diamond F) = 1$ and $\mathbb{P}_{\tau}^{\delta_0}(\square I) > 0$.

*Proof of Lemma 6.2.* Assume first that $B_0 \in Win$. We design a finite memory scheduler $\tau$ that is winning from any initial distribution $\delta_0$ with support $B_0$. In a first mode, $\tau$ aims at reaching a pair of beliefs $(B', B) \in Win_{=1}$ from $B_0$. More precisely, $\tau$ plays the sequence of actions that leads with positive probability from $B_0$ to some $B \in Bl$ such that there exists $B' \neq \emptyset$ with $(B', B) \in Win_{=1}$. If this succeeds, $\tau$ then switches to another mode, where it behaves as the winning scheduler that starts from $(B', B)$ in Lemma 6.1. If it fails, the play ends in a belief $B_1 \notin Lose$ (by definition of Win), and from there $\tau$ plays to ensure visiting $F$ infinitely often with probability 1. All in all, $\tau$ ensures almost surely visiting $F$ infinitely often, and with positive probability (the

<footnote>$^4$This can be ensured similarly to what was done for the set $Q_f$ in Subsection 1.4 of Chapter 2, page 43.</footnote>
probability of the prefix leading to $B$, times the probability that the play is in $B'$ at that time point) to stay in $I$. Note that the size of the memory $\tau$ uses is in $O(|Bl|^2)$. Indeed, in its first phase, it tries to reach a belief by using a set of actions of length smaller than $|Bl|$ as it does not need to visit the same belief twice. If it fails to reach the target belief, then ensuring the Büchi requirement can be done with a belief-based scheduler, i.e. a scheduler that only remembers the current belief, thus with memory of size $|Bl|$. If it reaches its target however, it needs to remember pairs of beliefs as done in Lemma 6.1, thus requires a memory of size $|Bl|^2$.

Let now $\delta_0$ be an initial distribution with support $B_0$, and assume that there exists a finite-memory scheduler $\tau$ such that $\mathbb{P}_{\tau}^{\delta_0}(\Box\diamond F) = 1$ and $\mathbb{P}_{\tau}^{\delta_0}(\Box I) > 0$. We consider $\mathcal{M}(\tau)$ the pLTS generated by $\tau$, with finite state space $Q \times \text{Mem}$, where Mem is a finite set of memory states. Without loss of generality, we iteratively tag each state of $\mathcal{M}(\tau)$ with its associated belief. Since $\tau$ is winning and almost surely a run reach a BSCC, there must exist a BSCC $C$ in $\mathcal{M}_{\tau}$, reachable from some $(q_0, m_0)$ via an $I$-run $\rho$ (a run where all state are included in $I$), and such that all states $(q, m) \in C$ satisfy $q \in I$, and there exists a state $(q_f, m_f) \in C$ such that $q_f \in F$. Let $(q, m) \in C$ be the state reached by run $\rho$, $B$ be the belief obtained after observing $\rho$. From $(q, m)$, under scheduler $\tau$, all plays stay in $I$. Moreover, for any $q' \in B$, from $(q', m)$, under scheduler $\tau$, almost all runs visit $F$ infinitely often. As a consequence, by the definition of $\text{Win}_{=1}$, $(\{q\}, B) \in \text{Win}_{=1}$. Then, we conclude that $B_0 \in \text{Win}$, exploiting the $I$-run $\rho$, and the fact that $\tau$ ensures $\Box\diamond F$ almost-surely, and thus always avoids Lose. $\square$

$\text{Win}$ characterizes the winning beliefs, and can be computed in EXPTIME. We thus showed the computability in EXPTIME of the set of supports $B$ from which for every distribution $\delta_0$ with $\text{Supp}(\delta_0) = B$ there exists a finite-memory scheduler $\tau$ such that $\mathbb{P}_{\tau}^{\delta_0}(\Box\diamond F) = 1$ and $\mathbb{P}_{\tau}^{\delta_0}(\Box I) > 0$. $\square$

Now the safe active diagnosis restricted to finite-memory strategies can be reduced to the existence for POMDP of a finite-memory scheduler that ensures a Büchi objective almost surely, and a safety objective with positive probability. As $M_C$ is exponential in the size of $C$ and the algorithm on the POMDP is in EXPTIME, we obtain a 2EX-PTIME complexity upper-bound. Fortunately, in order to avoid a doubly exponential blowup and to establish the EXPTIME complexity, we observe that the exponential comes in both cases from the computation of beliefs depending only on the original CLTS. This implies that the safe active probabilistic diagnosis problem is in EXPTIME when restricted to finite-memory strategies.

**Corollary 6.2.** *The safe active diagnosis problem restricted to finite-memory strategies is decidable in EXPTIME.*

*Proof.* Given a CLTS $C$, we build $M_C$ and decide if there exists a scheduler $\tau$ ensuring $\mathbb{P}_{\tau}^{\delta_0}(\Box\diamond F) = 1$ and $\mathbb{P}_{\tau}^{\delta_0}(\Box I) > 0$ with $I = \{(q, a, B) \mid q \in Q_c\}$ and $F = \{(q, a, B) \mid B \subseteq Q_f \lor q \in Q_c\}$ and $\delta_0$ is the Dirac distribution of support $\{q_0^{M_C}\}$. Due to the link between $M_C$ and $C$, this choice of $F$ corresponds to runs that are either correct or surely faulty in $C$ and this choice of $I$ corresponds to runs that are correct. Thus there exists a
finite-memory scheduler $\tau$ as defined above iff the corresponding strategy $\pi$ in $C$ ensures safe active diagnosis. Moreover, as explained above the corollary, deciding the existence of this scheduler can be done in EXPTIME. $\square$

A matching lower-bound is already known from the literature:

**Proposition 6.5 ([BFH$^{+}$14]).** The safe active diagnosis problem restricted to finite-memory strategies is EXPTIME-hard.

Obviously, this lower bound also holds for the more general problem: on POMDP, whether there exists a finite-memory strategy ensuring a Büchi objective almost-surely and a safety objective with positive probability.

# 3 Conclusion

Degradation of a controllable probabilistic system combines two objectives. The system must satisfy at the same time a diagnosability and a degradation condition. Interestingly and as shown first in [BFH$^{+}$14], having to satisfy both conditions at the same time increases the difficulty: safe active diagnosability combines two decidable problems yet ends up being undecidable. In order to regain decidability, we introduced two new degradation notions both in a qualitative and a quantitative ways. While the quantitative versions are undecidable, the qualitative ones brings interesting results. Indeed, on the one hand, they are close to safe active diagnosability as two of the notions are equivalent to it for finite pLTS. On the other hand, they are decidable in EXPTIME. As EXPTIME is the lower bound of the complexity of active diagnosability, it is unsurprisingly also a lower bound of the complexity of the combination of active diagnosability and of a degradation condition. Therefore we can test the combination of active diagnosability with a degradation condition without reaching a new complexity class.

This analysis however can result in diagnosers requiring infinite memory. When restricted to finite-memory controllers, many differences appear. First, as the pLTS obtained by controlling a CLTS with a finite-memory strategy is finite, then according to Theorem 6.1, safety, strong resiliency and lasting fault freeness are equivalent. Studying the safe active diagnosability, we showed it to be EXPTIME-complete. Thus, the restriction to finite memory helped regain decidability. For weakly resilient active diagnosability, the restriction to finite memory is not necessary as, as shown in Theorem 6.2, if the system is weakly resilient active diagnosable, there exists a strategy with finite memory.

The notions of degradation introduced here were inspired from the notion of safe active diagnosability. One could be interested in other notions of degradations representing different forms of failures within the system. For example, in our framework, the notion of faulty run is a Boolean one; once a fault occurred, the run is faulty. The fault is thus seen as a definitive and complete damage of the system. But a fault could only represent a small degradation of the system which would still be partially available. In this alternative framework, the degradation to be evaluated would be the evolution
of the number of faults in a run w.r.t. its length. Another possible direction of research
would be to take a more general approach to the notion of combined objectives. It
would be interesting to determine which pairs of objectives can be studied separately
and which ones lead to undecidability.
# Chapter 7

## Opacity

This thesis consists in a study of the control of the information in probabilistic systems, mainly focusing on diagnosis. While the goal of diagnosis is to analyse an observation in order to reveal a hidden information (the fault), one could be interested in asking a dual question: can we limit the amount of hidden information that is revealed by the system. This question belongs to an important domain of partial observation issues called opacity. While the two notions can appear similar, the motivations behind them are different. Diagnosability is a notion of safety of a system while opacity is one of security. This difference in motivations implies that the questions asked for opacity are not be the same as the ones asked for diagnosis. Moreover, the model itself can differ in order to possess different properties. In this introduction, we first present informally opacity and some questions related to this domain of research: in the passive framework then in the active one. Finally, we discuss the form of control used in the active opacity framework, emphasising the differences with active diagnosability.

**Opacity problems for passive systems.** Given a set of secret runs, a run discloses the secret if every run with the same observed sequence is secret. With this definition, the disclosure of the secret is akin to exact diagnosability. One can also define a notion of disclosure that would resemble approximate diagnosability: for $\varepsilon > 0$, a secret run $\varepsilon$-discloses the secret if the probability of runs with the same observed sequence that are not secret conditioned on the probability of the observed sequence is at most $\varepsilon$. For non-probabilistic systems, opacity boils down to detecting if there exist a run disclosing the secret to an observer. For probabilistic systems, we are interested in quantifying the opacity of the system [BMS15, SH14, BKM12]. For instance we would want to determine if the measure of disclosing runs of a given length is positive, if it is above a certain threshold, and how this measure evolves with the observed length of the runs. This precise quantification of the measure of disclosing runs, called *disclosure*, does not appear in the diagnosability notions we studied. Indeed, a fault was considered a dangerous event which cannot, in any case, be missed. For the disclosing of the secret however, it is more usual to tolerate that part of the secret may be leaked, as long as it is a limited amount.
**Opacity problems for active systems.** The focus on disclosure takes a whole new meaning when considering active systems. Indeed, a controller will have an effect on the system, and depending on its choices, this disclosure will increase or decrease. Existing works study the case where the controller maximises the disclosure [BCS15, BKMS18]. This corresponds to a worst-case analysis of the system, i.e. for the worst possible control. This kind of analysis aims at representing the case where the control is done by an attacker that is observing the system. This control can be obtained by the attacker by using a virus for example. The opposite direction, where the control tries to minimise the disclosure is also worthy of analysis. Indeed, for example, if a system has been designed in order to satisfy a specification, yet there are still some liberties within the system, some choices that are possible and that do not affect the specification, then these choices can be made in order to optimise opacity of the system. In this case, the control is realised during the design of the system and is made in order to minimise the disclosure of the system. Thus, both maximisation and minimisation corresponds to real issues.

**Formalisation of the control.** When we studied active diagnosis in Chapter 6, the control was exterior to the system: from the observations it received, it was able to stop some controllable actions from occurring. The controller and the observer had the same information and thus could be thought as the same mechanism. In the examples given earlier (the virus for maximisation and the system design for the minimisation), the control comes from within the system. There is thus a clear separation between the controller and the observer/attacker. To formalise this opposition, the control is realised with a full knowledge of the system: it knows what is the exact run that is followed and especially what is the current state and make its decision based on this. However, as the attacker is not himself within the system a run only discloses the secret with its observation. In other words, the controller will try to minimise or maximise a set of runs satisfying a condition that is based on their observations. Moreover, we assume the attacker is aware of how the controller makes its choices. Indeed, the security of the system should not be based on the black box hypothesis (that an attacker is lacking information). Especially when considering cases such as the virus example: the virus could very well have been implanted in the system by the attacker, ensuring he is aware of how the virus works.

In Section 1, we establish the specifications and important questions of opacity that we consider throughout the chapter. These definitions present two different horizons over which to consider opacity: a given fixed horizon and an unbounded yet finite horizon. In Section 2 and Section 3, we study opacity over finite horizon for maximisation and minimisation respectively. These two sections echo one another emphasising the differences between the two. Finally in Section 4 we detail our results for opacity over fixed horizon for both maximisation and minimisation.

This chapter develops and extends some of the results from [BHL17a].
# 1 Specification for Opacity

The notion of opacity is very similar to the one of diagnosis. They both consider the information revealed by runs of partially observable systems. The difference is that the goal of diagnosis is to reveal an information about the current state of the system, while opacity tries to hide an information. Despite these similarities, the framework of opacity contains important differences with the one of diagnosis. We first define formally the framework of opacity for passive systems (Subsection 1.1), then extend the definitions to allow a control of the system (Subsection 1.2).

## 1.1 Opacity for Markov chains

Labelled Markov chains, as introduced in Chapter 4, are pLTS where every event is observable. We now define another kind of Markov chains called *observable Markov chains* which are pLTS where the observation is associated with the state instead of the transition. This labelling of states thus describes what an external observer can see and is given by an *observation function*<fnref n="1" />. We use this new framework as, while diagnosis aimed to detect an event (the fault), opacity consists in hiding that the system is currently in a secret behaviour represented by its state. This could however easily be translated as the detection of a transition triggered when entering a secret state. In fact, the equivalence of associating events with transitions or with states is a folk result. Figure 7.1 gives the informal idea of how to push events from states to transitions and Theorem 7.1 starts by a modification of the system that is close to the usual transformation allowing to associate the labels with the states rather than with the transitions.

<figure><img src="image_86.png" /><figcaption>Figure 7.1: Pushing observations from states to transitions.</figcaption></figure>

**Definition 7.1.** An observable Markov chain (OMC) over alphabet $Σ_o$ is a tuple $M = (S, p, O)$ where $S$ is a countable set of states, $p: S \to \text{Dist}(S)$ is the transition function, and $O: S \to Σ_o \cup \{\varepsilon\}$ is the observation function.

We write $p(s'|s)$ instead of $p(s)(s')$ to emphasise the fact that the probability of going to state $s'$ is conditioned by being in state $s$. Given a distribution $\mu_0$ on $S$, we

<footnote n="1">¹The equivalent of the observation function for pLTS was called mask function.</footnote>
denote by $\mathcal{M}(\mu_0)$ the Markov chain with initial distribution $\mu_0$. The definitions of runs, observed sequences, probability measure, ... can easily be adapted to OMC. To give an example, an infinite run of $\mathcal{M}(\mu_0)$ is a sequence of states $\rho = s_0s_1... \in S^\omega$ such that $\mu_0(s_0) > 0$ and for each $i \ge 0$, $p(s_{i+1}|s_i) > 0$. The observed sequence of this infinite run is $O(\rho) = O(s_0)O(s_1)... \in \Sigma_o^\infty$. The observation function is called *non erasing* if $O(S) \subseteq \Sigma$ (all states are visible).

As in opacity one aims to hide a secret behaviour of the system, a way to represent
what is secret is needed. There are various ways to define it depending on if we want
the secret to be permanent, intermittent, described within the system... We consider
here the case where the secret is permanent and given by a subset of states $\text{Sec} \subseteq S$ of
the model: a (finite of infinite) run $s_0s_1...$ is secret if $s_i \in \text{Sec}$ for some $i$, otherwise it
is public. Under this choice, the secret itself behaves very similarly to the fault. As for
pLTS where we could make the partition between faulty and correct states without loss
of generality, we assume here that the set of secret states $\text{Sec}$ is absorbing. To show
this can be done without loss of generality, a new Markov chain $\mathcal{M}' = (S', p', O')$ is
defined from $\mathcal{M}$ by: $S' = (S \times \{0,1\})$, where $(s,0)$ represents state $s$ where the secret
has not been visited while $(s,1)$ represents the opposite situation. The transitions are
then duplicated accordingly: (1) $p'((s',i)|(s,i)) = p(s'|s)$ for all $s \in S$, $s' \in S \setminus \text{Sec}$, and
$i \in \{0,1\}$, (2) $p'((s',1)|(s,i)) = p(s'|s)$ for all $s \in S$, $s' \in \text{Sec}$, and $i \in \{0,1\}$. The new
observation function is defined by $O'((s,i)) = O(s)$ for all $s \in S$ and $i=0,1$ and the new
set of secrets is $S \times \{1\}$. There is a one-to-one probability-preserving correspondence
between the runs in $\mathcal{M}$ and the ones in $\mathcal{M}'$.

**Example 7.1.** Consider the OMC of Figure 7.2 with initial distribution $\mathbf{1}_{q_0}$. The observation associated with a state by the observation function is displayed next to it. The secret state is shaded. Assuming $o_1 \neq \varepsilon$ and $o_2 \neq \varepsilon$, every state is associated with an observation different than $\varepsilon$, therefore the observation function is non-erasing.

<figure><img src="image_87.png" /><figcaption>Figure 7.2: An infinitely-branching OMC with $\text{Sec} = \{q_s\}$.</figcaption></figure>

One quantitative way to define the disclosure of a system is to consider that a
run discloses the secret if the probability that the current run belongs to the secret, conditioned over the observation of the run, is greater than some given threshold $\epsilon > 0$.

**Definition 7.2.** Given an OMC $\mathcal{M} = (S, p, O)$, an initial distribution $\mu_0$, $\text{Sec} \subseteq S$ and an observation $w \in \Sigma^*$, the proportion of secret runs with observation $w$ is:

$$ \text{Psec}_{\mathcal{M}(\mu_0)}(w) = \frac{\mathbb{P}_{\mathcal{M}(\mu_0)}(\{\rho \in \mathcal{O}^{-1}(w) \mid \rho \text{ is secret}\})}{\mathbb{P}_{\mathcal{M}(\mu_0)}(w)}. $$

For $\epsilon > 0$, $w$ is $\epsilon$-min-disclosing if $\text{Psec}_{\mathcal{M}(\mu_0)}(w) > 1 - \epsilon$ and no prefix of $w$ satisfies this inequality. Writing $D_{\min}^{\epsilon}$ for the set of $\epsilon$-min-disclosing observations, the $\epsilon$-disclosure is defined by $\text{Disc}^{\epsilon}(\mathcal{M}(\mu_0)) = \sum_{w \in D_{\min}^{\epsilon}} \mathbb{P}_{\mathcal{M}(\mu_0)}(w)$. The positive $\epsilon$-disclosure problem consists in deciding whether $\text{Disc}^{\epsilon}(\mathcal{M}(\mu_0)) > 0$.

To establish a parallel with diagnosability, positive $\epsilon$-disclosure is similar to $\epsilon$FF-diagnosability. Indeed, in $\epsilon$FF-diagnosability (resp. the positive $\epsilon$-disclosure problem) one considers the fault (resp. secret) revealed if the likelihood of the fault (resp. secret) conditioned on the observation is above $1 - \epsilon$. The difference is that for opacity, we ask whether the measure of the set of runs disclosing the secret is positive while for diagnosability, we require this probability to be equal to the probability of faulty runs. In other words, considering a run to be faulty iff it is secret, the system is $\epsilon$FF-diagnosable iff $\text{Disc}^{\epsilon}(\mathcal{M}(\mu_0)) = \mathbb{P}(F_{\infty})$.

In this chapter, we aim at studying active notions of opacity. While being the most realistic notion of probabilistic disclosure, $\epsilon$-disclosure is unfortunately a too complex notion. Indeed, the problem is already undecidable for OMC:

**Theorem 7.1.** The positive $\epsilon$-disclosure problem is undecidable for OMC.

To establish this undecidability result, we reduce the emptiness problem for probabilistic automata. The reduction itself is pretty straightforward. Note however that the reduction requires to first translate the PA into an OMC such that the probability of acceptance of a word $w$ in the PA is equal to the probability to end in a secret state in the Markov chain knowing that the run has observed sequence $w$.

The emptiness problem and the value 1 problem<fnref n="2" /> are undecidable for PA already with a two-letter alphabet [Paz71, GO10]. Hence in the various reductions we use the alphabet $\{a, b\}$.

*Proof.* Given a PA $A = (Q, q_0, \{a, b\}, (\mathbf{P}_a, \mathbf{P}_b), F)$ that we suppose complete without loss of generality, we first transform $A$ into an incomplete OMC $\hat{A}$ where $\{a, b, \flat\}$ is the observation alphabet (an illustration is given in Figure 7.3). The set of states is $\hat{Q} = Q \cup \{q_{\text{tag}} \mid q \in Q \wedge \text{tag} \in \{a, b\}\}$, with initial distribution $\mathbf{1}_{q_0}$. The observation function $\hat{O}$ is defined by $\hat{O}(q) = \flat$ and $\hat{O}(q_c) = c$ for $q \in Q$ and $c \in \{a, b\}$. The transition function $\hat{p}$ is defined for $q, q' \in Q$ and $c \in \{a, b\}$ by $\hat{p}(q' \mid q_c) = \mathbf{P}_c(q, q')$ and $\hat{p}(q_c \mid q) = \frac{1}{4}$. This OMC is incomplete as for every state $q \in Q$, the sum of the probabilities exiting $q$ in $\hat{A}$ is $1/2$.

<footnote n="2">²These notions were defined before Theorem 4.3, page 115</footnote>
<figure><img src="image_88.png" /><figcaption>Figure 7.3: From PA A to incomplete OMC $\hat{A}$.</figcaption></figure>

<figure><img src="image_89.png" /><figcaption>Figure 7.4: Reduction to the positive $\varepsilon$-disclosure problem.</figcaption></figure>

We now build the OMC $\mathcal{M}_A = (S, p, \mathcal{O})$ over alphabet $\{a, b, \flat, \sharp\}$ by adding two states to complete $\hat{A}$ (see Figure 7.4 where the doubly circled state $q_f$ is a final state of A):

* $S = \{s_{\text{pub}}, s_{\text{sec}}\} \cup \hat{Q}$, with $\text{Sec} = \{s_{\text{sec}}\}$;

* The function $p$ is obtained from $\hat{p}$ by adding the transitions: For every $q \in F$, $p(s_{\text{sec}} | q) = \frac{1}{2}$, for every $q \in Q \setminus F$, $p(s_{\text{pub}} | q) = \frac{1}{2}$, and $p(s_{\text{pub}} | s_{\text{sec}}) = 1$;

* $\mathcal{O}$ extends $\hat{\mathcal{O}}$ by $\mathcal{O}(s_{\text{sec}}) = \mathcal{O}(s_{\text{pub}}) = \sharp$.

We now prove that, given $\varepsilon \in ]0, 1[$, A accepts a word with probability strictly greater than $1 - \varepsilon$ iff $\text{Disc}^{\varepsilon}(\mathcal{M}(\mu_0)) > 0$. First assume that there exists a word $w = a_1 \dots a_n \in \{a, b\}^*$ with $\mathbf{P}_A(w) > 1 - \varepsilon$. Then $w$ corresponds to a non secret run with observed sequence $\hat{w} = \flat a_1 \flat \dots a_n \flat$ in $\mathcal{M}_A$ and $\text{Psec}_{\mathcal{M}(\mu_0)}(\hat{w}\sharp) = \mathbf{P}_A(w) > 1 - \varepsilon$, which implies $\text{Disc}^{\varepsilon}(\mathcal{M}(\mu_0)) > 0$.
Conversely, if $Disc^\epsilon(M(\mu_0)) > 0$, then there exists an observation $w'$ in $(\{a, b, b, \#\})^*$ such that $\text{Psec}_{M(\mu_0)}(w') > 1 - \epsilon$. In this case, $w'$ is of the form $ba_1b...a_nb^\#\#^*$ where, letting $w = a_1...a_n$, we have $\text{Psec}_{M(\mu_0)}(w') = \text{Psec}_{M(\mu_0)}(ba_1b...a_nb^\#) = \mathbf{P}_A(w)$. Therefore $\mathcal{L}_{>1-\epsilon}(A)$ is not empty. $\square$

This undecidability result leads us to consider the simpler case where the disclosure is the probability of the set of runs surely leaking the secret, i.e., such that all runs with the same observation are secret. One such disclosure notion, the $\omega$-disclosure (used in [BCS15, BMS15, BKMS16]), was defined for a Markov chain $\mathcal{M} = (S, p, \mathcal{O})$ with initial distribution $\mu_0$ by considering a measurable set of secret runs $\text{SecRuns} \subseteq \Omega^{\mathcal{M}(\mu_0)}$. In our context, as mentioned earlier, $\text{SecRuns}$ is $\text{Reach}(\text{Sec})$, the set of infinite runs visiting a state from Sec. Moreover an infinite observation $w \in \Sigma^\omega$ discloses the secret if all runs $\rho \in \mathcal{O}^{-1}(w)$ are secret. Setting $\overline{\text{SecRuns}} = \Omega^{\mathcal{M}(\mu_0)} \setminus \text{SecRuns}$, we define:

**Definition 7.3.** For an OMC $\mathcal{M} = (S, p, \mathcal{O})$, an initial distribution $\mu_0$ and a subset $\text{Sec} \subseteq S$, with $\text{SecRuns} = \text{Reach}(\text{Sec})$, the $\omega$-disclosure of $\text{Sec}$ in $\mathcal{M}$ is:

$$ \text{Disc}_\omega(\mathcal{M}(\mu_0)) = \mathbb{P}_{\mathcal{M}(\mu_0)}(\text{SecRuns} \setminus \mathcal{O}^{-1}(\mathcal{O}(\text{SecRuns}))). $$

The downside of this definition is that it only considers infinite observed sequences. In reality, an attacker will only have access to finite observed sequences before having to deduce if the system is in a secret state. To obtain measures directly related to the finite observation of a potential attacker, we assume that $\mathcal{M} = (S, p, \mathcal{O})$ is convergent: each infinite run $\rho$ has an infinite observation $\mathcal{O}(\rho) \in \Sigma^\omega$. Two measures can then be defined: using fixed or finite horizon. In the fixed-horizon case, the attacker observes the system for a fixed amount of time and has to make his deduction at the end of this observation. In order to link the amount of time the attacker observes the system and the number of observations they receive, in this case, we only consider non-erasing observation functions $\mathcal{O}$. In the finite-horizon case, the attacker can wait as long as they want, as long as it is a finite amount of time.

**Definition 7.4.** Let $\mathcal{M} = (S, p, \mathcal{O})$ be an OMC, $\mu_0$ an initial distribution and $\text{Sec} \subseteq S$. A finite observation $w \in \Sigma^*$ discloses the secret if all runs $\rho \in \mathcal{O}^{-1}(w)$ are secret. It is min-disclosing if it discloses the secret and no strict prefix of $w$ does.

**n-disclosure** : When $\mathcal{O}$ is non-erasing, we denote by $D_n$, for $n \in \mathbb{N}$, the set of disclosing observations of length $n$. The n-disclosure (disclosure with fixed horizon $n$) is
$$ \text{Disc}_n(\mathcal{M}(\mu_0)) = \sum_{w \in D_n} \mathbb{P}_{\mathcal{M}(\mu_0)}(w); $$

**Disclosure** : Writing $D_{\min}$ for the set of min-disclosing observations, the disclosure (w.r.t. finite horizon) is defined by $\text{Disc}(\mathcal{M}(\mu_0)) = \sum_{w \in D_{\min}} \mathbb{P}_{\mathcal{M}(\mu_0)}(w)$.

Note that if $D$ is the set of disclosing observations, and $\mathcal{V}(\mu_0) = \cup_{w \in D} \cup_{\rho \in \mathcal{O}^{-1}(w)} \text{Cyl}(\rho)$ the set of runs disclosing the secret, then $\text{Disc}(\mathcal{M}(\mu_0)) = \mathbb{P}_{\mathcal{M}(\mu_0)}(\mathcal{V}(\mu_0))$. As waiting longer gives more information, the disclosure with finite horizon is always at least as large as the disclosure with fixed horizon. In fact, $(\text{Disc}_n(\mathcal{M}(\mu_0)))_{n \in \mathbb{N}}$ is a non-decreasing sequence with limit $\text{Disc}(\mathcal{M}(\mu_0))$.
**Example 7.2.** Consider the infinitely-branching OMC of Figure 7.2. The single secret run is $\text{SecRuns} = \{q_0q_s^\omega\}$ and its observation is $o_1^\omega$. Moreover, the observations of the public (as opposed to secret) infinite runs is $O(\overline{\text{SecRuns}}) = o_1^+o_2^\omega$. As a consequence, the infinite observed sequence of the secret run discloses the secret, $\text{Disc}_\omega = \frac{1}{2}$. However, no finite observation is disclosing: $\forall n \in \mathbb{N}, \text{Disc}_n = \text{Disc} = 0$.

This shows that disclosure and $\omega$-disclosure differ.

However, both notions coincide for convergent finitely-branching OMC.

**Lemma 7.1.** Let $\mathcal{M} = (S, \mathcal{P}, \mathcal{O})$ be a Markov chain, $\mu_0$ an initial distribution and $\text{Sec} \subseteq S$. For $\text{SecRuns} = \text{Reach}(\text{Sec})$, $\text{Disc}(\mathcal{M}(\mu_0)) \le \text{Disc}_\omega(\mathcal{M}(\mu_0))$ with equality when $\mathcal{M}$ is convergent and finitely branching.

*Proof.* We first establish the following claim: if $\mathcal{M}$ is convergent and finitely branching, then the set of runs $\rho$ such that $\mathcal{O}(\rho)$ has length $n$ is finite for any $n > 0$.

We first prove the claim for signalling runs. We proceed by induction on the observable length. There exist finitely many signalling runs of length 0: by convention they are the runs that (1) do not contain any event and (2) start in an unobservable state of $\text{Supp}(\mu_0) \cap \mathcal{O}^{-1}(\varepsilon)$. Let us assume the hypothesis holds for $n \in \mathbb{N}$. For every signalling run $\rho_0$ with $|\rho_0|_o = n$ we consider the tree formed by the set $\mathcal{O}_{n+1} = \{\rho \in \text{SR} \mid \rho_0 \preceq \rho \wedge \mathcal{O}(\rho) = n+1\}$ by sharing common prefixes. Internal nodes of this tree correspond to unobservable states while all leaves are observable. Since the OMC is finitely branching, the tree is of bounded degree. By contradiction, assume that the tree is infinite. König's lemma yields an infinite branch containing only unobservable states, which contradicts the convergence hypothesis. Therefore there exist only finitely many signalling runs of observable length $n+1$ extending $\rho_0$. As there exist finitely many signalling runs of observable length $n$ according to the induction hypothesis, one deduces that there exist finitely many signalling runs of observable length $n+1^3$. This concludes the induction. The result can then be extended to every runs as, from the convergence hypothesis, for every $n \in \mathbb{N}$ and every run $\rho$ of observable length $n$, there exists a signalling run $\rho' \in \text{SR}_{n+1}$ such that $\rho \preceq \rho'$. As $|\text{SR}_{n+1}| < \infty$, there are finitely many runs of observable length $n$.

We now prove that the set of infinite runs $\mathcal{V} = \cup_{w \in D} \cup_{\rho \in \mathcal{O}^{-1}(w)} \text{Cyl}(\rho)$ is contained in $\text{SecRuns} \setminus \mathcal{O}^{-1}(\mathcal{O}(\overline{\text{SecRuns}}))$. Let $\rho_1$ be an infinite run in $\mathcal{V}$. Then there is a disclosing observation $w_1 \in \Sigma^*$ and a signalling prefix $\rho'_1$ of $\rho_1$ such that $\mathcal{O}(\rho'_1) = w_1$ and $\rho'_1$ is secret. For any infinite run $\rho_2$ such that $\mathcal{O}(\rho_1) = \mathcal{O}(\rho_2)$, the observation $w_1$ is also a prefix of $\mathcal{O}(\rho_2)$, hence there is a finite signalling prefix $\rho'_2$ of $\rho_2$ such that $\mathcal{O}(\rho'_2) = w_1$. Since $w_1$ is disclosing, $\rho'_2$ is also secret, hence $\rho_1$ belongs to $\text{SecRuns} \setminus \mathcal{O}^{-1}(\mathcal{O}(\overline{\text{SecRuns}}))$ and $\text{Disc}(\mathcal{M}(\mu_0)) \le \text{Disc}_\omega(\mathcal{M}(\mu_0))$.

For the converse inclusion, let $\rho$ be an infinite run in $\text{SecRuns} \setminus \mathcal{O}^{-1}(\mathcal{O}(\overline{\text{SecRuns}}))$ with observation $\mathcal{O}(\rho) = w = o_1o_2\dots \in \Sigma^\omega$. We prove by contradiction that there is a finite disclosing prefix $\hat{w}$ of $w$ and a signalling prefix $\hat{\rho}$ of $\rho$ such that $\rho \in \text{Cyl}(\hat{\rho})$ and $\mathcal{O}(\hat{\rho}) = \hat{w}$.

<footnote n="3">³For the case $n=0$ one must also consider the signalling runs obtained from runs starting in states of $\text{Supp}(\mu_0) \setminus \mathcal{O}^{-1}(\varepsilon)$. There are finitely many such runs too.</footnote>
Otherwise, for any $n \ge 1$, $w_n = o_1 \dots o_n$ is not disclosing and there exists a signalling run $\rho_n$ such that $O(\rho_n) = w_n$ but $\rho_n$ is not secret. The set $\mathcal{T} = \{\rho' \in SR \mid \exists n \rho' \le \rho_n\}$ of all signalling prefixes of the $\rho_n$'s form a tree: the root of the tree is $\varepsilon$ and the nodes at level $k$ are the prefixes with observation $w_k$, $\{\rho' \in \mathcal{T} \mid |O(\rho')| = k\}$. A node $\rho''$ is a child of $\rho'$ if $|O(\rho')| = w_k$, $|O(\rho'')| = w_{k+1}$ for some $k$ and $\rho' \preceq \rho''$. From the claim, we know that $\mathcal{T}$ is of bounded degree. Assuming that it is infinite, König's lemma again yields an infinite branch $\rho_\infty$ such that each prefix of length $k$ is not secret and has observation $w_k$. Hence $\rho_\infty$ is not secret and has observation $O(\rho_\infty) = w$, which is a contradiction. $\square$

In the following we only consider finitely-branching convergent systems. As a consequence, we will only focus on disclosure over fixed or finite horizon.

## 1.2 Opacity for Markov Decision Processes

We now want to add control to the system. The form of control we define here differs from the one used in Chapter 6. Indeed, in the context of diagnosability, the controller observed the system and from this observation, they chose some controllable actions that they blocked until the next observation. Thus the control had to make decisions without an exact knowledge of the state of the system. For opacity we are interested by a control acting with full knowledge. Therefore, the control can be more accurate. We use Markov decision processes where in each state there is a set of possible actions and the controller chooses one of them. This action induces a probability distribution on the next state reached.

**Definition 7.5.** An observable Markov Decision Process (OMDP) over alphabet $\Sigma$ is a tuple $M = (S, \mathbf{Act}, p, \mathbf{O})$ where $S$ is a finite set of states, $\mathbf{Act} = \cup_{s \in S} A(s)$ where $A(s)$ is a finite non-empty set of actions for each state $s \in S$, $p: S \times \mathbf{Act} \to \text{Dist}(S)$ is a (partial) transition function defined for $(s, a)$ when $a \in A(s)$ and $\mathbf{O}: S \to \Sigma \cup \{\varepsilon\}$ is the observation function.

The difference with POMDP described in Definition 6.8, page 6.8, beside some syntactic modifications is on how the control is defined. As for OMC, we write $p(s'|s, a)$ instead of $p(s, a)(s')$. We use the same kind of definitions as usual for runs, observed sequences, ... For example, given an initial distribution $\mu_0$, an infinite run of $M$ is a sequence $\rho = s_0 a_0 s_1 a_1 \dots$ where $\mu_0(s_0) > 0$ and $p(s_{i+1}|s_i, a_i) > 0$, for $s_i \in S$, $a_i \in A(s_i)$, for all $i \ge 0$. We denote by $M(\mu_0)$ the OMDP $M$ with initial distribution $\mu_0$. For decidability and complexity results, we assume that all probabilities occurring in the model (transition probabilities and initial distribution) are rational.

**Example 7.3.** Consider the OMDP of Figure 7.5. From the initial state $q_0$, two actions are possible. If action a is chosen, the system moves to $q_1$ with probability 1/2 and to $q_2$ with probability 1/2. If b is chosen, every state has a probability 1/3 to be reached.

The OMDP model uses both non-deterministic choice (the choice of the action) and probabilistic choice (the induced distribution). The non-determinism is where the
<figure><img src="image_90.png" /><figcaption>Figure 7.5: An example of OMDP where the initial distribution is a Dirac distribution on $q_0$. Transitions are labelled by a set of pairs of actions and of the probability to take this transition under that action.</figcaption></figure>

control can be operated. It is resolved by a strategy which associates with every run a distribution on the actions enabled at the last state of the run. Given a finite run $\rho$ with $\text{last}(\rho) = s$, a *decision rule* of an OMDP for $\rho$ is a distribution $\delta \in \text{Dist}(A(s))$ representing the action chosen after $\rho$. For such a decision rule $\delta$, we write $p(s'|s, \delta) = \sum_{a \in A(s)} \delta(a)p(s'|s, a)$.

**Definition 7.6.** A strategy for the OMDP $\mathbf{M} = (S, \text{Act}, p, \mathbf{O})$ is a mapping $\sigma$ associating to every finite run $\rho$ a decision rule $\sigma(\rho)$.

Given a strategy $\sigma$, a run $\rho = s_0a_0s_1a_1\dots$ of $\mathbf{M}$ is $\sigma$-compatible if for all $i$, $a_i \in \text{Supp}(\sigma(s_0a_0s_1a_1\dots s_i))$.

In order to apply the strategies as defined here one requires to remember the whole run that occurred. Moreover, the strategies are allowed to choose randomly between the different allowed actions. All of this may not always be necessary however. We are thus interested specifically in strategies satisfying specific properties. A strategy $\sigma$ is *deterministic* if $\sigma(\rho)$ is a Dirac distribution for each finite run $\rho$. In this case, we denote by $\sigma(\rho)$ the single action $a \in A(\text{last}(\rho))$ such that $\sigma(\rho) = \mathbf{1}_a$. A strategy $\sigma$ is *observation-based* if for any finite run $\rho$, $\sigma(\rho)$ only depends on (1) the observed sequence $\mathbf{O}(\rho)$ and (2) the current state $\text{last}(\rho)$, i.e. given $\rho'$ such that $\mathbf{O}(\rho) = \mathbf{O}(\rho')$ and $\text{last}(\rho) = \text{last}(\rho')$, we have $\sigma(\rho) = \sigma(\rho')$. We then write $\sigma(\mathbf{O}(\rho), \text{last}(\rho))$ for $\sigma(\rho)$.

Let $\sigma$ be a strategy and $\rho$ be a $\sigma$-compatible run. We define $B_{\rho}^{\sigma}$ the *belief* of $\rho$ w.r.t. $\sigma$ about states as follows:

$$B_{\rho}^{\sigma} = \{s \in S \mid \exists \rho' \text{ } \sigma\text{-compatible, } \mathbf{O}(\rho') = \mathbf{O}(\rho) \wedge s = \text{last}(\rho') \wedge \mathbf{O}(s) \neq \varepsilon\}.$$

The belief $B_{\rho}^{\sigma}$ contains the set of states that can be reached under the strategy $\sigma$ and with observation $\mathbf{O}(\rho)$. A strategy $\sigma$ is *belief-based* if for all finite run $\rho$, $\sigma(\rho)$ only depends on the belief $B_{\rho}^{\sigma}$ and the current state $\text{last}(\rho)$, i.e. given $\rho'$ such that $B_{\rho}^{\sigma} = B_{\rho'}^{\sigma}$
and $\text{last}(\rho) = \text{last}(\rho')$, we have $\sigma(\rho) = \sigma(\rho')$. Observe that a belief-based strategy is observation-based since $B_{\rho}^{\sigma}$ only depends on $w = \mathbf{O}(\rho)$. So we also write $B_{w}^{\sigma}$ for $B_{\rho}^{\sigma}$. A strategy $\sigma$ is *memoryless* if $\sigma(\rho)$ only depends on $\text{last}(\rho)$ for all $\rho$.

The semantics of a OMDP $\mathcal{M}$ with initial distribution $\mu_0$ under the strategy $\sigma$ is a (possibly infinite) observable Markov chain $\mathcal{M}_{\sigma}(\mu_0)$ where each state is associated with a finite $\sigma$-compatible run of $\mathcal{M}(\mu_0)$, that can be equipped with the observation function mapping $\mathbf{O}(\text{last}(\rho))$ to the state associated with the finite run $\rho$. The transition function $p_{\sigma}$ is defined for $\rho$ a finite run and $\rho' = \rho \text{pas}'$ by $p_{\sigma}(\rho'|\rho) = \sigma(\rho)(a)p(s'|s, a)$ and we denote by $\mathbb{P}_{\mathcal{M}_{\sigma}(\mu_0)}$ (or $\mathbb{P}_{\sigma}$ for short when there is no ambiguity) the associated probability measure. Writing $\mathcal{V}_{\sigma}(\mu_0)$ for the set of runs disclosing the secret in $\mathcal{M}_{\sigma}(\mu_0)$, we have $\text{Disc}(\mathcal{M}_{\sigma}(\mu_0)) = \mathbb{P}_{\mathcal{M}_{\sigma}(\mu_0)}(\mathcal{V}_{\sigma}(\mu_0))$. We assume all OMDP considered are convergent (there is no cycle of unobservable states), which implies the convergence of all OMC induced by strategies.

**Example 7.4.** Consider the OMC of Figure 7.6. It represents the semantics of the OMDP of Figure 7.5 with the strategy $\sigma$ choosing the action $b$ initially, then always choosing action $a$. $\sigma$ is observation-based as the only run for which it does not select $a$ is the empty run, which is the only run with observed sequence $o_2$. It is also belief-based as the empty run is the only run with belief $\{q_0\}$. Indeed, after some observations, the current belief is either $\{q_0, q_2\}$ or $\{q_1\}$. It is however not memoryless as the empty run and $q_0bq_0$ both ends in $q_0$ but the same action is not chosen in both cases. After three observations, under $\sigma$, the system cannot be in $q_0$ any more, it is thus necessarily in a secret state. Therefore, $\text{Disc}(\mathcal{M}_{\sigma}(\mu_0)) = 1$.

<figure><img src="image_91.png" /><figcaption>Figure 7.6: The OMC induced by the strategy choosing the action $b$ initially, then always choosing action $a$ for the OMDP of Figure 7.5.</figcaption></figure>

The control can be either adversarial or cooperative with respect to the system: it
can try to either maximise or minimise the opacity. We therefore define the disclosure
value of an OMDP according to the type of the strategies. We only consider $\varepsilon$-disclosure
for fixed horizon in light of the undecidability result of Theorem 7.1.

**Definition 7.7.** Given an OMDP $\mathbf{M} = (S, \mathbf{Act}, p, O)$, an initial distribution $\mu_0$ and a secret $\text{Sec} \subseteq S$, for $\text{disc} \in \{\text{Disc}, \text{Disc}_n, \text{Disc}_n^\varepsilon\}$, $n \in \mathbb{N}$ and $0 < \varepsilon < 1$, the maximal disclosure of $\text{Sec}$ in $\mathbf{M}$ is $\text{disc}_{\max}(\mathbf{M}(\mu_0)) = \sup_\sigma \text{disc}(\mathbf{M}_\sigma(\mu_0))$ and the minimal disclosure of $\text{Sec}$ is $\text{disc}_{\min}(\mathbf{M}(\mu_0)) = \inf_\sigma \text{disc}(\mathbf{M}_\sigma(\mu_0))$.

Note that the construction ensuring that once a secret state is visited, the run
remains in a secret state forever, extends naturally from OMC to OMDP. We only
consider OMDP of this form in the rest of this chapter.

**Example 7.5.** Consider the OMDP of Figure 7.5. As soon as the strategy selects action *a*, the system enters a secret state and discloses the secret with probability 1. Therefore $\text{Disc}_{\max}(\mathbf{M}(\mu_0)) = 1$. If the strategy only selects action *b* however, observing a ‘$o_1$’ clearly shows the system is in $q_1$, thus disclosing the secret, while after observing at least two ‘$o_2$’, the belief is $\{q_0, q_2\}$ which does not disclose the secret. The probability to observe at some point ‘$o_1$’ being equal to 1/2, $\text{Disc}_{\min}(\mathbf{M}(\mu_0)) = 1$.

We study the following problems for OMDP over finite or fixed horizon:

• **Computation problems.**

- The *value problem*: compute the disclosure;

- The *strategy problem*: compute an optimal strategy whenever it exists.

• **Quantitative decision problems.** Let $\bowtie = \ge$ for maximisation and $\bowtie = \le$ for minimisation.

- The *disclosure problem*: Given $\mathbf{M}$ and a threshold $\theta \in [0, 1]$, decide if $\text{disc}(\mathbf{M}) \bowtie \theta$;

- The *strategy decision problem*: decide if there exist a strategy $\sigma$ such that $\text{disc}(\mathbf{M}_{\sigma}) \bowtie \theta$.

• **Qualitative decision problems.**

- The *limit-sure disclosure problem*: the disclosure problem when $\theta = 1$ for maximisation and $\theta = 0$ for minimisation;

- The *almost-sure disclosure problem*: the strategy decision problem when $\theta = 1$ for maximisation and $\theta = 0$ for minimisation.

For the complexity results regarding a fixed horizon *n*, we assume that *n* is written
in unary representation or bounded by a polynomial in the size of the model where
the polynomial is independent of the model as done in classical studies (see for in-
stance [PT87]).
As said earlier, the whole power of the strategies we defined may not be necessary to answer the above problems. Restricting ourself to a subset of strategies that gives the same disclosure values can help simplify the proofs and the representation in practice of these strategies. Moreover, it helps understanding what is important in the control of an OMDP to optimise the disclosure. We thus show that for disclosure problems we can restrict strategies to observation-based ones.

**Proposition 7.1.** Given an OMDP, a secret and a strategy $\sigma$, there exists an observation-based strategy $\sigma'$ such that for $disc \in \{\text{Disc}, \text{Disc}_n, \text{Disc}_n^\varepsilon\}$, $disc(M_\sigma(\mu_0)) = disc(M_{\sigma'}(\mu_0))$.

For this proof, from an arbitrary strategy $\sigma$, we build an observation-based strategy $\sigma'$ with the same disclosure value. The strategy $\sigma'$ is randomised and is obtained by choosing, after an observed sequence $w$, a distribution on the different choices made by $\sigma$ on runs with observed sequence $w$. This is done so that the probability of choosing an action after observing $w$ is the same for both strategies.

We then prove that $\sigma'$ meets the same disclosure value as $\sigma$. More precisely, we establish that the probability to reach a state with a given observation is the same for both strategies. This is done by induction on the length of the observed sequence and on an ordering of the unobservable states. Two cases have to be considered, depending on if the last state is observable or not. However, each case is dealt with in the same way (both for the initialisation and for the induction step). Thus we only detail the first one.

*Proof.* Let $M = (S, \text{Act}, p, \mathbf{O})$ be an OMDP with initial distribution $\mu_0$, and let $\sigma$ be a strategy. For an observation $w \in \Sigma^*$ and a state $s \in S$, we define the sets (note that these are finite sets given the claim in Lemma 7.1) $R(w, s) = \{\rho \text{ finite run of } M_\sigma(\mu_0) | \mathbf{O}(\rho) = w \wedge \text{last}(\rho) = s\}$.

We now define a mapping $\hat{\sigma}$ from $\Sigma^* \times S$ to $\text{Dist}(\text{Act})$ by

$$ \hat{\sigma}(w, s) = \frac{1}{\sum_{\rho \in R(w, s)} \mathbb{P}_{\sigma}(\rho)} \sum_{\rho \in R(w, s)} \mathbb{P}_{\sigma}(\rho)\sigma(\rho). $$

$\hat{\sigma}(w, s)$ corresponds to the average choice made by $\sigma$ after a run with observed sequence $w$ and ending in $s$. Using $\hat{\sigma}$, we define the new strategy $\sigma'$ for a finite run $\rho$ by $\sigma'(\rho) = \hat{\sigma}(\mathbf{O}(\rho), \text{last}(\rho))$. We claim that $\mathbb{P}_{\sigma'}(R(w, s)) = \mathbb{P}_{\sigma}(R(w, s))$ for any observation $w$ and any state $s$, which entails equality of disclosure.

Partitioning the set of states into $S = S_o \uplus S_u$ where $S_u = \mathbf{O}^{-1}(\varepsilon)$, we can assume a topological sort on the subgraph obtained by removing all edges in $S \times S_o$ (this subgraph is acyclic due to the hypothesis of convergence). This means that there exists a numbering $\eta$ of the states so that if $\eta(s') > \eta(s)$, there is no transition from $s$ to $s'$. We proceed to prove the above claim by a joint induction on the pairs $(w, s)$ using $|w|$ and $\eta(s)$.

For the base cases, we need to establish the property for $w = \varepsilon$ with $s \in S_u$, and for $w \in \Sigma$ with $s \in S_o$, where $\mu_0(s) > 0$ in both cases.
**Case 1.** By induction on $\eta(s)$, we consider a state $s \in S_u$ such that $\eta(s) = \min_{s' \in S_u}(\eta(s'))$. Then $\mathbb{P}_{\sigma'}(R(\varepsilon, s)) = \mu_0(s) = \mathbb{P}_{\sigma}(R(\varepsilon, s))$. Assuming the property holds for $(\varepsilon, s)$ with $\eta(s) \le n$, we prove it for $s'$ with $\eta(s') = n + 1$. We have:

$$ \mathbb{P}_{\sigma'}(R(\varepsilon, s')) = \mu_0(s') + \sum_{s \in S_u, \eta(s) < \eta(s')} \sum_{a \in A(s)} p(s'|s, a) \sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma'}(\rho)\sigma'(\rho)(a) $$

and using the definition of $\sigma'$ yields:

$$ \begin{aligned} \mathbb{P}_{\sigma'}(R(\varepsilon, s')) &= \mu_0(s') + \sum_{s \in S_u, \eta(s) < \eta(s')} \sum_{a \in A(s)} p(s'|s, a) \hat{\sigma}(\varepsilon, s)(a) \sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma'}(\rho) \\ &= \mu_0(s') + \sum_{s \in S_u, \eta(s) < \eta(s')} \sum_{a \in A(s)} p(s'|s, a) \frac{\sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma}(\rho)\sigma(\rho)(a)}{\sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma}(\rho)} \sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma'}(\rho). \end{aligned} $$

Applying the induction hypothesis on $(\varepsilon, s)$ yields $\sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma'}(\rho) = \mathbb{P}_{\sigma'}(R(\varepsilon, s)) = \mathbb{P}_{\sigma}(R(\varepsilon, s)) = \sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma}(\rho)$ thus:

$$ \mathbb{P}_{\sigma'}(R(\varepsilon, s')) = \mu_0(s') + \sum_{s \in S_u, \eta(s) < \eta(s')} \sum_{a \in A(s)} p(s'|s, a) \sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma}(\rho)\sigma(\rho)(a) = \mathbb{P}_{\sigma}(R(\varepsilon, s')). $$

**Case 2.** We now consider $w = o \in \Sigma$ and $s' \in S_o$, hence $O(s') = o$. Then:

$$ \mathbb{P}_{\sigma'}(R(o, s')) = \mu_0(s') + \sum_{s \in S_u} \sum_{a \in A(s)} p(s'|s, a) \sum_{\rho \in R(\varepsilon, s)} \mathbb{P}_{\sigma'}(\rho)\sigma'(\rho)(a) $$

and a reasoning similar as above yields the result.

For the induction step, we first need to prove the property for $(w, s')$ with $s' \in S_u$, assuming it holds for all $(w, s)$ with $s \in S_o$ and for all $(w, s)$ with $s \in S_u$ and $\eta(s) < \eta(s')$. Then we have:

$$ \mathbb{P}_{\sigma'}(R(w, s')) = \sum_{s \in S_o} \sum_{s \in S_u, \eta(s) < \eta(s')} p(s'|s, a) \sum_{\rho \in R(w, s)} \mathbb{P}_{\sigma'}(\rho)\sigma'(\rho)(a) $$

and we can conclude along the same lines as above.

Finally, we consider $(w', s')$ with $w' = wo \in \Sigma^*\Sigma_o$ and $s \in S_o$, with:

$$ \mathbb{P}_{\sigma'}(R(w', s')) = \sum_{s \in S} \sum_{a \in A(s)} p(s'|s, a) \sum_{\rho \in R(w, s)} \mathbb{P}_{\sigma'}(\rho)\sigma'(\rho)(a) $$

which again implies the desired result. □