As seen in the previous proof, erasing observations leads to technical and cum-
bersome developments. In order to avoid them in the design of procedures for the
finite-horizon case, we apply the preliminary transformation that ensures the observa-
tion is non-erasing described in the next proposition. We precisely state the size of the
obtained OMDP in view of complexity results.

**Proposition 7.2.** *Given an OMDP M = (S, Act, p, O), an initial distribution µ₀ and a secret Sec, one can build in exponential time an OMDP M' = (S', Act', p', O'), an initial distribution µ'₀ and a secret Sec' where O' is non-erasing and for disc ∈ {Disc<sub>min</sub>, Disc<sub>max</sub>} disc(M(µ₀)) = disc(M'(µ'₀)). In addition, the size of S', p' and µ'₀ is polynomial w.r.t. the ones of S, p and µ₀. The size of Act' is polynomial w.r.t. the size of Act and exponential w.r.t. the size of S.*

The main idea of the construction is that every time a run visits an observable state, an observation-based strategy can fix a set of action for the current state and for every unobservable state. It will then keep this choice until the run visits a new observable state. Once such a set of actions is fixed, one can easily compute the probability distribution to reach the next observable state. Unobservable states can thus be removed from the system. We also add a new state to deal with the possibility that an unobservable state had a positive probability in the initial distribution.

*Proof.* We first build the new OMDP and then explain the correspondence between strategies in both models, which induces the relationship between disclosures.

**Construction of the OMDP.** We start from OMDP $M = (S, Act, p, O)$ with $Act = \cup_{s \in S} A(s)$, observation alphabet $\Sigma$, and a set of secret states $Sec \subseteq S$. Choosing a fresh observation symbol $\sharp$ and a fresh state $s_\sharp$, we build an OMDP $M' = (S', Act', p', O')$ with set of states $S' = \{s_\sharp\} \cup (S \setminus O^{-1}(\varepsilon))$, and observation alphabet $\Sigma \cup \{\sharp\}$, where the initial distribution is $1_{s_\sharp}$. The observation function $O'$ is defined by $O'(s_\sharp) = \sharp$ and $O'(s) = O(s)$ otherwise. Note that all states have non-trivial observation. The set of actions of $M'$ is $Act' = DR$ where $DR$ is the set of vectors of deterministic decision rules $\vec{\delta}$ over $S$, i.e. such that $\vec{\delta}(s) \in A(s)$. The intuition of $DR$ is that the actions associated with the current state and any unobservable state by the strategy after an observation is fixed until the next observable state, so we can gather this set of action into a single action.

We now define the transition probabilities, starting by the transitions exiting $s_\sharp$. For a run $\rho = s_0 a_1 \dots a_n s_n$, we write $\pi(\rho) = \prod_{i=1}^n p(s_i|s_{i-1}, a_i)$ and $\text{first}(\rho) = s_0$. Given an observable state $s \in S$ and $\vec{\delta} \in \text{DR}$, the set $\hat{E}(s_\sharp, \vec{\delta}, s)$ contains the finite runs $\rho = s_0 a_1 s_1 \dots a_n s_n$ starting from some $s_0 \in \text{Supp}(\mu_0)$ and ending in $s_n = s$ such that $a_i = \vec{\delta}(s_{i-1})$ for all $i, 1 \le i \le n$ and all states $s_0, \dots, s_{n-1}$ are unobservable. Observe that the intermediary states are all distinct due to the convergence of the OMDP. We set $p'(s | s_\sharp, \vec{\delta}) = \sum_{\rho \in \hat{E}(s_\sharp, \vec{\delta}, s)} \mu_0(\text{first}(\rho))\pi(\rho)$. If $s \in \text{Supp}(\mu_0)$, the set $\hat{E}(s_\sharp, \vec{\delta}, s)$ contains the run reduced to $\rho = s$.

We turn to the transitions exiting the other states. It is easier as we do not need
to take the initial distribution into account. Given a state $s \neq s_\sharp$, an action $\vec{\delta} \in \text{DR}$
and an observable state $s'$, we consider the finite set $\hat{E}(s, \vec{\delta}, s')$ of signalling runs of
M $\rho = s_0 a_1 \dots a_n s_n$ starting in $s_0 = s$ and ending in $s_n = s'$ such that for each $i$, $1 < i \le n$, $a_i = \vec{\delta}(s_{i-1})$, and all intermediate states are unobservable. We set $p'(s'|s, \vec{\delta}) = \sum_{\rho \in \hat{E}(s, \vec{\delta}, s')} \pi(\rho)$. Note that $\hat{E}(s, \vec{\delta}, s')$ may include runs like $\rho = s \vec{\delta}(s)s'$.

In order to efficiently compute the transition function of some $\vec{\delta}$, one uses a topological sort of the unobservable states thanks to the convergence hypothesis, and then compute the probability from observable states to reach first the unobservable states topologically sorted and then the observable states. This gives a polynomial time computation of the transition function of $\vec{\delta}$. Thus, the size of $S'$, $p'$ and $\mu'_0$ is polynomial w.r.t. the ones of $S$, $p$ and $\mu_0$. Moreover, the size of $\text{Act}'$ is polynomial w.r.t. the size of $\text{Act}$ and exponential w.r.t. the size of $S$.

**Correspondence between strategies.** The above construction ensures that any run $\rho' = s_1 \vec{\delta}_1 s_1 \dots \vec{\delta}_k s_k$ of $M'$ corresponds to the set of runs $\rho = \rho_1 s_1, \dots, \rho_k s_k$ of $M$ containing the sequence $s_1 \dots s_k$ of observable states, with $\rho_1 \in \hat{E}(s_1, \vec{\delta}_1, s_1)$ and $\rho_i \in \hat{E}(s_{i-1}, \vec{\delta}_i, s_i)$ for $1 < i \le k$. All runs in the set have the same observation $w = O(s_1) \dots O(s_k)$ with $O'(\rho') = \#w$.

To show that disclosure over finite horizon is the same in both OMDP, we establish correspondences between the strategies of $M$ and $M'$ and the associated disclosure value. From Proposition 7.1, we can restrict to observation-based strategies.

* Let $\sigma'$ be an observation-based strategy of $M'$, defined on $\#\Sigma^* \times S'$. Given an observation $w \in \Sigma^*$ there exists $\vec{\delta}$ such that for every state $s \in S'$, we have $\sigma'(\#w, s) = \vec{\delta}$. We define $\sigma(w, s) = \vec{\delta}(s)$. Then, writing $\mathbb{P}_\sigma$ (resp. $\mathbb{P}_{\sigma'}$) instead of $\mathbb{P}_{M_\sigma(\mu_0)}$ (resp. $\mathbb{P}_{M'_{\sigma'}(\mu'_0)}$), and defining for $w \in \Sigma^*$ and $s \in S \setminus \mathcal{O}^{-1}(\varepsilon)$, $R(w, s) = \{\rho \in \mathbb{SR}^{M_\sigma(\mu_0)} \mid \mathcal{O}(\rho) = w \wedge \text{last}(\rho) = s\}$ and $R'(w, s) = \{\rho' \in \mathbb{SR}^{M'_{\sigma'}(\mu'_0)} \mid \mathcal{O}(\rho') = \#w \wedge \text{last}(\rho') = s\}$, we have $\mathbb{P}_\sigma(R(w, s)) = \mathbb{P}_{\sigma'}(R'(w, s))$.

* Conversely, given an observation-based strategy $\sigma$ of $M$, we build an observation-based strategy $\sigma'$ of $M'$ as follows: Given $w \in \Sigma^*$, we define the mapping $\sigma'(\#w) : S \to \text{Dist}(\text{DR})$ by $\sigma'(\#w)(s) = \sigma(w, s)$ for any $s \in S$. Then, using the same notations as above, we have $\mathbb{P}_\sigma(R(w, s)) = \mathbb{P}_{\sigma'}(R'(w, s))$.

Therefore, defining the set of secret states of $S'$ by $\text{Sec}' = \text{Sec} \cap S'$, as the set of secret states is absorbing, the disclosures over finite horizon are equal for $\sigma$ and $\sigma'$. $\square$

Thus for finite horizon, one can restrict oneself to non-erasing observation functions with some care on the complexity of the actions. Also, on fixed horizon, we assume the observation function is non-erasing. Thus in both cases we are able to use this assumption.

## 2 Maximisation with finite horizon

We start the study of the disclosure problem with the maximisation objective over finite horizon. In other words, here the strategy tries to maximise the disclosure of the secret after an arbitrarily long, yet finite, amount of time.

In Subsection 2.1, we show how to restrict the study to deterministic strategies without loss of generalities. We show that most of the notions are unfortunately un-
decidable in Subsection 2.2, and prove the decidability of the almost-sure disclosure in Subsection 2.3.

## 2.1 Deterministic strategies are sufficient

We showed in Proposition 7.1 that one can limit oneself to observation-based strategies. In fact, for maximisation problems, one can do even better. Indeed, the additional power given by randomisation is not useful and thus observation-based deterministic strategies are sufficient.

**Proposition 7.3.** Given an OMDP M, a secret Sec and a disclosure notion disc $\in \{\text{Disc}, \text{Disc}_n, \text{Disc}_n^\varepsilon\}$, for any observation-based strategy $\sigma$ there exists a deterministic observation-based strategy $\sigma'$ such that $\text{disc}(M_\sigma(\mu_0)) \le \text{disc}(M_{\sigma'}(\mu_0))$.

This proof strongly uses Lemma 1 of [CDGH10] (or alternatively [GS14]) which establishes, in an active stochastic setting, that deterministic strategies are sufficient to optimise an objective defined by a set of infinite runs. This Lemma does not directly give the result we want as, contrary to the objectives used in their paper, the choice of the strategy modifies which runs are disclosing. However, as a disclosing run for a randomised strategy is also a disclosing run for a deterministic strategy that does not introduce new runs, we can use parts of their proof to show our result.

*Proof.* In the proof of Lemma 1 of [CDGH10], the authors show that a randomised observation-based strategy can be seen as a convex combination of a family of deterministic observation-based strategy. As a consequence, in our framework, given an observation-based strategy $\sigma$ and a disclosure notion disc, there exists an observation-based deterministic strategy $\sigma_{det}$ such that for every finite run $\rho$, $\text{Supp}(\sigma_{det}(\rho)) \subseteq \text{Supp}(\sigma(\rho))$ and $\mathbb{P}_{M_{\sigma_{det}}(\mu_0)}(\mathcal{V}_{\sigma}(\mu_0)) \ge \mathbb{P}_{M_{\sigma}(\mu_0)}(\mathcal{V}_{\sigma}(\mu_0))$.

The second property is not enough to conclude, as a disclosing run under $\sigma$ is not necessarily a disclosing run under $\sigma'$. However, thanks to the first property we can obtain that $\mathcal{V}_{\sigma}(\mu_0) \cap \Omega^{M_{\sigma_{det}}(\mu_0)} \subseteq \mathcal{V}_{\sigma_{det}}(\mu_0)$. Indeed, as $\sigma$ is more permissive than $\sigma_{det}$, $\Omega M_{\sigma_{det}}(\mu_0) \subseteq \Omega M_{\sigma}(\mu_0)$. This implies that, given a run $\rho$, if $O(\rho)$ discloses the secret with the strategy $\sigma$ then either $O(\rho)$ discloses the secret with the strategy $\sigma_{det}$ or $O(\rho)$ cannot be observed with $\sigma_{det}$.

This implies: $\mathbb{P}_{\sigma_{det}}(\mathcal{V}_{\sigma}(\mu_0)) = \mathbb{P}_{\sigma_{det}}(\mathcal{V}_{\sigma}(\mu_0) \cap \Omega^{M_{\sigma_{det}}(\mu_0)}) \le \mathbb{P}_{\sigma_{det}(\mu_0)}(\mathcal{V}_{\sigma_{det}}(\mu_0))$.

Therefore, $\text{disc}(M_{\sigma_{det}}(\mu_0)) = \mathbb{P}_{\sigma_{det}}(\mathcal{V}_{\sigma_{det}}(\mu_0)) \ge \mathbb{P}_{\sigma_{det}}(\mathcal{V}_{\sigma}(\mu_0)) \ge \mathbb{P}_{\sigma}(\mathcal{V}_{\sigma}(\mu_0))$ and the result holds since $\mathbb{P}_{\sigma}(\mathcal{V}_{\sigma}(\mu_0)) = \text{disc}(M_{\sigma}(\mu_0))$. $\square$

Observe that this proof shows that the restriction to deterministic strategy does not decrease the disclosure. However, it does not necessarily keep the same disclosure as before contrary to the proof used to restrict to observation-based strategies. Therefore it cannot be applied for minimisation problems.
## 2.2 Undecidability of the disclosure and limit-sure disclosure problems

As mentioned in the previous proof, one of the difficulties of opacity is that the set of disclosing runs depends on the strategy: a transition can be completely blocked by some strategy, modifying the set of disclosing observations. This was illustrated in Figure 7.5, where choosing action *a* in state *q*₀ removes the edge to *q*₀. This situation was excluded in the computation of the disclosure presented in [BKMS16, BKMS18] where the authors study a restricted form of Interval Markov Chains [JL91]. The disclosure problem for the general class of OMDP was left open. We answer negatively to the general problem by proving undecidability of the disclosure problem, hence the disclosure cannot be computed in general. Undecidability also holds for limit-sure disclosure.

Writing $\mathbb{I}$ for the set of intervals in $[0, 1]$, an interval Markov chain (IMC) over an alphabet $\Sigma$ is a tuple $\mathbf{M} = (S, s_{init}, I, \mathcal{O})$ where $S$ is the set of states, $s_{init}$ is the initial state, $I: S \to \mathbb{I}^S$ associates with every state $s \in S$ a mapping from $S$ to $\mathbb{I}$, and $\mathcal{O}: S \to \Sigma \cup \{\varepsilon\}$ is the observation function. We abuse notations by writing $\mu \in I(s)$ to denote any distribution $\mu: S \to [0, 1]$ such that for all $s' \in S$, $\mu(s') \in I(s' | s)$. The notion of run $\rho$ is the same as for an OMC but a transition from $s = \text{last}(\rho)$ to some successor requires the choice of a distribution $\mu \in I(s)$. A strategy of IMC $\mathbf{M}$ is thus a mapping $\sigma$ associating with each finite run $\rho$ with $s = \text{last}(\rho)$ a distribution $\sigma(\rho) \in I(s)$. In other words, an IMC is a OMDP where the chosen action represents a set of probabilities satisfying the interval conditions set by $I$ and summing to 1. In fact, an IMC can be transformed into an (exponentially larger) OMDP where actions are the basic feasible solutions of the linear program specified by the constraints associated with intervals [SVA06, CSH08]. Thus undecidability results for IMC also hold for OMDP.

**Example 7.6.** Consider the IMC of Figure 7.7. From the initial state, the strategy must attach a probability $p_1 \in [0, \frac{1}{2}]$ to the transition to $s_1$ and a probability $p_2 \in [\frac{1}{4}, 1]$ to the transition to $s_2$. As, in order to obtain a distribution, we require that $p_1 + p_2 = 1$, $p_2$ is de facto restricted to the interval $[\frac{1}{2}, 1]$. If $p_1 = \frac{1}{4}$ is selected, then $p_2 = \frac{3}{4}$ and the run has a probability $p_1$ to move to $s_1$ and $p_2$ to move to $s_2$. In these two states, the only exiting transition is labelled by the interval $\{1\}$ which we simplified by removing the braces in the figure. Thus, the run then loops indefinitely on the state.

<figure><img src="image_92.png" /><figcaption>Figure 7.7: Example of IMC.</figcaption></figure>

**Theorem 7.2.** The maximal finite-horizon disclosure problem is undecidable for OMDP, even when the secret is reached with probability 1 and for a non-erasing observation function.
The maximal finite-horizon disclosure problem when restricted to finite-memory strategies is undecidable (even with the same additional assumptions).

Starting from a PA $A$, we build an IMC $M_A = (S, s_0, I, \mathcal{O})$ such that there exists a word $w \in \{a,b\}^*$ with $\mathbb{P}_A^F(w) > \frac{1}{2}$ if and only if $\text{Disc}_{\max}(M_A) > \frac{1}{4}$. The proof of Theorem 7.2 is more involved than the proof of Theorem 7.1 because the strategies must be taken into account. The goal is to have the strategy choose a single word then "plays" it in the IMC and the probability to disclose the secret is half of the probability of the selected word. However, just with this, nothing would prevent the strategy to switch words during the run if it realises that the current run will not disclose the secret. We add a second component that ensures that if the strategy deviated from the single selected word the current run will not disclose the secret. Doing so, the strategy loses the advantage of knowing the current state of the run.

*Proof.* We first give the construction in two steps. The first step is very similar to what was done in the proof of Theorem 7.1. Starting from a PA $A = (Q, q_0, \{a,b\}, T, F)$ that is supposed complete, we build an IMC $\hat{A} = (\hat{Q}, q_0, \hat{I}, \hat{\mathcal{O}})$ where $\Sigma = \{a,b\}$ is the observation alphabet. The set of states is $\hat{Q} = Q \cup \{q_c \mid q \in Q \wedge c \in \{a,b\}\}$, with initial state $q_0$. The observation function $\hat{\mathcal{O}}$ is defined by $\hat{\mathcal{O}}(q) = \varepsilon$ and $\hat{\mathcal{O}}(q_c) = c$ for $q \in Q$ and $c \in \{a,b\}$. The interval mapping $\hat{I}: \hat{Q} \to \mathbb{I}^{\hat{Q}}$ is defined for $q, q' \in Q$ and $c \in \{a,b\}$ by:

* $\hat{I}(q' \mid q_c) = T(q' \mid q, c)$ is a point interval;

* $\hat{I}(q_c \mid q) = [0, 1]$.

Compared to the illustration given in Figure 7.3, this construction amounts to replacing all $b$ by $\varepsilon$ (making the states non observable) and the probabilities $\frac{1}{4}$ from original states to new ones by the interval $[0, 1]$.

However, the construction of the complete IMC $M_A = (S, s_0, I, \mathcal{O})$ from $A$ is more involved and requires to add a supplementary gadget limiting the power of the strategy. This is why we first use an observation function which can erase states and explain at the end how to relax this hypothesis. The construction is illustrated in Figure 7.8 with some conventions to avoid too many edges, a final state from $A$ (e.g. like $q_f$) is doubly circled.

* $S = \{s_0, s_1, q_{\#}^1, q_{\#}^2, q_b, q_s\} \cup \hat{Q} \cup \{s_c \mid c \in \{a, b, \#\}\} \cup \{r_c \mid c \in \{a, b, \# , b\}\}$;

* $I(s_1 \mid s_0) = I(q_0 \mid s_0) = \frac{1}{2}$ and the restriction of $I$ to $\hat{Q}$ is $\hat{I}$. For all $c \in \{1, a, b, \#\}$, $c' \in \{a, b, \#\}$, $I(s_{c'} \mid s_c) = \frac{1}{6}$ and $I(r_{c'} \mid s_c) = [0, \frac{1}{4}]$, for all $c, c' \in \{a, b, \# , b\}$, $I(r_{c'} \mid r_c) = \frac{1}{5}$ and $I(q_s \mid r_c) = \frac{1}{5}$. For all $q \in Q \setminus F$, $I(q_{\#}^1 \mid q) = [0, 1]$, for all $q \in F$, $I(q_{\#}^2 \mid q) = [0, 1]$, and $I(q_s \mid q_{\#}^1) = I(q_b \mid q_{\#}^2) = I(q_s \mid q_b) = I(q_s \mid q_s) = 1$.

* $\mathcal{O}$ extends $\hat{\mathcal{O}}$ by: $\mathcal{O}(s_0) = \mathcal{O}(s_1) = \varepsilon$, $\mathcal{O}(q_{\#}^1) = \mathcal{O}(q_{\#}^2) = \mathcal{O}(q_s) = \#$, $\mathcal{O}(q_b) = b$, for all $c \in \{a, b, \# , b\}$, $\mathcal{O}(r_c) = c$, and for all $c \in \{a, b, \#\}$, $\mathcal{O}(s_c) = c$.
<figure><img src="image_93.png" /><figcaption>Figure 7.8: Reduction from the strict emptiness problem of PA to the maximal finite-horizon disclosure problem. An edge outgoing from a dotted box should be duplicated to originate from all states in the box and an edge entering a dotted box from a state s should be duplicated from s to any state in the box. Hence a loop on a dotted box represents a complete graph inside the box (including self-loops).</figcaption></figure>

Informally, for $\text{Sec} = \{q_s\}$, the upper gadget ensures that for any strategy $\sigma$ there is at most one word $w \in \{a, b\}^*$ such that the observation $w^\sharp b^\sharp$ discloses the secret. The lower gadget allows one to generate secret runs of observation $w^\sharp b^\sharp$ with half the probability as the one assigned by the PA to $w$.

We now formally prove that there exists a word $w \in \{a, b\}^*$ with $\mathbb{P}_A^F(w) > \frac{1}{2}$ if and only if $\text{Disc}_{\max}(M_A) > \frac{1}{4}$.

First suppose there exists a word $w = a_1 \dots a_n \in \{a, b\}^*$ accepted with probability greater than $\frac{1}{2}$ in $A$. We define the strategy $\sigma$ for a finite run $\rho$ in both parts of $M_A$ (when relevant) as follows:

* In the upper part, assume that $\rho$ ends in a state $s_c$ with $c \in \{1, a, b, \sharp\}$. If there exists $i < n$ such that $O(\rho) = a_1 \dots a_i$ then $\sigma(\rho)(r_{a_{i+1}}) = 0$, leaving no choice for the rest of the distribution: In order for the sum of probabilities to be equal to 1 we have for $b \neq a_{i+1}$, $\sigma(\rho)(r_b) = \frac{1}{4}$. If $O(\rho) = w$, then $\sigma(\rho)(r_\sharp) = 0$, which also
leaves no choice for the rest of the distribution.

* In the bottom part, we can assume that $\rho$ ends in a state $q \in Q$. If there exists $i < n$ such that $O(\rho) = a_1 \dots a_i$ then $\sigma(\rho)(q_{a_{i+1}}) = 1$. Finally, if $O(\rho) = w$ then $\sigma(\rho)(q_{\mathfrak{h}}^2) = 1$ if $q \in F$, and $\sigma(\rho)(q_{\mathfrak{h}}^1) = 1$ otherwise.

At the beginning the system will move with probability $\frac{1}{2}$ to $\hat{A}$, where the strategy ensures that the word $w\mathfrak{h}$ is observed. This leads to the state $q_{\mathfrak{h}}^1$ with probability $\frac{1}{2}\mathbb{P}_A^F(w)$ and thus the next observations belong to $\mathfrak{b}\mathfrak{h}^*$ and the runs with observations in $w\mathfrak{h}\mathfrak{b}\mathfrak{h}^+$ belong to the secret. On the other hand, the system can also go to $s_1$ with probability $\frac{1}{2}$ from where, due to the decisions of the strategy, a run with observation $w\mathfrak{h}$ ends in $s_{\mathfrak{h}}$ (the decisions of the strategy ensure that either the run does not have observation $w\mathfrak{h}$, or it could not go in a $r$ state). Moreover, from $s_{\mathfrak{h}}$, $\mathfrak{b}$ cannot be observed. This implies that $w\mathfrak{h}\mathfrak{b}\mathfrak{h}$ is a min-disclosing observation in $M_{A,\sigma}$, hence $\text{Disc}(M_{A,\sigma}) \ge \frac{1}{2}\mathbb{P}_A^F(w) > \frac{1}{4}$. Since $\text{Disc}_{\text{max}}(M_A) = \sup_{\sigma} \text{Disc}(M_{A,\sigma})$, we can conclude that $\text{Disc}_{\text{max}}(M_A) > \frac{1}{4}$.

Conversely, suppose that the disclosure is strictly greater than $\frac{1}{4}$ and let $\sigma$ be a strategy such that $\text{Disc}(M_{A,\sigma}) > \frac{1}{4}$. Then, $\sigma$ must forbid states in $\{r_c \mid c \in \{a, b, \mathfrak{h}\}\}$, otherwise there would be no disclosing observation since every observation can be simulated once a state $r_c$ is reached. Writing $\bar{\Sigma} = \{a, b, \mathfrak{h}\}$, we inductively define the word $\bar{w} \in \bar{\Sigma}^{\infty} \cup \bar{\Sigma}^*$ by a sequence $(\bar{w}_i)_{i \ge 0}$ of non-decreasing prefixes of $\bar{w}$:

* We start with $\bar{w}_0 = \varepsilon$;

* Assume $\bar{w}_i$ is built and let $\rho_i$ be a run ending in state $s_x$ for some $x \in \{1, a, b, \mathfrak{h}\}$, with $O(\rho_i) = \bar{w}_i$. If $\sigma(\rho_i)(r_c) = 0$ for some $c \in \{a, b, \mathfrak{h}\}$, then $\bar{w}_{i+1} = \bar{w}_i c$, otherwise $\bar{w}_{i+1} = \bar{w}_i$.

The set of ambiguous observations (i.e. corresponding to both secret and non-secret runs) are the ones reaching the set of states $\{r_c \mid c \in \{a, b, \mathfrak{h}, \mathfrak{b}\}\}$:

$$ \bigcup_{\substack{\bar{w}_i x \neq \bar{w}_{i+1} \\ x \neq \mathfrak{b}}} \overline{\bar{w}_i x (\bar{\Sigma} \cup \{\mathfrak{b}\})}^{*\mathfrak{h}^\omega}. $$

Hence, the set of disclosing observations is reduced to either $w\mathfrak{h}\mathfrak{b}\mathfrak{h}^\omega$, where $w$ is the largest prefix of $\bar{w}$ in $\{a, b\}^*$ if $\mathfrak{h}$ occurs in $\bar{w}$, and empty otherwise. Since the disclosure is greater than 0, we obtain $w\mathfrak{h}\mathfrak{b}\mathfrak{h}$ as the single min-disclosing observation with $\text{Disc}(M_{A,\sigma}) = \mathbb{P}_{M_{A,\sigma}}(w\mathfrak{h}\mathfrak{b}\mathfrak{h})$. Since $\mathbb{P}_A^F(w) \ge 2.\mathbb{P}_{M_{A,\sigma}}(w\mathfrak{h}\mathfrak{b}\mathfrak{h})$, we can conclude that $\mathbb{P}_A^F(w) > \frac{1}{2}$.

The proof can be extended with a non-erasing observation function by replacing $\varepsilon$ with a fresh symbol (like in the proof of Theorem 7.1). This requires to slightly modify the parts of the IMC corresponding to the sets of states $\{s_c \mid c \in \{a, b, \mathfrak{h}\}\}$ and $\{r_c \mid c \in \{a, b, \mathfrak{h}\}\}$ in order to ensure alternation of letters from $\{a, b\}$ and this new symbol.

The undecidability result holds even when restricted to finite-memory strategy as the strategy defined in the first direction of the proof only uses finite memory. $\square$
If we could compute the maximal finite-horizon disclosure, we could solve the asso-
ciated decision problem. Thus, as a consequence of the previous theorem, we obtain:

**Corollary 7.1.** *The maximal finite-horizon disclosure of an OMDP cannot be computed.*

We now turn to the qualitative disclosure problems, and using a reduction from the
value 1 problem in PA, we also have:

**Theorem 7.3.** *The maximal finite-horizon limit-sure disclosure problem is undecidable for OMDP.*

*Proof.* The reduction from the value 1 problem for PA done here is similar to the one of the proof of Theorem 7.2. The difference is that any run initially moving from $s_0$ to $s_1$ (thus moving to the part of the IMC which was used to limit the power of the strategy) will now almost-surely disclose the secret. More precisely, the construction of $M_A$ depicted in Figure 7.8 for the proof of Theorem 7.2 is slightly modified as follows (see Figure 7.9): a new state $q_\#$ with $O(q_\#) = \#A$ is added in the upper part just before reaching the secret state $q_s$. In this case, the runs reaching the secret in the upper part disclose the secret as they end with $\#A^\omega$.

The disclosure on the bottom part is performed as before. As a consequence, if a word $w$ is "selected" by the strategy, the finite-horizon disclosure will be equal to $1/2 \cdot (1 + \mathbb{P}_A^F(w))$. This value can be arbitrarily close to 1 iff $A$ accepts words with probabilities arbitrarily close to 1, which yields the result. $\square$

<figure><img src="image_94.png" /><figcaption>Figure 7.9: Modification of Figure 7.8 for limit disclosure.</figcaption></figure>

**2.3 Decidability of the almost-sure disclosure problem**

Fortunately the maximal finite-horizon almost-sure disclosure problem is decidable. The proof relies on results for partially observable MDP (POMDP) described in Definition 6.8, page 186.

**Theorem 7.4.** *The maximal finite-horizon almost-sure disclosure problem in OMDP is EXPTIME-complete. Moreover, if the system is almost-surely disclosing, one can build a belief-based strategy with disclosure 1.*

We reduce the almost-sure disclosure problem for maximisation in OMDP to almost-
sure reachability in POMDP. The POMDP we build is exponential in the size of the
original OMDP and the algorithm to solve almost-sure reachability is exponential in the size of the POMDP [CDH10]. A naive application of the two successive results would give a 2-EXPTIME algorithm. However, a finer analysis yields EXPTIME complexity of our algorithm as these two exponentials do not stack. The hardness is obtained by a reduction from the safety problem in games with imperfect information that was shown to be EXPTIME-complete in [BD08]. The reduction for the lower bound is similar to the one of Theorem 7.2.

*Proof.* We start by giving the construction of the POMDP, then we show that solving almost-sure reachability in the POMDP is equivalent to the finite-horizon almost-sure disclosure problem for maximisation. Finally we prove the hardness.

**Construction of the POMDP.** We start from an OMDP $M = (S, \text{Act}, p, O)$ with $\text{Act} = \cup_{s \in S} A(s)$, observation alphabet $\Sigma_o$, and a set of secret states $\text{Sec} \subseteq S$. Thanks to Proposition 7.2, we can assume $O$ to be non-erasing (the potentially exponential blow up of the number of actions does not affect the complexity result as we will see later). Let $\mu_0$ be an initial distribution. We assume w.l.o.g. that $\mu_0$ is a Dirac distribution on some state $s_0 \in S$. We build a POMDP $M' = (Q, q_0, \text{Obs}, \text{Act}, T)$ with set of states $Q = S \times 2^S$, with $q_0 = (s_0, \{s_0\})$ and observation alphabet $\Sigma_o$. The observation function $\text{Obs}$ is defined by $\text{Obs}((s, B)) = O(s)$. The set of actions of $M'$ is $\text{Act}' = \text{DR}$ where $\text{DR}$ is the set of vectors of deterministic decision rules $\vec{\delta}$ over $S$. Given a state $(s, B) \in S'$, an action $\vec{\delta} \in \text{DR}$ and an observable state $s'$, we have

$$ T((s, B), \vec{\delta})(s', B') = \begin{cases} p(s'|s, \vec{\delta}(s)), & \text{for } B' = \{s'' \mid O(s'') = O(s') \wedge \\ & \quad \exists \hat{s} \in B, p(s''|\hat{s}, \vec{\delta}(\hat{s})) > 0\} \\ 0, & \text{otherwise.} \end{cases} $$

**Correspondence between strategies.** To show that $M$ is almost-surely disclosing for $\text{Sec}$ iff $\text{Sec} \times 2^{\text{Sec}}$ can almost-surely be reached in $M'$, we establish a correspondence between the strategies of $M$ and the scheduler of $M'$. From Proposition 7.3, we can restrict to deterministic observation-based strategies for $M$, and from [CDH10], we also restrict to deterministic schedulers for $M'$.

In both direction of the equivalence, given a strategy $\sigma$ and a scheduler $\tau$, we write $\mathbb{P}_{\sigma}$ (resp. $\mathbb{P}_{\tau}$) instead of $\mathbb{P}_{M_{\sigma}(\mu_0)}$ (resp. $\mathbb{P}_{M'(\tau)}$), and define, for $w \in \Sigma_o^*$ and $s \in S$, the sets of finite runs $R(w, s) = \{\rho \text{ finite run of } M_{\sigma}(\mu_0) \mid O(\rho) = w \wedge \text{last}(\rho) = s\}$ and $R'(w, s) = \{\rho' \text{ finite run of } M'(\tau) \mid O(\rho') = w \wedge \text{last}(\rho') = (s, B_w^{\sigma})\}$.

• Let $\tau$ be a scheduler of $M'$, defined on $\Sigma_o^*$. We define $\sigma$ for any observation $w \in \Sigma_o^*$ and state $s \in S$ by $\sigma(w, s) = \tau(w)(s, B_w^{\sigma})$. Note that a $\tau$-compatible run $\rho'$ of $M'$ ends in a state $(s, B)$ where $B = B_w^{\sigma}$ (the belief w.r.t. $\sigma$) if $O(\rho') = w$. We have $\mathbb{P}_{\sigma}(R(w, s)) = \mathbb{P}_{\tau}(R'(w, s))$.

Now let $\text{Reach}(\text{Sec} \times 2^{\text{Sec}})$ be the set of runs reaching $\text{Sec} \times 2^{\text{Sec}}$ in $M'(\tau)$. Then we claim that $\text{Disc}_{\text{max}}(M_{\sigma}(\mu_0)) = \mathbb{P}_{\tau}(\text{Reach}(\text{Sec} \times 2^{\text{Sec}}))$. Indeed, an observation $w$ discloses the secret under strategy $\sigma$ iff all observable states reachable with observed sequence $w$ belong to the secret, i.e. iff $B_w^{\sigma} \subseteq \text{Sec}$. Thus the runs $\rho'$ in $M'$ with a disclosing observation for $M$ are the ones for which $\text{last}(\rho') \in \text{Sec} \times 2^{\text{Sec}}$. Therefore,
thanks to the earlier remark, we have that the probability of reaching $Sec \times 2^{Sec}$ in $M'$ under strategy $\tau$ is also the probability of disclosing Sec in $M$ under strategy $\sigma$.

• Conversely, given an observation-based strategy $\sigma$ of $M$, we build a scheduler $\tau$ of $M'$ as follows: we define the mapping $\tau(w) : \Sigma_o^* \to \text{Dist}(\text{Act})$ by $\tau(w)(s, B_w^\sigma) = \sigma(w, s)$ for any $s \in S$. With the same reasoning as above, we immediately get that the probability of reaching $Sec \times 2^{Sec}$ in $M'$ under strategy $\tau$ is also the probability of disclosing Sec in $M$ under strategy $\sigma$.

We can conclude that $M$ is almost-surely disclosing if and only if the runs of $M'$ reach almost-surely the set $Sec \times 2^{Sec}$. Moreover, if $M'$ almost-surely reaches the set $Sec \times 2^{Sec}$, we can build a scheduler $\tau$ doing so. Using the transformation described above and the results from [CDH10], we extract from $\tau$ a belief-based strategy $\sigma$ of $M$ that almost-surely discloses the secret.

Let us argue that the whole algorithm is in **EXPTIME**. The exponential in the algorithm of [CDH10] comes from a determinisation of the system, which is already done in our transformation from $M$ to $M'$, and thus not required a second time. Moreover, the non-erasing assumption on the observation could have created exponentially many new actions, which are exactly the ones built by the use of a vector of decision rules in our construction. Thus the exponentials do not stack.

The hardness is shown with a reduction from safety games with imperfect information.

**Definition 7.8.** A safety game with imperfect information is defined by a tuple $\mathcal{G} = (L, \ell_0, \Sigma, \Delta, O, F, \text{obs})$ where

• $L$ is a finite set of locations with initial location $\ell_0 \in L$;

• $\Sigma$ is a finite alphabet;

• $\Delta \subseteq L \times \Sigma \times L$ is the transition relation such that for all $\ell \in L$ and $a \in \Sigma$ there exists at least one $\ell'$ with $(\ell, a, \ell') \in \Delta$;

• $O$ is a finite set of observations, and $F \subseteq O$ are the final observations;

• **obs**: $L \to O$ is the observation mapping.

A safety game with imperfect information $\mathcal{G}$ is a turn-based game played by two players Control and Environment. It starts in location $\ell_0$ with Control to play. In the first round, Control chooses a letter $a_0 \in \Sigma$, then Environment chooses a location $\ell_1$ such that $(\ell_0, a_0, \ell_1) \in \Delta$ and Control only observes $o_1 = \text{obs}(\ell_1)$. The next rounds are played similarly and Control wins if for all $i, o_i \notin F$. The problem of existence of a winning strategy for Control is EXPTIME-complete [BD08]. We now describe a reduction from this problem to the almost-sure disclosure problem of OMDP.

The reduction is similar to the one in the proof of Theorem 7.2 except that we replace the probabilistic automaton by a safety game $\mathcal{G} = (L, \ell_0, \Sigma, \Delta, O, F, \text{obs})$ with imperfect information and directly build an OMDP $M = (S, \text{Act}, p, O)$ over alphabet $(O \cup \{\# , b, \$\}) \cup \Sigma \times (O \cup \{\# , b\})$, with:
* $S = \{s_0, \ell_0, q_\#^1, q_\#^2, q_b, q_s^1, q_s^2\} \cup \{\ell_c \mid \ell \in L, c \in \Sigma \times O\} \cup \{s_c \mid c \in \Sigma \times (O \cup \{\#\})\} \cup \{r_c \mid c \in \Sigma \times (O \cup \{\#\}, b)\}$;

* $\text{Act} = \Sigma$;

* For all $a \in \Sigma, o \in O, \ell_c \in S, \ell' \in \text{obs}^{-1}(o), p(\ell'_{a,o} | \ell_c, a) > 0$ iff $(\ell, a, \ell') \in \Delta$. If $\ell \in \text{obs}^{-1}(F)$ then $p(q_\#^1 | \ell_c, a) > 0$ and if $\ell \notin \text{obs}^{-1}(F)$ then $p(q_\#^2 | \ell_c, a) > 0$. For all $a \in \Sigma, c \in \{0\} \cup (\Sigma \times (O \cup \{\#\})), (b', o') \in \Sigma \times (O \cup \{\#\}), p(s_{(b',o')}) |_{s_c, a}) > 0$ and if $b' \neq a, p(r_{(b',o')}) |_{s_c, a}) > 0$. For all $c, c' \in \Sigma \times (O \cup \{\#\}), p(r_{c'}) |_{r_c, a}) > 0$ and $p(q_s^2 | r_c, a) > 0$. For all $a, a' \in \Sigma, p(q_s^1 | q_\#^1, a) = p(q_b | q_\#^2, a) = p(q_s^1 | q_b, a) = p(q_s^1 | q_s^1, a) = p(q_s^2 | q_s^2, a) = 1$.

* $O(s_0) = O(\ell_0) = \text{obs}(\ell_0)$; For $z \in L, s, r, a \in \Sigma, o \in O, O(z_{a,o}) = (a, o)$; For $o \in \{\#\}, b\}, O(z_{a,o}) = o$, and $O(q_\#^1) = O(q_\#^2) = \# = O(q_s^1), O(q_b) = b, O(q_s^2) = \blacksquare$.

The initial distribution is $\mu_0(s_0) = 1/2 = \mu_0(\ell_0)$ and the secret is $\text{Sec} = \{q_s^1, q_s^2\}$.

This proof being similar to the one of Theorem 7.2, we only detail here the differences. A run starting in $s_0$ will almost surely trigger a $\blacksquare$ and disclose the secret. A run starting in $\ell_0$ will almost surely reach $q_s^1$ as after any action in the copy of $\mathcal{G}$ there is a positive probability to reach $q_\#^1$ or $q_\#^2$. In order for a finite run starting in $\ell_0$ to disclose the secret, it cannot go through $q_\#^1$ and should not share its observed sequence with a run ending in a state $r_c$. Given a strategy $\sigma$ of $M$, if there exists a $\sigma$-compatible run $\rho$ visiting a state $\ell_c$ with an observation $O(\ell_c) \in \Sigma \times F$, then there is a $\sigma$-compatible path $\rho'$ visiting $q_\#^1$, therefore a set of runs with positive probability do not visit the secret. Thus a deterministic strategy almost surely disclosing the secret in $M$ never visits a state triggering an observation of the form $\Sigma \times F$. Moreover such a strategy does not take the current state into account. Indeed, let $\rho$ and $\rho'$ be two runs such that $O(\rho) = O(\rho')$ and ending in two states $\ell_c$ and $s_c$. If $\sigma(\rho) = a$ and $\sigma(\rho') = a'$ are two actions in $\Sigma$ with $a \neq a'$ then there exists $o \in O$ such that $\rho a \ell_{a,o}$ is a $\sigma$-compatible run. Since $a \neq a'$, $\rho' a r_{a,o}$ is also a $\sigma$-compatible run with same observation than $\rho a \ell_{a,o}$. Hence no observation prefixed by $O(\rho a \ell_{a,o})$ would disclose the secret.

Therefore, similarly as in Theorem 7.2, Control has a winning strategy iff there exists a deterministic strategy considering only the observed sequence that almost-surely discloses the secret. This implies EXPTIME-hardness of the maximal finite-horizon almost-sure disclosure problem. $\square$

In this section on the maximisation of the disclosure over finite horizon, we saw that although we could restrict ourselves to deterministic strategies, most of the finite-horizon problems are very complicated (all but one are undecidable).

# 3 Minimisation with finite horizon

We now turn to minimisation over finite horizon where strategies try to hide the secret from an observer, and thus to minimise the disclosure.
This section shows a surprising result. Indeed, in Subsection 3.1 we show that for minimisation we cannot assume strategies to be deterministic any more, thus the problem seems more complex. However, the disclosure value can be computed as we establish in Subsection 3.2.

**3.1 Deterministic strategies are not enough**

After the proof of Proposition 7.3, we remarked that the proof showed that deterministic strategies do not decrease the disclosure, thus the proof could only work for maximisation. In fact, the result itself is limited to maximisation as randomisation may be necessary to minimise the disclosure. Let us see that on an example. Consider the OMDP depicted in Figure 7.10 with $\text{Sec} = \{q_2, q_3\}$. There are two deterministic strategies, choosing respectively $a$ or $b$ in $q_0$. In both cases, the disclosure is $\frac{1}{2}$. On the other hand, for randomized strategies $\sigma_p$ such that $\sigma_p(q_0) = pa + (1-p)b$ with $0 < p < 1$, there are no disclosing observations, hence the disclosure is 0.

<figure><img src="image_95.png" /><figcaption>Figure 7.10: With $\text{Sec} = \{q_2, q_3\}$, deterministic strategies are not sufficient for minimisation.</figcaption></figure>

While we cannot restrict ourselves to deterministic strategies, we still use in the decision procedures a restricted class of strategies. These strategies are called families of almost-deterministic strategies and are based on $\varepsilon$-decision rules.

**Definition 7.9.** Let $\delta$ be the deterministic decision rule for state $s$ selecting action $a \in A(s)$. Then, for $\varepsilon > 0$, the $\varepsilon$-decision rule $\delta_{\varepsilon} \in \text{Dist}(A(s))$ is defined by:

1. If $|A(s)| > 1$ then $\delta_{\varepsilon}(a) = 1 - \varepsilon$ and for all $b \in A(s) \setminus \{a\}$, $\delta_{\varepsilon}(b) = \frac{\varepsilon}{|A(s)|-1}$;

2. Else $\delta_{\varepsilon} = \mathbf{1}_a$.

$\delta_{\varepsilon}$ is said to favour $a$.

$\varepsilon$-decision rules are used to define approximations of deterministic strategies.

**Definition 7.10.** Let $\sigma$ be an observation-based deterministic strategy. Then $\{\sigma_{\varepsilon}\}_{\varepsilon>0}$ is a family of observation-based almost-deterministic strategies defined for any state $s$ and $w \in \Sigma^n$ by: $\sigma_{\varepsilon}(w, s) = \sigma(w, s)_{2^{-n_{\varepsilon}}}$.
In other words, given a strategy $\sigma$ we define a family of strategies that have an increasingly high probability to play like $\sigma$ as the run goes on, yet always allow the other actions with positive probability. We will see that strategies of this form are dominant in the sense that they are sufficient to compute the disclosure value. However, if there exists a strategy that minimises the disclosure, this strategy does not always belong to a family of almost-deterministic strategy.

## 3.2 The minimal disclosure value is computable

Using Proposition 7.2, we assume in the following that the observation function we consider is non-erasing. The complexity of the transformation does not affect the results since the polynomial complexity in the number of actions is dominated by the exponential complexity in the number of states.

In order to compute the minimal disclosure value, we build from an OMDP $M$, another OMDP $M_{min}$ which is a “correct abstraction” (as is stated by Proposition 7.4) for reducing minimal disclosure problems to minimal reachability problems. Intuitively, in $M_{min}$, the states are enlarged by the maximal belief that can occur independently of the action that has been selected.

Given a set of potential current states $B$ and a new observation $o$, we define the maximal set of potential next states $\text{NextMax}(B, o)$ over decision rules applied to $B$ by:

$$ \text{NextMax}(B, o) = \{s' \in \mathcal{O}^{-1}(o) \mid \exists s \in B \ \exists a \in A(s) \ p(s'|s, a) > 0\}. $$

$\text{NextMax}$ is intuitively the belief obtained with a strategy allocating some probabilities to every action. Observe that given a family of almost deterministic strategies $\{\sigma_{\epsilon}\}$ and a run $\rho_{as}$ of $M$ with $\mathcal{O}(s) = o$, one has for all $\epsilon > 0$, $B_{\rho_{as}}^{\sigma_{\epsilon}} = \text{NextMax}(B_{\rho}^{\sigma_{\epsilon}}, o)$. Then $M_{min}$ is formally defined as follows:

* $S_{min}$, the set of states, is defined by: $S_{min} = \{(s, B) \mid s \in B \subseteq \mathcal{O}^{-1}(\mathcal{O}(s))\}$;

* for every $(s, B) \in S_{min}$, $A(s, B) = A(s)$;

* for every $(s, B), (s', B') \in S_{min}$,

$$ p((s', B')|(s, B), a) = \begin{cases} p(s'|s, a) & \text{if } B' = \text{NextMax}(B, \mathcal{O}(s')), \\ 0 & \text{otherwise;} \end{cases} $$

* for every $(s, B) \in S_{min}$, $\mathcal{O}(s, B) = \mathcal{O}(s)$.

Given $\mu_0$ an initial distribution over $S$, the associated initial distribution $\mu_{min}$ over $S_{min}$ is defined by $\mu_{min}(s, \text{Supp}(\mu_0) \cap \mathcal{O}^{-1}(\mathcal{O}(s))) = \mu_0(s)$ and $\mu_{min}(s, B) = 0$ for all other $B$. We define the subset $\text{Avoid}(\text{Sec}) \subseteq S_{min}$ by $\text{Avoid}(\text{Sec}) = \{(s, B) | B \subseteq \text{Sec}\}$.

**Proposition 7.4.** The minimal disclosure value for $\text{Sec}$ in $M(\mu_0)$ is equal to the minimal probability to reach $\text{Avoid}(\text{Sec})$ in $M_{min}(\mu_{min})$. Furthermore it is asymptotically reached by a family of belief-based almost deterministic strategies.
We show this result in two steps. First we show that, using families of belief-based almost-deterministic strategies, one can obtain a disclosure value in $\mathbf{M}$ arbitrarily close to the minimal reachability probability in $\mathbf{M}_{\min}$. This ensures that the disclosure value is below this probability. Second, we show that the disclosure obtained by an arbitrary strategy is greater or equal to the probability to reach Avoid(Sec).

*Proof.* We know that the minimal reachability probability for Avoid(Sec) in $\mathbf{M}_{\min}(\mu_{\min})$ is obtained by a memoryless deterministic strategy $\sigma_{\min}$ that selects some action $a_{s,B}$ in state $(s, B)$ (see e.g. [BK08]). Consider $\{\sigma_{\varepsilon}\}$ the family of belief-based almost-deterministic strategies defined by favouring $a_{s,B}$ in state $s$ after a run $\rho$ such that $B_{\rho}^{\sigma_{\varepsilon}} = B$. Given a run $\rho = s_0a_0\dots a_{n-1}s_n$ in $\mathbf{M}(\mu_0)$ we inductively define the run $b(\rho) = (s_0, S_0)a_0\dots a_{n-1}(s_n, S_n)$ in $\mathbf{M}_{\min}(\mu_{\min})$ by: $S_0 = \text{Supp}(\mu_0) \cap \mathbf{O}^{-1}(\mathbf{O}(s_0))$ and $S_{i+1} = \text{NextMax}(S_i, \mathbf{O}(s_{i+1}))$. Due to the observation given when introducing NextMax, with strategy $\sigma_{\varepsilon}$, the observation of run $\rho$ discloses the secret iff $b(\rho)$ reaches Avoid(Sec). Consider, under strategy $\sigma_{\varepsilon}$, the probability to disclose the secret with runs $\rho$ such that $b(\rho)$ includes at least once an action not selected by $\sigma_{\min}$. By construction, at each step $i$, the probability of not choosing the action favoured by $\sigma_{\varepsilon}$ is $\frac{\varepsilon}{2^i}$, hence the probability of this set of runs is $\sum_{i \ge 0} (1 - \varepsilon)^i \frac{\varepsilon}{2^i} \le 2\varepsilon$. Consider now a finite run $s_0a_0\dots a_{n-1}s_n$ such that $b(\rho)$ is $\sigma_{\min}$-compatible. Then the probability of the original run is less than or equal to the probability of its corresponding run. So we deduce that the minimal disclosure value of $\mathbf{M}(\mu_0)$ is bounded above by $\nu + 2\varepsilon$ where $\nu$ is the minimal reachability probability for Avoid(Sec) in $\mathbf{M}_{\min}(\mu_{\min})$. Since this holds for all $\varepsilon > 0$, we obtain that the minimal disclosure value of $\mathbf{M}(\mu_0)$ is bounded above by the minimal reachability probability for Avoid(Sec) in $\mathbf{M}_{\min}(\mu_{\min})$.

Conversely consider an arbitrary strategy $\sigma$ in $\mathbf{M}(\mu_0)$. This strategy may also be applied in $\mathbf{M}_{\min}(\mu_{\min})$ by forgetting the second component of the state, defining a strategy $\sigma'$. For any run $s_0a_0\dots s_n$ in $\mathbf{M}_{\sigma}(\mu_0)$, there is a single run $(s_0, S_0)a_0\dots (s_n, S_n)$ in $\mathbf{M}_{\min}(\mu_{\min})$ under $\sigma'$ with the same probability. Given the run $s_0a_0\dots s_n$, consider the successive associated subsets of beliefs according to $\sigma, B_0, \dots, B_n$. By induction (and definition of $\mathbf{M}_{\min}$) it is straightforward to show that $B_i \subseteq S_i$. So $s_0a_0\dots s_n$ does not disclose the secret in $\mathbf{M}$ under $\sigma$ implies that $(s_0, S_0)\dots (s_n, S_n)$ does not reach Avoid(Sec). This entails that the reachability probability of Avoid(Sec) in $\mathbf{M}_{\min}(\mu_{\min})$ under $\sigma'$ is less than or equal to the disclosure probability in $\mathbf{M}(\mu_0)$ under $\sigma$. $\square$

Since minimal reachability probability in OMDP can be computed in polynomial time(see e.g. [BK08])<fnref n="4" /> we immediately obtain the first part of the next theorem. We establish the second part (PSPACE-hardness) in the proof of Theorem 7.8 as the proof holds also for disclosure over fixed-horizon.

**Theorem 7.5.** The minimal disclosure value of $\mathbf{M}(\mu_0)$ can be computed in EXPTIME. The associated decision problem is PSPACE-hard.

<footnote n="4">⁴Note that since observations are not useful for this reachability objective, observations could be removed from the OMDP $\mathbf{M}_{\min}$, yielding a Markov decision process, which is the model studied in [BK08].</footnote>
We now turn to the existence of a strategy that achieves the minimal value. As remarked earlier, we cannot assume such a strategy belongs to an almost-deterministic family of strategies. We establish that it can be analysed without additional complexity.

**Theorem 7.6.** *The existence of a strategy that achieves the minimal disclosure value can be decided in EXPTIME. In the positive case, this strategy can be computed in EXPTIME.*

The main ingredient of the proof is an elimination algorithm that removes iteratively the beliefs from which no strategy can reach the maximal disclosure. Once all these beliefs were removed, if the initial belief was not deleted, then there exists a belief-based strategy minimising the disclosure and this strategy plays in order to stay within the beliefs kept by the algorithm.

*Proof.* Let us first introduce multiple notations that are used within the proof. We define disc*(M(s, B)) as the minimal disclosure value when starting in M in state s with belief B. Given some belief B and some decision rule vector $\vec{\delta}$ over B we introduce the possible successors of B when applying $\vec{\delta}$: $\text{Next}(B, \vec{\delta}) = \{s' | \exists s \in B \exists a \in \text{Supp}(\vec{\delta}[s]) p(s'|s, a) > 0\}$ and $\text{Next}(B, \vec{\delta}, o) = \text{Next}(B, \vec{\delta}) \cap \mathbf{O}^{-1}(o)$.

The algorithm simultaneously solves the existence and the synthesis problem. First, using Proposition 7.4, the algorithm computes for all $(s, B) \in S_{\min}$, disc*(M(s, B)). Then it maintains a set Win of beliefs initially set to all beliefs from which it iteratively eliminates items and stops when no more elimination is possible. Given $B \in \text{Win}$, it looks for a decision rule vector $\vec{\delta}$ over B such that:

* for all $o \in \mathbf{O}(\text{Next}(B, \vec{\delta}))$, $\text{Next}(B, \vec{\delta}, o) \in \text{Win}$;

* for all $s \in B$, $\text{disc}^*(M(s, B)) = \sum_{o \in \Sigma} \sum_{s' \in \mathbf{O}^{-1}(o)} p(s'|s, \vec{\delta}[s])\text{disc}^*(M(s', \text{Next}(B, \vec{\delta}, o)))$.

If such a $\vec{\delta}$ does not exist then B is eliminated from Win. In other words, a belief is eliminated if there does not exist a decision rule that meets the minimal disclosure value. Each iteration can be performed in polynomial time w.r.t. $|S_{\min}|$ and the number of iterations is at most $|S_{\min}|$. Observe that when a belief is eliminated, it should not be “reached” by a strategy that obtains the minimal disclosure value. So the elimination is sound.

When the elimination stops, the algorithm answers positively iff for all $o \in \mathbf{O}(\text{Supp}(\mu_0))$, $\text{Supp}(\mu_0) \cap \mathbf{O}^{-1}(o) \in \text{Win}$. Thus, by the soundness of the elimination step, if the answer is negative there is no optimal strategy for minimal disclosure value.

If the answer is positive, let us consider the belief-based strategy $\sigma$ defined by applying the decision rules obtained during the last iteration of the algorithm. On the one hand, under $\sigma$ when visiting a state s with belief B such that $\text{disc}^*(M(s, B)) = 0$, one never leaves such kind of pairs of states and beliefs. So the secret is never disclosed, showing that the disclosure value obtained by $\sigma$ for such $(s, B)$ is null. Under $\sigma$, the disclosure value of all the other pairs of states and beliefs fulfil the equations of the elimination step. It is known that the single solution of this system is the vector of minimal reachability probabilities of Avoid in $M_{\min}(\mu_{\min})$ (see [BK08] for instance) which yields the result. $\square$
# 4 Fixed-horizon problems

We focus now on fixed-horizon problems for both maximal (Subsection 4.1) and minimal (Subsection 4.2) disclosure. In both cases, the algorithms and hardness results have similarities.

## 4.1 Maximal disclosure

In order to compute the value of the maximal disclosure within a fixed horizon, one could build the POMDP described in the proof of Theorem 7.4, then use pre-existing results on POMDPs. This would result in an EXPTIME algorithm, whereas we provide below an algorithm with a better complexity in PSPACE.

**Theorem 7.7.** The fixed-horizon maximal value (when the horizon *n* is described in unary representation) is computable in PSPACE and the fixed-horizon maximal disclosure problem is PSPACE-complete.

Due to the complexity of the proof, we separate the algorithm computing the value from the hardness of the decision problem in two separate proofs.

In order to compute the value, we first order the observation alphabet $\Sigma$. Then, a non-deterministic decision procedure operating in PSPACE enumerates every observed sequence of length *n* while maintaining the sets of states that were possible after every prefix of this observation, the actions that were chosen non-deterministically in these states and values used in the computation of the disclosure. The information kept is of polynomial size and when every observation has been read, one of the values computed are exactly the disclosure of the system at time *n*. This provides an NPSPACE algorithm which can be turned in to a PSPACE one using Savitch's Theorem [Sav70]. In order to get the value we observe that we can compute the polynomially sized denominator of this value and then we make iterative calls to the decision algorithm.

*Proof.* We first present a non-deterministic procedure that decides in NPSPACE the disclosure problem. It can then be determinised using Savitch's Theorem [Sav70].

From an arbitrarily ordered observation alphabet $\Sigma$, the procedure operates as follows for horizon *n*:

* It maintains a disclosure value $v$, a sequence of observations $o_0 \cdots o_i$ with $i \le n$, a sequence of sets of states $B_1 \cdots B_i$ with $B_j \subseteq O^{-1}(o_j)$ for all $j \le i$, an action $a_{j,s} \in A(s)$ for all $(j,s)$ with $j < i$ and $s \in S_j$, and for all $(j,s)$ with $j \le i$ and $s \in B_j$ the probability $p_{j,s}$ to reach $s$ after the sequence of observations $o_0 \cdots o_i$;

* Initially $v = 0$, $o_0$ is the smallest observation in $O(\text{Supp}(\mu_0))$, where $\mu_0$ is the initial distribution, $B_0 = \text{Supp}(\mu_0) \cap O^{-1}(o_0)$ and $p_{0,s} = \mu_0(s)$ for $s \in B_0$;

* If $i < n$ then for all $s \in B_i$, the procedure guesses an action $a_{i,s} \in A(s)$. Let $o_{i+1}$ be the smallest observation such that there exists a state $s \in B_i$ and a state $s' \in O^{-1}(o_{i+1})$ with $p(s'|s, a_{i,s}) > 0$. Then $B_{i+1}$ is set to $\{s' \in O^{-1}(o_{i+1}) \mid \exists s \in B_i \ p(s'|s, a_{i,s}) > 0\}$ and for all $s' \in B_{i+1}$, $p_{i+1,s'} = \sum_{s \in B_i} p_{i,s}p(s'|s, a_{i,s})$;
* If $i = n$, the procedure examines $B_n$. If $B_n \subseteq \text{Sec}$ then $v = v + \sum_{s \in B_n} p_{n,s}$ otherwise $v$ is unchanged. Afterwards it “backtracks” to the greatest $0 < i \le n$ such that there exists $o'_i > o_i$ with some $s \in B_{i-1}$ and a state $s' \in O^{-1}(o'_i)$ with $p(s'|s, a_{i-1,s}) > 0$. Then $B_i$ and the $p_{i,s'}$'s are updated accordingly and the procedure carries on. If there is no such $i$, the procedure returns to $i = 0$ and similarly looks for some $o'_0 > o_0$, where the initialisation step is again performed except for the value of $v$ which is unchanged. When the maximal observation in $\Sigma \cap O(\text{Supp}(\mu_0))$ is handled, the procedure terminates by comparing $v$ to the threshold.

The correctness of the procedure follows from the fact that there exists an optimal deterministic strategy where the selection of the action for the current state depends only on the sequence of observations (and not on the sequence of visited states).

The space complexity of the procedure is in $O(n|S|(\log(|A|) + nb))$ where $b$ is the maximal number of bits used to represent a transition probability of the OMDP.

Observe now that, since the maximal value is obtained by a deterministic strategy, one knows a denominator of this value: it is $d^n$ where $d$ is the least common multiple of the denominators of the probabilities occurring in the model. Its bit size is polynomial w.r.t. the size of the model. So by iteratively solving the disclosure problem for $\frac{i}{d^n}$ for increasing values of $i$, one computes the maximal value in PSPACE. $\square$

As can be seen in the proof, the optimal strategy could be computed when solving the value problem. However the size of this strategy may be exponential due to the beliefs and thus this strategy is computable in EXPTIME.

For the hardness result, we reduce the validity of Quantified Boolean Formulae (QBF). Recall that QBF extends propositional formulas by allowing quantification over the Boolean variables. Syntactically, the formulae are described by the following grammar:

$$ \begin{aligned} \phi &::= \psi \mid \exists x. \phi \mid \forall x. \phi \\ \psi &::= x \mid \psi \land \psi \mid \psi \lor \psi \mid \neg \psi \mid \text{true} \end{aligned} $$

A QBF is closed if every Boolean variable is bound by a quantifier. Deciding if a closed QBF is valid (i.e. equivalent to true) is PSPACE-hard [Sip06].

The idea of the reduction is the following. Given $\phi$ a closed QBF (w.l.o.g. in 3CNF with $n$ variables and $m$ clauses), we build an OMDP M such that $\phi$ is true iff the disclosure of M is greater or equal to $\frac{1}{2^{2n}}$ in $2(n+m)+3$ steps. In fact, $\frac{1}{2^{2n}}$ is exactly the measure of runs reaching the secret in $2(n+m)+3$ steps, thus every path reaching the secret must be disclosing. Such a run discloses the secret iff some Boolean variable of $\phi$ and its negation ($x$ and $\neg x$ for example) do not occur in its observation.

In M, during the first $2n$ steps, an assignment is 'given' to each Boolean variable: (i) for each existentially quantified Boolean variable $x$, the strategy chooses whether $x$ or $\neg x$ occurs in the observation and (ii) for each universally quantified Boolean variable $y$, by a random choice with probability $\frac{1}{2}$. During the last $2m$ steps, the strategy must trigger a Boolean variable in every clause of $\phi$ so that if a clause is not satisfied by the
<figure><img src="image_96.png" /><figcaption>Figure 7.11: Reduction of the validity problem to the disclosure on a fixed horizon. The box $S_{x_1}$ is represented in Figure 7.12.</figcaption></figure>

current assignment, then a Boolean variable is observed as both true and false during the run. Thus the observation would not disclose the secret.

*Proof.* We reduce the validity of a quantified Boolean formula: Given a closed QBF in 3CNF $\phi = \exists x_1 \forall y_1 \exists x_2 \dots \forall y_n \psi$ with $\psi = \bigwedge_{i=1 \dots m} (z_{i1} \lor z_{i2} \lor z_{i3})$, we build an OMDP M such that $\phi$ is true if and only if $\text{Disc}_{2(n+m)+3, \max(M)} \ge \frac{1}{2^{2n}}$.

The OMDP M = (*S*, *Act*, *p*, *O*) (depicted in Figure 7.11 with some conventions to avoid having too many edges) is defined by:

* $S = \{s_{init}, s_{end}, s_{\#}\} \cup \{s_{z_i} \mid z \in \{x, y\}, i = 1 \dots n\} \cup \{s_{-z_i} \mid z \in \{x, y\}, i = 1 \dots n\} \cup \{s_t^i \mid i \in \{1, \dots, m\} \} \cup \{s_{z_{ij}}^i \mid i \in \{1, \dots, m\}, j \in \{1, 2, 3\} \} \cup_{i \in \{1, \dots, n\}} (S_{x_i} \cup S_{y_i} \cup S_{-x_i} \cup S_{-y_i})$ where for $z_i$ one of the Boolean variable, $S_{z_i} = \{s_a^{z_i, 1} \mid a \in \{\# , z_i, \neg z_i \mid z \in \{x, y\}, i \in \{1, \dots, n\} \} \cup \{s_a^{z_i, 2} \mid a \in \{\# , \flat, z_i, \neg z_i \mid z \in \{x, y\}, i \in \{1, \dots, n\} \}$. Similar for the box $S_{-z_i}$ of the negation of a variable.

* $A(s_{init}) = \{x_1, \neg x_1\}$, and for all $i < n$, $A(s_{y_i}) = A(s_{\neg y_i}) = \{x_{i+1}, \neg x_{i+1}\}$. For $i \in \{1, \dots, m\}$, $A(s_t^i) = \{1, 2, 3\}$ and $A(s) = \{\text{next}\}$ for all other states (even in boxes).
<figure><img src="image_97.png" /><figcaption>Figure 7.12: Representation of the box $S_{x_1}$. We use the convention of Figure 7.8.</figcaption></figure>

• $p(s_a | s_{init}, a) = p(s_a^{a,1} | s_{init}, a) = 1/2$. For all $i < n$, $p(s_a | s_{y_i}, a) = p(s_a^{a,1} | s_{y_i}, a) = p(s_a^{a,1} | s_{\neg y_i}, a) = 1/2$. For all $i \le n$, $p(s_{y_i} | s_{x_i, next}) = p(s_{y_i,1} | s_{x_i, next}) = p(s_{\neg y_i} | s_{x_i, next}) = p(s_{\neg y_i,1} | s_{x_i, next}) = p(s_{y_i} | \neg s_{x_i, next}) = p(s_{y_i,1} | \neg s_{x_i, next}) = p(s_{\neg y_i} | s_{\neg x_i, next}) = p(s_{\neg y_i,1} | s_{\neg x_i, next}) = 1/4$, and $p(s_t^1 | s_\sharp, next) = 1$. For all $i = 1...m, j \in \{1, 2, 3\}, p(s^{z_{ij}} | s_t^i, j) = 1$, and if $i < m, p(s_t^{i+1} | s^{z_{ij}, next}) = 1$. Finally, $p(s_{end} | s^{z_{mj}, next}) = p(s_{end} | s_{end, next}) = 1$.

We now describe $p$ for the box $S_{x_1}$ other boxes being similar. For all $a, b \in \{\sharp, x_1, z_i, \neg z_i \mid z \in \{x, y\}, i \in \{2, \dots, n\}\}, p(s_b^{x_1,1} | s_a^{x_1,1}, next) = p(s_{\neg x_1}^{x_1,2} | s_a^{x_1,1}, next) = 1/(4n+1)$ and for all $c, d \in \{\sharp, \flat, z_i, \neg z_i \mid z \in \{x, y\}, i \in \{1, \dots, n\}\}, p(s_d^{x_1,2} | s_c^{x_1,2}, next) = 1/(4n+2)$.

• $O(s_{end}) = \flat, O(s_a^b) = a$ and $O(s^a) = a$ when $a$ is a Boolean variable or its negation and for all other state $s$, $O(s) = \sharp$.

The initial distribution $\mu_0$ is $1_{s_{init}}$ and the set of secret states is $\text{Sec} = \{s_{end}\}$.

We show that $\phi$ is true iff the disclosure of $M$ for observations of length $2(n+m)+3$ is greater than or equal to $\frac{1}{2^{2n}}$. First observe that for any strategy, the measure of runs reaching state $s_{end}$ with observation of length $2(n+m)+3$ is exactly $\frac{1}{2^{2n}}$. Indeed, during each of the first $2n$ actions, whatever the choices of the strategy, there is a probability $\frac{1}{2}$ to go in one of the boxes and $\frac{1}{2}$ to advance to the next choice, thus a probability $\frac{1}{2^{2n}}$ to reach the state $s_\sharp$. From there every run reaches $s_{end}$ in $2(m+1)$ steps. If the strategy is such that some variable and its negation are read on the way to $s_{end}$, then there exists a run with same observation reaching the second part of a box where every observation can be triggered, and thus the run reaching $s_{end}$ will not disclose the secret.

Intuitively, during the first $2n$ steps, every Boolean variable is assigned a value:
either chosen by the strategy as it chooses whether $x_i$ or $\neg x_i$ occurs in the observation for all $1 \le i \le n$, or randomly as $y_i$ and $\neg y_i$ both have equal chance of being triggered. During the last $2m$ steps, the strategy must trigger a Boolean variable in every clause of the disjunction so that if a clause is not satisfied by the current assignment, then a Boolean variable is observed as both true and false during the run. Thus the observation would not disclose the secret. In order for a measure of $\frac{1}{2^{2n}}$ of runs to disclose the secret, for every assignment of the $y_i$ the controller must force the run reaching $s_{end}$ to disclose the secret.

Suppose that $\phi$ is equivalent to true. Thus there exist functions $(f_i)_{i=1\dots n}$ (expressing the choices for $x_1, \dots, x_n$) such that for every set of assignments $(a_1, \dots, a_n)$ of the variables $y_1, \dots, y_n$ the Boolean formula $\psi[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$ is true. We choose a strategy $\sigma$ such that for every possible set of assignments $(a_1, \dots, a_n)$ for the variables $y_1, \dots, y_n$, for all $i \in \{0, \dots, n-1\}$, $\sigma(\sharp f_1())a_1 f_2(a_1) \dots a_i) = f_{i+1}(a_1, \dots, a_i)$. Moreover for $i_1, \dots, i_k \in \{1, 2, 3\}$, there exists $z_{k+1}_{i_1 \dots i_k} \in \{f_1(), a_1, f_2(a_1), \dots, a_n\}$ such that $\sigma(\sharp f_1())a_1 f_2(a_1) \dots a_n \sharp \sharp z_{1i_1} z_{2i_2} \dots z_{ki_k}) = z_{k+1i_{k+1}}$. The choice of the strategy is arbitrary in the other cases. Such a strategy can be defined since the formula $\psi[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$ is true and thus every clause is satisfied by this choice of assignments.

With this strategy, the fixed-horizon disclosure in $2(n+m+1)$ steps is $\frac{1}{2^{2n}}$. In other words, all the runs reaching the secret disclose it. Indeed let $\rho$ be a secret run of length $2(n+m+1)$. There exists an assignment $a_1, \dots, a_n \in \{y_1, \neg y_1, \dots, y_n, \neg y_n\}$ such that $O(\rho) = \sharp f_1()a_1 f_2(a_1) \dots a_n \sharp \sharp z_{1i_1} z_{2i_2} \dots z_{ki_m}$. By choice of $\sigma$, if, for $z \in \{x, y\}$ and $i \in \{1, \dots, n\}$, $z_i$ appears in the observation of $\rho$, $\neg z_i$ does not appear, and vice versa. Therefore as $\flat$ can be read either in $s_{end}$ or in a state reachable only by runs observing a Boolean variable and its negation, $\rho$ discloses the secret.

Conversely, suppose that $\phi$ is not equivalent to true and let $\sigma$ be a strategy, which can be assumed to be deterministic thanks to Proposition 7.3. We build partial functions $f_i : \Sigma^{2i} \to \text{Act}$ consistent with $\sigma$: for every observation $\sharp w \in \sharp \Sigma^{2i}$ of some run $\rho$, if $\sigma$ chooses action $a \in A(\text{last}(\rho))$ for $\rho$ (i.e., $\sigma(\rho)(a) = 1$) then $f_i(w) = a$. As $\phi$ is not equivalent to true, there exists an assignment $(a_1, \dots, a_n)$ for the variables $y_1, \dots, y_n$ such that the Boolean formula $\psi[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$ is false. We now build a run with non null probability, reaching the secret but not disclosing it.

By construction, there exists $\rho$ such that $O(\rho) = \sharp f_1()a_1 f_2(a_1) \dots f_n(a_1 \dots a_{n-1})a_n \flat$, with $\text{last}(\rho) = s_\sigma$ and $P_\sigma(\rho) > 0$ (where again $P_\sigma$ stands for $P_{M_\sigma(\mu_0)}$). Let $i \in \mathbb{N}$ be an integer such that the clause $z_{i_1} \lor z_{i_2} \lor z_{i_3}$ is not true under the assignment $[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$, in other words such that the negations of $z_{i_1}, z_{i_2}$ and $z_{i_3}$ were chosen as assignment. Let $\rho'$ be the run of length $2(n+m)+2$ extending $\rho$ and ending in $s_{end}$. Then $\rho'$ does not disclose the secret: indeed, there exists $j \in \{1, 2, 3\}$ such that $z_{ij}$ appears in its last $2m$ observations while its negation (written $\neg z_{ij}$ here) appears in the first $2n+1$ observations. Thus there exists a run with same observation leading to the second part of the box $S_{\neg z_{ij}}$ which is outside the secret and where every observation is possible. As the total measure of runs reaching the secret is $\frac{1}{2^{2n}}$ and at least a subset of measure $P_\sigma(\rho)$ of the runs reaching the secret do not disclose it, the disclosure of M is strictly smaller than $\frac{1}{2^{2n}}$ in $2(n+m)+3$ observation
steps.

☐

The existence of an optimal strategy in the first part of the proof implies that the limit-sure and the almost-sure problem are equivalent. Moreover, the secret being revealed with probability 1 in a given number of steps, every run must reach the secret in this number of steps. Testing if there exists a strategy such that every run reaches a set of target states in a given number of steps in an OMDP can be solved in polynomial time.

**Remark 7.1.** The proof of hardness can be adapted for maximal fixed-horizon ε-disclosure, but the algorithm for membership cannot be directly applied. The ε-disclosure could however be computed by maximising an exponential system of equations, resulting in an exponential time algorithm.

## 4.2 Minimal disclosure

The proof of the next theorem is similar to the proof of Theorem 7.7 on the fixed-horizon maximal disclosure.

The hardness result is obtained once again using a reduction from the validity of a QBF. Many of the ideas used in the proof of Theorem 7.7 reappears here: the run is still composed of two parts, in the first one it gives an assignment to the Boolean variables and in the second one the strategies goes through the clauses of the formula and verify it can satisfy them. We however give the full proof due to non-negligible differences. Now the strategy must satisfy every clause of the formula in order for the run not to disclose the secret.

For the strategy decision problem, contrary to the maximisation case, due to the randomisation, there does not necessarily exists an optimal strategy. In order to get the same complexity for the strategy decision problem, we establish that when a randomised decision rule must be selected in the optimal strategy, it can always be uniformly distributed over its support.

**Theorem 7.8.** *The fixed-horizon minimal value is computable in PSPACE. The fixed-horizon minimal disclosure problem is PSPACE-complete. In addition, the strategy decision problem is also decidable in PSPACE.*

*Proof.* The procedures for the first two problems are very similar to the ones used in Theorem 7.7. There are only two differences. First, given $B_i$ the current belief and $o_{i+1}$ one computes $B_{i+1} = \text{NextMax}(B_i, o_{i+1})$ (independently of the guessed actions $a_{i,s}$). Second, the computation procedure operates by decreasing values of $i$ when the value is less or equal than $\frac{i}{d^n}$.

In order to decide whether a strategy exists that provides the minimal value, one guesses this strategy in PSPACE as before. However there is an additional difficulty since the (possible) optimal strategy may be randomised. Thus during the procedure, given some belief $B$ and some state $s$, one guesses the support $A' \subseteq A_s$ of the decision rule and one defines the decision rule say $\delta$ as a uniform choice over $A'$. We claim that this restriction is sound. Assume another decision rule $\delta'$ with same support would provide
a smaller value. Then, since the support are unchanged, the decision rule informally
described as $(1+\varepsilon)\delta' - \varepsilon\delta$ for small enough $\varepsilon$ would still provide a better value, meaning
that the support $A'$ cannot be used to find an optimal strategy.

<figure><img src="image_98.png" /><figcaption>Figure 7.13: Reduction of the validity problem to the disclosure on a fixed horizon. The box $S_{x_1}$ is represented in Figure 7.14</figcaption></figure>

Like for the case of maximisation, the hardness of the fixed-horizon minimal disclosure problem is obtained by a reduction from the validity of a quantified Boolean formula. Let $\phi = \exists x_1 \forall y_1 \exists x_2 \dots \forall y_n \psi$ with $\psi = \bigwedge_{i=1}^{m} (z_{i1} \lor z_{i2} \lor z_{i3})$ a closed QBF where we assume w.l.o.g. that in every clause the literals are distinct. We build the OMDP $M = (S, \mathbf{Act}, p, O)$ (represented in Figure 7.13) where:

* $S = \{s_{init}, s_{end}, s_{\#}\} \cup \{s_{z_i} \mid z \in \{x, y\}, i = 1 \dots n\} \cup \{s_{\neg z_i} \mid z \in \{x, y\}, i = 1 \dots n\} \cup \{s_t^i \mid i \in \{1, \dots, m\} \} \cup \{s_{ij}^z \mid i \in \{1, \dots, m\}, j \in \{1, 2, 3\} \} \cup \{s_{end}^z \mid z \in \{x, y\}, i = 1 \dots n\} \cup \{i \in \{1, \dots, n\} \} (S_{x_i} \cup S_{y_i} \cup S_{\neg x_i} \cup S_{\neg y_i})$ where for $z_i$ one of the Boolean variable, $S_{z_i} = \{s_a^z \mid a \in \{\# , z_i, \neg z_i \mid z \in \{x, y\}, i \in \{1, \dots, n\} \} \cup \{s_b^z, s_f^z\}$.

* $A(s_{init}) = \{x_1, \neg x_1\}$, and for all $i < n$, $A(s_{y_i}) = A(s_{\neg y_i}) = \{x_{i+1}, \neg x_{i+1}\}$. For $i \in \{1, \dots, m\}$, $A(s_t^i) = \{1, 2, 3\}$ and for every other state (even in boxes), $A(s) = \{\text{next}\}$.
<figure><img src="image_99.png" /><figcaption>Figure 7.14: Representation of the box $S_{x_1}$ (with the conventions of Figure 7.8).</figcaption></figure>

• $p(s_a | s_{init}, a) = p(s_a^{a,1} | s_{init}, a) = 1/2$. For all $i < n$, $p(s_a | s_{y_i}, a) = p(s_a^{a,1} | s_{y_i}, a) = p(s_a^{a,1} | s_{\neg y_i}, a) = 1/2$. For all $i \le n$, $p(s_{y_i} | s_{x_i}, \text{next}) = p(s_{y_i}^{1,1} | s_{x_i}, \text{next}) = p(s_{\neg y_i}^{1,1} | s_{x_i}, \text{next}) = p(s_{s_{y_i}|\neg x_i}, y_i) = p(s_{y_i}^{1,1} | s_{\neg x_i}, y_i) = p(s_{\neg y_i} | s_{\neg x_i}, \text{next}) = p(s_{\neg y_i}^{1,1} | s_{\neg x_i}, \text{next}) = 1/4$. $p(s_t^1 | s_\#^1, \text{next}) = 1$. For all $i = 1...m, j \in \{1,2,3\}, p(s^{z_{ij}} | s_t^i, j) = 1$, and if $i < m, p(s_t^{i+1} | s^{z_{ij}}, \text{next}) = 1$. Finally $p(s_{end} | s^{z_{mj}}, \text{next}) = 1$, and for all $z \in \{x,y\}, i = 1...n, p(s_{end}^{z_i} | s_{end}, \text{next}) = 1/(2n)$.

We now describe $p$ for the box $S_{x_1}$ other boxes being similar. For all $a \in \{\# , x_1, z_i, \neg z_i | z \in \{x,y\}, i \in \{2,...,n\}\}, b \in \{\# , b, z_i, \neg z_i | z \in \{x,y\}, i \in \{1,...,n\}\} p(s_b^{x_1} | s_a^{x_1}, \text{next}) = 1/(4n + 2)$, and $p(s_{\neg x_1}^{x_1} | s_{\neg x_1}, \text{next}) = p(s_f^{x_1} | s_b^{x_1}, \text{next}) = p(s_f^{x_1} | s_f^{x_1}, \text{next}) = 1$.

• $O(s_{end}) = b$, $O(s_a^b) = a$ and $O(s^a) = a$ when $a$ is a Boolean variable, its negation or $b$. For $i = 1...n$, $O(s_{end}^{x_i}) = O(s_f^{x_i}) = O(s_{\neg x_i}) = 2i - 1$ and $O(s_{end}^{y_i}) = O(s_f^{y_i}) = O(s_f^{\neg y_i}) = 2i$, and for any other state $s$, $O(s) = \#$.

The initial distribution $\mu_0$ is $1_{s_{init}}$ and the secret runs are the ones visiting $s_{end}$ (Sec = $\{s_{end}\} \cup \{s_{end}^{z_i} | z \in \{x,y\}, i = 1...n\}$).

In a similar fashion as what was done in the hardness part of the proof of Proposition 7.7, we show that $\phi$ is true iff the disclosure of $M$ is equal to 0 in $2(n+m+2)$ steps. First observe that a run $\rho$ reaching $s_{end}$ can be extended for all $j \in \{1,...,2n\}$ in a run $\rho_j$ such that $O(\rho_j) = O(\rho)j$. Moreover, $\rho_1$ discloses the secret iff $x_1$ and $\neg x_1$ both occur in $O(\rho_1)$ (and similarly for the other $\rho_j$s). Indeed a run reaching $S_{x_1}$ or $S_{\neg x_1}$ cannot have triggered both observations $x_1$ and $\neg x_1$ and also end with observation 1.

Intuitively, during the first $2n$ steps, all Boolean variables are assigned a value: either chosen by the strategy as it chooses whether $x_i$ or $\neg x_i$ occurs in the observation
for each $1 \le i \le n$, or randomly as $y_i$ and $\neg y_i$ both have half a chance of being triggered. During the last $2m+1$ steps, the strategy must choose a Boolean formula in every clause so that if a clause is not satisfied by the current assignment, then a Boolean variable is observed as both true and false during the run. The last step then triggers randomly the observation $j$ for $j \in \{1, \dots, 2n\}$.

Suppose that $\phi$ is equivalent to true. Then there exist functions $(f_i)_{i=1\dots n}$ such that for every set of assignments $(a_1, \dots, a_n)$ for the variables $y_1, \dots, y_n$ the Boolean formula $\psi[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$ is true. We choose a strategy $\sigma$ such that for every possible set of assignments $(a_1, \dots, a_n)$ for the variables $y_1, \dots, y_n$, and for all $i$, $0 \le i \le n-1$, $\sigma(\sharp f_1())a_1f_2(a_1)\dots a_i = f_{i+1}(a_1, \dots, a_i)$. Moreover for $k \in \{1, \dots, m\}$ and $i_1, \dots, i_k \in \{1, 2, 3\}$, there exists $z_{k+1_{i_k+1}} \in \{f_1(), a_1, f_2(a_1), \dots, a_n\}$ such that $\sigma(\sharp f_1())a_1f_2(a_1)\dots a_n \sharp z_{1_{i_1}} z_{2_{i_2}} \dots z_{k_{i_k}} = z_{k+1_{i_k+1}}$. The choice of the strategy is arbitrary in the other cases. Since $\psi[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$ is true, every clause is satisfied by this choice of assignments, hence it is possible to define such a strategy.

With this strategy, the fixed-horizon disclosure in $2(n + m + 2)$ steps is 0. In other words, none of the runs reaching the secret discloses it. Indeed let $\rho$ be a secret run of length $2(n + m + 2)$, then there exist $a_1, \dots, a_n \in \{y_1, \neg y_1, \dots, y_n, \neg y_n\}$ and $j \in \{1, \dots, 2n\}$ such that $O(\rho) = \sharp f_1()a_1f_2(a_1)\dots a_n \sharp z_{1_{i_1}} z_{2_{i_2}} \dots z_{m_{i_m}} \flat j$. By choice of $\sigma$, if, for $z \in \{x, y\}$ and $i \in \{1, \dots, n\}$, $z_i$ appears in the observation of $\rho$, $\neg z_i$ does not, and vice versa. Therefore as $\flat j$ can be read either from $s_{end}$ or in a box state outside of the secret reachable only by runs that do not observe a Boolean variable and its negation, $\rho$ does not disclose the secret.

Conversely, suppose that $\phi$ is not equivalent to true and let $\sigma$ be an arbitrary strategy. We first build a deterministic strategy $\sigma'$ with smaller or equal disclosure. The first choice concerns $\{x_1, \neg x_1\}$ and the next observation in a run corresponds to that choice. Consider $\sigma_1$ (resp. $\sigma'_1$) the strategy that selects $x_1$ (resp. $\neg x_1$) and then plays like $\sigma$. Due to the fact that observations are distinct, the disclosure value w.r.t. $\sigma$ is a convex combination of the ones of $\sigma_1$ and $\sigma'_1$. So one substitutes $\sigma$ by the one with smaller or equal disclosure. A similar pattern applies for every choice until reaching the horizon. Thus by iterating this transformation we obtain a deterministic strategy. So we assume now that $\sigma$ is deterministic. Since there is a finite number of such strategies for fixed horizon, it only remains to prove that the disclosure value under $\sigma$ is positive. We build partial functions $f_i : \Sigma^{2i} \to \text{Act}$ consistent with $\sigma$: for every observation $\sharp w \in \sharp \Sigma^{2i}$ of some run $\rho$, if $\sigma$ chooses action $a \in A(\text{last}(\rho))$ for $\rho$, then we set $f_i(w) = a$. As $\phi$ is not equivalent to true, there exists an assignment $(a_1, \dots, a_n)$ for the variables $y_1, \dots, y_n$ such that the Boolean formula $\psi[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$ is false.

We now build a run disclosing the secret. By construction, there exists $\rho$ such that $O(\rho) = \sharp f_1()a_1f_2(a_1)\dots f_n(a_1\dots a_{n-1})a_n \sharp$, leading to $\text{last}(\rho) = s_\sharp$ with $\mathbb{P}_\sigma(\rho) > 0$. Let $i \in \{1, \dots, m\}$ such that the negations of $z_{i_1}, z_{i_2}$ and $z_{i_3}$ were chosen as assignment hence $z_{i_1} \vee z_{i_2} \vee z_{i_3}$ is not true under the assignment $[f_1(), a_1, f_2(a_1), \dots, f_n(a_1, \dots, a_{n-1}), a_n]$. Let $\rho'$ be a run of length $2(n+m)+3$ extending $\rho$ and ending in $s_{end}$. Then $\rho'$ does
not disclose the secret because there exists $j \in \{1, 2, 3\}$ such that $z_{ij}$ appears in the
previous $2m$ observations while its negation (written $\neg z_{ij}$ here) appears in the first
$2n+1$ observations. Let $\rho''$ of length $2(n+m+2)$ extending $\rho'$ by ending in $s_{end}^{z_{ij}}$. There
is no other run with the same observation and $\rho''$ is a secret run, thus $\rho''$ discloses the
secret. Therefore the disclosure of $M$ is positive.

Observe that this reduction also works for finite horizon since no further disclosure
may occur after the first occurrence of a state in {$s_{end}^{x_1}, \dots, s_{end}^{x_n}, s_{end}^{y_1}, \dots, s_{end}^{y_n}$}. $\square$

Contrary to the case of maximisation, the above proof implies PSPACE-completeness
for the limit-sure and almost-sure problem for disclosure minimisation.

**Remark 7.2.** As for maximisation, the proof of hardness can be adapted for $\varepsilon$-disclosure and the algorithm for membership cannot be directly applied. The minimal fixed horizon $\varepsilon$-disclosure could however be computed by minimising an exponential system of equations, resulting in an exponential time algorithm.

# 5 Conclusion

To our knowledge, the opacity of probabilistic systems had only been studied in order
to maximise the disclosure of the system. Moreover, these studies always restricted the
framework so that the strategy that is chosen does not modify if an observed sequence
is disclosing or not, leaving the general case open. In the context of the previous
studies, only maximisation was considered, which is understandable as maximisation
and minimisation of disclosure are similar: they both consists in the optimisation of
a fixed event. We, however, focused on the general case, both for maximisation, and
for minimisation. In our framework, maximisation and minimisation present a strong
asymmetry. Indeed, when considering finite horizon, most maximisation problems are
undecidable although deterministic strategies are optimal. In contrast, minimisations
problems are decidable, but good strategies often require randomisation. Note that
a complexity gap (PSPACE-hard versus in EXPTIME) remains to fill for the finite-
horizon minimisation problem. For fixed horizon, there is still an asymmetry between
maximisation and minimisation that clearly appears in some parts of the proofs. But
it is not as strong as in finite horizon and algorithms with good complexities can be
obtained for both.

Although we used a variant of Markov decision processes enriched with observation)
to represent our models, opacity is not an usual MDP problem. Indeed, opacity is an
hyper property as the disclosure depends on a set of paths linked by their observation.
This gives a partial observation flavour to opacity. Opacity as seen here is therefore
a problem in between OMDP and POMDP. For this kind of problems, as seen in this
chapter, it is important to determine whether the problem can be translated to an
MDP or a POMDP problem in order to use the results known on these models. Here,
maximisation of the disclosure was closer to POMDP problems while minimisation was
closer to OMDP problems.
A promising research direction to consider is the approximate notion of opacity. It is the most natural notion of opacity. Indeed, if an attacker knows there is a 99% chance to be in the secret, the secret could be considered to be disclosed. As we have shown in Section 1, the most naive definition of approximate opacity is undecidable even without control. For diagnosability, we showed in Chapter 4 that AFF-diagnosability, an elaborate notion of approximate diagnosability was decidable for passive systems. A natural question is thus to determine if we can define a similar notion of opacity. A notion that would measure the set of infinite secret runs which disclose with arbitrarily high probability the secret for example. As it is close to AFF-diagnosability, we conjecture that it should be decidable for observable Markov chains. However, in active system, the finite-horizon maximisation/minimisation disclosure problem are likely to be undecidable.
# Chapter 8

# Conclusion

## Contributions

This thesis constitutes part of the work towards a theoretical analysis of partial observation problems in a stochastic framework. More specifically it focused on the problem of diagnosis. Diagnosis had already been studied for stochastic systems [TT05, CK13, BFH$^+$14], however the definitions used varied and many central issues had been left open. The first step to set solid foundations for the analysis of diagnosis in probabilistic systems was thus to define precise and realistic notions of diagnosis which would encompass the ones already established. This was done in Chapter 2. Before focusing on any specific framework, we performed in Chapter 3 a semantical analysis of the different notions of diagnosability. While some intuitions on the relations between the notions could be obtained directly from the definitions, the analysis allowed, among other things, to establish formally these links, with a few surprises due mostly to the distinction between finite systems, finitely-branching systems and infinitely-branching systems.

We then turned to multiple specific frameworks and developed methods to decide diagnosability with optimal complexity. First, we focused on passive systems. Moreover, in Chapter 4, we restricted ourselves to finite systems. This important restriction pushed us to make once again some semantical analysis in order to obtain refined results exploiting the finite number of states. This gave us precise characterisations of the decidable notions of diagnosis, allowing us to establish the exact complexities of the problems. We also showed how to automatically build diagnosers associated with each notion of diagnosability. In Chapter 5, we extended our analysis to infinite-state systems. This immediately raised one important issue that we did not have for finite systems: how to represent such systems. In consequence, we studied several possible representations, one of which yielded multiple decidability results. These decidability results were obtained in large part thanks to the analysis made in Chapter 3. This emphasizes the importance of a good understanding of a notion and how to characterise it as a preamble to study the problem.

We then considered active systems. As for stochastic infinite systems, many different
frameworks may be studied. But contrary to stochastic infinite systems, diagnosis had
already been studied for stochastic active systems [BFH<sup>+</sup>14], providing a framework
our developments. The latter revealed an issue with the control of a system: ensur-
ing diagnosability could be at the expense of the correct performance of the system.
We studied in Chapter 6 how to limit the degradation of the system while preserving
diagnosability. More precisely, we defined notions of the degradation of a system and
showed the decidability and precise complexity for some of them, and established the
undecidability of the others.

In the last chapter, Chapter 7, we switched our focus to opacity, another partial
observation problem. In active systems, we showed how, when possible, one could
develop strategies maximising or minimising the opacity of a system. The main element
that made this analysis successful is the understanding of the forms that the optimal
strategies would take.

Our contributions, while providing a good foundation for the diagnosis of proba-
bilistic systems and many interesting results, are far from giving the whole picture. In
the next section we provide a list of remaining open questions and research directions
extending the thesis.

Perspectives

The current thesis opens quite a few perspectives, some of which were already given
in each chapter conclusion and are partially repeated here. We classify these ideas
depending on whether they are short-term, mid-term or long-term objectives. This
decomposition represents how direct the link between the current work and the per-
spective is. We start with the short-term perspectives, *i.e*. the problems immediately
raised by the works presented here.

* The most immediate perspectives are the ones given by the gaps within our results: notions for which we could not establish the decidability status, complexities that are not tight, etc. For example, the algorithms given to decide the exact notions of diagnosability in probabilistic visibly pushdown automata are in EXPSPACE while the proven lower bound is only EXPTIME. Another open question is the exact complexity of computing the minimal disclosure of the opacity (PSPACE lower bound versus EXPTIME upper bound). The main open question however is the decidability status of the FA-diagnosability in pVPA. We showed that this notion was harder than the other notion of exact diagnosability by studying its membership in the Borel hierarchy, but could not give an algorithm nor an undecidability proof. We conjecture that this notion is decidable and, in fact, with an algorithm of the same complexity than the other. Indeed, the proofs of the the non-expressivity results that limited the study of FA-diagnosability uses systems that cannot be expressed by pVPA. There could exists a pathL formula that would characterise FA-diagnosability when restricted to pVPA. An ongoing work seems to confirm this to be true.
* Another immediate perspective is raised by the introduction of the *pathL* logic. It was used in Chapter 5 in order to decide some notions of exact diagnosability. This logic may be useful for example to test properties such as the uniformity of the speed of diagnosis, the boundedness of the mean detection time of a fault (or mean time before an information about the correctness of a run), etc. Moreover, if the *pathL* logic cannot be used directly, one could define an enriched version of this notion with greater expressive power. This enriched version must be carefully designed so that the generated formulae can be checked.

* The last immediate perspective relates to the active framework. Whether it be for diagnosis or opacity, we only focused on exact notions. It would be natural to tackle the, usually harder, approximate notions. This is in fact an ongoing work. The current results seem to point toward decidability for AFF-diagnosability in active systems while similar approximate notions are undecidable for opacity, both for maximisation and minimisation.

We now turn to mid-term perspectives. They correspond to problems that are strongly connected to this thesis, while not being immediate.

* In our active framework, the observations are clearly given by the model. This represents in reality sensors within the system. Using a sensor has a cost. Therefore, instead of having fixed sensors, one could have a list of potential sensors associated with costs. The goal would then be to obtain diagnosability while minimising the cost. A cost could also be given to having the sensor turned on, forcing the optimal strategy to decide when it needs to have the sensor operating. Some works were already done on this subject, see [CT08] and [TT07].

* Faults, as defined in this document, are a boolean property: a system is either faulty or correct. Moreover, they are permanent. Once a fault occurred, we did not consider as important to decide if more faults would be created later for example. No matter the number of faults, the run is deemed faulty. One could envision a different idea for the fault. A fault could represent a partial degradation of the system, the failure of one of its non-vital component or something that can be repaired (see [FHLM18] for a study of repairable faults in a non-stochastic framework). Seen this way, many new questions arise. In passive systems, this means defining measures of correctness for a system and testing properties, for example on the delay of the fault counter (one can test if this delay is bounded, if it is unbounded but in $o(n)$ where $n$ is the length of the run, in $O(n)...$). In active systems, we would wish to find controllers that optimise the measures of interests or that ensure good delays of detection for the fault counter. This would obviously only be an interesting study for systems where many faults will be triggered. However, this is not an unrealistic assumption as every system is slowly degraded due to time elapsing.

* Our diagnosability algorithms currently only gives a Boolean answer. In order for system designers to modify its system so that it becomes diagnosable for example,
they need to know what is the cause of the missed fault. As a consequence, it
would be interesting to design algorithm able to give a counter-example to the
diagnosability of the system whenever it exists. This notion of counter-example
needs to be made precise. In an LTS, a counter-example can be given by an
ambiguous cycle of the system. As with probabilistic systems, this cycle may
have a zero probability, the counter-example must thus be able to describe a set
of runs with positive probability. For example, by giving a finite faulty run such
that any extension of it is ambiguous. However, this kind of counter-example
does not necessarily exist, in pushdown systems for example. The generation of
counter-examples in stochastic systems has been studied, see [ÁBD<sup>+</sup>14], but for
different objectives than diagnosability.

* The main formalism we chose, probabilistic labelled transition systems, has its limitations. One could be interested in studying higher-level models such as stochastic Petri nets, stochastic process algebra (with PEPA for example [Hil96, Chapter 3]), etc. can be more appropriate to represent some real life systems. Indeed, high-level formalisms usually are (often exponentially) more concise than low level formalisms, hence a greater comfort for designers. Moreover, high-level formalisms usually have a structure, which allows to conceive more efficient algorithms as the generated systems (pLTS, MDP, etc.) benefit from additional properties. For example, when a system is a synchronised product of several components, the transition matrix or the infinitesimal generator can be computed using tensor products of the matrix representing the different components (see e.g. [HM95, HM96]).

* During this thesis, we designed many algorithms. In parallel to the previous item, it would be useful to implement these algorithms. This tool could then be used to solve the diagnosability problems for pLTS or for some higher-level models whose semantics is an appropriate pLTS. This implementation should be integrated within an existing tool to benefit from the possibilities offered while enriching it. A good candidate would be COSMOS [BBD<sup>+</sup>15], a statistical model checker for the hybrid automata stochastic logic.

We now end with the long-term perspectives, more remote to our current work.

* We established many results within this thesis. Some of which used methods that are quite usual, some required to use new ideas such as the *pathL* logic. These new ideas may be useful in order to tackle other issues related to partial observation such as identification problems, stochastic games. . . It could therefore be interesting to see which kind of problems, in these other frameworks, would benefit from our approach.

* Another direction comes from another interpretation of faults. Let us proceed through an example. When someone is sick, multiple symptoms appear or do not appear in the body. These symptoms each correspond to a failure of the human body, so each are a fault that must be detected. However, in order to
cure the patient one needs to link the patterns to a common cause: an illness. In other words, one wants to deduce a meta-information from the behaviour of the system. Finding the origin of the fault has been studied under the term causality, but, as explained in [GSS17], this approach focused on static systems. In dynamic systems, this meta-information may be seen as a pattern that must be detected [JMPC06]. This objective can be seen as an extension of diagnosis, but it goes into the long-term category as it corresponds to what seems to be a far more general question. It can also be linked to questions of identification of complex behaviour, possibly similar to what was studied in [Pie14].

* Diagnosis is a research domain with clear applications. As a consequence, it would gain a lot from being studied in cooperation with the industry. This would allow researchers to better understand the industry's need. For example, there could exist definitions of diagnosability that we did not focus on, yet have relevance from an industrial point of view. Moreover, while our methods are efficient in theory, they may raise practical issues that we did not consider. There are already some cooperations such as [HF12] where the authors investigate the problem of building a model appropriate for diagnosis out of a real system, in their case, a network.

* The last perspective discussed here is of a different nature: it is not a research direction. However, it could still have a great impact on the domain of research. There exist many contributions which either establish a known result or have an erroneous proof for a theorem that was already proven false (trying to give a PTIME algorithm for a PSPACE-hard problem for example). This clearly shows the difficulty for researchers to know the current state of the research, even for a specific domain such as diagnosis. To tackle this issue, one possibility may be to try to build a cooperative website that would gather all the results on diagnosis, something in the spirit of the POMDP webpage [POM]. This way, one could efficiently find the current state of the art on the domain and this would save a lot of useful time to many researchers. This obviously has some issues. To be useful, the existence of such a website has to be spread and people must keep it up to date. It would also raise many questions of organisation due to the width of the domain, even when restricted to diagnosis (the many existing frameworks, diagnosability notions, methods of approach,...). The various surveys on diagnosis issues [ZL13, Bas14] would help dealing with this point. But most of all, building such a website is extremely time-consuming.
Bibliography

[ABCP13] M. E. Andrés, N. E. Bordenabe, K. Chatzikokolakis, and C. Palamidessi. Geo-indistinguishability: Differential privacy for location-based systems. In *Proceedings of CCS'13*, pages 901–914. ACM, 2013.

[ÁBD+14] E. Ábrahám, B. Becker, C. Dehnert, N. Jansen, J.-P. Katoen, and R. Wimmer. Counterexample generation for discrete-time Markov models: an introductory survey. In *Proceedings of SFM'14*, volume 8483 of LNCS, pages 65–121. Springer, 2014.

[ADD99] R. B. Ash and C. A. Doleans-Dade. *Probability and measure theory*. Academic Press, 1999.

[Agu10] M. K. Aguilera. *Stumbling over consensus research: misunderstandings and issues, in Replication: theory and practice*, volume 5959 of LNCS. Springer, 2010.

[AM04] R. Alur and P. Madhusudan. Visibly pushdown languages. In *Proceedings of STOC'04*, pages 202–211. ACM, 2004.

[Bar14] B. Barbot. *Acceleration for statistical model checking*. (*Accélérations pour le model checking statistique*). PhD thesis, École normale supérieure de Cachan, France, 2014.

[Bas14] F. Basile. Overview of fault diagnosis methods based on Petri net models. In *Proceedings of ECC'14*, pages 2636–2642. IEEE, 2014.

[BBB+14] N. Bertrand, P. Bouyer, T. Brihaye, Q. Menet, C. Baier, M. Größer, and M. Jurdzinski. Stochastic timed automata. *Logical Methods in Computer Science*, 10(4), 2014.

[BBD+15] P. Ballarini, B. Barbot, M. Duflot, S. Haddad, and N. Pekergin. HASL: A new approach for performance evaluation and model checking from concepts to experimentation. *Performance Evaluation*, 90:53–77, 2015.

[BBS06] C. Baier, N. Bertrand, and P. Schnoebelen. A note on the attractor-property of infinite-state markov chains. *Information Processing Letters*, 97(2):58 – 63, 2006.
[BCS15] B. Bérard, K. Chatterjee, and N. Sznajder. Probabilistic opacity for Markov decision processes. *Information Processing Letters*, 115(1):52–59, 2015.

[BD08] D. Berwanger and L. Doyen. On the power of imperfect information. In *Proceedings of FSTTCS'08*, volume 2 of LIPIcs, pages 73–82. Leibniz-Zentrum für Informatik, 2008.

[BEKK13] T. Brázdil, J. Esparza, S. Kiefer, and A. Kučera. Analyzing probabilistic pushdown automata. *Formal Methods in System Design*, 43(2):124–163, 2013.

[BFG17] H. Bazille, E. Fabre, and B. Genest. Diagnosability degree of stochastic discrete event systems. In *Proceedings of CDC'17*, pages 5726–5731. IEEE, 2017.

[BFH$^{+}$14] N. Bertrand, E. Fabre, S. Haar, S. Haddad, and L. Hélouët. Active diagnosis for probabilistic systems. In *Proceedings of FoSSaCS'14*, volume 8412 of LNCS, pages 29–42. Springer, 2014.

[BGG09] N. Bertrand, B. Genest, and H. Gimbert. Qualitative determinacy and decidability of stochastic games with signals. In *Proceedings of LICS'09*, pages 319–328. IEEE, 2009.

[BGI$^{+}$01] B. Barak, O. Goldreich, R. Impagliazzo, S. Rudich, A. Sahai, S. P. Vadhan, and K. Yang. On the (im)possibility of obfuscating programs. In *Proceedings of CRYPTO'01*, pages 1–18. ACM, 2001.

[BHL14] N. Bertrand, S. Haddad, and E. Lefauchez. Foundation of diagnosis and predictability in probabilistic systems. In *Proceedings of FSTTCS'14*, volume 29 of LIPIcs, pages 417–429. Leibniz-Zentrum für Informatik, 2014.

[BHL16a] N. Bertrand, S. Haddad, and E. Lefauchez. Accurate approximate diagnosability of stochastic systems. In *Proceedings of LATA'16*, volume 9618 of LNCS, pages 549–561. Springer, 2016.

[BHL16b] N. Bertrand, S. Haddad, and E. Lefauchez. Diagnosis in infinite-state probabilistic systems. In *Proceedings of CONCUR'16*, volume 59 of LIPIcs, pages 37:1–37:14. Leibniz-Zentrum für Informatik, 2016.

[BHL17a] B. Bérard, S. Haddad, and E. Lefauchez. Probabilistic disclosure: Maximisation vs. minimisation. In *Proceedings of FSTTCS'17*, volume 93 of LIPIcs, pages 13:1–13:14. Leibniz-Zentrum für Informatik, 2017.

[BHL17b] N. Bertrand, S. Haddad, and E. Lefauchez. Diagnostic et contrôle de la dégradation des systèmes probabilistes. In *Proceedings of MSR'17*. HAL, 2017.
[BHSS18] B. Bérard, S. Haar, S. Schmitz, and S. Schwoon. The complexity of diagnosability and opacity verification for Petri nets. *Fundamenta Informatica*, 2018. To appear.

[BK08] C. Baier and J.-P. Katoen. *Principles of model checking*. MIT Press, 2008.

[BKM12] J. W. Bryans, M. Koutny, and C. Mu. Towards quantitative analysis of opacity. In *Proceedings of TGC'12*, volume 8191 of LNCS, pages 145-163. Springer, 2012.

[BKMS16] B. Bérard, O. Kouchnarenko, J. Mullins, and M. Sassolas. Preserving opacity on interval Markov chains under simulation. In *Proceedings of WODES'16*, pages 319-324. IEEE, 2016.

[BKMS18] B. Bérard, O. Kouchnarenko, J. Mullins, and M. Sassolas. Opacity for linear constraint Markov chains. *Discrete Event Dynamic Systems*, 28(1):83-108, 2018.

[BMS15] B. Bérard, J. Mullins, and M. Sassolas. Quantifying opacity. *Mathematical Structures in Computer Science*, 25(2):361-403, 2015.

[BS84] B. G. Buchanan and E. H. Shortliffe. *Rule based expert systems: the MYCIN experiments of the stanford heuristic programming project*. Addison-Wesley, 1984.

[CDGH10] K. Chatterjee, L. Doyen, H. Gimbert, and T. A. Henzinger. Randomness for free. In *Proceedings of MFCS'10*, volume 6281 of LNCS, pages 246-257. Springer, 2010.

[CDH10] K. Chatterjee, L. Doyen, and T. A. Henzinger. Qualitative analysis of partially-observable Markov decision processes. In *Proceedings of MFCS'10*, volume 6281 of LNCS, pages 258-269. Springer, 2010.

[CGLS12] M. P. Cabasino, A. Giua, S. Lafortune, and C. Seatzu. A new approach for diagnosability analysis of petri nets using verifier nets. *Transactions on Automatic Control*, 57(12):3104-3117, 2012.

[CGS09] M. P. Cabasino, A. Giua, and C. Seatzu. Diagnosability of bounded Petri nets. In *Proceedings of CDC'09*, pages 1254-1260. IEEE, 2009.

[CGS14] M. P. Cabasino, A. Giua, and C. Seatzu. Diagnosability of discrete-event systems using labeled Petri nets. *Transactions Automation Science and Engineering*, 11(1):144-153, 2014.

[CK13] J. Chen and R. Kumar. Polynomial test for stochastic diagnosability of discrete-event systems. *Transactions on Automation Science and Engineering*, 10(4):969-979, 2013.
[CK14] T. Chen and S. Kiefer. On the total variation distance of labelled Markov chains. In *Proceedings of CSL-LICS'14*, pages 33:1–33:10. ACM, 2014.

[CK15] J. Chen and R. Kumar. Stochastic failure prognosability of discrete event systems. *Transactions on Automatic Control*, 60(6):1570–1581, 2015.

[CP09] E. Chanthery and Y. Pencolé. Monitoring and active diagnosis for discrete-event systems. *IFAC Proceedings Volumes*, 42(8):1545–1550, 2009.

[CSH08] K. Chatterjee, K. Sen, and T. A. Henzinger. Model-checking omega-regular properties of interval Markov chains. In *Proceedings of FOSSACS'08*, volume 4962 of LNCS, pages 302–317. Springer, 2008.

[CT08] F. Cassez and S. Tripakis. Fault diagnosis with static and dynamic observers. *Fundamenta Informaticae*, 88:497–540, 2008.

[CY95] C. Courcoubetis and M. Yannakakis. The complexity of probabilistic verification. *Journal of the ACM*, 42(4):857–907, 1995.

[DHR08] L. Doyen, T. A. Henzinger, and J-F. Raskin. Equivalence of labeled markov chains. *International Journal of Foundations of Computer Science*, 19(3):549–563, 2008.

[Dia09] M. Diaz. *Petri nets: fundamental models, verification and applications*. Wiley, 2009.

[DLT00] R. Debouk, S. Lafortune, and D. Teneketzis. Coordinated decentralized protocols for failure diagnosis of discrete event systems. *Discrete Event Dynamic Systems*, 10(1-2):33–86, 2000.

[DMK$^{+}$99] K. Doi, H. MacMahon, S. Katsuragawa, R. M. Nishikawa, and Y. Jiang. Computer-aided diagnosis in radiology: potential and pitfalls. *European Journal of Radiology*, 31(2):97–109, 1999.

[Eme90] E. A. Emerson. Handbook of theoretical computer science (vol. B). In *Temporal and Modal Logic*, pages 995–1072. MIT Press, 1990.

[EMT16] R. Ehlers, S. Moarref, and U. Topcu. Risk-averse control of Markov decision processes with $\omega$-regular objectives. In *Proceedings of CDC'16*, pages 426–433. IEEE, 2016.

[EN94] J. Esparza and M. Nielsen. Decidability issues for Petri nets - a survey. *Elektronische Informationsverarbeitung und Kybernetik*, 30(3):143–160, 1994.

[EY09] K. Etessami and M. Yannakakis. Recursive Markov chains, stochastic grammars, and monotone systems of nonlinear equations. *Journal of the ACM*, 56(1), 2009.
[EY12] K. Etessami and M. Yannakakis. Model checking of recursive probabilistic systems. *Transactions on Computational Logic*, 13(2):12, 2012.

[FHLM18] E. Fabre, L. Hélouët, E. Lefaucheux, and H. Marchand. Diagnosability of repairable faults. *Discrete Event Dynamic Systems*, 28(2):183–213, 2018.

[FS01] A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! *Theoretical Computer Science*, 256(1):63–92, 2001.

[GL09] S. Genc and S. Lafortune. Predictability of event occurrences in partially-observed discrete-event systems. *Automatica*, 45(2):301–311, 2009.

[GO10] H. Gimbert and Y. Oualhadj. Probabilistic automata on finite words: Decidable and undecidable problems. In *Proceedings of ICALP’10*, volume 6199 of LNCS, pages 527–538. Springer, 2010.

[GS14] J. Goubault-Larrecq and R. Segala. Random measurable selections. In *Horizons of the Mind. A Tribute to Prakash Panangaden*, volume 8464 of LNCS, pages 343–362. Springer, 2014.

[GSS17] G. Göfler, O. Sokolsky, and J.-B. Stefani. Counterfactual causality from first principles? In *Proceedings of CREST@ETAPS’17*, volume 259 of EPTCS, pages 47–53, 2017.

[GTWJ03] J. Z. Gao, J. Tsao, Y. Wu, and T. H.-S. Jacob. *Testing and quality assurance for component-based software*. Artech House, Inc., 2003.

[HC94] L. Holloway and S. Chand. Time templates for discrete event fault monitoring in manufacturing systems. In *Proceedings of ACC’94*, pages 701–706. IEEE, 1994.

[HF12] C. Hounkonnou and E. Fabre. Empowering self-diagnosis with self-modeling. In *Proceedings of CNSM’12*, pages 364–370. IEEE, 2012.

[HHMS13] S. Haar, S. Haddad, T. Melliti, and S. Schwoon. Optimal constructions for active diagnosis. In *Proceedings of FSTTCS’13*, volume 24 of LIPIcs, pages 527–539. Leibniz-Zentrum für Informatik, 2013.

[HHMS17] S. Haar, S. Haddad, T. Melliti, and S. Schwoon. Optimal constructions for active diagnosis. *Journal of Computer and System Sciences*, 83(1):101–120, 2017.

[Hil96] J. Hillston. *A Compositional approach to performance modelling*. Cambridge University Press, 1996.

[HM95] Serge Haddad and Patrice Moreaux. Evaluation of high-level Petri nets by means of aggregation and decomposition. In *Proceedings of PNPM’95*, pages 11–20. IEEE, 1995.
[HM96] Serge Haddad and Patrice Moreaux. Asynchronous composition of high level Petri nets: A quantitative approach. In *Proceedings of APN'96*, volume 1091 of LNCS, pages 192-211. Springer, 1996.

[HM09] S. Haddad and P. Moreaux. *Stochastic Petri nets, in Petri nets: fundamental models, verification and applications*. Wiley, 2009.

[HS10] J. Hromkovič and G. Schnitger. On probabilistic pushdown automata. *Information and Computation*, 208(8):982-995, 2010.

[JHCK01] S. Jiang, Z. Huang, V. Chandra, and R. Kumar. A polynomial algorithm for testing diagnosability of discrete-event systems. *Transactions on Automatic Control*, 46(8):1318-1321, 2001.

[JL91] B. Jonsson and K. G. Larsen. Specification and refinement of probabilistic processes. In *Proceedings of LICS'91*, pages 266-277. IEEE, 1991.

[JMPC06] T. Jeron, H. Marchand, S. Pinchinat, and M. O. Cordier. Supervision patterns in discrete event systems diagnosis. In *Proceedings of WODES'06*, pages 262-268. IEEE, 2006.

[KEM06] A. Kučera, J. Esparza, and R. Mayr. Model checking probabilistic pushdown automata. *Logical Methods in Computer Science*, 2(1):12-21, 2006.

[KLC98] L. P. Kaelbling, M. L. Littman, and A. R. Cassandra. Planning and acting in partially observable stochastic domains. *Artificial Intelligence*, 101(1):99-134, 1998.

[KS60] John G Kemeny and James Laurie Snell. *Finite Markov chains*, volume 356. van Nostrand Princeton, 1960.

[KS16] S. Kiefer and A. P. Sistla. Distinguishing hidden Markov chains. In *Proceedings of LICS'16*, pages 66-75. ACM, 2016.

[Kur64] S.-Y. Kuroda. Classes of languages and linear-bounded automata. *Information and Control*, 7(2):207-223, 1964.

[LGS18] E. Lefaucheux, A. Giua, and C. Seatzu. Basis coverability graph for partially observable Petri nets with application to diagnosability analysis. In *Proceedings of PETRI NETS'18*, volume 10877 of LNCS, pages 164-183. Springer, 2018.

[MHC03] O. Madani, S. Hanks, and A. Condon. On the undecidability of probabilistic planning and related stochastic optimization problems. *Artificial Intelligence*, 147(1-2):5-34, 2003.

[Mos80] Y. N. Moschovakis. Studies in logic and the foundations of mathematics. In *Descriptive Set Theory*, volume 100, pages 11-64. Elsevier, 1980.
[MP09] C. Morvan and S. Pinchinat. Diagnosability of pushdown systems. In *Proceedings of HVC'09*, volume 6405 of LNCS, pages 21–33. Springer, 2009.

[MS72] A. R. Meyer and L. J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In *SWAT'72*, pages 125–129. IEEE, 1972.

[Mur89] T. Murata. Petri nets: properties, analysis and applications. *Proceedings of the IEEE*, 77(4):541–580, 1989.

[ND08] F. Nouioua and P. Dague. A probabilistic analysis of diagnosability in discrete event systems. In *Proceedings of ECAI'08*, volume 178 of FAIA, pages 224–228. IOS Press, 2008.

[Paz71] A. Paz. *Introduction to probabilistic automata*. Academic Press, 1971.

[Pie14] A. Piel. *Online event flow processing for complex behaviour recognition*. PhD thesis, Paris 13 University, France, 2014.

[Pnu77] A. Pnueli. The temporal logic of programs. In *Proceedings of FOCS'77*, pages 46–57. IEEE, 1977.

[POM] POMDP webpage. http://www.pomdp.org/.

[Pos46] E. L. Post. A variant of a recursively unsolvable problem. *Bulletin of the American Mathematical Society*, 52:264–268, 1946.

[PT87] C. H. Papadimitriou and J. N. Tsitsiklis. The complexity of Markov decision processes. *Mathematics of Operations Research*, 12(3):441–450, 1987.

[Put94] M. L. Puterman. *Markov decision processes: discrete stochastic dynamic programming*. Wiley, 1994.

[Å65] K.J. Åström. Optimal control of markov processes with incomplete state information. *Journal of Mathematical Analysis and Applications*, 10(1):174 – 205, 1965.

[Rac78] C. Rackoff. The covering and boundedness problems for vector addition systems. *Theoretical Computer Science*, 6(2):223 – 231, 1978.

[RSX12] N. Rampersad, J. Shallit, and Z. Xu. The computational complexity of universality problems for prefixes, suffixes, factors, and subwords of regular languages. *fundamenta informaticae*, 116(1-4):223–236, 2012.

[Sav70] W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. *Journal of Computer and System Sciences*, 4(2):177 – 192, 1970.
[SH14] A. Saboori and Ch. N. Hadjicostis. Current-state opacity formulations in probabilistic finite automata. *Transactions on Automatic Control*, 59(1):120–133, 2014.

[Sip06] M. Sipser. *Introduction to the theory of computation*. Thomson Course Technology, 2006.

[SLT98] M. Sampath, S. Lafortune, and D. Teneketzis. Active diagnosis of discrete-event systems. *Transactions on Automatic Control*, 43(7):908–929, 1998.

[SSL+95] M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis. Diagnosability of discrete-event systems. *Transactions on Automatic Control*, 40(9):1555–1575, 1995.

[SVA06] K. Sen, M. Viswanathan, and G. Agha. Model-checking Markov chains in the presence of uncertainties. In *Proceedings of TACAS’06*, volume 3920 of LNCS, pages 394–410. Springer, 2006.

[SZF11] A. P. Sistla, M. Zefran, and Y. Feng. Monitorability of stochastic dynamical systems. In *Proceedings of CAV’11*, volume 6806 of LNCS, pages 720–736. Springer, 2011.

[TT05] D. Thorsley and D. Teneketzis. Diagnosability of stochastic discrete-event systems. *Transactions on Automatic Control*, 50(4):476–492, 2005.

[TT07] D. Thorsley and D. Teneketzis. Active acquisition of information for diagnosis and supervisory control of discrete-event systems. *Discrete Event Dynamic Systems*, 17:531–583, 2007.

[Var96] M. Y. Vardi. *An automata-theoretic approach to linear temporal logic, in Logics for concurrency: structure versus automata*, volume 1083 of LNCS. Springer, 1996.

[Var99] M. Y. Vardi. Probabilistic linear-time model checking: An overview of the automata-theoretic approach. In *Proceedings of ARTS’99*, volume 1601 of LNCS, pages 265–276. Springer, 1999.

[YL02] T-S. Yoo and S. Lafortune. Polynomial-time verification of diagnosability of partially observed discrete-event systems. *Transactions on Automatic Control*, 47(9):1491–1495, 2002.

[ZL13] J. Zaytoon and S. Lafortune. Overview of fault diagnosis methods for discrete event systems. *Annual Reviews in Control*, 37(2):308–320, 2013.
<figure><img src="image_100.png" /></figure>
**Titre** : Le contrôle de l'information dans les systèmes probabilistes

**Mot clés** : Vérification de modèles, systèmes probabilistes, diagnostic, chaînes de Markov, observation partielle

**Resumé** : Le contrôle de l'information émise par un système a vu son utilité grandir avec la multiplication des systèmes communicants. Ce contrôle peut être réalisé par exemple pour révéler une information du système, ou au contraire pour en dissimuler une. Le diagnostic notamment cherche à déterminer, grâce à l'observa-

tion du système, si une faute a eu lieu au sein de celui-ci. Dans cet document, nous établissons des bases formelles à l'analyse des problèmes du diagnostic pour des modèles stochastiques. Nous étudions ensuite ces problèmes dans plusieurs cadres (fini/infini, passif/actif).

**Title** : Controlling Information in Probabilistic Systems

**Keywords** : Model checking, probabilistic systems, diagnosis, Markov chains, partial observation

**Abstract** : The control of the information given by a system has recently seen increasing importance due to the omnipresence of communicating systems, the need for privacy, etc. This control can be used in order to disclose an information of the system, or, oppositely, to hide one. Diagnosis for instance tries to determine from the observation produced by

the system whether a fault occurred within it or not. In this PhD, we study the diagnosis of stochastic systems through a model-based approach. The goal is to establish the decidability and optimal complexity of the decision problems and to build the adequate diagnosers. We consider these problems in multiple frameworks (finite/infinite, passive/active).