THÈSE DE DOCTORAT DE

L'UNIVERSITE DE RENNES 1
COMUE UNIVERSITE BRETAGNE LOIRE

Ecole Doctorale N°601
Mathématique et Sciences et Technologies
de l'Information et de la Communication

Spécialité : Informatique

Par

« Engel LEFAUCHEUX »

« Controlling Information in Probabilistic Systems »

Thèse présentée et soutenue à RENNES, le 24 Septembre 2018

Unité de recherche : IRISA, Equipe SUMO

**Rapporteurs avant soutenance :**

Stefan KIEFER, Associate Professor at Oxford

Antonin KUCERA, Professor at Masaryk University

**Composition du jury :**

Président : Sophie PINCHINAT Professeur à l'Université Rennes 1

Examinateurs :
Stefan KIEFER, Associate Professor at Oxford
Antonin KUCERA, Professor at Masaryk University
Nihal PEKERGIN, Professeur à l'Université Paris-Est Créteil
Wiesław ZIELONKA Professeur à l'Université Paris 7

Dir. de thèse : Nathalie BERTRAND, Chargée de recherche INRIA

Co-dir. de thèse : Serge HADDAD, Professeur de l'ENS Paris-Saclay
<figure><img src="image_1.png" /></figure>
*En essayant continuellement on finit par réussir. Donc : plus ça rate, plus on a de chance que ça marche.*

Les Shadoks

*(By trying over and over, one finally succeeds. Thus: the more you fail, the more you have a chance that it will work.)*
<figure><img src="image_2.png" /></figure>
# Contents

<table><tr><td>Contents</td><td>0</td></tr></table>

<table><tr><td>I</td><td>Introduction</td><td>23</td></tr></table>

<table><tr><td>1</td><td>General Introduction</td><td>25</td></tr></table>

<table><tr><td>2</td><td>Preliminaries</td><td>35</td></tr></table>

<table><tr><td>1</td><td>Framework</td><td>35</td></tr><tr><td>1.1</td><td>Descriptive set theory</td><td>35</td></tr><tr><td>1.2</td><td>Probabilistic Labelled Transition Systems</td><td>38</td></tr><tr><td>1.3</td><td>Partial observation</td><td>41</td></tr><tr><td>1.4</td><td>Fault and ambiguity</td><td>43</td></tr><tr><td>1.5</td><td>Which diagnosis for pLTS?</td><td>44</td></tr><tr><td>2</td><td>State of the art on diagnosis</td><td>49</td></tr></table>

<table><tr><td>II</td><td>Analysing information in passive systems</td><td>53</td></tr></table>

<table><tr><td>3</td><td>Semantical analysis of diagnosability</td><td>55</td></tr></table>

<table><tr><td>1</td><td>Diagnoser and diagnosability</td><td>57</td></tr><tr><td>1.1</td><td>FF-diagnosers</td><td>59</td></tr><tr><td>1.2</td><td>FA-diagnosers</td><td>61</td></tr><tr><td>1.3</td><td>IA-diagnosers</td><td>64</td></tr><tr><td>1.4</td><td>εFF-diagnosers</td><td>68</td></tr><tr><td>2</td><td>Relationships between diagnosability notions</td><td>71</td></tr><tr><td>3</td><td>Characterisation of diagnosability</td><td>77</td></tr><tr><td>3.1</td><td>The logic pathL</td><td>77</td></tr><tr><td>3.2</td><td>Logical characterisation of diagnosability</td><td>80</td></tr><tr><td>3.3</td><td>Non-expressivity results</td><td>82</td></tr><tr><td>4</td><td>Conclusion</td><td>87</td></tr></table>
4 Algorithmic analysis of the diagnosability of finite pLTS 89

<table><tr><td>1</td><td>Characterisations of diagnosability</td><td>90</td></tr><tr><td>1.1</td><td>Exact diagnosis</td><td>91</td></tr><tr><td>1.1.1</td><td>FF-diagnosability</td><td>93</td></tr><tr><td>1.1.2</td><td>FA-diagnosability</td><td>96</td></tr><tr><td>1.1.3</td><td>IA-diagnosability</td><td>99</td></tr><tr><td>1.2</td><td>Approximate diagnosis</td><td>100</td></tr></table>

<table><tr><td>2</td><td>Verification of the diagnosability</td><td>111</td></tr><tr><td>2.1</td><td>Decidability results and upper bounds</td><td>111</td></tr><tr><td>2.2</td><td>Hardness of Diagnosability.</td><td>113</td></tr><tr><td>2.2.1</td><td>Undecidability results</td><td>113</td></tr><tr><td>2.2.2</td><td>PSPACE-hardness of exact diagnosability</td><td>121</td></tr></table>

<table><tr><td>3</td><td>Diagnoser construction</td><td>124</td></tr><tr><td>3.1</td><td>FF-diagnoser</td><td>124</td></tr><tr><td>3.2</td><td>FA-diagnoser</td><td>125</td></tr><tr><td>3.3</td><td>IA-diagnoser</td><td>127</td></tr></table>

<table><tr><td>4</td><td>Conclusion.</td><td>128</td></tr></table>

5 Algorithmic analysis of the diagnosability of infinite pLTS 129

<table><tr><td>1</td><td>Diagnosability of probabilistic pushdown automata</td><td>130</td></tr><tr><td>1.1</td><td>Probabilistic pushdown automata.</td><td>130</td></tr><tr><td>1.2</td><td>Undecidability of diagnosability for POpPDA</td><td>133</td></tr></table>

<table><tr><td>2</td><td>Diagnosability of probabilistic visibly pushdown automata</td><td>138</td></tr><tr><td>2.1</td><td>Probabilistic visibly pushdown automata and diagnosis-oriented determinisation</td><td>138</td></tr><tr><td>2.2</td><td>Decidability of diagnosability for POpVPA</td><td>146</td></tr><tr><td>2.3</td><td>EXPTIME-hardness of the diagnosability for POpVPA</td><td>150</td></tr></table>

<table><tr><td>3</td><td>Diagnosability of infinite pLTS represented by stochastic Petri nets</td><td>153</td></tr><tr><td>3.1</td><td>Stochastic Petri nets</td><td>154</td></tr><tr><td>3.2</td><td>Undecidability of diagnosability for stochastic Petri nets</td><td>157</td></tr></table>

<table><tr><td>4</td><td>Conclusion.</td><td>160</td></tr></table>

III Controlling Information in Active Systems 163

6 Control of the degradation in probabilistic systems 165

<table><tr><td>1</td><td>Degradation of a probabilistic system</td><td>166</td></tr><tr><td>1.1</td><td>Degradation in passive systems</td><td>166</td></tr><tr><td>1.2</td><td>Controlled systems</td><td>169</td></tr></table>

<table><tr><td>2</td><td>Algorithmic analysis of degradation</td><td>174</td></tr><tr><td>2.1</td><td>Undecidability of the quantitative problems</td><td>174</td></tr><tr><td>2.2</td><td>Decidability of the Qualitative Problems</td><td>180</td></tr><tr><td>2.3</td><td>Safe active diagnosis problem under finite-memory strategies</td><td>186</td></tr></table>

<table><tr><td>3</td><td>Conclusion.</td><td>193</td></tr></table>
<table><tr><td>7</td><td>Opacity</td><td>195</td></tr><tr><td>1</td><td>Specification for Opacity</td><td>197</td></tr><tr><td>1.1</td><td>Opacity for Markov chains</td><td>197</td></tr><tr><td>1.2</td><td>Opacity for Markov Decision Processes</td><td>203</td></tr><tr><td>2</td><td>Maximisation with finite horizon</td><td>210</td></tr><tr><td>2.1</td><td>Deterministic strategies are sufficient</td><td>211</td></tr><tr><td>2.2</td><td>Undecidability of the disclosure and limit-sure disclosure problems</td><td>212</td></tr><tr><td>2.3</td><td>Decidability of the almost-sure disclosure problem</td><td>216</td></tr><tr><td>3</td><td>Minimisation with finite horizon</td><td>219</td></tr><tr><td>3.1</td><td>Deterministic strategies are not enough</td><td>220</td></tr><tr><td>3.2</td><td>The minimal disclosure value is computable</td><td>221</td></tr><tr><td>4</td><td>Fixed-horizon problems</td><td>224</td></tr><tr><td>4.1</td><td>Maximal disclosure</td><td>224</td></tr><tr><td>4.2</td><td>Minimal disclosure</td><td>229</td></tr><tr><td>5</td><td>Conclusion</td><td>233</td></tr><tr><td>8</td><td>Conclusion</td><td>235</td></tr><tr><td colspan="2">References</td><td>248</td></tr></table>
# Résumé en français

## Introduction

De nombreux systèmes critiques doivent satisfaire une spécification donnée. Cette spécification peut comprendre des critères de sécurité, des mesures de rendement ou d'autres conditions. Le processus de vérification, dont le but est de vérifier que le système satisfordit une spécification, peut être réalisé de différentes manières. Chacune ayant ses avantages et inconvénients, le choix de la méthode à utiliser dépend à la fois du système qui est étudié et de la spécification. Une des méthodes de vérification possibles est de réaliser des batteries de tests sur le système. Cette méthode est notamment utile lorsqu'on ne connaît pas le fonctionnement interne d'un système (le code d'un programme par exemple). Le choix des tests est alors basé sur la spécification [GTWJ03]. Au contraire, si l'on a accès au système complet, un modèle formel et opérationnel du système peut être construit. Ce modèle peut ensuite être étudié avec des méthodes dédiées.

La complexité de certains systèmes peut rendre la construction du modèle difficile. Celle-ci peut être accomplie grâce à une analyse du code du système, en réalisant des tests spécifiques dans certaines configurations du système permettant de déterminer comment il évolue (par exemple en surchargeant le processeur d'un ordinateur afin d'observer comment le programme réagit face à ce type de pression), etc. Quand elle est possible, cette approche a de nombreux avantages :

* Lors de la conception d'un système, si le prototype actuel n'accompli pas les objectifs voulus, il doit être modifié. Construire de nouveaux prototypes jusqu'à en obtenir un qui soit satisfaisant est coûteux. Il est plus économique et simple, de modifier un modèle jusqu'à ce que celui-ci satisfasse la spécification, et seulement alors de construire le système associé.

* Un modèle est souvent conçu afin de vérifier plusieurs propriétés. Si l'on désire vérifier de nouvelles propriétés à une date ultérieure, utiliser le modèle existant peut suffire. Dans le cas contraire, il n'est pas forcément nécessaire de construire entièrement un nouveau modèle. Il peut être suffisant de raffiner le modèle actuel, en y incorporant les informations appropriées. Utiliser un tel raffinement réduit fortement la complexité de la nouvelle étude.

* Enfin, si le modèle est suffisamment proche de la réalité, il permet une analyse
précise du système. Ce n’est pas le cas lors d’utilisation de batteries de tests, qui ne couvrent qu’une partie des situations possibles. Le même souci existe pour d’autres méthodes telles que la vérification statistique de modèle [Bar14].

Il existe de nombreux formalismes permettant de représenter un système. Plus celui-ci est complexe (représentation du temps, de l’aléatoire...), plus on peut modéliser de systèmes et de spécifications et plus l’étude de ce formalisme est difficile. Notamment, les formalismes possédant une composante probabiliste tels que les chaînes de Markov [KS60] ont de nombreuses applications. En effet, certains systèmes nécessitent des probabilités pour être représentés de façon précise. C’est le cas des systèmes contenant des comportements intrinsèquement probabilistes, par exemple un programme utilisant l’aléatoire afin de briser les symétries. Le hasard peut aussi être une conséquence de l’interaction du système avec l’environnement dont le comportement n’est pas entièrement prévisible. De plus, les probabilités permettent de représenter les incertitudes d’un modèle construit de façon approchée, par analyse statistique par exemple. Enfin, l’utilisation de probabilités élargit l’ensemble des propriétés qui peuvent être spécifiées en permettant de les quantifier. Par exemple, si un système (qui n’est pas un système critique) peut commettre des erreurs, mais que celles-ci ont peu de chances d’avoir lieu, ceci peut suffire pour satisfaire la spécification.

Le choix du formalisme utilisé détermine également quelles sont les informations accessibles aux utilisateurs : lorsque l’on construit un modèle, les différents évènements qui peuvent avoir lieu dans le système et leurs effets sont décrits ; certains de ces évènements ont lieu de façon interne et ne sont donc pas observables par un utilisateur extérieur. Le contrôle de l’information transmise par un système a vu son importance augmenter ces dernières années à cause de l’omniprésence des instruments électroniques communicants. Certaines informations du système doivent être maintenues secrètes (les mots de passe par exemple) alors que d’autres doivent être rendues publiques (les erreurs du système par exemple). Les problèmes liés à l’*observation partielle* peuvent être groupés en trois familles selon le type d’objectif à accomplir : (1) la planification sous observation partielle, (2) la dissimulation d’information à l’observateur et (3) la récupération d’information.

Le *diagnostic* est l'un des problèmes principaux de cette troisième catégorie. Le terme diagnostic vient du domaine médical dans lequel il désigne l'identification d'une maladie à partir de symptômes. Dans la communauté des systèmes à évènements discrets, cette identification est appliquée à des systèmes dynamiques (les centrales électroniques, les chaînes de production...). Dans cette approche, une exécution du système est observée et on essaie de détecter si un évènement particulier, appelé la *faute*, a eu lieu. La faute ne représente pas forcément une défaillance du système, cependant cette terminologie est utilisée principalement car une irrégularité est l'un des évènements les plus importants à détecter durant une exécution. En effet, celles-ci menacent la sureté et la disponibilité du système. Ceci peut provoquer des dégâts catastrophiques à la fois en termes économiques et humains. L'étude des fautes est également justifiée du fait que tout système peut, et en fait va, faire une erreur. En effet, les systèmes que l'on construit sont de plus en plus complexes et ont des interactions de plus en plus
importantes avec l'environnement. Il est donc extrêmement difficile de ne pas introduire d'erreurs lors de la conception d'un système et il est presque impossible de prédire toutes les actions que l'environnement aura sur le système. Enfin, des fautes auront lieu à cause du vieillissement des composants du système.

Comme les fautes sont dangereuses, inévitables et potentiellement difficiles à identifier, une méthode automatique de détection est nécessaire. Par ailleurs, cette méthode doit être précise car stopper un système à cause d'un faux positif est coûteux et elle doit être réactive de façon à ce que les fautes soient repérées avant tout dommage sérieux. En réaction à une faute, on peut soit (1) essayer d'optimiser le comportement du système durant la période préalable à la faute [EMT16], ce qui est particulièrement utile pour des systèmes dont les composants sont régulièrement remplacés, ou (2) essayer de détecter la faute de façon à réagir à son occurrence. Comme l'on désire réagir aussi vite que possible, prédire l'occurrence de la faute permettrait de réagir avant même que le système ne commette l'erreur. Cette question est étudiée dans le contexte des problèmes de prédiction [GL09]. Cependant, il est rare qu'un système permette une pré-diction efficace des fautes. Détecter les fautes *a posteriori* est plus plausible. L'étude du diagnostic soulève deux problèmes importants : comment décider si un système est diagnostiquable, ce qui est appelé *diagnostiquabilité*, et, dans le cas positif, comment construire un *diagnostiqueur* la fonction réalisant le diagnostic et qui satisferait potentiellement des conditions supplémentaires sur la taille de la mémoire utilisée, le délai de détection, etc. Dans le domaine des systèmes à évènements discrets, le diagnostic a été défini initialement pour des systèmes finis tels que les *systèmes à transitions étiquetées partiellement observables* [SSL+95] puis a été étendu à de nombreux modèles complexes (e.g. les réseaux de Petri [CGLS12, BHSS18], les systèmes à pile [MP09], etc.) et cadres (e.g. décentralisés [DLT00], distribués [HC94]). De plus, plusieurs travaux rassemblés sous le nom diagnostic actif étudient comment contrôler le système pour en assurer la diagnostiquabilité [SLT98, TT07, CT08, CP09].

Notre but dans ce document est d'étudier le diagnostic de systèmes probabilistes. Par conséquent, la première question qui se doit d'être abordée est le choix du formalisme (probabiliste) à utiliser. On doit notamment déterminer si, en plus des probabilités, le modèle est partiellement contrôlable, s'il peut représenter une infinité d'états différents ou s'il doit décrire efficacement des comportements concurrents. Par ailleurs, comme le diagnostic est un problème d'observation partielle, le modèle doit indiquer quelle observation est associée à une exécution.

Dans un deuxième temps, il va nous falloir établir les différents problèmes que nous allons étudier. De nombreuses notions de diagnostic ont déjà été définies, chacune accomplissant un objectif différent. Nous devons donc présenter un ensemble cohérent de notions qualitatives et quantitatives appropriées englobant les définitions importantes déjà établies. De plus, les définitions formelles des problèmes que nous étudions doivent être choisies prudemment. En effet, comme ces problèmes mélangent observation partielle, probabilités et, dans certains cas, contrôle, ils ont de fortes chances d'être indécidables. Une petite modification dans la définition peut faire la différence entre un problème pouvant se résoudre efficacement et un problème indécidable.

Une fois les notions de diagnostic définies, notre but sera d'établir les complexités
précises de la diagnostiquabilité et de la synthèse des diagnostiqueurs pour chaque no-
tion, ceci, dans les différents formalismes que nous aurons choisis. Nous chercherons
également à déterminer comment modifier un système afin qu’il devienne diagnosti-
quable. Ceci donne deux approches: une approche passive, de vérification, et une
active, de contrôle.

Définitions du modèle et du diagnostic

Le modèle le plus utilisé dans ce document est celui des systèmes probabilistes à trans-
sitions étiquetées partiellement observables (dont le nom anglais est abrégé en pLTS).
Un pLTS est formellement défini par un tuple (Q, q₀, Σ, T, **P**) où Q est un ensemble
dénombrable d'états, q₀ est l'état initial, Σ est un ensemble d'évènements pouvant avoir
lieu dans le système, T est un ensemble de transitions indiquant comment un évènement
de Σ affecte l'état courant du système et **P** donne la probabilité de chaque transition.
Afin de représenter l'observation partielle du système, l'ensemble d'évènements Σ est
partitionné entre évènements observables Σ₀ et évènements inobservables Σ_u.

Une exécution $\rho$ du système est une suite d'états et de transitions liant deux états
consécutifs. Grâce à $\mathbf{P}$, on peut attribuer une probabilité à toute exécution finie. En-
suite, et en utilisant des résultats de théorie de la mesure, on peut définir une mesure
de probabilité sur l'ensemble des exécutions infinies. Par ailleurs, à toute exécution on
peut associer une observation qui est la projection sur $\Sigma_o$ de la séquence d'évènements
étiquetant ses transitions. On suppose que le pLTS est convergent ce qui signifie que
toute exécution infinie possède une observation infinie.

**Example 0.1.** Considérons le pLTS représenté dans la figure 0.1. Une utilisation
normale de la machine à café est donnée par exemple par l'exécution $\rho = q_0$ **pièce**
$q_1$ **sucre** $q_1$ **café** $q_0$. Cependant dans l'état $q_1$ une erreur représentée par l'évènement
'f' peut avoir lieu, menant à l'état $f_1$ à partir duquel on ne peut plus obtenir de café.
Cet évènement a cependant une faible probabilité d'avoir lieu. L'exécution normale
$\rho$ a pour probabilité le produit des probabilités des transitions empruntées, c'est-à-dire
$1 \times 0.29 \times 0.7 = 0.203$. Un comportement fautif de la forme $\rho' = q_0$ **pièce** $q_1$ **sucre** $q_1$
$f$ $f_1$ a probabilité 0.0029 d'avoir lieu.

Comme dans l'exemple précédent, les exécutions du modèle peuvent être fautives
ou correctes. Ceci est indiqué par la présence (ou absence) de la faute (l'évènement
f) à l'intérieur de celle-ci. Le but du diagnostic est d'utiliser l'observation d'une exé-
cution pour déterminer si celle-ci est correcte ou fautive. Comme plusieurs exécutions
différentes peuvent posséder la même observation, une exécution est surement fautive
данne (resp. surement correcte) si toute les exécutions partageant la même observation sont
fautives (resp. correctes). Sinon, l'exécution est ambiguë. Si une exécution est surement
correcte ou surement fautive, un verdict peut être rendu. Le souci vient des exécutions
ambiguës.
<figure><img src="image_3.png" /><figcaption>Figure 0.1: Un pLTS représentant une machine à café. $q_0$ est l'état initial, ce qui est représenté par la flèche entrante. Les transitions entre les états sont étiquetées par l'évènement provoquant cette transition ainsi que par la probabilité que cette transition soit prise.</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Figure 0.2: Résumé des variantes du diagnostic exact.</figcaption></figure>

Plusieurs définitions de diagnostiquabilité peuvent être proposées. Pour des systèmes non probabilistes, la définition originelle de diagnostiquabilité requiert que toute séquence fautive devienne finalement surement fautive [SSL+95]. Ainsi, toute faute est finalement détectée. Cette condition est trop forte pour des systèmes probabilistes car un système pourrait être déclaré non diagnostiquable à cause d'une exécution de probabilité nulle. Une adaptation possible est de demander qu'avec probabilité 1 une exécution fautive devienne surement fautive [TT05]. Nous appelons cette notion FF-diagnostiquabilité. Cette notion ignore l'ambiguïté des exécutions correctes. Le système peut donc rester ambigü infiniment, ce que l'on peut vouloir éviter. La diagnostiquabilité peut être étendue aux exécutions correctes en requérant que la probabilité des séquences ambigües (fautives et correctes) converge vers 0. Cette notion se nomme FA-diagnostiquabilité (le A signifie "all" alors que F signifie fautif). Pour ces deux notions de diagnostiquabilité, l'ambiguïté est résolue sur des exécutions finies (le premier F signifi-
ant justement fini). Si l'on autorise l'ambiguïté à être résolue lorsque la séquence devient infinie, la FF- et la FA-diagnostiquabilité deviennent la IF- et la IA-diagnostiquabilité. Les quatre notions sont résumées dans la figure 0.2.

Ces notions de diagnostiquabilité ne permettent aucune erreur de verdict. Ce sont des notions dites exactes. Il peut cependant être intéressant d'affaiblir cette condition. Considérons le pLTS de la figure 0.3. Toute exécution fautive est ambiguë. Cependant, de par le choix des probabilités, une exécution fautive a plus de chances de produire un 'b' qu'un 'a' et inversement pour les exécutions correctes. Par conséquent, en comparant le nombre de 'b' et de 'a' dans l'observation, on peut déduire avec forte probabilité si l'exécution est correcte ou fautive. Nous considérons donc plusieurs notions de diagnostiquabilité dites approchées dans ce document (l'une d'entre elle ayant été introduite dans [TT05] et pour laquelle seule une condition suffisante avait été donnée).

<figure><img src="image_5.png" /><figcaption>Figure 0.3: Quand un diagnostic approché est nécessaire.</figcaption></figure>

La formalisation du modèle et des notions de diagnostiquabilité est réalisée dans le chapitre 2. Nous expliquons maintenant comment ces notions de diagnostiquabilité peuvent être étudiées.

## Vérification de la diagnostiquabilité

L'étude d'un problème commence par une analyse sémantique (développées dans le chapitre 3) de façon à bien le comprendre. Dans le cas de la diagnostiquabilité, cette analyse sémantique prend tout d'abord la forme d'une étude des liens entre les différentes notions de diagnostiquabilité. Certains sont assez clairs. Par exemple, les notions de FA- et IA-diagnostiquabilité considèrent les exécutions fautives ainsi que les exécutions correctes alors que FF- et IF-diagnostiquabilité ne considèrent que les notions fautives. Donc un système FA-diagnostiquable (resp. IA-) est FF-diagnostiquable (resp. IF). Similairement, observer des exécutions infinies donne plus d'informations que leurs préfixes finis, donc les notions de diagnostiquabilité finies impliquent leur équivalent infini. De façon intéressante, si on ne s'intéresse qu'aux exécutions fautives, on a une réciproque partielle : si le système est à branchement fini, la FF-diagnostiquabilité est équivalente à la IF-diagnostiquabilité.

La deuxième étape d'une analyse sémantique est de déterminer des caractérisations efficaces des notions étudiées. Avoir des contraintes sur le système étudié permet d'avoir
des caractérisations plus simple. Nous étudions donc d'abord le cas des systèmes ayant
un nombre d'états fini.

Étude des systèmes finis

Les systèmes représenté par un modèle ayant un nombre d'états fini possèdent des pro-
priétés extrêmement utiles pour le diagnostic. Notamment, on sait qu'avec probabilité 1,
une exécution atteint une composante strictement connexe terminale (CSCT) du graphe
induit par le pLTS. Comme la diagnostiquabilité s'intéresse à des comportements "avec
probabilité 1", l'étude peut se concentrer sur les CSCT du système. Par ailleurs, il
existe une méthode simple de déterminisation de l'automate induit par le pLTS. Cette
déterminisation est très utile pour caractériser l'ambiguïté d'une exécution. En effet,
l'automate déterminisé associe à chaque séquence d'observations l'ensemble d'états du
pLTS pouvant être atteint par des exécutions associées à cette séquence. Par conséquent,
en supposant sans perte de généralité que les états du pLTS sont partitionnés entre états
fautifs (atteint par une exécution fautive) et états corrects, une exécution surement fau-
tive est une exécution dont la séquence d'observation mène à un état de l'automate
déterminisé ne possédant que des états fautifs. Observons ceci sur un exemple. La
figure 0.4 représente un pLTS qui est FF-diagnostiquable ainsi que IA-diagnostiquable
mais qui n'est pas FA-diagnostiquable. En effet, toute faute est suivie finalement par
un 'b' révélant la faute. L'observation a<sup>ω</sup> est donc au contraire associée à une exécution
surement correcte, mais tout préfixe fini de cette exécution est ambigu. Donc toute
exécution correcte finie est ambiguë.

<figure><img src="image_6.png" /><figcaption>Figure 0.4: Un pLTS qui est IA et FF-diagnostiquable mais n'est pas FA-diagnostiquable.</figcaption></figure>

Le pLTS de la figure 0.4 respecte la partition entre états fautifs (les $f_i$) et états corrects (les $q_i$) mentionnée plus tôt. Nous représentons l'automate déterminisé induit en figure 0.5. Un état de cet automate atteint par l'observation $w$ contient deux ensembles : nous séparons les états du pLTS pouvant être atteint par une exécution correcte de ceux atteints par une exécution fautive, de plus on ne considère que les exécutions terminant par un évènement observable. Les états doublement entourés ne contiennent soit aucun état correct, soit aucun état fautif. Les observations menant à ces états correspondent donc à des exécutions non ambiguës.

En observant cet automate et au vu de notre remarque antérieure sur les CFCT, on
pourrait penser que le diagnostic de ce système est simple étant donné que le seul état
pour lequel le verdict ne peut être rendu ne fait pas parti d'une CFCT de l'automate
déterminisé. Cependant, si les CFCT sont atteintes avec probabilité 1 dans le pLTS, ce
<figure><img src="image_7.png" /><figcaption>Figure 0.5: L'automate déterminisé associé au pLTS de la figure 0.4.</figcaption></figure>

n'est pas forcément le cas dans l'automate déterminisé. Afin de regagner cette propriété tout en conservant les informations données par l'automate déterminisé, on réalise le produit synchronisé sur les évènements observables du pLTS et de l'automate. Celui-ci est représenté dans la figure 0.6.

<figure><img src="image_8.png" /><figcaption>Figure 0.6: Produit synchronisé du pLTS de la figure 0.4 et de son automate déterminisé. Les probabilités sont omises pour faciliter la lisibilité.</figcaption></figure>

Le produit synchronisé conserve le comportement probabiliste du système. C'est-à-dire, qu'il y a une bijection entre les exécutions du pLTS et celles du produit, les deux exécutions ayant la même observation, correction et probabilité. Par conséquent, la diagnostiquabilité du pLTS est équivalente à celle de son produit synchronisé. Par contre, ce dernier possède plus d'informations car la composante des états correspondants à l'automate déterminisé indique si une exécution finissant dans cet état est surement fautive, surement correcte ou ambigüe. Observons les CFCT de ce système. Il y en a 3, toutes réduites à un état: $(q_1, s_1)$, $(f_2, s_2)$ et $(f_2, s_4)$. Les ensembles $s_2$ et $s_4$ impliquent que les exécutions atteignant la deuxième et troisième CFCT sont surement fautives. $s_1$ en revanche, montre une ambiguïté dans la première CFCT. Comme $s_1$ est associé à un état correct $q_1$, cette ambiguïté n'existe que pour des exécutions correctes. Ce produit synchronisé montre donc que le pLTS est bien FF-diagnostiquable, mais pas FA-diagnostiquable.
En utilisant le produit synchronisé, une caractérisation peut être établie pour toutes les notions de diagnostiquabilité exacte<fnref n="1" />. Cette caractérisation peut ensuite être vérifiée en espace polynomial. La principale source de complexité de l'algorithme est la déterminisation qui produit un automate de taille au plus exponentielle en la taille du pLTS. Utilisant une réduction du problème de l'universalité du langage généré par un automate non déterministe, on montre que les notions de diagnostiquabilité exacte sont PSPACE- difficiles. Elles sont donc PSPACE-complètes pour les pLTS finis.

En ce qui concerne le diagnostic approché, seule une notion, construite en modifiant
subtilement celle introduite dans [TT05], est décidable. La décidabilité est montrée en
réduisant le problème à un nombre au plus quadratique d'instances du problème de
la distance 1 de deux chaînes de Markov étiquetées, problème qui a été montré décid-
able en PTIME dans [CK14]. Ceci donne *in fine* un algorithme PTIME. Les résultats
d'indécidabilité quant à eux sont montrés grâce à des réductions du problème du vide
des automates probabilistes [Paz71].

Construction des diagnostiqueurs

Le but de l'étude du diagnostic est la détection automatique de la faute. Cette détection est réalisée par un diagnostiqueur qui observe le système et donne son verdict. Formelle-ment, un diagnostiqueur est une fonction D : Σ*₀ → {?, ⊤, ⊥}. Un verdict ? ne fournit aucune information, un verdict ⊤ déclare l'exécution actuelle fautive et un verdict ⊥ fournit une information relative à la correction de l'exécution. Un diagnostiqueur a trois caractéristiques principales: verdict, sureté et réactivité. Le verdict formule la nature de l'information que le diagnostiqueur doit fournir au cours d'une exécution (détection de fautes uniquement, ou aussi de la correction de l'exécution par exemple). La sureté formule quand le diagnostiqueur peut émettre son verdict. Dans le cas du diagnostic exact, la sureté requiert que si le diagnostiqueur produit un verdict, celui-ci est correct. Ce n'est pas forcément le cas dans le cadre du diagnostic approché. La réactivité ex-prime à quelle régularité le diagnostiqueur doit fournir des informations sur le statut de l'exécution courante.

Les notions de diagnostiquabilité ayant été présentées sous la forme d'un problème de décision, la troisième étape de l'étude sémantique consiste à établir le lien entre chaque notion de diagnostiquabilité et l'existence d'un diagnostiqueur avec un verdict, une sureté et une réactivé donnés. La preuve permettant d'établir le lien entre diagnostiquabilité et existence d'un diagnostiqueur est constructive. Par conséquent, nous disposons d'un algorithme permettant de construire automatiquement un diagnostiqueur pour chaque système diagnostiquable. Cependant, le diagnostiqueur en question utilise une mémoire non bornée. En vue d'une possible implémentation, il est préférable de pouvoir se limiter à des diagnostiqueurs à mémoire finie. Un tel diagnostiqueur est représenté par un automate déterministe sur Σ₀ enrichi d'un verdict (*M*, Σ₀, *m*₀, up, *D*<sub>*fm*</sub>) où *M* est un ensemble d'états de la mémoire avec *m*₀ l'état initial, up est la fonction de tran-

<footnote n="1">¹Pour la IA-diagnostiquabilité, une information supplémentaire est nécessaire. L'automate déterminisé que l'on construit possède un troisième ensemble permettant de partitionner les états fautifs en deux groupes, selon le moment où la faute a été commise.</footnote>
sition, mettant à jour la mémoire du diagnostiqueur et $D_{fm}: M \to \{?, \top, \bot\}$ associe un verdict à chaque état de la mémoire. La taille d'un tel diagnostiqueur à mémoire finie est le nombre d'états de la mémoire qu'il possède. La fonction de mise à jour peut être étendue à des séquences d'observations de façon inductive : pour $\varepsilon$ le mot vide $w \in \Sigma_o^*$ et $a \in \Sigma_o$, $up(m, \varepsilon) = m$ et $up(m, wa) = up(up(m, w), a)$. Si un diagnostiqueur à mémoire finie n'est pas un diagnostiqueur selon la définition établie plus haut, il en induit un qui est définit par $D(w) = D_{fm}(up(m_0, w))$ pour tout $w \in \Sigma_o^*$.

**Example 0.2.** La figure 0.7 représente un diagnostiqueur à mémoire finie qui ne fournit aucune information (verdict ?) initialement puis déclare une faute (verdict $\top$) dès qu'un 'b' est observé.

Considérons le pLTS de la figure 0.4. La faute est identifiée dès qu'un 'b' est observé. Par conséquent, le diagnostiqueur induit par le diagnostiqueur à mémoire finie de la figure 0.7 peut être utilisé pour détecter les fautes de ce pLTS. Ce diagnostiqueur ne détecte pas les exécutions correctes, il correspond à la notion de FF-diagnostiquabilité. On l'appelle donc un FF-diagnostiqueur.

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

Figure 0.7: Exemple de diagnostiqueur à mémoire finie. Le verdict donné par $D_{fm}$ dans un état de la mémoire est indiqué sous l'état.

Pour toute notion de diagnostic exact, un diagnostiqueur peut être construit à partir de l'automate déterminisé qui a été utilisé pour vérifier la diagnostiquabilité. Le diagnostiqueur peut donc avoir une taille exponentielle. C'est malheureusement inévitable : certains pLTS n'admettent pas de diagnostiqueurs de taille sous-exponentielle. Pour le diagnostic approché, aucune borne sur la taille de la mémoire n'existe dans le cas général. En d'autres mots, on ne peut pas toujours construire de diagnostiqueur à mémoire finie. Pire encore, déterminer s'il existe un diagnostiqueur à mémoire finie est un problème indécidable.

Ces résultats, reposant fortement sur la limitation à un nombre d'états finis pour le modèle, sont rassemblés dans le chapitre 4. Nous allons maintenant discuter de ce qui peut être fait pour lever cette restriction.

## Étude des systèmes infinis

De nombreux systèmes réels nécessitent un nombre infini d'états pour être décrit de façon précise. Afin de rendre une analyse possible, on ne peut pas utiliser directement un pLTS infini. On a besoin d'un modèle de plus haut niveau, capable de représenter de façon finie un pLTS infini. De nombreux formalismes permettent ceci. Les automates à
pile et les réseaux de Petri notamment représentent deux classes orthogonales de LTS infinis. Le choix du formalisme est très important car plus un formalisme est expressif, plus les problèmes seront compliqués à résoudre. Les automates à pile et les réseaux de Petri sont trop puissants par exemple, toutes les notions de diagnostiquabilité exacte étant indécidables dans ces deux formalismes.

Nous nous sommes donc intéressés à un formalisme légèrement plus faible, plus précisément une sous-classe des automates à pile : les automates à pile visibles. Les automates à pile sont des automates enrichis d'une pile qui leur permet de conserver de l'information au cours d'une exécution. Les transitions de l'automate disponibles dépendent de l'état courant ainsi que de la tête de la pile. Une fois sélectionnée, une transition peut soit (1) modifier la tête de la pile (transition locale), (2) ajouter un nouveau symbole en tête de pile (transition d'empilement) ou (3) retirer la tête de pile actuelle, s'il y en a une (transition de dépilage). La sémantique d'un automate à pile probabiliste est un pLTS infini dont les états représentent l'état actuel de l'automate à pile ainsi que le contenu de la pile. Ce pLTS peut être infini car la taille de la pile n'est pas bornée. La restriction aux automates à pile visible requiert que l'ensemble des évènements est partitionné selon le type de transitions auquel ils correspondent, $\Sigma = \Sigma_{\#} \cup \Sigma_{\flat} \cup \Sigma_{\natural}$. Les évènements de $\Sigma_{\#}$, $\Sigma_{\flat}$ et $\Sigma_{\natural}$ sont respectivement associés à des transitions d'empilement, de dépilage et des transitions locales. De plus, $\Sigma_{\#} \cup \Sigma_{\flat} \subseteq \Sigma_{\text{o}}$. Un observateur voit donc quand un élément est ajouté ou retiré de la pile. La taille de la pile est donc connue à tout moment, son contenu par contre peut être inconnu.

**Example 0.3.** La figure 0.8 donne un exemple d'automate à pile probabiliste. Une exécution démarre dans l'état $q_0$ avec pour contenu de pile le symbole $\perp_0$. Celui-ci est appelé élément de fond de pile et ne peut pas être retiré ou modifié. Le reste de la pile n'est composé que d'un certain nombre de $\gamma$. La seule transition d'empilement est in et les transitions de dépilage sont out et abort.

Ce système reçoit un certain nombre d'ordres qu'il note dans la pile. Puis il commence à servir ses clients, chaque ordre reçu reçoit donc une réponse soit sous la forme d'un *out*, soit de façon fautive sous la forme d'un *abort*. Enfin, il retourne à son point initial. Les deux exécutions données en exemple présentent un comportement correct et fautif pour deux ordres reçus.

Il y a une claire partition entre transitions d'empilement, de dépilage et locales. Par conséquent si in, out et abort sont observables, cet automate à pile probabiliste est visible.

La restriction aux automates à pile probabilistes visibles limite peu l'expressivité du formalisme, mais donne des propriétés supplémentaires utiles au modèle, notamment elle permet de réaliser une déterminisation de l'automate à pile. On ne peut cependant pas faire comme dans les systèmes finis et étudier les CFCT du produit du modèle et de son automate déterminisé. Notamment car ces CFCT peuvent ne pas exister (cas où aucune borne sur la taille de la pile n'existe). Une autre forme de caractérisation de la diagnostiquabilité est donc nécessaire. Pour ce faire, une logique nommée *pathL* a été introduite et des formules caractérisant plusieurs notions de diagnostiquabilité exacte ont été établi. Ensuite, en utilisant notamment l'automate à pile déterminisé, ces formules ont pu être traduites en des formules de pLTL, une logique connue et pour laquelle des
<figure><img src="image_10.png" /><figcaption>Figure 0.8: Un automate à pile probabiliste et deux de ses exécutions finies.</figcaption></figure>

algorithmes de vérification existe pour les automates à pile. En utilisant ces résultats nous avons obtenu des algorithmes EXPSPACE pour les notions de diagnostiquabilité caractérisées (la borne inférieure prouvée étant EXPTIME). La FA-diagnostiquabilité, qui requiert la détection des séquences fautives et correctes en temps fini n'a cependant pas pu être caractérisée. En fait, des résultats de non-expressivité ont été établi pour montrer que cette notion ne pouvait pas être exprimée en pathL.

Ces résultats sont développés dans le chapitre 5.

Contrôle d'un système

Les pLTS donnent une représentation passive d'un système. Ainsi, étudier le diagnostic sur des pLTS est purement un travail de vérification. Il ne permet donc pas de questionner efficacement comment modifier le système afin de le rendre diagnostiquable. Afin d'étudier ce genre de problème, on ajoute une forme de contrôle dans le pLTS. Le formalisme obtenu, appelé CLTS partitionne l'ensemble des évènements observables en évènements contrôlables $\Sigma_c$ et évènements incontrôlables $\Sigma_e$. Après chaque observation, un contrôleur choisit un ensemble d'évènements autorisés excluant potentiellement certains évènements contrôlables. Ceci limite donc les transitions pouvant être prise par le système.

**Example 0.4.** Un exemple de CLTS est représenté dans la figure 0.9. Initialement, deux évènements de poids 1 sont possibles et forcément autorisés par le contrôle. Par
<figure><img src="image_11.png" /><figcaption>Figure 0.9: Un exemple de CLTS. Les probabilités sont remplacées par des poids. Le seul évènement contrôlable est ‘b’.</figcaption></figure>

conséquent chacune a une probabilité $\frac{1}{2}$ d'être prise. En $q_1$, 'b' peut être interdit par le contrôleur. Si c'est le cas, la transition étiquetée par 'a' est choisie avec probabilité 1.

Ainsi, si le contrôleur autorise tous les évènements en permanence, l'exécution $q_0 u q_1 a q_1 b q_2$ a probabilité $1/8$. S'il interdit 'b' en permanence, cette exécution a probabilité 0. Finalement, s'il n'autorise un 'b' qu'après l'observation d'un 'a', l'exécution a probabilité $1/4$.

Le contrôle est formellement défini par l'utilisation de stratégies. Une stratégie $\pi$: $\Sigma_o^* \mapsto \text{Dist}(2^\Sigma)$ est une fonction associant à une séquence d'observations une distribution probabiliste sur les ensembles d'évènements autorisés. Par ailleurs, si l'ensemble $\Sigma^\bullet$ est sélectionné par la stratégie, on a $\Sigma_u \cup \Sigma_e \subseteq \Sigma^\bullet$. En d'autres mots, la stratégie ne peut exclure que des évènements contrôlables. Un CLTS $C$ équipé d'une stratégie $\pi$ génère un pLTS infini dénoté $C_\pi$.

**Example 0.5.** Considérons le CLTS $C$ représenté dans la figure 0.9. Il y a deux ensembles d'évènements possibles à autoriser: $\Sigma$ et $\Sigma \setminus \{b\}$ que nous abrigeons en $\Sigma^-$. Définissons la stratégie $\pi$ par $\pi(a^n) = p_n \cdot \Sigma^- + r_n \cdot \Sigma$ avec $p_n + r_n = 1$ pour tout $n \in \mathbb{N}$ et $\pi(w) = 1 \cdot \Sigma$ sinon. C'est-à-dire, après avoir observé $a^n$, avec probabilité $p_n$ l'ensemble $\Sigma^-$ est autorisé par la stratégie et avec la probabilité complémentaire $\Sigma$ est autorisé. Le pLTS généré $C_\pi$ est infini. Une partie de celui-ci est représenté en figure 0.10.

Expliquons la distribution de probabilité à la sortie de la configuration $(\varepsilon, q_1, \Sigma)$. Les deux transitions sortant de $q_1$ ont le même poids, comme elles sont toutes deux autorisées par la stratégie, la probabilité de chaque transition est $\frac{1}{2}$. Comme 'a' et 'b' sont observables, un nouveau contrôle est choisi. Si un 'b' est observé, de par la définition de $\pi$, le nouveau contrôle est $\Sigma$. Par contre, si un 'a' est observé, le nouveau contrôle est $\Sigma^-$ avec probabilité $p_1$ et $\Sigma$ sinon. Il y a donc trois transitions sortantes de $(\varepsilon, q_1, \Sigma)$ ayant pour probabilité respectivement 0.5, 0.5$p_1$ et 0.5$r_1$.

Nous discutons maintenant des questions abordées pour les CLTS.
<figure><img src="image_12.png" /><figcaption>Figure 0.10: Un pLTS obtenu en contrôlant le CLTS de la figure 0.9.</figcaption></figure>

## Diagnostic actif et dégradation

Lorsque l'on étudie le diagnostic d'un CLTS, la question n'est plus si le CLTS est diagnostiquable (ce qui n'a techniquement pas de sens en soi) mais s'il existe une stratégie telle que le pLTS induit est diagnostiquable. Cette problématique a été étudiée pour des systèmes probabilistes dans $[BFH^+14]$. Afin de déterminer s'il existe une stratégie satisfaisant la notion de diagnostiquabilité qu'ils étudient, ils traduisent le problème du diagnostic en une condition de Büchi pour un processus de décision Markovien partiellement observable. Le problème peut ensuite être résolu avec des techniques connues. La stratégie obtenue a de bonnes propriétés : elle est notamment ce qu'on appelle "basée sur la croyance", ce qui implique entre autres que le pLTS généré est fini.

Leur travail soulève un souci important : afin de rendre le système diagnostiquable, la stratégie peut faire des choix problématiques comme forcer l'occurrence d'une faute. Bien que ceci permette de détecter le mauvais comportements du système, cela va à l'encontre du but initial du diagnostic qui est de pouvoir utiliser un système fonctionnel. Ils introduisent donc le problème du diagnostic sûr. Celui-ci demande s'il existe une stratégie satisfaisant à la fois le diagnostic et assurant une probabilité positive aux exécutions correctes. Cette notion est malheureusement indécidable dans le cas général et un algorithme NEXPTIME est donné dans le cadre limité des stratégies à mémoire finie (i.e. pour lesquelles le pLTS engendré est fini).

Continuant sur cette idée, nous avons introduit de nouvelles notions permettant
de mesurer la dégradation du système. Ces notions ne s'assurent pas que le système reste correct infiniment avec une probabilité positive comme le diagnostic sûr, mais demandent que, si faute il y a, celle-ci puisse être retardée fortement. Le diagnostic longtemps correct et le diagnostic fortement résistant sont deux telles notions, mesurant différemment le délai à imposer à l'occurrence de la faute. Ces deux notions sont impliquées par le diagnostic sûr et sont différentes quand appliquées à des pLTS infinies (i.e. il existe des pLTS infinis satisfaisant chacune des notions sans satisfaire l'autre).

Parmi les notions de dégradation que nous avons introduites, certaines sont quantitatives, d'autres, comme le diagnostic longtemps correct et le diagnostic fortement résistant, sont qualitatives. Les notions quantitatives sont toutes indécidables, même limitées à des stratégies à mémoire finie. Au contraire, des algorithmes ont pu être établis pour les notions qualitatives. Ceux-ci procèdent en deux étapes. Tout d'abord et en enrichissant les états du CLTS comme fait dans le cas passif grâce à une détermination du CLTS, on identifie l'ensemble des états du CLTS enrichi que l'on peut visiter tout en respectant la diagnostiquabilité. Cette méthode permet en fait de construire la stratégie la plus permissive assurant la diagnostiquabilité du système. Dans un second temps, on étudie le CLTS réduit aux états accessibles sous cette stratégie et on identifie comment restreindre la stratégie afin de rester suffisamment longtemps dans une exécution correcte. Cette étude peut se réaliser en EXPTIME. Le diagnostic actif étant EXPTIME-difficile, les notions qualitative de dégradation introduites sont donc EXPTIME-complètes dans le cas général. Nous avons également montré comment réduire à EXPTIME la complexité du diagnostic sûr limité aux stratégies à mémoire finie. Sous cette restriction, le diagnostic sûr est donc EXPTIME-complet également.

Ces travaux sont présentés dans le chapitre 6.

## Assurer l'opacité d'un système

Dans cette thèse, le diagnostic est le problème d'observation partielle auquel nous avons prêté le plus d'attention. D'autres problèmes d'observation partielle sont également intéressants à étudier, notamment l'opacité que nous étudions formellement dans le chapitre 7. Le but de l'opacité est de cacher une information à l'observateur. En conséquent, sur bien des aspects cette notion apparaît comme un dual du diagnostic.

Formellement, un système possède deux types d'exécutions : publiques ou secrètes. Pour déterminer, si une exécution est secrète, on pourrait faire comme pour le diagnostic et utiliser un évènement particulier qui, s'il est présent dans une exécution, la rend secrète. De façon équivalente, ceci peut être représenté en partitionnant l'ensemble des états du système en états publics et états secrets et en considérant ces derniers absorbants. Une exécution est secrète ici si elle visite un état secret. C'est cette seconde option que nous utilisons pour l'opacité. Parmi les exécutions secrètes, certaines révèlent le secret. Ce sont celles pour lesquelles toute exécution ayant la même observation est secrète. Notons le parallèle avec le diagnostic : en considérant les exécutions secrètes comme fautives, une telle exécution serait appelée surement fautive. Lorsqu'on étudie l'opacité d'un système, nous désirons mesurer à quel point le secret est révélé, c'est-à-dire quelle est la mesure de probabilité des exécutions révélant le secret. Cette mesure
est appelée la révélation.

L'opacité a été étudiée dans un contexte passif, ainsi que dans un contexte actif. Le contrôle utilisé dans l'étude de l'opacité est fortement différent de celui utilisé pour le diagnostic. En effet, le contrôleur est une fonction associant à une exécution (et non à une séquence d'observations) une distribution sur un ensemble d'action. Chaque action correspond à une distribution de probabilité sur un ensemble de transitions. Ce formalisme donne beaucoup plus de puissance au contrôleur. Il connait précisément quelle est l'exécution actuelle, et son choix n'est pas forcément limité à quels évènements contrôlables il autorise, mais à un ensemble d'actions décrivant potentiellement des choix plus complexes.

Autre différence avec les CLTS, dans le cadre de l'opacité, les observations ne sont plus mises sur les transitions, mais sur les états. Pour noter ces différences, on parlera d'OMC pour les systèmes passifs et d'OMDP pour les systèmes contrôlables.

**Example 0.6.** Considérons l'OMC représenté en figure 0.11. L'observation associée avec chaque état est indiquée à côté de celui-ci. Les états secrets sont indiqués en grisé. En supposant que $o_1$ et $o_2$ sont deux observations autre que $\varepsilon$, toute exécution contenant au moins 3 observations révèle le secret. La révélation est donc de 1.

<figure><img src="image_13.png" /><figcaption>Figure 0.11: Un exemple d'OMC.</figcaption></figure>

Considérons maintenant l'OMDP de la figure 0.12. Dans l'état initial $q_0$, deux actions sont possibles. Si l'action 'a' est choisie, l'exécution entre en $q_1$ avec probabilité $\frac{1}{2}$ et en $q_2$ avec la même probabilité. Si 'b' est choisie, tous les états ont une probabilité $\frac{1}{3}$ d'être atteint.

Définissons la stratégie $\pi$ choisissant initialement l'action 'b', puis toujours l'action 'a'. L'OMC induit par ce OMDP contrôlé par la stratégie $\pi$ est celui représenté dans la figure 0.11. Ainsi, en utilisant la stratégie $\pi$, on assure une révélation de 1. En utilisant une stratégie $\pi'$ qui sélectionne 'b' à tout les coups, la révélation n'aurait été que de $\frac{1}{2}$.
<figure><img src="image_14.png" /><figcaption>Figure 0.12: Un example d'OMDP. Les transitions sont étiquetées par des paires d'action et de la probabilité de prendre cette transition si cette action est choisie.</figcaption></figure>

Intuitivement, lorsqu'on contrôle un système pour augmenter la révélation, on réalise une analyse du pire cas pour le système. Dans la réalité, ce pire cas est atteint si, par exemple, le contrôle est effectué par un virus ayant accaparé certaines fonctionnalités du système. L'inverse, quand le contrôle cherche à minimiser la révélation, est aussi intéressant à étudier. Cela représente, par exemple, le cas où un concepteur possède quelques degrés de liberté dans son système et désire choisir l'option qui maximisera l'opacité du système. Ces deux problèmes semblent symétriques au premier abord, mais leur analyse est en fait extrêmement différente.

Pour la maximisation de la révélation, une simplification est possible au niveau des stratégies : les stratégies déterministes sont suffisantes. C'est-à-dire, afin de maximiser la révélation, on peut se contenter de considérer des stratégies qui associent à chaque exécution finie non pas une distribution sur les actions, mais directement une action. Malgré cette simplification cependant, presque tous les problèmes sont indécidables. La seule question importante que l'on peut résoudre est : étant donné une OMDP $M$, existe t-il une stratégie $\pi$ telle que l'OMC induite $M_\pi$ a une révélation de 1. Ce problème peut se traduire en un problème d'accessibilité avec probabilité 1 dans un processus de décision Markovien partiellement observable, problème pour lequel des algorithmes efficaces existent. Le processus construit est de taille exponentielle et l'algorithme ré-solvant le problème d'accessibilité est en EXPTIME. Par conséquent une application di-recte donne un algorithme 2EXPTIME. Cependant, une analyse précise montre qu'une seule exponentielle est nécessaire. En effet, la complexité de l'algorithme vient prin-cipalement de l'utilisation d'une forme de déterminisation du processus de décision Markovien partiellement observable. Hors, celle-ci est déjà nécessaire à la transforma-tion de l'OMDP vers le processus et n'a donc pas à être répétée. Le problème est également EXPTIME-difficile (réduction depuis les jeux de sécurité à information partielle), il est donc EXPTIME-complet.

Pour la minimisation, la situation est différente, d'une façon surprenante. Tout
d'abord, on ne peut pas se limiter à des stratégies déterministes. La capacité du con-
trôleur à agir de façon randomisée est importante pour rendre le système opaque. Pour
autant, les problèmes sont beaucoup plus facile à résoudre : la révélation exacte de
l'OMDP peut être calculée. En effet, bien que l'on ne puisse pas utiliser de stratégies
déterministes, on peut se limiter à un type de stratégies particulier, que nous avons
nommé quasi-déterministe. Ces stratégies choisissent une action et lui associent une
probabilité proche de 1, puis partagent le reste de la probabilité sur toutes les autres
actions. N'utiliser que des stratégies de cette forme permet de réduire le problème de
la minimisation de la révélation à un problème d'accessibilité dans les processus de dé-
cision Markovien. Contrairement au cas de la maximisation, ceux-ci sont totalement
observables et plus de problèmes sont décidables dans ce cas. Notamment, minimiser la
probabilité d'accessibilité lorsque l'observation est complète peut être réalisé en temps
polynomial. Donc comme le processus que l'on construit est de taille exponentielle, on
obtient un algorithme EXPTIME. Le problème n'est cependant pas prouvé EXPTIME-
difficile. La meilleure borne inférieure dont l'on dispose est PSPACE et est obtenue par
réduction de la validité d'une formule booléenne quantifiée (QBF).

Conclusion

Cette thèse présente principalement une analyse des problèmes liés au diagnostic de systèmes probabilistes. Sa première contribution est de rassembler en un tout cohérent les différentes définitions existantes sur ce problème. Ceci permet à la fois de donner une base solide à la recherche présentée ici, et de servir de fondations à toute recherche future sur ce sujet.

En deuxième point, cette thèse explique comment vérifier les notions de diagnosti-
quabilité définies pour différents systèmes, que ceux-ci soient constitués d'un nombre
d'états fini ou infini. Pour les systèmes infinis, la décidabilité de certaines notions reste
ouverte et certains algorithmes ne sont pas prouvés optimaux. Il reste donc du travail
à réaliser dans cette direction.

Le cas des systèmes contrôlables a enfin été étudié. Pour ceux-ci, un autre angle
de questionnement a été utilisé : il ne s'agit plus seulement de déterminer la diagnos-
tiquabilité du système. En premier lieu, il s'est agi de combiner le diagnostic avec une
limitation de la dégradation du système. Combiner ces deux problèmes ne fait sens
que pour des systèmes actifs : pour un système passif, les deux problèmes peuvent être
vérifiés séparément, au contraire, dans des systèmes actifs, il peut exister pour chaque
propriété une stratégie la vérifiant, mais aucune stratégie ne satisfait les deux simul-
tanément. Dans un second temps, il a été question de l'analyse de l'opacité, une autre
notion de contrôle de l'information produite par un système.
# Part I

## Introduction
<figure><img src="image_15.png" /></figure>
# Chapter 1

# General Introduction

**Model-based verification.** Many critical systems must fulfil a given specification. This specification may include security criteria, efficiency measures or other kinds of requirements. The verification process, which checks if the system respects the specifications, can be performed in several manners. Each one having its pros and cons, the choice of the best method to use strongly depends on the kind of systems to be verified and on the specification. One of the possible method of verification is to perform tests on the system. If one wants to test a program for example, yet does not have access to the internal structures or working of it, the tests can be realised through specification-based testing [GTWJ03]. In this method, one considers the program as a black-box and focuses on the specification in order to determine which inputs are the most likely to show a failure of the system. If one has access to the content of the program, one can build a formal and operational *model* of the system. Then this model can be analysed via dedicated methods.

Building the model may be difficult for some complex systems. It can be done by analysing the code of the system, by making specific tests in its different states to understand its evolution (for example by overloading the CPU to see how a program reacts faced to this kind of stress), etc. When possible, this approach has many benefits:

* When designing a system, if the current prototype does not satisfy our goals, it must be modified. Building iteratively a new prototype until one gets a good result is expensive. It is easier and cheaper to modify a model of the system until it satisfies the requirements and only then implement the system.

* A model is often built for checking several properties. If one wishes to check for additional properties at a later date, verifying the existing model may be sufficient. If not, one does not necessarily have to build a fully new model. One only needs to refine the existing one with the appropriate, missing information, which strongly reduces the complexity.

* Finally, if the model is close enough to reality, then it allows for an accurate analysis of the system. This is not the case when using arrays of tests which only
partially cover the range of possibilities. The same issue exists for other methods
such as statistical model checking [Bar14].

**Probabilistic models.** There exist several different formalisms for representing a system. The more complete the formalism is (by adding time, multiple players...), the more systems and specifications can be described in it, but also the more complex it is to study.

In particular, stochastic models such as Markov chains [KS60] or Markov decision processes [Put94] have many applications. There are some systems that require probabilities in order to be accurately represented. For example, they can be used to represent systems that contains inherent random behaviours. This occurs in any program using randomisation in order to break symmetries for instance, such as the algorithms dealing with the consensus problem [Agu10]. The randomisation also appears in the processes used in the consensus problem as one might represent the possibility that these processes fail with some probability. Another example of application of stochastic models is the case of systems that face unpredictable behaviours from the environment. This can be the case for a server that receives requests. These requests have randomised content and their timing of arrivals can also be random. The latter requires to mix probabilities and time in the model, as in stochastic timed automaton [BBB+14]. Moreover, probabilities can also be used in the model to represent the uncertainty created when the modelling is done through a statistical analysis.

Using probabilities also enlarges the set of properties that can be specified by giving
a measure on the runs of the system. For example, if a non-critical system possesses
failures, yet one can determine that they are not likely to occur, this may be enough.
Let us also consider a security example: if an attacker tries a password and discovers
that it is wrong, he technically gets an information, however this information is not
important enough to be worrisome. With probabilities, the specification can quantify
the properties of the system the designer wants to verify. Moreover, even a qualitative
quantification is useful as it allows to neglect behaviours that are present in the model,
yet have a zero probability of occurring.

**Paradigms of partial observation.** Another important component of a system that can be modelled is related to the observation available to the users: when one builds a model, one describes the different actions that can be taken by the system, however, these actions may be internal and are not necessarily visible by an external observer. Managing the information exchanged with a system has shown increasing importance in recent years due to the omnipresence of communicating electronic devices. Some of the actions of the system may need to be kept private (passwords) while others must be made public (failures). The problems raised by partial observation can be grouped in three families thanks to the different types of goals the system has: (1) planning under partial observation, (2) hiding information from the observer and (3) getting information from the system.

This first category appears for example when studying games. In a game of poker,
a player has to select a decision based on some observations (his cards) and on some
partial information (his opponents choices), moreover probabilities are involved in order
to determine the likelihood to draw a specific card. Such a case falls under the study of
works such as [BGG09] where the authors look for almost-surely winning or positively
winning strategies in stochastic games. Partially observable Markov decision process
(POMDP) is the stochastic one-player (also called one and a half player) special case of
the above (See [CDH10] for algorithms to achieve qualitative objectives in POMDP).
POMDP have been extensively used in the IA community, for example in order to plan
the actions of a moving robot [KLC98].

Many works focus on hiding information from an attacker. For instance code ob-
fuscation [BGI+01], albeit in a complete observation setting. In a partial observation
setting, many theoretical hiding problems are gathered under the general name “opac-
ity”. An opaque system hides an information by ensuring the observation given by
a secret behaviour of the system will be identical to the observation triggered by a
non-secret behaviour. A practical example is given in [ABCP13] where the authors
investigate how to hide the position of a cellphone user (by randomising the position
declared by the phone) while getting relevant answers to location-based requests. In
a theoretical and stochastic setting, [BKM12, BMS15] defined probabilistic measures
of the opacity of a model. The studied model is passive: once defined, one cannot
modify its behaviour in order to ensure better properties. A form of control is quickly
introduced in [BMS15] and expanded in [BCS15, BKMS16, BKMS18]. More precisely,
the authors of [BCS15] investigate Markov decision processes (MDP) with or without
partial observation and secrets given by the infinite language of an automaton (using
various accepting conditions). In [BKMS16, BKMS18], a model in between MDP and
POMDP is used: the control is realised as in an MDP (thus the controller uses complete
information) but the winning condition (opacity) uses partial observation and is thus
more related to POMDP problems. One issue with these approaches is that they all
rely on the black-box hypothesis: it is assumed that the opponent does not know how
the non-determinism of the system is resolved. This hypothesis simplifies the problem,
but is unrealistic in many cases. For example, the control within the system could be
the result of a virus implanted by the attacker. In this case, it is natural for the attacker
to know how the virus is implemented.

On the opposite, if the goal is to get information from the system, the first question
to answer is to determine the kind of information that must be detected. One possibility
is to determine, given a set of partially observable systems, which system is producing
the current observation. In [CK14], the authors investigate how far two labelled Markov
chains are one to the other in terms of the probabilities of the observed behaviours. They
use a distance to measure the importance of the difference between the two models and
approximate (or in some cases compute) this distance. The identification of a system
can be applied to other questions such as the identification of its initial state, the
equivalence of Markov chains (when the distance is equal to 0, see [DHR08]) or the
monitoring of hidden Markov chains (HMC). In this last example, one monitor observes
a random run of one of two given HMC and must determine which HMC is the origin
with appropriately high probability. The case of the monitor required to be correct
with probability 1 on infinite sequences was introduced in [SZF11] and solved using the
distance of [CK14] in [KS16]. Instead of identifying the current system, one can wish to obtain a specific information from the observations of the current system. We develop this kind of problems in the next part due to their importance within this thesis.

**Diagnosis.** *Diagnosis*, from the greek “διάγνωσις” which means “to distinguish” or “to discern”, is by the definition of the wiktionary the “identification of the nature and cause of something (of any nature)”. This describes many different problems in various domains. In medicine, a doctor analyses the symptoms to deduce the illness causing them. There has been multiple works in order to automatise this kind of diagnosis such as the rule-based expert system MYCIN [BS84]. Another approach in the medical domain can be found in computer-aided diagnosis [DMK+99] where the computer analyses medical image such as radios of a patient and points towards the abnormalities it detects. Due to the non-negligible number of false positives and negatives, these works are far from replacing the experts opinion. Forms of diagnosis can also be found in network management for example, where it is more often called *fault management*. More precisely, fault management has two aspects. The first one, passive, consists in receiving messages from the devices on the network and if an alarm was sent, to understand the cause and react to it. The second one takes an active step by considering that a failing device may not be able to detect its own fault and warn the system. Thus, the fault manager will interact regularly to check the behaviour of the devices. Fault managing therefore requires to do tests, diagnosis and possibly reparation. These diagnosis notions deal with systems that can be extremely complex but that are most often static. One wants to identify the current status of the system from what it is emitting currently, the evolution of the system is not monitored. Diagnosis, as seen in the discrete event systems community, focus in contrast on dynamic systems.

**Diagnosis of discrete event systems.** For many systems (power systems, manufacturing systems...) one needs to take into account the evolution of the system when analysing it. Such systems can be analysed with the approach from the discrete event systems community. In this approach, while the system is running, one follows a run of the system and tries to deduce the occurrence (or absence of) of a specific event called the *fault*. While one may want to detect any kind of important action of the system, the term “fault” is chosen both to correspond to the name “diagnosis” which, as shown in the previous examples, is mostly used to detect failures, and because faults are often one of the most important elements to detect within a run. They threaten the safety and availability of the system. In many of the systems listed above, a safety issue may lead to catastrophic damages both in terms of economic and human loses. The study of faults in particular is also justified by the fact that every system may, and will, fail. Indeed, the systems we build are increasingly complex and have increasingly intricate interactions with the environment. It is thus extremely difficult when designing a system not to introduce errors and it is almost impossible to predict every reaction the environment will have to the system. Finally, at the very least, failures will occur because of components ageing.
As faults are dangerous, unavoidable and potentially hard to detect (especially in large-scale complex systems), one needs an automated way to detect them. Moreover this method has to be accurate as stopping a system due to a false positive is costly and it must be reactive so that the failure is detected before too many damages were done. In order to react to the fault, one may either (1) wish to optimise the behaviour of a system in the delay before the occurrence of a fault [EMT16], which is particularly useful for systems which components are automatically replaced on a regular basis, thus hopefully before the occurrence of any fault, or (2) try to detect the fault. As one wants to react quickly to the fault, predicting its occurrence before the system even enters a faulty behaviour would be very efficient. This view is the one studied in prediction problems [GL09]. However, enabling prediction is a very strong requirement for a system. Detecting the fault a posteriori is more likely. The study of diagnosis raises two important issues: deciding whether the system is diagnosable which is called diagnosability and, in the positive case, synthesising a diagnoser possibly satisfying additional requirements about memory size, detection delays, etc. In the discrete event system context, diagnosis was first defined for finite systems such as partially observable Labelled Transition Systems [SSL<sup>+</sup>95] then was extended to numerous more complex models (e.g. Petri nets [CGLS12, BHSS18], pushdown systems [MP09], etc.) and settings (e.g. decentralised [DLT00], distributed [HC94]). Also, several contributions, gathered under the generic term of active diagnosis, focus on enforcing the diagnosability of a system [SLT98, TT07, CT08, CP09].

**Useful techniques.** By observing the previously mentioned works on diagnosis, it appears that some methods and results are recurrent. Let us mention and explain some of them here.

Diagnosability is an *hyper property*, it cannot be checked by analysing every run of the system separately. On the contrary, some runs are *faulty* (contain the fault) while the others are *correct* and we want to compare the observations triggered by faulty runs to the ones produced by correct runs. A key object (e.g. see [JHCK01, YL02]) used to decide diagnosability is the *twin-plant*: a new model is built by making the product of the initial model with itself. A run of the twin-plant consists of a pair of runs of the model. As one wants to compare the observations of the runs, the product is made so that the two runs that are followed simultaneously have the same sequence of observations. This way, one can determine if there exist two runs with the same sequence of observations and some appropriate properties only by checking a single run of the twin-plant. Another often used construction (see [SSL<sup>+</sup>95]) is the *belief construction*. This construction can be seen as an expanded twin-plant or as a form of determinisation of the model: instead of following a pair of runs, the belief automaton instead follows every possible run. More precisely, we keep every state that could be reached with the current sequence of observations, sometimes enhanced with some additional information. This construction is more useful than the twin-plant as it keeps much more information, however it is of exponential size w.r.t. the size of the original model while the twin-plant is only quadratic. The belief automaton by itself gives some information, but can also be used to enrich the initial model. For example,
assume the belief automaton of a stochastic model was built, one can now build the product of this model with its belief automaton [Var99, BK08]. The result, thanks to the determinism of the belief automaton, has the same stochastic behaviour as the original model, however configurations now contain two information: (1) the current state of the associated run in the initial model and (2) the current belief, *i.e.* the set of states that could be reached with the current sequence of observations.

Enriching a model this way is very useful to apply *model-checking* results. Model checking consists in, given a model of a system, verifying if it satisfies a property, often given by a logical formula. The two most famous logics used are LTL (linear temporal logic) [Pnu77] and CTL (computational tree logic) [Eme90]. The first one focuses on properties of individual run while the second is mostly interested in branching properties. As diagnosis is not a branching property we only discuss LTL here. In LTL, one can encode formulae about the future of a run, *e.g.*, a condition will eventually be true, a condition will remain true until another one becomes true, etc. The basic components of a formula are propositional variables whose truth value depends, in our framework, on the current state of the model. The more information is contained within a state, the more precise the use of propositional variables can be. How to verify that a “simple” model satisfies an LTL formula is known for a long time [Var96]<fnref n="1" />. Complications occur however when the model is more complex or when the property one wants to check requires more expressive power than what LTL can offer. For stochastic specifications, LTL was extended to pLTL. The extension allows to quantify the measure of the paths satisfying a given LTL formula (the probabilistic operator cannot be nested in the formula). Verifying these formulae is more difficult in terms of complexities. It has been studied both for finite systems [CY95] or infinite ones [EY12]. One can refer to [BK08, Chapter 10] for details about the model checking of probabilistic systems. One important point is that the main source of the complexity of the algorithms is the size of the formula. For example, in [EY12], the qualitative model checking of a recursive Markov chain (a model of infinite-state stochastic system) is PSPACE in the size of the model (and can drop to PTIME under some restrictions) but is EXPTIME in the formula. When studying diagnosis, most problems can be expressed with a simple and fixed formula, which means that the part of the complexity depending on then size of the formula is not our concern.

Another set of techniques that can be used are the results known for POMDP. They have two main interests. First, when studying diagnosis on active systems, some problems can be translated into POMDP problems for which there exist efficient algorithms (as done in [BFH+14]). The second interest of POMDP comes in fact mostly from probabilistic automata (PA), which are a subclass of POMDP. Many problems are known to be undecidable for PA [Paz71, GO10] and due to the simplicity of the PA model, these problems are often easier to use to prove undecidability than problems for POMDP (such as the policy-existence problem under the infinite-horizon average reward criterion [MHC03]).

<footnote n="1">¹One technique is to obtain a Büchi automaton that is equivalent to the model and another one that is equivalent to the negation of the property. The intersection of the two non-deterministic Büchi automata is empty if the model satisfies the property.</footnote>
Finally, as there exist many problems using partial observation, the first thing to do when studying a new notion is to check if there already exists a similar problem for which an analysis was realised. In the positive case, one only has to establish a translation. A relevant example of this was mentioned earlier when we stated that [CK14] was used to solve a monitoring problem. The authors of [CK14] established a polynomial algorithm in order to determine if the distance of the language of two labelled Markov chains is equal to 1. In other words, to decide if, almost surely, given an infinite observed sequence, one can determine which labelled Markov chain emitted it. The algorithm relies on the existence of algorithms to detect when two systems have exactly the same language (distance 0) and that if the models are not at distance 1, then a “part” of them is at distance 0. While diagnosis focuses mostly on finite runs and this problem considers infinite runs, strong links can be identified.

**Challenges and objectives.** As our global goal is to perform model-based verification, the first question that needs to be tackled in this thesis is the choice of the formalism. This formalism has to include probabilities as we want to be able to quantify the specification. But some points are still open: we must determine whether the model incorporates non-determinism, represents infinitely many states or expresses efficiently concurrent behaviours for example. Moreover, we intend to work on partial observation problems. This requires the model to select what observation is associated with a run.

Our second issue lies in the choice of the problems to focus on. Many notions of diagnosis have been defined over the years with different goals in mind. We have to find a set of appropriate qualitative/quantitative diagnosis notions that encompass the important, already known, notions that focus on realistic relevant issues, and that is coherent as a whole. Moreover, the formal definitions of the problems we work on must be carefully chosen. Indeed, mixing partial observation, probabilities and control quickly leads to undecidability results (as is the case for PA, mentioned earlier). A slight modification of the definitions may strongly modify the complexity. For example we will see a case, where inverting two quantifiers turn a problem of complexity PTIME to an undecidable one.

Once the properties are defined, our goal is to establish precisely the complexities of verifying if the model satisfies the chosen specification. We are also interested in determining how to modify the system so that it satisfies the properties. This gives two main approaches, a passive one associated with observation and an active one associated with observation and control.

**Outline.** This thesis is organised as follows.

* In Chapter 2, we introduce notations useful all along the document. While it does not contain any result *per se*, it includes the definitions of the notions of diagnosis that we introduced. The choice of appropriate definitions is already a contribution. In the second part of this chapter, we present a state of the art on the diagnosis problem.
* In Chapter 3, we realise a semantical analysis of the problems of diagnosability we defined in Chapter 2. More precisely, we first present the notion of diagnoser, i.e. the function realising the diagnosis, and prove the equivalence between the existence of a diagnoser and the diagnosability of a system. We also establish the relations between the various notions of diagnosability and, when possible, characterise these notions. The semantical analysis of a problem as done here is very important as understanding the problems is the first step to solving them. This chapter is based on [BHL14, BHL16a, BHL16b].

* In Chapter 4, we focus on our simplest model, representing finite stochastic systems. Using the finiteness, we strengthen our characterisations of the diagnosability notions and use them in order to establish algorithms to decide the problems when possible or to prove undecidability in the opposite case. We also show how to build diagnosers using finite memory. This chapter develops contributions from [BHL14, BHL16a].

* In Chapter 5, we turn to systems with infinitely many states. We cannot use the characterisations obtained in Chapter 4, but the results of Chapter 3 still hold. We study different models and clearly observe the increase in difficulty compared to finite-state models. We still manage to obtain decidability results for one model. This chapter extends [BHL16b].

* In Chapter 6, we consider controllable systems. Using the control, one can ensure properties for the system. However, controlling the system with one objective in mind can have negative side-effects. For example, ensuring diagnosability can increase the likelihood of faults within the system. We are therefore interested in combining multiple objectives, one of them being diagnosability. This chapter is based on [BHL17b].

* In Chapter 7, we instead focus on another partial observation problem: opacity, which, on many aspects, appears like a dual of diagnosability. We introduce the notion and explain the impact opacity has on the choice of the framework: we consider here active systems as is done in Chapter 6, however the type of control is different as the controller is not interpreted in the same manner. We define multiple measures of opacity and explain how to maximise or minimise them when possible. The results of this chapter were published in [BHL17a].

**Other works.** In order to limit the number of frameworks and problems to define and to give a better coherence to the thesis, some of the works we realised are not detailed in this document. We give a short description of these results here.

The results of [BHL14] serve as a foundation to our analysis of diagnosability. They are thus, for the most part, necessary for this thesis and are therefore developed in Chapter 3 and Chapter 4. However, this work also contains contributions on *prediction* and *prediagnosis*. Prediction describes the ability to detect the fault before its occurrence. It had been shown to be in NLOGSPACE for logical systems [GL09]. While using
probabilities usually increases the difficulty, we gave an NLOGSPACE algorithm for the prediction problem in stochastic systems. The authors of [CK15] present a similar result with a notion called “prognosis”. While prediction is limited to the detection of faults before their occurrence, diagnosis is itself limited to their detection after the occurrence. That is why we also introduced prediagnosis where one is allowed to either predict or diagnose the fault. Any predictable or diagnosable system is thus prediagnosable, but the converse does not hold. We showed that prediagnosability (i.e. the problem of deciding if a system is prediagnosable) is PSPACE-complete.

For the diagnosability notions studied in this thesis, faults are permanent: once a fault is triggered, any following behaviour is faulty. However, one may want to consider faults that are only temporary. For example, a model could contain the possibility of a reparation. This raises many new problems: one may wish to detect the fault before the reparation, to count the number of faults occurring within the system, etc. These questions were investigated in [FHLM18] in a non-stochastic setting. While diagnosability of permanent faults is known to be in NLOGSPACE for logical systems, we showed that with repairable faults, it becomes PSPACE-complete. We also discussed multiple methods to count faults and presented among other things an NLOGSPACE algorithm to decide if one can count the number of faults while having a delay of at most one count of fault.

One of the non-stochastic framework where diagnosability was studied is Petri nets (PN) [CGLS12, BHSS18]. For bounded PN, the usual method to solve diagnosability is to build the reachability graph of the net, which is an automaton structure representing the behaviour of the PN and then to use existing results on this kind of models [JHCK01, YL02]. The issue with this method is the size of the reachability graph. In order to face this issue, many works try to abstract the graph in order to reduce its size while keeping the relevant information. In a partial observation setting, this led to the introduction of the *basis reachability graph* [CGS09]. In [LGS18], we showed how to extend this abstraction to unbounded PN, calling the new object “Basis coverability graph”. We established some results about the properties of the basis coverability graph and explained how to use it to solve diagnosability of unbounded PN.
# Chapter 2

# Preliminaries

The first step of the theoretical analysis of a problem is the definition of the framework. The chosen framework possesses different properties depending on the specificities of the system one wishes to study. Some frameworks are thus better adapted to represent concurrency, to express infinite-state systems... In the first section of this Chapter, we introduce the main definitions that are used throughout the thesis. More precisely, in Subsection 1.1, we recall some definitions and results of descriptive set theory. We then define in Subsection 1.2 the main probabilistic model used in this document and define a probabilistic measure. In Subsection 1.3, we explain how partial observation can be added to this model. These definitions give a framework for various problems linked to partial observation. In this section, we also give definitions related to diagnosis, which is the main partial observation problem studied during this thesis. Diagnosis corresponds to a family of questions, focusing on the identification of a faulty behaviour within the system. We explain in Subsection 1.4 how the notion of fault can be formalised in our model. Finally, in Subsection 1.5, we discuss different notions of diagnosability. These notions are used to capture when and how the faulty (or correct) behaviour of the system must be identified, and with which accuracy. Section 2 finally presents a state of the art on diagnosis.

## 1 Framework

Let us start with a few general notations. We denote by $\mathbb{N}$ the set of natural numbers, $\mathbb{Q}$ the set of rational numbers and $\mathbb{R}$ the real numbers. For a finite alphabet $\Sigma$, we denote by $\Sigma^*$ (resp. $\Sigma^\omega$) the set of finite (resp. infinite) words over $\Sigma$. $\varepsilon$ represents the empty word.

### 1.1 Descriptive set theory

Descriptive set theory [Mos80, Chapter 1] defines and studies classes of “well-behaved” sets. These sets having good properties, they have applications in many areas. In this thesis, they have two main applications. First, they are used to evaluate the complexity of some problems. This is achieved using a hierarchy ranking these sets: the higher a
set is in the hierarchy, the more complex it is. Therefore if we can express a property with a set, the problem complexity can be related to the set complexity. Secondly, these sets form a building block of the formal definition of the stochastic behaviour of our model.

Let us first recall some standard facts about Borel sets.

**Definition 2.1.** Given a space $X$, the set $Y$ is a topology on $X$ if

* $X \in Y$ and $\emptyset \in Y$,

* $Y$ is stable by union, i.e. given $(O_i)_{i \in I}$ a family of elements of $Y$, $\cup_{i \in I} O_i \in Y$,

* $Y$ is stable by finite intersection, i.e. given $(O_i)_{i \in I}$ a finite family of elements of $Y$, $\cap_{i \in I} O_i \in Y$,

We call the sets in $Y$ the open sets.

**Example 2.1.** Consider the space of infinite words over two letters $\{a, b\}^\omega$. On such a space, the usual topology uses the notion of cylinder. Given a finite word $w$ of $\{a, b\}^*$, the cylinder of $w$ is the set of infinite words extending $w$, $\text{Cyl}(w) = w\{a, b\}^\omega$. One obtains a topology by choosing the set of cylinders as its basic components and by adding the sets created through union and finite intersection. $\{a, b\}^\omega$ belongs to this topology as it is the cylinder of $\varepsilon$, the empty set can be obtained as the intersection of the cylinders of ‘a’ and of ‘b’.

Under this topology, the set of words containing at least $k$ ‘a’, for $k \in \mathbb{N}$ is an open set as it is a countable union of cylinders.

Given a space $X$ and a topology $Y$ on $X$, we define the *Borel hierarchy* (represented in Figure 2.1) as the three classes of sets $\Sigma_n^0$, $\Pi_n^0$ and $\Delta_n^0$ obtained inductively by

* $\Sigma_1^0 = Y$ is the set of open sets;

* $\forall n \ge 1$, a set belongs to $\Pi_n^0$ if its complement belongs to $\Sigma_n^0$

* $\forall n \ge 2$, $O$ is in $\Sigma_n^0$ if there exists a family $(O_i)_{i \in I}$ of elements of $\Pi_{n-1}^0$ such that $O = \cup_{i \in I} O_i$;

* $\forall n \ge 1$, $\Delta_n^0 = \Pi_n^0 \cap \Sigma_n^0$.

The sets in $\Pi_1^0$ are called *closed*, the sets $\Sigma_2^0$ and $\Pi_2^0$ are respectively called $F_\sigma$ and $G_\delta$. A *Borel set* is a set belonging to some level of the Borel hierarchy. The set of Borel sets is denoted $\mathfrak{B}$.

**Example 2.2.** Continuing Example 2.1, the set composed of the single word $a^\omega$ is closed. Indeed, its complement is $\cup_{n \in \mathbb{N}} \text{Cyl}(a^n b)$ which is an open set. The set of words with infinitely many ‘a’ is neither open, nor closed. It however belongs to $G_\delta$. Indeed, it is the complement of the set of words ending by $b^\omega$. As this set of words is an infinite union of closed set (each closed set containing a single infinite word), it belongs to $F_\sigma$, thus its complement is a $G_\delta$ set.
<figure><img src="image_16.png" /><figcaption>Figure 2.1: Representation of the Borel hierarchy.</figcaption></figure>

In our models, we need to measure the probabilities of certain events. This is done thanks to Carathéodory's extension theorem [ADD99]. Before stating this theorem, we need to introduce some definitions used in measure theory.

**Definition 2.2.** Given a space $X$, a ring of sets $R$ of $X$ is a subset of the powerset of $X$ satisfying:

* $\emptyset \in R$;

* $R$ is closed under pairwise union, $\forall A, B \in R, A \cup B \in R$;

* $R$ is closed under relative complements, $\forall A, B \in R, A \setminus B \in R$.

**Definition 2.3.** Given a space $X$, a $\sigma$-algebra $S$ of $X$ is a subset of the powerset of $X$ satisfying:

* $\emptyset \in S$;

* $S$ is closed under countable union, $\forall (A_i)_{i \in \mathbb{N}} \in S, \bigcup_{i \in \mathbb{N}} A_i \in S$;

* $S$ is closed under complement, $\forall A \in S, S \setminus A \in S$.

By definition, a $\sigma$-algebra is a ring of sets. Observe that the set of Borel sets $\mathfrak{B}$ is a $\sigma$-algebra. More precisely, it is the $\sigma$-algebra generated by the open sets (i.e. it is the smallest $\sigma$-algebra containing the open sets).

**Definition 2.4.** Given a ring of sets $R$ on a space $X$, a pre-measure $\mu$ on $R$ is a function $\mu: R \to [0, +\infty]$ such that:

* $\mu(\emptyset) = 0$;

* for all countable family of sets of $R$ pairwise disjoint, $(A_i)_{i \in \mathbb{N}}$, we have

$$ \mu\left(\bigcup_{n=1}^{\infty} A_n\right) = \sum_{n=1}^{\infty} \mu(A_n). $$

A pre-measure $\mu$ is called $\sigma$-finite if there exist a countable number of sets $A_1, A_2, \dots \in R$ such that $X = \bigcup_{k=1}^{\infty} A_k$ and for all $k \in \mathbb{N}, \mu(A_k) < \infty$.

If $R$ is a $\sigma$-algebra, then $\mu$ is called a measure.
A measure $\mu$ is called inner regular if for every set $E$, we have

$$ \mu(E) = \sup\{\mu(F) \mid F \subseteq E \wedge F \text{ is a closed set}\}. $$

In the current work, we require a measure, yet only a pre-measure can efficiently be defined. Fortunately, Carathéodory's extension theorem allows to bridge the gap.

**Theorem 2.1 ([ADD99]).** Let $R$ be a ring on a space $X$, $\mu$ be a pre-measure on $R$. There exists a measure $\mu'$ extending $\mu$ on the $\sigma$-algebra generated by $R$. Moreover, if $\mu$ is $\sigma$-finite, then $\mu'$ is unique and also $\sigma$-finite.

**Example 2.3.** Let us continue Example 2.1 and consider the ring of sets $R$ generated by the topology based on the cylinders. We define the pre-measure $\mu$ on this ring as the only pre-measure satisfying $\forall n \in \mathbb{N}, w \in \{a, b\}^n, \mu(\text{Cyl}(w)) = \frac{1}{2^n}$.

One could interpret the represented system as an infinite number of coin flips, each result ('a' or 'b') having $\frac{1}{2}$ probability. $\mu$ gives the probability of cylinders (a given finite number of flips) and finite unions of them.

The pre-measure $\mu$ is $\sigma$-finite as $\mu(\{a, b\}^\omega) = 1$. According to Carathéodory's extension theorem, there is thus an unique measure $\mu'$ extending $\mu$ on the $\sigma$-algebra generated by $R$: the Borel sets. Observe that $\mu'$ is inner regular.

## 1.2 Probabilistic Labelled Transition Systems

We now define the model that represent the system. The choice of the model depends on the properties one wishes to have. Petri nets [Dia09] for example, efficiently represent concurrent systems. Another possibility is to use automata structures as in the seminal work of [SSL+95] formally defined by:

**Definition 2.5.** A labelled transition system (LTS) is a tuple $\mathbb{A} = (Q, q_0, \Sigma, T)$ where:

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

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

* $T \subseteq Q \times \Sigma \times Q$ is a set of transitions;

Informally, the states of $Q$ represent the different configurations the system can be in, an event of $\Sigma$ is an action that can be taken by the system (sending a request, activating a component...) and $T$ describes how this action affects the system.

Formally, we write $q \xrightarrow{a} q'$ when there exists a transition $(q, a, q') \in T$; this transition is then said to be enabled in state $q$. We assume all LTS we consider are live, i.e. in every state of the LTS at least one transition is enabled. This ensures the system will not reach a deadlock position and stop activating events. A run $\rho$ of an LTS $\mathbb{A}$ is a (finite or infinite) sequence $\rho = q_0 a_0 q_1 \dots$ such that for all $i \ge 0$, $q_i \in Q$, $a_i \in \Sigma$ and when $q_{i+1}$ is defined, $q_i \xrightarrow{a_i} q_{i+1}$. A run thus represents the evolution of a system over time. The notion of run can be generalised, starting from an arbitrary state $q$. Given
an LTS $\mathsf{A}$, we write $\Omega^\mathsf{A}$ for the set of all infinite runs starting from $q_0$. We only write $\Omega$
when the LTS $\mathsf{A}$ is clear from context. When it is finite, $\rho$ ends in a state that we denote
$\mathsf{last}(\rho)$ and its length, denoted by $|\rho|$, is the number of events occurring in it. Given a
finite run $\rho = q_0 a_0 q_1 \dots q_n$ and a (finite or infinite) run $\rho' = q_n a_n q_{n+1} \dots$ starting in
$\mathsf{last}(\rho)$, we call concatenation of $\rho$ and $\rho'$ the run $\rho\rho' = q_0 a_0 q_1 \dots q_n a_n q_{n+1} \dots$.
The run $\rho$ is then a prefix of $\rho\rho'$, which we denote by $\rho \preceq \rho'$. The cylinder generated by a
finite run $\rho$ consists of all the infinite runs that extend $\rho$: $\mathrm{Cyl}(\rho) = \{\rho' \in \Omega \mid \rho \preceq \rho'\}$.
The sequence associated with $\rho = q_0 a_0 q_1 \dots$ is the word $\sigma_\rho = a_0 a_1 \dots$, and we write
indifferently $q \stackrel{\rho}{\Rightarrow} q$ or $q \stackrel{\sigma_\rho}{\Rightarrow} (\text{resp. } q \stackrel{\rho}{\Rightarrow} q'$ or $q \stackrel{\sigma_\rho}{\Rightarrow} q')$ for an infinite (resp. finite) run
$\rho$ starting in $q$ (resp. and ending in $q'$). A state $q$ is reachable (from the initial state
$q_0$) if there exists a run $\rho$ such that $q_0 \stackrel{\rho}{\Rightarrow} q$, which we alternatively write $q_0 \Rightarrow q$. The
language of an LTS $\mathsf{A}$ consists of all infinite words that label runs of $\mathsf{A}$ and is formally
defined as $\mathcal{L}^\omega(\mathsf{A}) = \{\sigma \in \Sigma^\omega \mid \exists q_0 \stackrel{\sigma}{\Rightarrow} \sigma\}$. A bottom strongly connected component
(BSCC) of an LTS is a strongly connected component from which no state outside of
the BSCC are reachable.

**Example 2.4.** Consider the LTS represented in Figure 2.2. It contains three states. $q_0$ is the initial state, representing the machine waiting to receive an order. When such an order occurs the run takes the transition labelled by the ‘coin’ event and enters the second state. In this second state, the machine is preparing the coffee, it has the possibility to add sugar, and after a certain amount has been added, it returns to its initial state by giving a coffee. In this operating state, the machine can also commit an error, event ‘f’, leading to a faulty state $f_1$. In $f_1$, the machine cannot serve coffee any more and sends an ‘out of order’ signal. A normal use of this system by a consumer is given for example by the run $\rho = q_0 \ \text{coin} \ q_1 \ \text{sugar} \ q_1 \ \text{coffee} \ q_0$.

<figure><img src="image_17.png" /><figcaption>Figure 2.2: An LTS representing a coffee machine. $q_0$ is the initial state, which is represented by the incoming arrow. Transitions between two states are labelled by the event associated with the transition.</figcaption></figure>

In order to represent the unpredictability of the environment and to neglect events
that have a null probability of occurring, we want to represent stochastic behaviours. To
do so, the model must be enriched using probabilities. More precisely, this is achieved
by adding a probability matrix indicating how the transitions, labelled by events, are
randomly chosen.
**Definition 2.6.** A probabilistic labelled transition system (pLTS) is a tuple $\mathcal{A} = \langle Q, q_0, \Sigma, T, \mathbf{P} \rangle$ where:

• $\mathcal{A} = \langle Q, q_0, \Sigma, T \rangle$ is an LTS;

• $\mathbf{P}$ is the transition matrix from $T$ to $\mathbb{Q}_{>0}$ fulfilling for all $q \in Q$:

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

The LTS $\mathcal{A}$ is called the underlying labelled transition system of $\mathcal{A}$.

Note that since we assume the state space to be at most countable, a pLTS is by definition at most countably branching: in every state $q$, only countably many transitions are enabled, so that the summation $\sum_{(q,a,q') \in T} \mathbf{P}[q, a, q']$ is well-defined. The definitions introduced for LTS are naturally lifted to pLTS. Given a countable set $Z$, a distribution on $Z$ is a mapping $\mu: Z \to [0, 1]$ such that $\sum_{z \in Z} \mu(z) = 1$. The support of $\mu$ is $\text{Supp}(\mu) = \{z \in Z | \mu(z) > 0\}$. If $\text{Supp}(\mu) = \{z\}$ is a single element, $\mu$ is a Dirac distribution on $z$ written $\mathbf{1}_z$. We denote by $\text{Dist}(Z)$ the set of distributions on $Z$. The transition matrix defines in every state $q$ a distribution on the transitions whose support are exactly the transitions enabled in $q$.

**Example 2.5.** Consider the pLTS represented in Figure 2.3. Its underlying LTS is represented in Figure 2.2. The difference is thus that probabilities were added on the transitions so that the sum of the probabilities exiting any state is equal to one. The run $\rho$ that was described as being a normal use of the system in Example 2.4 can now be associated with a probability, which is the product of the probability of the events it triggered. Here, $1 \times 0.29 \times 0.7 = 0.203$. This result, being low, seems to point out that, in this representation, most consumers do not take exactly one unit of sugar in their coffee or do not even get their coffee.

<figure><img src="image_18.png" /><figcaption>Figure 2.3: A pLTS representing a coffee machine. The probability of a transition is given next to the event labelling it.</figcaption></figure>

We now use the probabilities within the system to formally define the probability measure that are used on runs. This is done using the descriptive set theory presented in Subsection 1.1. The construction of the measure uses the Carathéodory's extension theorem, similarly to what is done in Example 2.3.
Here, the set space $X$ we are interested in is the set of all infinite runs $\Omega$. The open set $\Sigma_1^0$ is built from the cylinders: $\Sigma_1^0$ is the smallest set containing $\emptyset$, $\Omega$, such that for all finite run $\rho$, $\mathrm{Cyl}(\rho) \in \Sigma_1^0$, and such that $\Sigma_1^0$ is stable by union and finite intersection. The complement of a cylinder is a finite union of cylinders, the complement of an (potentially infinite) union is an (potentially infinite) intersection and the complement of a finite intersection is a finite union. A set $F$ is thus closed if and only if $F = \bigcap_{n \in \mathbb{N}} O_n$ where $O_n$ is a union of cylinders. Therefore an $F_\sigma$ set $F$ can be written as $F = \bigcup_{m \in \mathbb{N}} \bigcap_{n \in \mathbb{N}} O_{m,n}$ where $O_{m,n}$ is a union of cylinders whose associated paths have length $n$. Without loss of generality, the sequence of closed sets may be chosen as a non-decreasing sequence. The cylinders are thus used as the basis to build a Borel hierarchy on $\Omega$.

Given a pLTS $\mathcal{A}$, in order to have a probabilistic measure spanning all the sets of infinite runs of the Borel hierarchy generated by the cylinders, we define a pre-measure $\mathbb{P}_{\mathcal{A}}$ on the ring of sets generated by the open sets by: for all finite run $q_0 a_0 q_1 \dots q_n$,

$$ \mathbb{P}_{\mathcal{A}}(\mathrm{Cyl}(q_0 a_0 q_1 \dots q_n)) = \mathbf{P}[q_0, a_0, q_1] \cdots \mathbf{P}[q_{n-1}, a_{n-1}, q_n] $$

and for all finite sequence of pairwise disjoint cylinders $A_1, \dots, A_n$,

$$ \mathbb{P}_{\mathcal{A}}(\cup_{i=1,\dots,n} A_i) = \sum_{i=1,\dots,n} \mathbb{P}_{\mathcal{A}}(A_i). $$

According to Carathéodory's extension theorem, this pre-measure can be extended uniquely on the whole $\sigma$-algebra generated by this ring. We still write $\mathbb{P}_{\mathcal{A}}$ for the obtained measure. Moreover, when $\mathcal{A}$ is fixed, we may omit the subscript. To simplify, for $\rho$ a finite run, we sometimes abuse notation and write $\mathbb{P}(\rho)$ for $\mathbb{P}(\mathrm{Cyl}(\rho))$. If $R$ is a (countable) set of finite runs such that no run is a prefix of another one, we write $\mathbb{P}(R)$ for $\sum_{\rho \in R} \mathbb{P}(\rho)$ which is consistent since all intersections of associated cylinders are empty.

## 1.3 Partial observation

In partial observation problems, one considers an observer of the system (a user, an attacker...) who perfectly knows the model, yet only partially observes its behaviours. In this case, one needs to formalise which information can be observed. This allows to associate with every run of the system, an observation or sequence of observations.

The first question is to determine what part of a run gives an information: events, states or both. In fact, these three options are equivalent in terms of expressibility. Thus, for every problem, one selects the option that is the more efficient at representing the specificities of the problem. For example, when studying diagnosis, we try to detect a faulty action of the system. As this faulty action is an event, observations are put on events. This is the option we follow in most chapters of this thesis, see Chapter 7, page 195, for a model with observations on states.

Events represent actions taken by the system. A formalisation of the observation could be made by distinguishing internal and external actions. This would mean that some actions occur within the system and are thus *unobservable* while others are done
publicly and are thus observable. Formally, one partitions the set of events $\Sigma$ into two disjoint sets $\Sigma_o$ and $\Sigma_u$, the sets of observable and unobservable events, respectively.

**Example 2.6.** Consider the pLTS of Figure 2.3. Clearly, introducing a coin, adding sugar to the cup and receiving the coffee are observable actions. The other two are more subject to discussion. Depending on the fault and the sensors within the system, $f$ could be considered observable or unobservable. Indeed, if $f$ stands for the explosion of the machine, it would clearly be observable, however if $f$ is an internal error, detecting it requires the existence of an appropriate sensor within the system. The status of the last event also depends on which fault occurred. For our example, let us assume $f$ is unobservable, but the failure of the system is detected, allowing the machine to publicly send an ‘out of order’ message. In this case, the run “$q_0$ coin $q_1$ sugar $q_1$ $f$ $f_1$ out of order” produces the sequence of observations “coin sugar out of order”.

A more sophisticated method than this partition would be to equip the pLTS with a mask function. This mask function associates every event with an observation, taken from an observation alphabet. This function can map an event to $\varepsilon$ meaning that the event is unobservable or project multiple events onto the same observation, making them indistinguishable. When using a mask function, $\Sigma_o$ is the observation alphabet and $\Sigma_u$ is the set of unobservable events (i.e. events which observation is $\varepsilon$).

**Example 2.7.** Consider the pLTS of Figure 2.3 again. We use the observation alphabet $\Sigma_o = \{\text{coin}, \text{coffee}, \text{beep}\}$ and the mask function $\mathcal{P}$ such that $\mathcal{P}(\text{coin}) = \text{coin}, \mathcal{P}(\text{coffee}) = \text{coffee}, \mathcal{P}(\mathbf{f}) = \varepsilon$ and $\mathcal{P}(\text{sugar}) = \mathcal{P}(\text{out of order}) = \text{beep}$. Here, we see that two of the events are indistinguishable as they share the same observation beep. When a beep is produced, a user does not know whether the machine is out of service or if it is adding more sugar. In other words, the infinite runs “$q_0$ coin $q_1$ $f$ $f_1$ (out of order $f_1$)$^\omega$” and “$q_0$ coin $q_1$ (sugar $q_1$)$^\omega$” share the same observation sequence “coin sugar beep$^\omega$”.

Observe that the mask function setting generalises the partition discussed above. Indeed, the partition is mimicked by the mask function which projects every unobservable event to $\varepsilon$ and every observable event onto itself. We now define multiple notations using the mask function formalism. Due to the previous remark, these definitions can easily be applied to the partition setting. In the future chapters, we mostly use partitions for simplicity. We state explicitly when we use mask functions.

Given an observation alphabet, a mask function is a mapping $\mathcal{P}: \Sigma \to \Sigma_o$. It is extended to words from $\Sigma^*$ inductively by: $\mathcal{P}(\varepsilon) = \varepsilon$ and $\mathcal{P}(\sigma a) = \mathcal{P}(\sigma)\mathcal{P}(a)$. We write $|\sigma|_o$ for the observable length of $\sigma$, that is $|\mathcal{P}(\sigma)|$. The observable length of a run $\rho$, denoted $|\rho|_o$, is the observable length of its associated sequence. Given a run $\rho$ and its sequence $\sigma_\rho$ we sometimes use $\mathcal{P}(\rho)$ for $\mathcal{P}(\sigma_\rho)$. When $\sigma$ is an infinite word over $\Sigma$, its projection (resp. observable length) is the limit of the projections (resp. observable length) of its finite prefixes. Given $a \in \Sigma_o$, $|\sigma|_a$ is the number of occurrences of $a$ in $\sigma$. As usual the mask function $\mathcal{P}$ is extended to languages: for $L \subseteq \Sigma^* \cup \Sigma^\omega$, $\mathcal{P}(L) = \{\mathcal{P}(\sigma) \mid \sigma \in L\}$.

With respect to the mask function $\mathcal{P}$, a pLTS $\mathcal{A}$ is said convergent if there is no infinite sequence of unobservable events from any reachable state: $\mathcal{L}^\omega(\mathcal{A}) \cap \Sigma^*\Sigma_u^\omega = \emptyset$.
When $\mathcal{A}$ is convergent, for every $\sigma \in \mathcal{L}^\omega(\mathcal{A})$, $\mathcal{P}(\sigma) \in \Sigma_o^\omega$. In the rest of the thesis we assume that pLTS are convergent. We refer to a sequence for a finite or infinite word over $\Sigma$, and to an observed sequence for a finite or infinite word over $\Sigma_o$. The projection of a sequence onto $\Sigma_o$ is thus an observed sequence. The prefix of length $n \in \mathbb{N}$ of an observed sequence $w$ is denoted $w_{\le n}$.

We now define the notion of *signalling runs*. They correspond to the finite runs which last event was observable (i.e. finite runs $q_0 a_0 q_1 \cdots a_{n-1} q_n$ such that $\mathcal{P}(a_{n-1}) \neq \varepsilon$). Signalling runs are precisely the relevant runs w.r.t. partial observation issues since each observable event provides additional information about the execution to an external observer. In the sequel, $\text{SR}(\mathcal{A})$ denotes the set of signalling runs of the pLTS $\mathcal{A}$, and $\text{SR}_n(\mathcal{A})$ the set of signalling runs of observable length $n$. The pLTS is dropped from the notation when it is clear from context. Since we assume that the pLTS are convergent, for every $n > 0$, $\text{SR}_n$ is equipped with a probability distribution defined by assigning measure $\mathbb{P}(\rho)$ to each $\rho \in \text{SR}_n$. Given $\rho$ a finite or infinite run, and $n \le |\rho|_o$, $\rho_{\downarrow n}$ denotes the unique prefix of $\rho$ that belongs to $\text{SR}_n$. For convenience, the empty run $q_0$ is defined as the single signalling run of null length. For an observed sequence $w \in \Sigma_o^*$, we define its cylinder $\text{Cyl}(w) = w\Sigma_o^\omega$ and the associated probability $\mathbb{P}(\text{Cyl}(w)) = \mathbb{P}(\{\rho \in \Omega \mid \mathcal{P}(\rho_{\downarrow|w|}) = w\}) = \mathbb{P}(\{\rho \in \text{SR}_{|w|} \mid \mathcal{P}(\rho) = w\})$, often shortened as $\mathbb{P}(w)$.

## 1.4 Fault and ambiguity

We now give definitions and notations for a partial observation problem, which is particularly of interest to us, diagnosis. Diagnosis focuses on the detection of a special unobservable event called the *fault* $\mathbf{f} \in \Sigma_u$ thanks to the observations received from the system. Let us now classify runs depending on whether they contain a fault or not. A run $\rho$ is *faulty* if its associated sequence $\sigma_\rho$ contains $\mathbf{f}$, otherwise it is *correct*. For $n \in \mathbb{N}$, we write $F_n$ (resp. $C_n$) for the set of infinite runs whose signalling prefix of observable length $n$ is faulty (resp. correct). We further define the sets of all finite faulty and correct signalling runs $\mathbf{F}$ and $\mathbf{C}$ and the sets of infinite faulty and correct runs $\mathbf{F}_\infty = \bigcup_{n \in \mathbb{N}} F_n$ and $\mathbf{C}_\infty = \bigcup_{n \in \mathbb{N}} C_n$. A run $\rho$ is a *minimal faulty run* if it is a faulty run and there does not exist a prefix $\rho'$ of $\rho$ that is a faulty run. We write, for all $n \in \mathbb{N}$, $\min F_n$ for the set of minimal faulty runs of length $n$ and $\min \mathbf{F} = \bigcup_{n \in \mathbb{N}} \min F_n$ for the set of all minimal faulty runs.

Given two states $q$ and $q'$ and an observation $a \in \Sigma_o$, we write $q \Rightarrow^a q'$ if there exists a run $\rho = q_0 a_0 q_1 \dots q_n$ with $q_0 = q, q_n = q'$, $\rho \in \text{SR}_1$ and $\mathcal{P}(\rho) = a$. We also write $q \Rightarrow_f^a q'$ (resp. $q \Rightarrow_c^a q'$) if there exists a faulty (resp. correct) run $\rho = q_0 a_0 q_1 \dots q_n$ with $q_0 = q, q_n = q'$, $\rho \in \text{SR}_1 \cap \mathbf{F}$ (resp. $\rho \in \text{SR}_1 \cap \mathbf{C}$) and $\mathcal{P}(\rho) = a$.

Except explicit mention of the opposite, we assume that the state space $Q$ of $\mathcal{A}$ is partitioned into correct states and faulty states: $Q = Q_f \uplus Q_c$ such that faulty (resp. correct) states, i.e. states in $Q_f$ (resp. $Q_c$), are only reachable by faulty (resp. correct) runs. This can be done without loss of generality. Indeed, considering a pLTS $\mathcal{A} = \langle Q, q_0, \Sigma, T, \mathbf{P} \rangle$, we can build the pLTS $\mathcal{A}' = \langle Q', (q_0, \perp), \Sigma, T', \mathbf{P}' \rangle$ where:

$$ \bullet \ Q' = Q \times \{\perp, \top\}, $$
• $((q, i), a, (q', j)) \in T'$ if $(q, a, q') \in T$, and either $a \neq \mathbf{f}$ and $i = j$ or $a = \mathbf{f}$ and $j = \top$,

• for $((q, i), a, (q', j)) \in T'$, $\mathbf{P}'((q, i), a, (q', j)) = \mathbf{P}(q, a, q')$.

Denoting $Q_f = Q \times \{\top\}$ and $Q_c = Q \times \{\bot\}$, the pLTS $\mathcal{A}'$ has the same behaviour as $\mathcal{A}$ and verifies the partition mentioned above as a run enters $Q_f$ if and only if its last transition was a fault and can never go back to $Q_c$.

While the correct or faulty status of the current run may not be known to the observer, the observed sequences carry some information about them. An infinite (resp. finite) observed sequence $w \in \Sigma_o^\omega$ (resp. $\Sigma_o^*$) is called *ambiguous* if there exists a correct infinite (resp. signalling) run $\rho$ and a faulty infinite (resp. signalling) run $\rho'$ such that $\mathcal{P}(\rho) = \mathcal{P}(\rho') = w$. Otherwise, it is either *surely faulty*, or *surely correct* depending on whether $\mathcal{P}^{-1}(w) \cap \text{SR} \subseteq \mathbf{F}$ or $\mathcal{P}^{-1}(w) \cap \text{SR} \subseteq \mathcal{C}$. A run is ambiguous, surely correct or surely faulty if its observed sequence is ambiguous, surely correct or surely faulty respectively. We write $\mathbf{Sf}_\infty$ (resp. $\mathbf{Sc}_\infty$) for the set of infinite surely faulty (resp. correct) runs. In addition $\mathbf{Sf}_n$ (resp. $\mathbf{Sc}_n$) is the set of infinite runs whose signalling prefix of observable length $n$ is surely faulty (resp. correct).

**Example 2.8.** Consider the pLTS of Figure 2.3 associated with the mask function $\mathcal{P}$ such that $\mathcal{P}(\mathbf{f}) = \varepsilon$, $\mathcal{P}(\text{out of order}) = \mathcal{P}(\text{sugar}) = \text{beep and every other event is projected on itself.}$

First observe that this pLTS satisfies the partition between faulty and correct states. Indeed, a run ends in $f_1$ iff it is faulty.

The observed sequence “coin beep” is ambiguous as it can be generated by the correct run “$q_0$ coin $q_1$ sugar $q_1$” and the faulty signalling run “$q_0$ coin $q_1 \mathbf{f} f_1$ out of order $f_1$”. Extending this observed sequence with other observations of beep maintains the ambiguity. Extending it with ‘coffee’ however makes it surely correct. There does not exist any surely faulty observed sequence in this pLTS.

## 1.5 Which diagnosis for pLTS?

The goal of diagnosis is the automatic detection of the fault event. This detection is performed by a diagnoser, a function observing the system and giving its verdict. Formally, a diagnoser is a function $D: \Sigma_o^* \to \{?, \top, \bot\}$ assigning to every finite observed sequence a verdict. Informally, when a diagnoser outputs $?$ it does not provide any information, while $\top$ means that the diagnoser announces a fault and $\bot$ that the diagnoser provides some information about the correctness of the current run. Multiple notions of diagnoser, and thus of diagnosis, can be defined depending on the properties that we require. In logical systems, three main features of the diagnoser are considered: *verdict, correctness and reactivity*. Verdict specifies the nature of the information the diagnoser provides along the run: it may only be related to detection of faults or may also assert that (some prefix of) the run does not include a fault. Correctness specifies that when the diagnoser outputs a verdict, this verdict holds. Reactivity expresses the regularity at which the diagnoser must provide information about the status of the run.
The aim of this section is to define appropriate verdict, correctness and reactivity requirements for probabilistic systems. We start with informal explanations that also motivate the need for considering different variants of diagnosis. We present these variants as decision problems which are intuitively easier to understand and simpler to use. We make the link with diagnosers in Chapter 3.

In seminal works about probabilistic systems, the verdict is limited to fault detections and the reactivity is usually relaxed by requiring that when a fault occurs, a diagnoser almost surely detects it after a finite delay [TT05]. Let us look at the pLTS of Figure 2.4. One cannot detect that the run $q_0f(f_1a)^\omega$ is faulty due to the correct run $q_0u(q_1a)^\omega$ with same observed sequence $a^\omega$. However with probability 1, a faulty run will produce a ‘b’ and thus almost all faulty runs are unambiguous, so that faults are almost surely detected. On the other hand, one cannot provide any information about the single correct run $q_0u(q_1a)^\omega$ since its observed sequence is ambiguous as well as any of its prefix. Observe that the notion of ambiguity described here is qualitative: the observation of the correct run is considered ambiguous even though the probability to be faulty, conditioned on the observation, converges to 0.

<figure><img src="image_19.png" /><figcaption>Figure 2.4: Detecting faults but not correct runs. When probabilities are not specified, we assume uniform distributions. Dashed edges are used for unobservable transitions. For observable transitions, the observation given by the mask function labels the edge.</figcaption></figure>

In order to examine which verdict could be provided about correct runs, let us look at the pLTS of Figure 2.5. The sequence $a^n$ is ambiguous. However up to the $n - 1^{th}$ observation, all the runs that correspond to this observed sequence were correct which is a useful information for instance to restart later the system from a correct state. Along the (surely correct) observed sequence $a^\omega$, the observer can always deduce that longer and longer prefixes of the run were correct while never being able to assert that the current run is correct.

<figure><img src="image_20.png" /><figcaption>Figure 2.5: Detecting correctness for longer and longer prefixes of correct runs.</figcaption></figure>
The correctness requirement may be specified in different ways. For an exact diagnosis, we ask that a fault can be claimed only when a fault surely happened (as it is the case in non-probabilistic systems). However it may be necessary to weaken the correctness requirement as illustrated by the pLTS of Figure 2.6. Since all observed sequences are ambiguous no exact diagnosis can be provided. However it is clear that when in a long enough observed sequence the ratio between occurrences of ‘b’ and ‘a’ is close to 3, the probability that the corresponding run is faulty is close to 1. Let us fix any $\epsilon > 0$ and only require that the probability for the verdict to be erroneous should be less than $\epsilon$. Then using the strong law of large numbers, (approximate) fault detection is possible in this pLTS.

<figure><img src="image_21.png" /><figcaption>Figure 2.6: When approximate diagnosis is necessary.</figcaption></figure>

To formalise later the correctness of an approximate diagnoser, with every observed sequence $w \in \Sigma_o^*$ we associate a *correctness proportion*

$$ \mathrm{CorP}(w) = \frac{\mathbb{P}(\{\rho \in \mathbf{C} \cap \mathbf{SR}_{|w|} | \mathcal{P}(\rho) = w\})}{\mathbb{P}(\{\rho \in \mathbf{SR}_{|w|} | \mathcal{P}(\rho) = w\})}, $$

which is the conditional probability that a signalling run is correct given that its observed sequence is $w$.

The standard way to specify reactivity in probabilistic systems for fault detection is to require that whatever the minimal faulty run, almost surely the diagnoser will output its (faulty) verdict. We may also consider *uniform reactivity* which strengthens reactivity by requiring that the (random) delay is independent of the minimal faulty run. More formally, uniform reactivity ensures that given any positive probability threshold $\alpha > 0$ there exists a delay $n_\alpha$ independent of the considered minimal faulty run such that the probability to exceed this detection delay is bounded by $\alpha$.

<figure><img src="image_22.png" /><figcaption>Figure 2.7: When reactivity cannot be uniform.</figcaption></figure>
Let us illustrate these reactivity features with the pLTS of Figure 2.7 for which only approximate diagnosis is possible. Fix some $\varepsilon > 0$ and consider the minimal faulty run $q_0 u q_1 (aq_1)^m f q_f$. After a certain number of occurrences of 'b' (say $n$), the correctness proportion of the observed sequence $a^m b^n$ will be less than $\varepsilon$ and thus the diagnoser can output its verdict. However due to the probabilities of an occurrence of 'a' in correct and faulty runs respectively equal to $\frac{3}{4}$ and $\frac{3}{16}$, $n$ must depend on $m$ and so this reactivity cannot be uniform. This can be mathematically seen through the definition of CorP: for $n \ge 1$,

$$ \text{CorP}(a^m b^n) = \frac{\frac{3^m}{4^{m+n}}}{\frac{3^m}{4^{m+n}} + \left(\frac{3}{16}\right)^m \times \frac{15}{16}} = \frac{1}{1 + \frac{15}{16} \times 4^{n-m}} $$

In order to have $\text{CorP}(a^m b^n) \le 1/2$, one needs $n > m$. Therefore uniform diagnosis is not possible.

In order to formalise the different requirements discussed above, we first define several sets of runs related to ambiguity.

**Definition 2.7 (Ambiguous runs).** Let $\mathcal{A}$ be a pLTS, $\varepsilon \ge 0$ and $n \in \mathbb{N}_{>0}$. Then:

* $\text{FAmb}_\infty$ is the set of infinite faulty ambiguous runs of $\mathcal{A}$;

* $\text{CAmb}_\infty$ is the set of infinite correct ambiguous runs of $\mathcal{A}$;

* $\text{FAmb}_n$ is the set of infinite runs of $\mathcal{A}$ whose signalling prefix of observable length $n$ is faulty and ambiguous;

* $\text{CAmb}_n$ is the set of infinite runs of $\mathcal{A}$ whose signalling prefix of observable length $n$ is correct and ambiguous.

* $\text{FAmb}_n^\varepsilon$ is the set of infinite faulty ambiguous runs of $\mathcal{A}$ whose observed sequence of length $n$, $w$ fulfils: $\text{CorP}(w) > \varepsilon$.

By definition, for all $n \in \mathbb{N}$, $\text{FAmb}_n^0 = \text{FAmb}_n$. Observe that, for all $n \in \mathbb{N}$, and $\varepsilon \ge 0$, $\text{CAmb}_n$, $\text{FAmb}_n$ and $\text{FAmb}_n^\varepsilon$ are open sets, thus measurable. However, $\text{CAmb}_\infty$ and $\text{FAmb}_\infty$ are not Borel sets in the general case (e.g. see Chapter 3, Section 3).

We propose five specifications of exact diagnosability for probabilistic systems based on three discriminating criteria: whether the unambiguity requirement holds for faulty runs only or for all runs, whether ambiguity is defined at the level of infinite runs or for longer and longer finite signalling prefixes, and whether the delay before detection of minimal faulty runs is uniform. These notions are summarised in Figure 2.8 except for uniformity postponed to next figure.

**Definition 2.8 (Exact diagnosability).** Let $\mathcal{A}$ be a pLTS.

* $\mathcal{A}$ is IF-diagnosable if $\mathbb{P}(\text{FAmb}_\infty) = 0$.

* $\mathcal{A}$ is IA-diagnosable if $\mathbb{P}(\text{FAmb}_\infty \uplus \text{CAmb}_\infty) = 0$.
<figure><img src="image_23.png" /><figcaption>Figure 2.8: Summarising the variants of exact diagnosis.</figcaption></figure>

* A is FF-diagnosable if $\limsup_{n \to \infty} \mathbb{P}(\text{FAmb}_n) = 0$.

* A is FA-diagnosable if $\limsup_{n \to \infty} \mathbb{P}(\text{FAmb}_n \uplus \text{CAmb}_n) = 0$.

* A is uniformly FF-diagnosable if for all $\alpha > 0$ there exists $n_\alpha \in \mathbb{N}$ such that for all $n \ge n_\alpha$ and all minimal faulty run $\rho \in \min F$

$$ \mathbb{P}(\{\rho' \in \text{FAmb}_{n+|\rho|_o} \mid \rho \preceq \rho'\}) \le \alpha \cdot \mathbb{P}(\rho). $$

Uniform and/or approximate diagnoses are defined for FF-diagnosis as summarised in Figure 2.9. We chose FF-diagnosis as it corresponds to the classical notion of diagnosis. Moreover there is no clear intuition on what would be the meaning of uniformity and approximation for the other variants. $\varepsilon$FF-diagnosability allows the diagnoser to claim a fault when the correctness proportion does not exceed $\varepsilon$, and accurate approximate diagnosability denoted by AFF-diagnosability corresponds to $\varepsilon$FF-diagnosability for arbitrary $\varepsilon > 0$.

**Definition 2.9** (Approximate diagnosability). Let A be a pLTS, and $\varepsilon \ge 0$.

* A is $\varepsilon$FF-diagnosable if for every minimal faulty run $\rho \in \min F$ and all $\alpha > 0$ there exists $n_{\rho,\alpha}$ such that for all $n \ge n_{\rho,\alpha}$:

$$ \mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^{\varepsilon}) \le \alpha \cdot \mathbb{P}(\rho). $$

* A is uniformly $\varepsilon$FF-diagnosable if for all $\alpha > 0$ there exists $n_\alpha$ such that for all minimal faulty run $\rho \in \min F$ and all $n \ge n_\alpha$:

$$ \mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^{\varepsilon}) \le \alpha \cdot \mathbb{P}(\rho). $$
<figure><img src="image_24.png" /><figcaption>Figure 2.9: Summarising the approximate variants of FF-diagnosis.</figcaption></figure>

• *A* is (resp. *uniformly*) *AFF*-diagnosable *if it is* (resp. *uniformly*) $\varepsilon\text{FF}-\text{diagnosable}$ for all $\varepsilon > 0$.

When studying diagnosis, we are interested in the following problems. First, for every notion of diagnosability, we want to determine if it is possible to automatically decide whether a given system is diagnosable. Moreover, in the positive case, we want to establish the exact complexity of the problem. Then, given a diagnosable system, we want to build a diagnoser satisfying the corresponding verdict, correctness and reactivity features. When possible, we represent the diagnoser using a finite-state automaton to express that only a finite memory is necessary. The problems can vary depending on the framework. For example, when the system is controllable, we want to decide if one can control the system in a way ensuring diagnosability.

## 2 State of the art on diagnosis

**Diagnosis of finite LTS.** For LTS, diagnosability requires that the occurrence of unobservable faults can be deduced after a finite delay from the sequence of observable events occurring before and after the fault [SSL+95]. Using the definitions we introduced in this chapter, an LTS is diagnosable iff $\bigcup_{n \in \mathbb{N}} \bigcap_{m \ge n} \text{FAmb}_m = \emptyset$. Diagnosability of finite LTS was shown to be decidable in NLOGSPACE [JHCK01, YL02]. The algorithm relies on the twin-plant described page 29. An LTS is not diagnosable iff there exists a reachable cycle in the twin-plant in which each state is a pair composed of a faulty and a correct state. Detecting such a cycle can be done in non-deterministic logarithmic space in the twin-plant, which is quadratic in the size of the original LTS, hence the result.
Surprisingly, while deciding diagnosability is easy, the construction of the diagnoser can
require exponential time. This construction is based on the belief construction quickly
presented page 29.

**Diagnosis of infinite LTS.** An LTS with infinitely many states must be represented by a higher level model in order to be studied. This can be done using Petri nets (PN) for example. The semantics of a PN is called the reachability graph and can be represented by an LTS. This LTS is finite iff the PN is bounded. Cabasino et al. studied diagnosis of both bounded and unbounded PN [CGLS12]. In order to solve diagnosability in the unbounded case they first build the verifier net, which is a construction similar to the twin-plant, then construct the coverability graph (a finite abstraction of the reachability graph) of the verifier net and finally analyse the cycles of the coverability graph. This final analysis requires some additional properties of the cycles compared to the analysis in the twin-plant for finite LTS. This algorithm however has a complexity that depends on the size of the coverability graph, which may be Ackermanian in the size of the description of the PN. An algorithm with better complexity was developed in [BHSS18]. It still uses the verifier net, but transforms the diagnosability problem into an LTL formula and uses model-checking results to obtain an EXPSPACE upper bound. Interestingly, this paper also studies opacity, confirming the intuition that opacity and diagnosis are two close problems. See [Bas14] for a presentation of the usual techniques used for fault diagnosis in PN. LTS with infinitely many states can also be represented by pushdown systems. Morvan and Pinchinat showed that diagnosability in the general case is undecidable [MP09]. However, for a large subclass called visibly pushdown automata, diagnosability can be decided in PTIME. This is done by building once again a form of twin-plant, this time making the product of the visibly pushdown automata. Thanks to this product, they can define an appropriate Büchi condition on the twin-plant so that diagnosability can be deduced from the emptiness of the obtained Büchi pushdown automaton (checking the emptiness can be done in PTIME). The restriction to visibly pushdown automata, which we discuss in Chapter 5, is required in order to build the twin-plant.

**Diagnosis of stochastic systems.** When diagnosability was adapted to stochastic
systems by Thorsley and Teneketzis in [TT05], two notions of diagnosability were ini-
tially defined: A-diagnosability and AA-diagnosability. In finite pLTS, A-diagnosability
corresponds to our uniform FF-diagnosability and AA-diagnosability corresponds to our
uniform AFF-diagnosability. For A-diagnosability, they gave a necessary and sufficient
condition based on the belief construction: they first build a diagnoser similarly to
what was done for logical systems, then test for the recurrence of ambiguous states
of the belief (i.e. states that can contain both correct and faulty states). The com-
plexity of the algorithm checking this characterisation is not mentioned however. For
AA-diagnosability, they only give a sufficient condition, leaving the general problem
open. The questions left opened by [TT05] were tackled by Chen and Kumar who
gave algorithms with PTIME complexities to answer both diagnosability decision prob-
lems [CK13]. Their algorithm for AA-diagnosability is particularly interesting as they
translate the problem into a question of language equivalence (in terms of probability of words) for the original pLTS in a specific initial distribution. Unfortunately, these two algorithms are erroneous (see Chapter 4 for details on these two problems).

When a pLTS is not diagnosable, one interesting question that can be raised is how far from diagnosability it is. If there is only a very little chance that the fault is not detected, the system may be “diagnosable enough”. This direction was studied in [ND08] where Nouioua and Dague consider an exact notion of diagnosability and wish to measure the probability of the faulty ambiguous runs. To realise this measure, they make the product of the pLTS with its belief construction (thus a method that we already presented page 29). Then they measure the asymptotic probability to be in each state of this product pLTS. As, thanks to the belief, states contain the relevant information to determine if they were reached by a faulty ambiguous run, they can determine the probability to be faulty and ambiguous at the limit. This approach is continued in [BFG17] where Bazille et al. introduce a notion of *k*-diagnosability degree, which is defined as the probability to detect a fault at most *k* steps after it occurs, conditioned to the occurrence of a fault. They measure this degree by (1) building the product of the pLTS with the belief construction and (2) using polynomial time algorithms that compute the sum of the probabilities of the runs that reach a target state set (in this case, the states which belief component show they were reached by faulty ambiguous runs). Using the computation of *k*-diagnosability degrees for different values of *k*, they also investigate the average speed of detection of a fault.

**Active diagnosis.** One can enrich an LTS by allowing a form of control. This is done by introducing non-determinism, that is resolved at every step by a controller. One possibility of control is done through restriction of the enabled events: at every step, the controller selects a set of observable events $\Sigma^\bullet \subseteq \Sigma_o$ and the next transition taken by the LTS is labelled either by an unobservable event or by an observable one which observation belongs to $\Sigma^\bullet$. Some observable events can also be considered uncontrollable and are enabled no matter the choice of the controller. In this framework, the diagnosability of a system depends on the choice of the controller. Finding a controller such that the controlled system is diagnosable is the goal of *active diagnosis*. This problem was introduced in [SLT98]. Sampath, Lafortune and Teneketzis then solve the question by building the most permissive controller through a complicated iterative procedure which complexity is not given (and seems to be doubly exponential). Later, a planning-based approach via a twin-plant construction was proposed in [CP09]. The exact complexities were finally established in [HHMS13, HHMS17], where the active diagnosis problem was shown to be EXPTIME-complete and finite-memory controllers (most permissive and optimal in memory size) are given. This is done by translating the active diagnosis problem into a Büchi game (using a variant of the product with the belief) and then solving the Büchi game, which gives an optimal strategy which can be translated back into a controller. This analysis was extended to controllable stochastic systems [BFH$^{+14}$]. Here, instead of translating the problem to a Büchi game, Bertrand et al. use partially observable Markov decision processes and show that the problem of stochastic active diagnosis is also EXPTIME-complete. They also study a safe notion of
stochastic active diagnosis where the controller is required to keep a positive probability of infinite correct runs. This second problem is then showed to be undecidable in the general case and EXPTIME-complete when limited to finite-memory strategies.

The control on the system is not necessarily related to the events, it can also be applied on the observations. The observations of a system are given by sensors. In order to detect an event, one needs to have a sensor at the appropriate position and for it to be switched on. In [CT08] and [TT07] the authors investigate in slightly different frameworks, how to limit the number of sensors needed and how to build a controller which chooses at every step which sensor is switched on or off. The main differences between the two papers are twofold: (1) [TT07] considers both logical and stochastic systems while [CT08] only focuses on logical systems and (2) [CT08] establishes that a most permissive finite-state controller can be computed in doubly exponential time, using a game-theoretic approach while [TT07] does not give the exact complexity of their algorithm.

See [ZL13] for a survey on diagnosis mainly describing results for logical systems, but discussing also timed, stochastic and active systems.
# Part II

## Analysing information in passive
systems
<figure><img src="image_25.png" /></figure>
# Chapter 3

## Semantical analysis of diagnosability

As explained in Chapter 2, diagnosers observe the system to determine if its behaviour is correct or not. They are formalised as functions giving a verdict to each sequence of observation produced by a run of the system. There exist many different ways to define a diagnoser, depending on the properties a system designer may want. We identified as the most important features of a diagnoser its verdict, correctness and reactivity.

* The *verdict* determines what information is given by the diagnoser. Consequently, changing the verdict literally means modifying the purpose of the diagnoser. For example, when testing a car, if a component malfunctions, the company needs to detect it. The diagnoser thus only needs to detect the faulty behaviour of the system. However, the verdict of a diagnoser could also require to detect the correct behaviour of a system. For example, when following online a critical system like a power plant, the technicians needs to know that the system is correct. If the system can be faulty, they may need to shut it down in order not to take any risk, which can have an important cost.

* The *correctness* determines if the diagnoser is allowed to make an erroneous claim and, if so, how accurate must its claim be. It is of course better to have a diagnoser that does not make any error, but this restriction is not always realistic. Consider a program simulating dice throws. If the program outputs 4 a high number of times in a row, this may be a correct behaviour as such a throw has a positive probability. However, the longer this streak of 4 continues, the more likely it is caused by a malfunction of the program.

* The *reactivity* determines how quickly and how often the diagnoser must output a verdict. One possibility would be to require that if a fault occurs, after a bounded delay this fault will be detected. This is the reactivity that is often required in non-probabilistic systems represented by an automaton [SSL+95]. This requirement is too strong however for probabilistic systems. Indeed, in probabilistic systems, one can have for example an event which can occur at every step after a fault
with some probability, say 1/2, and which allows the detection of the fault. In
expectation, the fault is thus detected after two steps, but no bound can be given
on the maximum delay. This is a situation occurring in every system where, after
a fault, the system can, with some probability, continue to act normally. When
studying probabilistic systems, the reactivity requirement must thus be adapted.
This can be done, for example, by requiring that with probability 1 the fault will
be detected. This version of reactivity allows to ignore runs that have a zero
probability of occurring.

The choice of the verdict, correctness and reactivity notions of a diagnoser thus depends
on what information the designer of the system desires and on which guarantees are
demanded. The decisions that are taken also affect the complexity of determining
the diagnosability and of building the diagnoser. They thus also affect the capacities
required from the computer that will carry out the diagnosis. Studying as many relevant
notions as possible and clearly establishing their complexity is thus necessary for an
appropriate application of diagnosis.

In Chapter 2, multiple notions of diagnosability were defined for probabilistic sys-
tems based on the ambiguity of specific sets of runs. This allowed us to establish
diagnosability analysis as a decision problem which is easier to use in proofs and more
intuitive. However, the end goal of analysing the diagnosability of a system being to
build a diagnoser, one could also use the following definition: given notions of verdict,
correctness and reactivity, a system is called diagnosable if there exists a diagnoser of
the system achieving these features. We will show in Section 1 how to reconcile these
two approaches: we will associate a diagnoser with each diagnosability notion previously
defined. Having defined these associated diagnosers will allow us to see how the notions
of diagnosability translate on an actual run of the system.

Once the notions of diagnoser have been clearly defined, we must determine how
the different variants of diagnosability relate to one another. Establishing links between
multiple notions is a classical part of the semantical analysis of a problem. Through
this analysis, one can establish that two definitions that are syntactically different,
are in fact equivalent. In this case, one can choose to use either definition in a proof
for example. Implications between two notions are also useful. If a system verifies a
stronger property, we will not have to check for the weaker ones. For diagnosability, it
allows the system designer to select the strongest available diagnoser without having to
check every notion. Or at least one of the strongest notions as some of them may be
incomparable. Therefore, establishing the links between the notions of diagnosability
defined previously will be the focus of Section 2

The last goal of this chapter, presented in Section 3 will be to give, when possible,
a characterisation of the notions of diagnosability. As we wish to have the simplest
possible characterisation, an important question is to determine what information is
needed to characterise diagnosability. For example, can we restrict ourselves to studying
the structure of the system or do probabilities matter? And if they do, in what way?
In fact, in the general case, a characterisation relies both on the structure of the system
and on its probabilities.
* The structural part of the characterisation is based on descriptive set theory called in Chapter 2, Section 1.1. We will define a logic generating sets of runs belonging to a low level of the Borel hierarchy and associate, when possible, a formula with every notion of diagnosability.

* The probabilistic part then consists in measuring the probability of the set of runs identified above. The system is then diagnosable if and only if this measure verifies a qualitative requirement.

Having such a characterisation has multiple advantages. For example, using model-checking techniques, one could use these characterisations to solve diagnosability as we explain in Chapter 5. However this is not necessarily the optimal method as shown in Chapter 4. As another example, each Borel set is associated with a level of the Borel hierarchy. The higher this level, the more complicated the set is. This complexity reflects a complexity to measure the probability of the set but also a complexity of understanding the meaning behind this set. Having a characterisation with a set belonging to a low level of the Borel hierarchy thus makes it easier for the system designer to understand the associated diagnosability notion.

This chapter presents and extends some of the results given in [BHL14, BHL16a, BHL16b].

# 1 Diagnoser and diagnosability

In this section we focus on the synthesis of diagnosers for the notions of diagnosis defined in Chapter 2. Recall the definition of diagnosers:

**Definition 3.1.** A diagnoser is a function $D : \Sigma_o^* \to \{?, \top, \bot\}$ assigning to every finite observed sequence a verdict.

Multiple verdicts can be required for the diagnosers. Intuitively, ? does not provide any information, $\top$ claims the occurrence of a fault and $\bot$ provides information about the correctness of the current run.

Diagnosability as defined in Chapter 2 considers infinite behaviours: either by focusing on the ambiguity of infinite runs, or by requiring that the probability of a set of finite runs converge to 0 when their length diverges to infinity. On the contrary, diagnosers are built to react and give an information after a finite number of observations. There is therefore no easy direct link between diagnosability and diagnosers.

Due to its definition, a diagnoser may use infinite memory or more precisely, unbounded memory. While infinite memory is not achievable in real systems, unbounded memory is. It however raises a question on how to implement this memory and how much information has to be kept by the diagnoser. For example, if a diagnoser only needs to remember how many observations occurred, it may rely on a counter which, although unbounded, is easy to represent and to modify. When implementing a diagnoser (which will be done in Chapter 4), it is still natural to limit oneself to finite memory. We therefore define now the notion of finite-memory diagnosers.
**Definition 3.2.** A finite-memory diagnoser is given by a tuple $(M, \Sigma_o, m_0, \text{up}, D_{fm})$ where:

* $M$ is a finite set of memory states,

* $m_0 \in M$ is the initial memory state,

* $\text{up} : M \times \Sigma_o \to M$ is a memory update function,

* $D_{fm} : M \to \{?, \top, \bot\}$ is a diagnoser function.

A finite-memory diagnoser $(M, \Sigma_o, m_0, \text{up}, D_{fm})$ can be seen as a deterministic automaton over $\Sigma_o$ where the set of states is $M$, the initial state is $m_0$ and the transition function is up. Moreover the states of this automaton are labelled by an element of $\{?, \top, \bot\}$ which is given by the function $D_{fm}$. The update up is extended into a function $\text{up} : M \times \Sigma_o^* \to M$ defined inductively by $\text{up}(m, \varepsilon) = m$ and $\text{up}(m, wa) = \text{up}(\text{up}(m, w), a)$. The size of a finite-memory diagnoser is given by its number of memory states. A finite-memory diagnoser is not a diagnoser as defined in Chapter 2 and recalled in Definition 3.1, yet it induces the diagnoser $D$ defined by $D(w) = D_{fm}(\text{up}(m_0, w))$.

**Example 3.1.** Consider the finite-memory diagnoser $(M, \{a, b\}, m_0, \text{up}, D_{fm})$ (represented in Figure 3.1) where

* $M = \{m_0, m_b\}$,

* $\text{up}(m_0, a) = m_0$, $\text{up}(m_0, b) = \text{up}(m_b, a) = \text{up}(m_b, b) = m_b$,

* $D_{fm}(m_0) = ?$ and $D_{fm}(m_b) = \top$.

It induces a diagnoser $D$ which makes no claim as long as it only observes 'a' and claims a fault as soon as a 'b' is observed. It then commits to this choice and keeps claiming a fault whatever is observed next.

<figure><img src="image_26.png" /><figcaption>Figure 3.1: The finite-memory diagnoser of Example 3.1. The verdict given by $D_{fm}$ in a memory state is written below the state.</figcaption></figure>

Each following subsection focuses on one notion of diagnosability. They are ordered from the easiest to the most difficult definition of diagnoser. Due to the relations that will be established in Section 2, we won't detail every notion of diagnosability here.
## 1.1 FF-diagnosers

We will start by defining the FF-diagnosers of a pLTS, which is the diagnoser associated with FF-diagnosability. Recall that FF-diagnosability requires the probability of the set of faulty ambiguous finite runs to converges to 0 (i.e. $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_n) = 0$). These diagnosers only provide information about faulty runs, they therefore never raise a $\perp$ verdict. However they need to raise a $\top$ verdict almost surely after a finite delay in a faulty run. We can thus restrict their verdict to the set $\{?, \top\}$. We require from diagnosers associated with exact diagnosability notions that they satisfy an additional property, commitment, which means that when it claims a fault it will persistently claim it in the future. This can be done thanks to the permanence of the fault, i.e. a faulty run will remain faulty.

**Definition 3.3.** An FF-diagnoser for a pLTS $\mathcal{A}$ is a function $D : \Sigma_o^* \to \{\top, ?\}$ such that:

**commitment** For every $w \preceq w' \in \Sigma_o^*$, if $D(w) = \top$ then $D(w') = \top$.

**correctness** For every $w \in \Sigma_o^*$, if $D(w) = \top$ then $w$ is surely faulty.

**reactivity** For every $\rho \in \min\mathbf{F}$, $\mathbb{P}(\{\rho' \in \Omega \mid \rho \preceq \rho' \wedge D(\mathcal{P}(\rho')) = ?\}) = 0$ where for $w \in \Sigma_o^\omega$, $D(w) = \lim_{n \to \infty} D(w_{\le n})$.

Let us comment on this definition. The commitment property ensures that if the diagnoser outputs $\top$ at some point it will always output $\top$. The correctness property forbids the diagnoser to claim a fault during the observation of a correct run. This reflects that FF-diagnosability is a notion of *exact diagnosability*. Thus the FF-diagnoser is *exact* too. The limit in the reactivity condition of the above definition is well defined. Indeed, note that if $\top$ is produced, due to the commitment property, the limit is $\top$. Otherwise the diagnoser always outputs $?$ so that the limit is also a $?$ verdict.

<figure><img src="image_27.png" /><figcaption>Figure 3.2: An FF-diagnosable pLTS.</figcaption></figure>

**Example 3.2.** For the pLTS of Figure 3.2, we define the diagnoser $D$ such that $D(\varepsilon) = ?, \text{ for all } n \in \mathbb{N}, D(a^n) = ? \text{ and for every word } w \notin a^*, D(w) = \top$. This diagnoser is in fact the one induced by the finite-memory diagnoser of Example 3.1. Such a diagnoser is indeed an FF-diagnoser:

**commitment** Once a 'b' is observed, every subsequent observation is also a 'b', therefore once $D$ produces $\top$, it will keep outputting $\top$.
**correctness** If a $\top$ has been produced, b was observed. The only transition labelled by a 'b' is the self-loop on $f_2$ which can only be reached by faulty runs. Therefore any observed sequence for which D outputs $\top$ is surely faulty.

**reactivity** Let $\rho$ be a minimal faulty run. It ends either in $f_1$ or in $f_2$. If it ends in $f_1$, then with probability 1 a run extending $\rho$ takes the transition to $f_2$. In $f_2$, it will read a 'b' in the next step. In other words, with probability 1, a faulty run will trigger a 'b' and thus $\top$ is raised by the diagnoser. Due to the commitment property, given a faulty run $\rho$, the probability that the diagnoser outputs $?$ infinitely often during the observation of a run extending $\rho$ is thus 0.

Observe also that this pLTS is indeed FF-diagnosable as for $n \ge 1$, we have

$$ \mathbb{P}(\mathbf{FAmb}_n) = \mathbb{P}(\{\rho \in \mathbb{F}_n \mid \mathcal{P}(\rho_{\downarrow n}) = a^n\}) = \frac{1}{2^n} $$

As suggested by the above example, there exists an FF-diagnoser if and only if the system is FF-diagnosable. We now prove this formally.

**Proposition 3.1.** A pLTS is FF-diagnosable if and only if it admits an FF-diagnoser.

This proof is done in the following way. Assuming there exists an FF-diagnoser we study a family of sets of faulty runs $FD_n$ that corresponds to runs where the fault is claimed after $n$ observations. We compute the probability of this set and link this value to the probability of $FAmb_n$. This then allow us to show that the probability of $FAmb_n$ converges to 0, proving thus the FF-diagnosability of the pLTS. Assuming the pLTS is FF-diagnosable, we present a diagnoser and then show it is an FF-diagnoser by proving the properties one by one.

*Proof.* Let $\mathcal{A}$ be a pLTS, and assume there exists an FF-diagnoser $D$ for $\mathcal{A}$. For every $n \in \mathbb{N}$, we define $FD_n = \{\rho \in \mathbb{F}_\infty \mid D(\mathcal{P}(\rho_{\downarrow n})) = \top\}$ the set of faulty runs that are diagnosed faulty after $n$ observed events. We will start by showing that $\lim_{n \to \infty} \mathbb{P}(FD_n) = \mathbb{P}(\mathbb{F}_\infty)$. As a consequence of the commitment property, the sequence $(FD_n)_{n \in \mathbb{N}}$ is non-decreasing and for every faulty run $\rho \in \mathbb{F}_\infty$, $D(\mathcal{P}(\rho)) = \lim_{n \to \infty} D(\mathcal{P}(\rho_{\downarrow n})) = ?$ is equivalent to $\rho \notin \bigcup_{n \in \mathbb{N}}(FD_n)$, i.e. $\lim_{n \to \infty} FD_n = \bigcup_{n \in \mathbb{N}}(FD_n) = \{\rho \in \mathbb{F}_\infty \mid D(\mathcal{P}(\rho)) \neq ?\}$. Since $D$ is reactive, for every minimal faulty run $\rho \in \min\mathbb{F}$, we have $\mathbb{P}(\{\rho' \in \Omega \mid \rho \le \rho' \wedge D(\mathcal{P}(\rho')) = ?\}) = 0$. As every faulty run is prefixed by an unique minimal faulty run, we have

$$ \mathbb{P}(\{\rho' \in \mathbb{F}_\infty \mid D(\mathcal{P}(\rho')) = ?\}) = \sum_{\rho \in \min\mathbb{F}} \mathbb{P}(\{\rho' \in \Omega \mid \rho \le \rho' \wedge D(\mathcal{P}(\rho')) = ?\}) = 0. $$

Thus,

$$ \begin{align*} \mathbb{P}(\bigcup_{n \in \mathbb{N}} (FD_n)) &= \mathbb{P}(\{\rho' \in \mathbb{F}_\infty \mid D(\mathcal{P}(\rho')) \neq ?\}) \\ &= \mathbb{P}(\mathbb{F}_\infty) - \mathbb{P}(\{\rho' \in \mathbb{F}_\infty \mid D(\mathcal{P}(\rho')) = ?\}) \\ &= \mathbb{P}(\mathbb{F}_\infty). \end{align*} $$
Moreover since $D$ is correct, for every $n \in \mathbb{N}$, $\mathrm{FD}_n \subseteq \mathrm{Sf}_n$. Therefore, for every $n \in \mathbb{N}$, $\mathbb{P}(\mathrm{FAmb}_n) = \mathbb{P}(\mathrm{F}_n) - \mathbb{P}(\mathrm{Sf}_n) \le \mathbb{P}(\mathrm{F}_n) - \mathbb{P}(\mathrm{FD}_n)$ and

$$ \lim_{n \to \infty} \mathbb{P}(\mathrm{FAmb}_n) \le \lim_{n \to \infty} \mathbb{P}(\mathrm{F}_n) - \mathbb{P}(\mathrm{FD}_n) = 0. $$

This shows that $\mathcal{A}$ is FF-diagnosable.

Assume now that $\mathcal{A}$ is FF-diagnosable. We define the function $D: \Sigma_o^* \to \{\top, ?\}$ by $D(w) = \top$ if and only if $w$ is a surely faulty observed sequence. Let us check that $D$ is an FF-diagnoser. As a surely faulty ambiguous sequence cannot become ambiguous again, $D$ fulfils the commitment property. Moreover, since $D(w) = \top$ iff $w$ is a surely faulty sequence, $D$ is correct. Now, let $\rho$ be a minimal faulty run.

$$ \mathbb{P}(\{\rho' \in \Omega \mid \rho \preceq \rho' \wedge D(\mathcal{P}(\rho')) = ?\}) = \lim_{n \to \infty} \mathbb{P}(\{\rho' \in \mathrm{FAmb}_{n+|\rho|_o} \mid \rho \preceq \rho'\}) . $$

For every $n \in \mathbb{N}$, we have $\{\rho' \in \mathrm{FAmb}_{n+|\rho|_o} \mid \rho \preceq \rho'\} \subseteq \mathrm{FAmb}_{n+|\rho|_o}$ and, as $\mathcal{A}$ is FF-diagnosable, $\lim_{n \to \infty} \mathbb{P}(\mathrm{FAmb}_n) = 0$. Therefore $\mathbb{P}(\{\rho' \in \Omega \mid \rho \preceq \rho' \wedge D(\mathcal{P}(\rho')) = ?\}) = 0$ and $D$ is reactive. $\square$

The notion of FF-diagnoser we defined is therefore appropriate for FF-diagnosability.

## 1.2 FA-diagnosers

FA-diagnosability and IA-diagnosability not only consider the diagnosis of faults but also of correct runs. Indeed, recall that they require respectively that the probability of the set of ambiguous finite runs converges to 0 (i.e. $\lim_{n \to \infty} \mathbb{P}(\mathrm{FAmb}_n \cup \mathrm{CAmb}_n) = 0$) and that the probability of infinite ambiguous runs is equal to 0 (i.e. $\mathbb{P}(\mathrm{FAmb}_\infty \cup \mathrm{CAmb}_\infty) = 0$). Contrary to FF-diagnosers, FA- and IA-diagnosers have three possible verdicts: $\top$, related to faulty sequences, $\bot$, linked with correctness, and $?$ when no information can be derived from the observation. We consider the partial order $\prec$ on these values defined by $?$ $\prec \top$ and $?$ $\prec \bot$. This order is natural as $?$ gives less information than the other verdicts. Although we consider the detection of correct and faulty runs, note that the situation is not symmetric given that the faults are persistent while correct runs may become faulty.

**Definition 3.4.** An FA-diagnoser for a pLTS $\mathcal{A}$ is a function $D: \Sigma_o^* \to \{\top, \bot, ?\}$ such that:

**commitment** For every $w \preceq w' \in \Sigma_o^*$, if $D(w) = \top$ then $D(w') = \top$.

**correctness** For every $w \in \Sigma_o^*$,

* if $D(w) = \top$ then $w$ is surely faulty;

* if $D(w) = \bot$ then $w$ is surely correct.

**reactivity** $\mathbb{P}(\{\rho \in \Omega \mid D(\mathcal{P}(\rho)) = ?\}) = 0$ where for $w \in \Sigma_o^\omega$, $D(w) = \liminf_{n \to \infty} D(w_{\le n})$.
Let us comment on this definition. The commitment property is similar to the one of the notion of FF-diagnoser. In particular, there is no commitment for a $⊥$ verdict. This is natural as a fault could appear later, forcing the diagnoser to change its verdict. The correctness property is also similar to the FF-diagnoser for a $⊤$ verdict. For the $⊥$ verdict, it is the dual, the diagnoser cannot output $⊥$ while observing a faulty run. This diagnoser is ‘exact’. The limit in the reactivity requires the partial order. While if a $⊤$ is claimed, the limit will be $⊤$, a $⊥$ verdict can be followed by a $?$ verdict. Due to the correctness property, the limit is equal to $⊥$ if the observed sequence is, after a finite number of observations, always surely correct.

<figure><img src="image_28.png" /><figcaption>Figure 3.3: An FA-diagnosable pLTS.</figcaption></figure>

**Example 3.3.** For the pLTS of Figure 3.3, we define the diagnoser D such that $D(ε) = ⊥$ and given an observed sequence $w \in \Sigma_o^*$, then $D(wb) = ⊤$, $D(wc) = ⊥$ and $D(wa) = D(w)$. Remarking that once a b or a c is observed, the other cannot appear any more, this diagnoser is induced by the finite-memory diagnoser of Figure 3.4. Such a diagnoser is indeed an FA-diagnoser:

**commitment** Once a 'b' is observed, every subsequent observation is also a 'b', therefore once D produces $⊤$, it will keep outputting $⊤$.

**correctness** If a $⊤$ has been produced, 'b' was observed previously. The only transition labelled by a 'b' is the self-loop on $f_2$ which can only be reached by faulty runs. Therefore any observed sequence for which D outputs $⊤$ is surely faulty. Similarly, when D outputs $⊥$ it means that a 'c' was observed previously and such an observation can only be made in $q_1$ which is a correct state from which no fault can ever be triggered. Thus the observed sequence is surely correct.

**reactivity** The set of infinite observed sequences $w$ for which $D(w) =?$ is restricted to $\{a^ω\}$. There exist exactly two runs corresponding to this observed sequence $ρ_1 = q_0u(q_1a)^ω$ and $ρ_2 = q_0f(f_1a)^ω$. Moreover, the probability of each of these two runs is 0 as firing 'a' in $q_1$ or in $f_1$ only has probability $1/2$. Thus with probability 1, a 'b' or a 'c' will be observed, ensuring the reactivity of D.

Observe also that this pLTS is indeed FA-diagnosable as for every $n \ge 1$, we have $FAmb_n = \{q_0u(q_1a)^nq_1, q_0f(f_1a)^nf_1, q_0f(f_1a)^{n-1}f_1af_2\}$. Thus $P(FAmb_n) = \frac{3}{2^{n+1}}$.

We now want to establish the link between the existence of an FA-diagnoser and FA-diagnosability. However, there is no equivalence in the general case. Indeed, let us
<figure><img src="image_29.png" /><figcaption>Figure 3.4: The finite-memory diagnoser of Example 3.3.</figcaption></figure>

consider the pLTS of Figure 3.5. The probability of the set of ambiguous runs of length $n \ge 1$ starting by $u_1$ is the probability to have read a ‘b’ on the $n-1$'th observation. This is equal to $\frac{1}{n+1}$. Moreover, runs initially starting by $u_2$ will almost surely trigger a ‘c’, removing the ambiguity. Thus it is FA-diagnosable. However, a run starting with $u_1$ will almost surely trigger infinitely many ‘b’s. Because of the correctness property, we have for every diagnoser $D$, $\mathbb{P}(\{\rho \in \Omega \mid D(\mathcal{P}(\rho)) =?\}) \ge \mathbb{P}(\{\rho \in \Omega \mid q_0u_1q_1 \preceq \rho\}) = \frac{1}{2}$. Thus, $D$ is not reactive.

<figure><img src="image_30.png" /><figcaption>Figure 3.5: An infinite FApLTS which does not accept any FA-diagnoser.</figcaption></figure>

Fortunately, the equivalence holds when restricted to finite pLTS. We postpone the proof of the following proposition to Chapter 4 (more precisely to Proposition 4.14, page 126) which focuses on finite pLTS.

**Proposition 3.2.** A finite pLTS $\mathcal{A}$ is FA-diagnosable if and only if it admits an FA-diagnoser.

As a conclusion, the definition of FA-diagnosers is similar to the one of FF-diagnosers, but with additional requirements to deal with the correct ambiguous runs. This fits the definition of FA-diagnosability which becomes equivalent to the one of FF-diagnosability when the set of correct ambiguous runs can be neglected. However, due to the complexity created by the fact that being correct is not a permanent status of runs (contrary to being faulty), the link between existence of an FA-diagnoser and FA-diagnosability cannot be established in the general case.
## 1.3 IA-diagnosers

The problem in defining IA-diagnosers is that IA-diagnosability defines ambiguity for infinite runs while a diagnoser must give its verdict after a finite observation. As a consequence, the information an IA-diagnoser gives after a finite run is weaker than the information an FA-diagnoser has to give.

**Definition 3.5.** An IA-diagnoser for A is a function $D : \Sigma_o^* \to \{\top, \bot, ?\}$ such that:

**commitment** For every $w \preceq w' \in \Sigma_o^*$, if $D(w) = \top$ then $D(w') = \top$.

**correctness** For every $w \in \Sigma_o^*$

* if $D(w) = \top$, then *w* is surely faulty;

* if $D(w) = \bot$, letting $|D(w)|_{\bot} = |\{0 < n \le |w| \mid D(w_{\le n}) = \bot\}|$, then for every signalling run $\rho$ such that $\mathcal{P}(\rho) = w$, $\rho_{\bot|D(w)|_{\bot}}$ is correct.

**reactivity** $\mathbb{P}(\{\rho \in \Omega \mid D(\mathcal{P}(\rho)) = ?\}) = 0$ where for any observed sequence $w \in \Sigma_o^\omega$, $D(w) = \limsup_{n \to \infty} D(w_{\le n})$.

Let us comment on the definition. Commitment is once again focused only on the $\top$ verdict. Correctness is usual for $\top$ but quite different for $\bot$. Indeed, the correctness of FA-diagnosers requires that a $\bot$ verdict means the observed sequence is surely correct. The interpretation of $D(w) = \bot$ for IA-diagnoser is that the diagnoser ensures that any signalling subrun of length $|D(w)|_{\bot} \le |w|$ of a signalling run for *w* is correct. Of course it may deduce this information from the last $|w| - |D(w)|_{\bot}$ observations. This does not reveal if the current run is correct or not. However, if the diagnoser outputs $\bot$ infinitely often along an observed sequence *w*, $\lim_{n \to \infty} |D(w_{\le n})|_{\bot} = \infty$. Therefore the infinite observed sequence *w* is surely correct. The reactivity condition uses a limit superior as we only need $\bot$ to be claimed infinitely often but not necessarily without ? in between.

<figure><img src="image_31.png" /><figcaption>Figure 3.6: An IA-diagnosable pLTS.</figcaption></figure>

**Example 3.4.** For the pLTS of Figure 3.6 we define the diagnoser *D* by: for any observed sequence *w* if there exists an observed sequence *w'* such that *w* = *w'*c then *D*(*w*) = $\top$, if *w* ∈ {*w'*aa, *w'*ab}, *D*(*w*) = $\bot$ else *D*(*w*) =? . This diagnoser is induced by the finite-memory diagnoser represented in Figure 3.7 Such a diagnoser is indeed an IA-diagnoser:

**commitment** Once a 'c' is observed, only a 'c' can appear, thus the diagnoser keep the $\top$ verdict.
**correctness** Observing a 'c' can only be made for faulty run, thus D correctly raises a $\top$. For the correct runs the idea is the following. After observing any sequence waa or wab, with $w \in \{a,b\}^*$, the diagnoser knows a posteriori that one step before, that is after the observation of wa, the run was necessarily correct. Indeed, observing the suffix aa is not possible after a fault, yet wba is not surely correct. After a run $\rho$ with such an observation we thus know that $\rho_{\downarrow|P(\rho)|-1}$ is correct and $|D(w)|_{\perp}$ is at most equal to $|P(\rho)| - 2$ as no $\perp$ can be claimed after 0 or 1 observation. Thus D is correct.

**reactivity** With probability 1 a faulty run will trigger a 'c' (raising a $\top$ verdict) and a correct run will trigger infinitely many 'a's (raising infinitely many $\perp$ verdicts).

Moreover this pLTS is IA-diagnosable as $\mathcal{C}Amb_\infty \cup \mathcal{F}Amb_\infty = \mathcal{P}^{-1}(\{a,b\}^*b^\omega)$ which has probability 0 as in every state there is a positive probability to trigger an action whose observation is different than b.

<figure><img src="image_32.png" /><figcaption>Figure 3.7: The finite-memory diagnoser of Example 3.3.</figcaption></figure>

We now aim at establishing the link between IA-diagnosability and the existence of an IA-diagnoser. Since IA-diagnosability gives an information about infinite runs, we need a way to translate it to finite runs in order to establish the link with the diagnoser. Hence, we first introduce a lemma linking the sets $\mathcal{F}Amb_n$ and $\mathcal{F}Amb_\infty$ for $n \in \mathbb{N}$. This lemma will be reused in the next section when establishing the link between FF-diagnosability and IF-diagnosability.

**Lemma 3.1.** Let $\mathcal{A}$ be a pLTS. Then $\lim_{n\to\infty} \mathcal{P}(\mathcal{F}Amb_\infty \setminus \mathcal{F}Amb_n) = 0$. Moreover, if $\mathcal{A}$ is finitely branching, then $\lim_{n\to\infty} \mathcal{P}(\mathcal{F}Amb_n \setminus \mathcal{F}Amb_\infty) = 0$.

The main difficulty of the following proof is in the second point. There, using the finitely-branching assumption and invoking König's lemma, we show that if the prefixes of a finite run are never surely faulty, then we can build an infinite correct run with the same observed sequence.
*Proof.* Observe that $\Omega$ admits the following partitions $\Omega = \mathbf{FAmb}_{\infty} \uplus \mathbf{C}_{\infty} \uplus \mathbf{Sf}_{\infty}$ and for all $n \in \mathbb{N}$, $\Omega = \mathbf{FAmb}_{n} \uplus \mathbf{C}_{n} \uplus \mathbf{Sf}_{n}$. Thus, for all $n \in \mathbb{N}$,

$$ \begin{aligned} \mathbf{FAmb}_{\infty} \setminus \mathbf{FAmb}_{n} &= (\mathbf{C}_{n} \uplus \mathbf{Sf}_{n}) \cap \mathbf{FAmb}_{\infty} \\ &= (\mathbf{C}_{n} \uplus \mathbf{Sf}_{n}) \setminus (\mathbf{C}_{\infty} \uplus \mathbf{Sf}_{\infty}) \subseteq (\mathbf{C}_{n} \setminus \mathbf{C}_{\infty}) \uplus (\mathbf{Sf}_{n} \setminus \mathbf{Sf}_{\infty}). \end{aligned} $$

Since for all $n$, $\mathbf{Sf}_{n} \subseteq \mathbf{Sf}_{\infty}$, one gets:

$$ \mathbf{FAmb}_{\infty} \setminus \mathbf{FAmb}_{n} \subseteq \mathbf{C}_{n} \setminus \mathbf{C}_{\infty}. $$

$\{\mathbf{C}_{n}\}_{n \in \mathbb{N}}$ is a non-increasing family of sets and we claim that $\mathbf{C}_{\infty} = \bigcap_{n \in \mathbb{N}} \mathbf{C}_{n}$. Indeed an infinite run $\rho$ is correct if and only if $f$ does not occur in it i.e. if and only if all its signalling subruns are correct. Thus, $\lim_{n \to \infty} \mathbb{P}(\mathbf{C}_{n} \setminus \mathbf{C}_{\infty}) = 0$ which implies $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_{\infty} \setminus \mathbf{FAmb}_{n}) = 0$.

For the other direction, using again the two partitions we obtain:

$$ \begin{aligned} \mathbf{FAmb}_{n} \setminus \mathbf{FAmb}_{\infty} &= (\mathbf{C}_{\infty} \uplus \mathbf{Sf}_{\infty}) \cap \mathbf{FAmb}_{n} \\ &= (\mathbf{C}_{\infty} \uplus \mathbf{Sf}_{\infty}) \setminus (\mathbf{C}_{n} \uplus \mathbf{Sf}_{n}) \subseteq (\mathbf{C}_{\infty} \setminus \mathbf{C}_{n}) \uplus (\mathbf{Sf}_{\infty} \setminus \mathbf{Sf}_{n}). \end{aligned} $$

Since for all $n$, $\mathbf{C}_{\infty} \subseteq \mathbf{C}_{n}$, one gets:

$$ \mathbf{FAmb}_{n} \setminus \mathbf{FAmb}_{\infty} \subseteq \mathbf{Sf}_{\infty} \setminus \mathbf{Sf}_{n} $$

Let us show that, under the assumption that $\mathcal{A}$ is finitely branching, $\mathbf{Sf}_{\infty} \subseteq \bigcup_{n \in \mathbb{N}} \mathbf{Sf}_{n}$. Let $\rho \notin \bigcup_{n \in \mathbb{N}} \mathbf{Sf}_{n}$. We build a tree as follows:

* Nodes at level $n$ correspond to the correct signalling runs whose observed sequence is $\mathcal{P}(\rho_{\downarrow n})$;

* The node at level $n+1$ associated with $\rho'$ is a child of the node at level $n$ associated with $\rho''$ if $\rho'' \le \rho'$.

Since $\rho \notin \bigcup_{n \in \mathbb{N}} \mathbf{Sf}_{n}$, for all $n \in \mathbb{N}$, there exists a correct run with observed sequence $\mathcal{P}(\rho_{\downarrow n})$, so that the above-defined tree is infinite. Since the pLTS is finitely branching and convergent, the tree is also finitely branching. By König's lemma, it must contain an infinite branch, thus there exists an infinite correct run whose observed sequence is $\mathcal{P}(\rho)$. As a consequence $\rho$ is not surely faulty: $\rho \notin \mathbf{Sf}_{\infty}$. This establishes that $\mathbf{Sf}_{\infty} \subseteq \bigcup_{n \in \mathbb{N}} \mathbf{Sf}_{n}$. Thus $\lim_{n \to \infty} \mathbb{P}(\mathbf{Sf}_{\infty} \setminus \mathbf{Sf}_{n}) = 0$ implying $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_{n} \setminus \mathbf{FAmb}_{\infty}) = 0$ which concludes the proof. □

We can now establish the following proposition.

**Proposition 3.3.** A finitely-branching pLTS $\mathcal{A}$ is IA-diagnosable if and only if it admits an IA-diagnoser.
*Proof.* Assume first that there exists an IA-diagnoser $D$ for $\mathcal{A}$, and let $\rho$ be an infinite run. By reactivity, almost surely $D(\mathcal{P}(\rho)) \in \{\top, \bot\}$. If $D(\mathcal{P}(\rho)) = \top$ then there exists some $n$ such that $D(\mathcal{P}(\rho_{\downarrow n})) = \top$. By correctness, $\rho_{\downarrow n}$ is surely faulty and thus $\rho$ is surely faulty. If $D(\mathcal{P}(\rho)) = \bot$, we claim that $\rho$ is surely correct. Observe that the diagnoser infinitely often outputs $\bot$, so by correctness, for all $n$, $\mathcal{P}(\rho_{\downarrow n})$ is surely correct and thus in particular $\rho_{\downarrow n}$ is correct. Assume there exists an infinite faulty run $\rho'$ with $\mathcal{P}(\rho') = \mathcal{P}(\rho)$. There exists a $n$ such that for all $m \ge n$, $\rho'_{\downarrow n}$ is faulty. Thus by correctness there can be no more than $n \bot$ verdicts for $\mathcal{P}(\rho)$ contradicting the fact that $D(\mathcal{P}(\rho)) = \bot$. Thus with probability 1, an infinite run is unambiguous.

Conversely, assume that $\mathcal{A}$ is IA-diagnosable. Given an observed sequence $w$, we denote by $N_w$ the largest integer such that $\text{Cyl}(\mathcal{P}^{-1}(w)) \cap \text{F}_{N_w} = \emptyset$, i.e. the largest integer such that every run with observation $w$ was correct after $N_w$ observations. We define the diagnoser $D$ such that $D(\varepsilon) =?$ and for every observed sequence $w$ and observation $a \in \Sigma_o$, if $wa$ is surely faulty, then $D(wa) = \top$, if $N_{wa} > N(w)$, then $D(wa) = \bot$ else $D(wa) = ?$.

* Commitment is direct from the definition of $D$.

* Correctness is achieved as $\top$ is raised for surely faulty runs and $\bot$ is raised when $N_w$ (for appropriate observed sequence $w$) increased, thus for all $w \in \Sigma_o^*$, $|D(w)|_{\bot} \le N_w$ which implies that for a run $\rho \in \mathcal{P}^{-1}(w)$, $\rho_{\downarrow|D(w)|_{\bot}}$ is correct.

* Reactivity, however, is a bit more complicated, we need the result of Lemma 3.1. Let $\rho \notin \text{FAmb}_{\infty} \cup \text{CAmb}_{\infty}$.

- If $\rho$ is correct, then suppose that there exists $n_0$ such that for all $n \in \mathbb{N}$, there exists a run $\rho^f \in \text{F}_{n_0}$ with $\mathcal{P}(\rho^f) = \mathcal{P}(\rho_{\downarrow n})$. Then using König's lemma and a construction similar to the one of Lemma 3.1, there exists $\rho_f \in \text{F}_{n_0}$ such that $\mathcal{P}(\rho) = \mathcal{P}(\rho^f)$ which would mean $\rho \in \text{CAmb}_{\infty}$ and raise a contradiction. Thus, as for each $n_0$ there exists $n \in \mathbb{N}$ such that $N_{\mathcal{P}(\rho_{\downarrow n})} \ge n_0$, $N_{\mathcal{P}(\rho)} = \lim_{n \to \infty} N_{\mathcal{P}(\rho_{\downarrow n})} = \infty$. As every time this value increases, $\bot$ is produced by $D$, $D$ outputs infinitely many $\bot$, thus $D(\mathcal{P}(\rho)) = \bot$.

- If $\rho$ is faulty, according to Lemma 3.1, $\lim_{n \to \infty} \mathbb{P}(\text{FAmb}_n \setminus \text{FAmb}_{\infty}) = 0$. Therefore, with probability one, there exists $n_0 \in \mathbb{N}$ such that $\rho \notin \text{FAmb}_n$ for $n \ge n_0$. Let $n_1$ such that $\rho \in \text{F}_{n_1}$ and $n_2 = \max(n_0, n_1)$, then by definition of $D$, $D(\mathcal{P}(\rho_{\downarrow n_2})) = D(\mathcal{P}(\rho)) = \top$.

Therefore $D$ is reactive.

Thus, $D$ is an IA-diagnoser.

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

IA-diagnosers are thus appropriately associated with IA-diagnosability. They manage to give information after a finite amount of time about infinite ambiguity. We start to see a complexity hierarchy between the various exact diagnosability notions. FF-diagnosability appears as the simplest notion as its equivalence with the existence of
an FF-diagnoser was established in the general case. Second comes IA-diagnosability for which we needed to restrict our framework to finitely-branching pLTS. Finally, the most difficult notion is FA-diagnosability for which the equivalence only holds for finite pLTS. This hierarchy is however only an intuition for now as it could be the result of an inappropriate choice of diagnosers definitions.

## 1.4 εFF-diagnosers

We now define the εFF-diagnosers corresponding to εFF-diagnosability for ε > 0. Recall that εFF-diagnosability requires that, after any minimal faulty run ρ, the probability of the set of faulty runs extending ρ whose observed sequence has a correctness proportion (CorP, defined page 46) above ε converges to 0 (i.e. $\lim_{n \to \infty} \mathbb{P}(\text{FAmb}_n^\varepsilon) = 0$)<fnref n="1" />. Given ε ≥ 0, εFF-diagnosers are similar to FF-diagnosers in the sense that both only consider faulty runs and thus never output a ⊥ verdict that would give information about correct runs. However, εFF-diagnoser may make errors: when they give a ⊤ verdict, then the probability that the claim is wrong is at most ε.

**Definition 3.6.** Let ε ≥ 0. An εFF-diagnoser for A is a function D : Σ<sub>o</sub>* → {⊤, ?} such that:

**correctness** For every w ∈ Σ<sub>o</sub>* if D(w) = ⊤ then CorP(w) ≤ ε;

**reactivity** $\limsup_{n \to \infty} \mathbb{P}(\{\rho \in \mathbf{F} \cap \mathbf{SR}_n \mid D(\mathcal{P}(\rho)) = ?\}) = 0$.

Let us comment on this definition. This diagnoser is no longer exact. Given an observed sequence w, it is allowed to output ⊤, if the probability of error is below ε as shown by the requirement CorP(w) ≤ ε. There is no longer a notion of commitment, allowing the diagnoser to go back from a ⊤ verdict to a ? verdict. This absence of commitment is one of the differences between the definition of εFF-diagnosers and the one of monitors for distinguishability of hidden Markov chains [SZF11, KS16]. See the discussion after Lemma 4.3, page 108, for more details about the links between monitoring and diagnosability. Finally, the reactivity condition as defined here is different from what was done for the other diagnosers. This choice was made in order to be closer to the corresponding diagnosability notion as approximate notions of diagnosis are harder to handle than exact ones.

One could introduce a uniform variant of this definition that would correspond to uniform εFF-diagnosability. However, this definition would not follow the same structure as the other ones as a uniform reactivity would have to be defined on individual runs instead of on the global conditions we used here.

**Example 3.5.** Let us observe the pLTS on the left of Figure 3.8. We define the diagnoser D such that given an observed sequence w ∈ Σ<sub>o</sub>* , then D(w) = ⊤ iff w contains at least as many ‘b’ than ‘a’, else D(w) =?. Clearly, this diagnoser does not satisfy any

<footnote n="1">¹This definition is written slightly differently from the one of Definition 2.9, page 48. Yet, one can quickly see that they are equivalent. However, we cannot easily express uniformity with a similar definition.</footnote>
<figure><img src="image_34.png" /><figcaption>Figure 3.8: Left: an 1/2FF-diagnosable pLTS. Right: a pLTS which is not εFF-diagnosable for any ε > 0.</figcaption></figure>

commitment property, but it is not required for εFF-diagnosers. Moreover, this diagnoser
cannot be translated into a finite-memory diagnoser as we need to keep the difference
between the number of occurrences of ‘a’ and ‘b’. We give a visual representation, using
an infinite number of states, of this diagnoser in Figure 3.9. Such a diagnoser is a
1/2FF-diagnoser:

**correctness** Given an observed sequence w, if $D(w) = \top$, then $\text{CorP}(w) = \frac{3^{|w|_a}}{3^{|w|_a} + 3^{|w|_b}}$.
As by definition of D, $|w|_a \le |w|_b$, $\text{CorP}(w) \le 1/2$, thus D is correct.

**reactivity** Let $\alpha > 0$, as faulty runs have a probability $3/4$ to raise a 'b' at each step, according to the weak law of large number there exists $n_0 \in \mathbb{N}$ such that for all $n \ge n_0$, $\mathbb{P}(\{\rho \in \mathbb{F}_n \mid |\mathcal{P}(\rho)|_a > |\mathcal{P}(\rho)|_b\}) < \alpha$. Let $\rho$ be a faulty run such that $D(\mathcal{P}(\rho)) =?$. Thus by definition of D, $\rho \in \{\rho' \in \mathbb{F}_n \mid |\mathcal{P}(\rho')|_a > |\mathcal{P}(\rho')|_b\}$. Therefore, for $n \ge n_0$, $\mathbb{P}(\{\rho \in \mathbb{F} \cap \text{SR}_n \mid D(\mathcal{P}(\rho)) =?\}) \le \mathbb{P}(\{\rho \in \mathbb{F}_n \mid |w|_a > |w|_b\}) < \alpha$. Thus D is reactive.

Observe also that this pLTS is indeed 1/2FF-diagnosable as for $n \ge 1$, $\mathbb{P}(\text{FAmb}_n^{1/2}) = \mathbb{P}(\{\rho \in \mathbb{F}_n \mid |\mathcal{P}(\rho_{\downarrow n})|_a > |\mathcal{P}(\rho_{\downarrow n})|_b\})$ which converges to 0 according to the weak law of large numbers.

<figure><img src="image_35.png" /><figcaption>Figure 3.9: An automaton representing the diagnoser of Example 3.5.</figcaption></figure>

The diagnoser used in Example 3.5 requires unbounded memory. In fact, there is
no finite-memory 1/2FF-diagnoser for the pLTS on the left of Figure 3.8.

**Proposition 3.4.** There exists a 1/2FF-diagnosable pLTS that admits no finite-memory 1/2FF-diagnoser.
*Proof.* Consider the 1/2FF-diagnosable pLTS on the left of Figure 3.8 and assume there exists a 1/2FF-diagnoser with $m$ states. After any sequence $a^n$ for $n \ge 1$, it cannot claim a fault as $\text{CorP}(a^n) = \frac{3^n}{3^{n+1}} > \frac{1}{2}$. So there exist $1 \le i < j \le m+1$ such that the diagnoser is in the same memory state after observing $a^i$ and $a^j$.

Consider the faulty run $\rho = q_0 \mathbf{f} q_f (aq_f)^i$. Due to the reactivity requirement, there must be a run $\rho\rho'$ for which the diagnoser claims a fault. Thus for all $n$, the diagnoser also claims a fault after $\rho_n = q_0 \mathbf{f} q_f (aq_f)^{i+n(j-i)} \rho'$ but $\lim_{n \to \infty} \text{CorP}(\mathcal{P}(\rho_n)) = 1$, which contradicts the correctness requirement. $\square$

We now establish the link between $\varepsilon$FF-diagnoser and $\varepsilon$FF-diagnosability.

**Proposition 3.5.** Let $\varepsilon \ge 0$. A pLTS $\mathcal{A}$ is $\varepsilon$FF-diagnosable if and only if it admits an $\varepsilon$FF-diagnoser.

This proof has more computations than the previous ones due to the approximate notion of correctness, however the main ideas are similar: from an $\varepsilon$FF-diagnoser we relate $\text{FAmb}_n^\varepsilon$ to $\{\rho' \in \mathbb{F}_n \mid D(\mathcal{P}(\rho')) =?\}$ in order to show that the probability of $\text{FAmb}_n^\varepsilon$ converges to 0. In the other direction, assuming $\mathcal{A}$ is $\varepsilon$FF-diagnosable, we build an $\varepsilon$FF-diagnoser that is reactive for the runs that do not belong to $\text{FAmb}_n^\varepsilon$ infinitely often.

*Proof.* Let $\mathcal{A}$ be a pLTS and $\varepsilon \ge 0$. Assume that there exists an $\varepsilon$FF-diagnoser $D$ for $\mathcal{A}$. Let $\rho$ be a minimal faulty run and $\alpha > 0$. Since $D$ is reactive, there exists $n_{\rho,\alpha} \in \mathbb{N}$ such that for all $n \ge n_{\rho,\alpha}$,

$$ \mathbb{P}(\{\rho' \in \mathbb{F} \cap \text{SR}_n \mid D(\mathcal{P}(\rho')) =?\}) \le \alpha \cdot \mathbb{P}(\rho). $$

Thus for all $n \ge n_{\rho,\alpha}$:

$$ \begin{aligned} \mathbb{P}(\{\rho' \in \text{SR}_{n+|\rho|_o} \mid D(\mathcal{P}(\rho')) =? \wedge \rho \le \rho'\}) &\le \mathbb{P}(\{\rho' \in \mathbb{F} \cap \text{SR}_{n+|\rho|_o} \mid D(\mathcal{P}(\rho')) =?\}) \\ &\le \alpha \cdot \mathbb{P}(\rho). \end{aligned} $$

Since $D$ is correct, $\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^\varepsilon \subseteq \text{Cyl}(\{\rho' \in \text{SR}_{n+|\rho|_o} \mid D(\mathcal{P}(\rho')) =? \wedge \rho \le \rho'\})$. Thus $\mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^\varepsilon) \le \alpha \cdot \mathbb{P}(\rho)$. This establishes that $\mathcal{A}$ is $\varepsilon$FF-diagnosable.

Conversely assume that $\mathcal{A}$ is $\varepsilon$FF-diagnosable. Let $D$ be the diagnoser defined by: for all $w \in \Sigma_o^*$, $D(w) = \top$ iff $\text{CorP}(w) \le \varepsilon$. Such an $\varepsilon$FF-diagnoser is correct by definition. Let $\alpha > 0$. Since $(\mathbb{F}_n)_{n \in \mathbb{N}}$ is a non-decreasing sequence converging to $\mathbb{F}_\infty$, there exists $n_0 \in \mathbb{N}$ such that for all $n \ge n_0$, $\mathbb{P}(\mathbb{F}_n \setminus \mathbb{F}_{n_0}) < \alpha/2$. By $\varepsilon$FF-diagnosability of $\mathcal{A}$, for all $\rho \in \bigcup_{k \le n_0} \min \mathbb{F}_k$, there exists $n_\rho$ such that for all $n \ge n_\rho$

$$ \mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{n+|\rho|_o}^\varepsilon) \le \frac{\alpha}{2} \cdot \mathbb{P}(\rho). $$
Define $n_{max} = \max_{\rho \in \bigcup_{n \le n_0} \min F_n} n_{\rho}^2$. Then for $n \ge n_0 + n_{max}$ we have

$$ \begin{align*} \mathbb{P}(\mathrm{FAmb}_n^\epsilon) &\le \mathbb{P}(\mathrm{FAmb}_n^\epsilon \cap F_{n_0}) + \mathbb{P}(\mathrm{FAmb}_n^\epsilon \setminus F_{n_0}) \\ &\le \sum_{\rho \in \bigcup_{k \le n_0} \min F_k} \mathbb{P}(\mathrm{Cyl}(\rho) \cap \mathrm{FAmb}_n^\epsilon) + \mathbb{P}(F_n \setminus F_{n_0}) \\ &\le \sum_{\rho \in \bigcup_{k \le n_0} \min F_k} \frac{\alpha}{2} \cdot \mathbb{P}(\rho) + \frac{\alpha}{2} \le \alpha. \end{align*} $$

So we have established that $\lim_{n \to \infty} \mathbb{P}(\mathrm{FAmb}_n^\epsilon) = 0$.

By definition of $D$, $\mathrm{FAmb}_n^\epsilon = \{\rho \in F_n \mid D(\mathcal{P}(\rho)) = ?\}$. Thus $D$ is reactive. $\square$

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

For every $\epsilon \ge 0$ we have thus an appropriate notion of $\epsilon$FF-diagnoser associated with $\epsilon$FF-diagnosability. As a pLTS is AFF-diagnosable if it is $\epsilon$FF-diagnosable for every $\epsilon > 0$, we directly obtain the following corollary.

**Corollary 3.1.** A finite pLTS $\mathcal{A}$ is AFF-diagnosable if and only if for all $\epsilon > 0$ it admits an $\epsilon$FF-diagnoser.

In other words, when a pLTS is AFF-diagnosable, the designer can choose the accuracy they want for the diagnoser.

## 2 Relationships between diagnosability notions

In this section, we establish the links between the multiple notions of diagnosability defined in Section 1.5. We gave in Section 1 diagnosers associated with the various notions of diagnosability. Thus, intuitively requiring a stronger version of one feature (verdict, correctness or reactivity) defines a diagnoser that gives more information and thus which is less likely to exist. For example, the difference between FF-diagnosability and FA-diagnosability is that FA-diagnosability must identify faulty and correct runs, while FF-diagnosability only cares about faulty runs. Thus FA-diagnosability implies FF-diagnosability, which can be formally proven immediately since for all $n$, $\mathrm{FAmb}_n \subseteq \mathrm{FAmb}_n \uplus \mathrm{CAmb}_n$. The two notions being entirely distinct as FF-diagnosability does not imply FA-diagnosability as shown by the pLTS of Figure 3.10: there is a single ambiguous observed sequence for every $n \in \mathbb{N}$, $a^n$, this sequence can be observed with a probability $1/2$ of correct runs and by a probability $1/2^n$ of faulty runs, i.e. $\forall n \in \mathbb{N}, \mathbb{P}(\mathrm{CAmb}_n) = 1/2$ and $\mathbb{P}(\mathrm{FAmb}_n) = 1/2^n$ therefore it is FF-diagnosable without being FA-diagnosable. Similarly, as $\mathrm{FAmb}_\infty \subseteq \mathrm{FAmb}_\infty \uplus \mathrm{CAmb}_\infty$, IA-diagnosability implies IF-diagnosability. The converse is not true however as the pLTS of Figure 3.10³ is IF-diagnosable while it is not IA-diagnosable.

An interesting case is the link between IF-diagnosability and FF-diagnosability. Intuitively, as for IF-diagnosability we can observe the infinite run before giving a verdict

<footnote n="2">²Note that $\bigcup_{n \le n_0} \min F_n$ is finite due to $\mathcal{A}$ being finitely branching and convergent.</footnote>

<footnote n="3">³This pLTS was already displayed in Figure 3.2.</footnote>
<figure><img src="image_37.png" /><figcaption>Figure 3.10: An FF/IF-diagnosable pLTS which is not FA/IA-diagnosable.</figcaption></figure>

while FF-diagnosability only allows for a finite observation, FF-diagnosability implies IF-diagnosability. This is indeed true. Using the first direction of the Lemma 3.1 we know that $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_\infty \setminus \mathbf{FAmb}_n) = 0$. Thus if a pLTS is FF-diagnosable, $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_n) = 0$, therefore $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_\infty) \le \lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_\infty \setminus \mathbf{FAmb}_n) + \lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_n) = 0$. Hence the pLTS is IF-diagnosable. Moreover, the implication is strict. Observe the pLTS of Figure 3.11, it is IF-diagnosable (and even IA-diagnosable in fact) as every correct run ends with an infinity of $b$ which cannot be observed with a faulty run and the only faulty run only triggers the observation $a$, thus $\mathbf{FAmb}_\infty \uplus \mathbf{CAmb}_\infty = \emptyset$. However, it is not FF-diagnosable as for all $n \in \mathbb{N}$, $\mathbb{P}(\mathbf{FAmb}_n) = 1/2$. Indeed, for $n \in \mathbb{N}$, there exists a transition from $q_0$ to a state $q_{n1}$ labelled by an $a$ and with probability $1/2^{n+1}$, the one correct run $\rho$ of observable length $n$ starting by this transition has observation $\mathcal{P}(\rho) = a^n$, thus the only faulty run of observable length $n$, $q_0 \mathbf{f}(f_1 a)^n f_1$ is ambiguous. Moreover this faulty run has probability $1/2$. Although we have a strict implication, the pLTS used to prove the strictness has an infinite branching. This is in fact necessary: given a finitely-branching convergent pLTS, IF-diagnosability is equivalent to FF-diagnosability. Given a pLTS $\mathcal{A}$, the implication from IF-diagnosability to FF-diagnosability is shown using once again Lemma 3.1, which, assuming finite branching, says that $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_n \setminus \mathbf{FAmb}_\infty) = 0$. Thus if $\mathcal{A}$ is IF-diagnosable, $\lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_n) = \lim_{n \to \infty} \mathbb{P}(\mathbf{FAmb}_n \setminus \mathbf{FAmb}_\infty) + \mathbb{P}(\mathbf{FAmb}_\infty) = 0$. Thus $\mathcal{A}$ is FF-diagnosable.

<figure><img src="image_38.png" /><figcaption>Figure 3.11: An infinitely-branching pLTS that is IA-diagnosable but not FF-diagnosable.</figcaption></figure>

Although the relationship between IA-diagnosability and FA-diagnosability is the same as the one between IF-diagnosability and FF-diagnosability, the same link cannot be established. Indeed, even for finite pLTS, IA-diagnosability does not imply FA-diagnosability. Let us observe the pLTS of Figure 3.12. It is IA-diagnosable, indeed, every infinite correct run have observed sequence $a^\omega$ while the observed sequence of every infinite faulty run is of the form $a^n b^\omega$ for $n > 0$, thus $\mathbf{CAmb}_\infty \uplus \mathbf{FAmb}_\infty = \emptyset$.
Consider however the infinite correct run $\rho = q_0 u q_1 (a q_1)^\omega$. It has probability $\frac{1}{2}$, and all its finite signalling subruns are ambiguous since their observed sequence is $a^n$, for some $n \in \mathbb{N}$ which is the observed sequence of the faulty signalling run $q_0 u (q_2 a)^{n-1} q_2 \mathbf{f} f_1 a f_2$. Thus for all $n \ge 1$, $\mathbb{P}(\mathbf{C}\text{Amb}_n) \ge \frac{1}{2}$, so that this pLTS is not FA-diagnosable.

<figure><img src="image_39.png" /><figcaption>Figure 3.12: An IA-diagnosable pLTS which is not FA-diagnosable.</figcaption></figure>

The next theorem summarises the connections between the different diagnosability notions.

**Theorem 3.1.** The diagnosability notions for pLTS are related according to the diagram below, where arrows represent implications. All implications, except the one from IF-diagnosability to FF-diagnosability and the one from FF-diagnosability to uniform FF-diagnosability, hold for arbitrary infinite-state pLTS. The latter implications holds for finitely-branching pLTS and finite pLTS respectively. Implications that are not depicted do not hold, already in the case of finite-state pLTS.

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

Let us first describe this diagram. Omitting 0FF-diagnosability which is equivalent to FF-diagnosability, the first two columns correspond to exact diagnosis (thus diagnosis where the diagnoser cannot claim a fault if there is a probability that the fault did not occur) while the last two rows correspond to approximate diagnosis. The lower row contains the notions of diagnosis considering infinite runs, the middle row the ones considering finite runs and the upper rows the ones considering finite runs and requiring uniformity on the speed of reactivity of the diagnoser. From any notion of diagnosability, the notion above it, if there is one, has a more restrictive reactivity and the one on its left requires a better correctness or has a verdict extended to more elements.
FF-diagnosability plays a central role in the diagram as the notion of uniformity and approximate diagnosis was built from this notion. This notion was chosen as it is the traditional notion of diagnosis [TT05], moreover there is no clear intuition of what approximation and uniformity means for infinite runs.

*Proof.* We prove all implications that were not already stated in the beginning of this section. Most are pretty straightforward. For all $\varepsilon > 0$, the implications from AFF- to $\varepsilon$FF, uniform AFF- to uniform $\varepsilon$FF- and uniform $\varepsilon$FF- to $\varepsilon$FF- are direct by definitions. The implications from uniform AFF- to AFF-, uniform FF- to FF-, FF- to AFF- and uniform FF- to uniform AFF- comes partially from definitions and from application of other implications (mostly the equivalence between FF- and 0FF- proven below). The most complicated implications are (1) the equivalence between FF- and 0FF-diagnosis which is a careful inspection of sets of runs, taking account the possibly infinite branching, (2) the implication from FA- to IA-diagnosis which is inspired by Lemma 3.1 and (3) the implication from FF- to uniform FF-diagnosability for finite pLTS which requires the characterisation of FF-diagnosability for finite pLTS which will be established later and is thus postponed (See Proposition 4.3, page 95).

$$ FF \Leftrightarrow 0FF. $$

Let $\mathcal{A}$ be a 0FF-diagnosable pLTS and $\varepsilon > 0$. Since $(F_n)_{n \in \mathbb{N}}$ is a non-decreasing sequence converging to $F_\infty$, there exists $n_0 \in \mathbb{N}$ such that for all $n \ge n_0$, $\mathbb{P}(F_n \setminus F_{n_0}) < \frac{\varepsilon}{2}$. By 0FF-diagnosability of $\mathcal{A}$, for all $\rho \in \bigcup_{k \le n_0} \min F_k$, there exists $n_\rho$ such that for all $n \ge n_\rho$

$$ \mathbb{P}(\mathrm{Cyl}(\rho) \cap \mathrm{FAmb}_{n+|\rho|_o}) \le \frac{\varepsilon}{4} \cdot \mathbb{P}(\rho). $$

Notice that, because the pLTS may be infinitely branching, the set $\bigcup_{k \le n_0} \min F_k$ may be infinite. We therefore define $n_{max}$ such that $\mathbb{P}(\{\rho \in \bigcup_{k \le n_0} \min F_k \mid n_\rho > n_{max}\}) \le \frac{\varepsilon}{4}$. Thus, only a small portion of runs $\rho$ in $\bigcup_{k \le n_0} \min F_k$ have $n_\rho > n_{max}$. Then for $n \ge n_0 + n_{max}$ we have

$$ \begin{aligned} \mathbb{P}(\mathrm{FAmb}_n) &\le \mathbb{P}(\mathrm{FAmb}_n \setminus F_{n_0}) + \mathbb{P}(\mathrm{FAmb}_n \cap F_{n_0}) \\ &\le \mathbb{P}(\mathrm{FAmb}_n \setminus F_{n_0}) + \mathbb{P}(\{\rho \in \bigcup_{k \le n_0} \min F_k \mid n_\rho > n_{max}\}) \\ &\quad + \mathbb{P}(\{\rho' \in \mathrm{FAmb}_n \mid \exists \rho \in \bigcup_{k \le n_0} \min F_k, \rho \le \rho', n_\rho \le n_{max}\}) \\ &\le \frac{\varepsilon}{2} + \frac{\varepsilon}{4} + \frac{\varepsilon}{4} \mathbb{P}(\{\rho \in \bigcup_{k \le n_0} \min F_k \mid n_\rho \le n_{max}\}) \le \varepsilon. \end{aligned} $$

Let $\mathcal{A}$ be a FF-diagnosable pLTS. Consider $\rho \in \min F$ and $\alpha > 0$. There exists $n_0 \in \mathbb{N}$ such that for all $n \ge n_0$, $\mathbb{P}(\mathrm{FAmb}_n) \le \alpha \cdot \mathbb{P}(\rho)$. Thus for all $n \ge n_0$:

$$ \mathbb{P}(\mathrm{Cyl}(\rho) \cap \mathrm{FAmb}_{n+|\rho|_o}) \le \mathbb{P}(\mathrm{FAmb}_{n+|\rho|_o}) \le \alpha \cdot \mathbb{P}(\rho). $$
FA $\Rightarrow$ IA.

For all $n \in \mathbb{N}$, define $\mathcal{CAmb}_{n,\infty}$ the set of correct ambiguous runs that admit an observationally equivalent run which is faulty before its $n^{th}$ observable event. Observe that the sequence of sets $\{\mathcal{CAmb}_{n,\infty}\}_{n \in \mathbb{N}}$ is non-decreasing and that $\mathcal{CAmb}_{\infty} = \bigcup_{n \in \mathbb{N}} \mathcal{CAmb}_{n,\infty}$. Moreover, by definition, $\mathcal{CAmb}_{n,\infty} \subseteq \mathcal{CAmb}_n$. Assume that $\limsup_{n \to \infty} \mathbb{P}(\mathcal{FAmb}_n \uplus \mathcal{CAmb}_n) = 0$. By Lemma 3.1, $\mathbb{P}(\mathcal{FAmb}_{\infty}) = 0$. For all $\varepsilon > 0$, there exists $n_1 \in \mathbb{N}$ such that for all $n \ge n_1$, $\mathbb{P}(\mathcal{CAmb}_n) < \varepsilon$ and thus $\mathbb{P}(\mathcal{CAmb}_{n,\infty}) < \varepsilon$. On the other hand, there exists $n_2 \in \mathbb{N}$ such that for all $n \ge n_2$, $\mathbb{P}(\mathcal{CAmb}_{\infty}) - \mathbb{P}(\mathcal{CAmb}_{n,\infty}) < \varepsilon$. Combining these two inequalities for $n = \max(n_1, n_2)$, one obtains $\mathbb{P}(\mathcal{CAmb}_{\infty}) < 2\varepsilon$. As $\varepsilon$ is arbitrary, $\mathbb{P}(\mathcal{CAmb}_{\infty}) = 0$.

We now provide counter-examples for the implications that do not hold and which were not already developed at the beginning of the section. The most interesting example is the one establishing the difference between FA-diagnosis to uniform $\varepsilon$FF-diagnosis as it requires an infinite pLTS.

uniform AFF $\Leftrightarrow$ IF.

Consider the pLTS depicted on the left of Figure 3.8. All infinite faulty runs are ambiguous, and the probability of faulty runs is $\frac{1}{2}$, thus this pLTS is not IF-diagnosable. Fix some $\varepsilon > 0$ and $0 < \alpha < 1$. There are two minimal faulty runs $\rho_a = q_0 \mathbf{f} q_f a q_f$ and $\rho_b = q_0 \mathbf{f} q_f b q_f$. Consider first $\rho_a$ and let $\rho$ be the random variable of a signalling run of length $n$ that extends $\rho_a$. One can express the correctness proportion of $\rho$ in terms of the number of $a$'s in its observed sequence, written $|\rho|_a$:

$$ \mathrm{CorP}(\rho) = \frac{\left(\frac{3}{4}\right)^{|\rho|_a} \left(\frac{1}{4}\right)^{|\rho|-|\rho|_a}}{\left(\frac{3}{4}\right)^{|\rho|_a} \left(\frac{1}{4}\right)^{|\rho|-|\rho|_a} + \left(\frac{1}{4}\right)^{|\rho|_a} \left(\frac{3}{4}\right)^{|\rho|-|\rho|_a}} $$

Simplifying this expression, we obtain: $\mathrm{CorP}(\rho) = \frac{1}{1+3^{|\rho|-2|\rho|_a}}$. Now, by the strong law of large numbers, for any $\eta > 0$, there exists $n_\eta$ such that for every $n \ge n_\eta$, $\mathbb{P}(|4|\rho|_a - |\rho|| > \eta) < \alpha$. So with probability at least $1 - \alpha$, the correctness proportion of $\rho$ is bounded by $\frac{1}{1+3^{\frac{\eta+|\rho|}{2}}}$. For a sufficiently large $\eta$, this value is smaller than $\varepsilon$, so that $\mathbb{P}(\mathrm{CorP}(\rho) \le \varepsilon) \ge 1 - \alpha$.

A similar reasoning applies to $\rho_b$, and one can then take the maximum of the two integers $n_\eta$ to prove that the pLTS is uniformly AFF-diagnosable.

<figure><img src="image_41.png" /><figcaption>Figure 3.13: An AFF-diagnosable pLTS which is not uniformly $\varepsilon$FF-diagnosable for $\varepsilon < 3/4$.</figcaption></figure>
### AFF $\rightleftharpoons$ uniform $\varepsilon$FF.

Consider the pLTS of Figure 3.13. Fix some $0 < \varepsilon < \frac{3}{4}$, $0 < \alpha < 1$ and $n_\alpha$. Consider the minimal faulty run $\rho = q_0 u q_1 (aq_1)^{n_\alpha+1} f q_f b q_f$. Let $\rho'$ be the signalling run of length $2n_\alpha + 2$ such that $\rho \preceq \rho'$. $\mathcal{P}(\rho') = a^{n_\alpha+1} b^{n_\alpha+1}$. Thus, $\text{CorP}(\mathcal{P}(\rho')) \ge \frac{3}{4}$. So

$$ \mathbb{P}(\text{Cyl}(\rho) \cap \text{FAmb}_{2n_\alpha+2}^{\varepsilon}) = \mathbb{P}(\rho) > \alpha \cdot \mathbb{P}(\rho). $$

Thus the pLTS is not uniformly $\varepsilon$FF-diagnosable.

Let $\rho$ be a minimal faulty run. Then $\mathcal{P}(\rho) = a^{n_0} b$ for some $n_0$. For all $n$, let $\rho_n$ be the single the single signalling run of observable length $|\rho| + n$ that extends $\rho$. It fulfils $\mathcal{P}(\rho_n) = a^{n_0} b^{n+1}$ and $\mathbb{P}(\rho_n) = \mathbb{P}(\rho)$. The single correct signalling run $\rho'_n$ with $\mathcal{P}(\rho'_n) = \mathcal{P}(\rho_n)$ fulfils $\mathbb{P}(\rho'_n) = \frac{3^{n_0}}{2 \cdot 4^{n_0+n+1}}$. Thus $\lim_{n \to \infty} \text{CorP}(\mathcal{P}(\rho_n)) = 0$. So the pLTS is $\varepsilon$FF-diagnosable for all $\varepsilon > 0$ and thus AFF-diagnosable.

### FA $\rightleftharpoons$ uniform $\varepsilon$FF when considering infinite pLTS.

Let us consider the pLTS of Figure 3.14. It is FA-diagnosable as almost surely a faulty (resp. correct) run contains a $b$ (resp. $c$) after a finite number of steps that cannot be mimicked by a correct (resp. faulty) run. We claim that it is not uniformly $\varepsilon$FF-diagnosable for all $\varepsilon$ such that $0 < \varepsilon < \frac{1}{2}$. Note that for all $n \in \mathbb{N}$, $\text{CorP}(a^n) \ge \frac{1}{2}$. Fix some $0 < \alpha < 1$ and $n_\alpha \in \mathbb{N}$. Consider the minimal faulty run $\rho = q_0 u f_1 a f_2 \dots a f_{n_\alpha} f f'_{n_\alpha}$. The shortest extension of $\rho$ that is not ambiguous (i.e. contains a $b$) contains $n_\alpha + 1$ observable events more than $\rho$ does. Therefore, $\mathbb{P}(\{\rho' \in \text{FAmb}_{n_\alpha+|\rho|_o}^{\varepsilon} | \rho \preceq \rho'\}) = \mathbb{P}(\rho) > \alpha \cdot \mathbb{P}(\rho)$.

<figure><img src="image_42.png" /><figcaption>Figure 3.14: An infinite FA-diagnosable pLTS that is not uniformly $\varepsilon$FF-diagnosable.</figcaption></figure>

### uniform $\varepsilon$FF $\rightleftharpoons$ AFF.

Consider the pLTS of Figure 3.15. There is a single signalling minimal faulty run $q_0 f q_f a q_f$. Any observed sequence of length at least 1 is ambiguous and corresponds with equal probability to a signalling correct or a faulty run. Consequently it is not AFF-diagnosable, yet it is uniformly $\varepsilon$FF-diagnosable for $\varepsilon = \frac{1}{2}$.

This concludes the proof.

□