💻 computer science

Visualising CTL Witnesses and Counterexamples -- Extended Version

Cet article propose un modèle formel d'évidence pour les propriétés CTL sur des modèles à états explicites, permettant de visualiser et de comprendre à la fois les contre-exemples et les témoins de satisfaction, tout en fournissant les preuves des résultats annoncés dans la version courte de SPIN 2026.

Auteurs originaux : Arend Rensink

Publié 2026-04-23

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Arend Rensink

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un détective chargé d'enquêter sur le comportement d'un système complexe, comme un jeu vidéo, un logiciel de banque ou un système de freinage d'avion. Ce système peut évoluer de nombreuses façons différentes, comme un arbre qui se divise en de nombreuses branches.

L'objectif est de vérifier si une règle précise est respectée. Par exemple : « Est-il possible de gagner le jeu sans jamais lancer un dé ? » ou « Est-il certain que le système ne tombera jamais en panne ? ».

Dans le monde de l'informatique théorique, il existe deux façons de poser ces questions :

LTL (Logique Linéaire) : On regarde une seule trajectoire, comme un film. Si le film montre une erreur, on a une preuve simple : la bande vidéo de l'erreur. C'est facile à comprendre.
CTL (Logique Arborescente) : On regarde tout l'arbre des possibilités. C'est beaucoup plus puissant, mais si quelque chose ne va pas, trouver la preuve est plus difficile. On ne peut pas juste montrer un film, il faut montrer pourquoi toutes les branches possibles mènent à l'erreur ou à la réussite.

C'est là que ce papier d'Arend Rensink intervient. Il propose une méthode pour créer et visualiser ces preuves (qu'on appelle des « témoins » pour les succès et des « contre-exemples » pour les échecs) de manière que n'importe quel humain puisse les comprendre.

Voici les idées clés expliquées simplement :

1. La Preuve : Le « Dossier de l'Enquête »

L'auteur définit ce qu'est une preuve (ou « evidence »).

Si le système respecte la règle, la preuve est un témoin : un petit morceau du système qui suffit à prouver que tout va bien.
Si le système viole la règle, la preuve est un contre-exemple : un morceau du système qui montre exactement comment l'erreur se produit.

L'analogie du détective :
Imaginez que vous cherchez à prouver qu'un suspect est innocent. Vous n'avez pas besoin de montrer toute la vie du suspect, juste le moment précis où il était ailleurs (le témoin). À l'inverse, pour prouver sa culpabilité, vous n'avez pas besoin de tout filmer, juste de montrer l'arme du crime et le moment précis (le contre-exemple).

2. Le Secret des « États Fermés » (Closed States)

C'est la grande innovation du papier. Pour prouver qu'une chose est fausse dans un système qui a des branches, il faut prouver qu'il n'y a aucune issue possible.

L'auteur introduit le concept d'états fermés.

État ouvert : C'est comme une porte entrouverte. On ne sait pas encore si le système peut continuer ou non.
État fermé : C'est comme une porte verrouillée et scellée. Cela signifie : « Ici, il n'y a aucune autre issue possible. C'est la fin de la route. »

Pourquoi c'est génial ?
Sans cette notion, pour prouver qu'un système ne peut pas atteindre un état dangereux, il faudrait montrer toutes les branches infinies qui ne mènent pas là-bas. C'est impossible à visualiser.
Avec les « états fermés », on peut dire : « Regardez, à ce point précis, toutes les portes sont fermées. Il est impossible de sortir. » Cela permet de condenser une information énorme en un petit dessin simple.

3. La Visualisation : Rendre le complexe lisible

Le papier ne se contente pas de la théorie ; il propose de dessiner ces preuves.

L'Arbre Syntaxique (AST) : Dans chaque état du système, on affiche l'arbre de la règle que l'on teste.
Les Couleurs :
- 🟢 Vert : La règle est vraie ici.
- 🔴 Rouge : La règle est fausse ici.
- ⚪ Gris : On n'en a pas besoin pour cette preuve (information superflue).
Les États Fermés : Ils sont marqués d'une manière spéciale (comme des hachures ou des pointsillés) pour indiquer qu'aucune autre issue n'est possible.

L'analogie de la carte au trésor :
Imaginez une carte de labyrinthe.

Si vous cherchez le trésor (témoignage), on vous montre un seul chemin clair et court qui mène au but.
Si vous cherchez à prouver qu'il n'y a pas de trésor (contre-exemple), on vous montre un chemin où toutes les portes sont murées (états fermés), prouvant qu'on ne peut pas avancer.

4. L'Idée de « Preuve Naturelle »

Parfois, la preuve mathématiquement la plus petite est trop abstraite pour un humain. Par exemple, pour prouver qu'on peut atteindre un but, la preuve minimale pourrait omettre de dire comment on y arrive, ce qui est déroutant.
L'auteur propose donc la preuve naturelle : on ajoute un peu plus d'informations (comme les étapes intermédiaires) pour que l'humain comprenne l'histoire de la preuve, pas juste la logique froide. C'est comme passer d'un résumé télégraphique à une histoire bien racontée.

5. Le Résultat Final : Une Vue d'Ensemble

Au lieu de devoir cliquer sur chaque état pour voir sa petite preuve individuelle (ce qui serait fastidieux), l'auteur montre qu'on peut fusionner toutes ces preuves en un seul modèle global.
C'est comme si, au lieu de recevoir 100 petits rapports séparés, le détective vous donnait un seul tableau blanc géant où toutes les pièces du puzzle sont assemblées, avec les zones importantes mises en évidence.

En résumé

Ce papier dit : « Vérifier un système complexe est dur. Trouver la preuve qu'il fonctionne (ou qu'il échoue) est encore plus dur. Mais si on utilise des portes verrouillées (états fermés) pour bloquer les possibilités inutiles, et si on dessine ces preuves avec des couleurs et des histoires claires, alors n'importe qui peut comprendre pourquoi un système est sûr ou dangereux. »

C'est un pont entre la logique mathématique rigoureuse et la compréhension humaine intuitive.

1. Problématique

L'article aborde un défi majeur dans la vérification de modèles (model checking) : la compréhension humaine des résultats de vérification pour la logique temporelle CTL (Computation Tree Logic).

Le contraste LTL vs CTL : En logique linéaire (LTL), la notion de contre-exemple est intuitive : il s'agit d'une trajectoire (trace) unique qui viole la propriété. En revanche, en CTL (logique temporelle arborescente), la structure de branchement du modèle est fondamentale. L'absence de satisfaction d'une propriété CTL ne peut pas toujours être expliquée par une simple trajectoire linéaire, car elle dépend de la structure globale des branches possibles.
La lacune actuelle : Il n'existe pas de notion simple et unifiée de "contre-exemple" en CTL qui soit aussi facile à visualiser et à traiter que pour le LTL. De plus, en CTL, la violation d'une propriété $\phi$ est équivalente à la satisfaction de sa négation $\neg\phi$ . Il est donc plus pertinent de parler d'"evidence" (preuve/indice) qui sert soit de témoin (witness) si la propriété est satisfaite, soit de contre-exemple si elle est violée.
L'objectif : Définir la notion la plus simple d'"evidence" pour capturer précisément la raison de la satisfaction ou de la violation d'une formule CTL arbitraire, et proposer une méthode efficace pour la visualiser afin d'améliorer la compréhension humaine.

2. Méthodologie

L'auteur propose une approche formelle basée sur des modèles explicites et des graphes dirigés, introduisant des concepts novateurs pour gérer la structure de branchement.

Modélisation formelle :
- Utilisation de modèles $M = \langle S, C, R, L \rangle$ où $S$ est l'ensemble des états, $R$ les transitions, $L$ l'étiquetage (partiel), et $C \subseteq S$ un ensemble d'états "fermés" (closed states).
- États fermés : C'est la contribution technique clé. Un état fermé dans un sous-modèle signifie qu'il ne possède aucune transition sortante dans ce sous-modèle, et que toutes les transitions sortantes de l'état original sont absentes. Cela permet de capturer formellement l'absence de branches futures, ce qui est crucial pour les contre-exemples en CTL.
- Preuve (Proof) : Une preuve est définie comme un modèle muni d'une fonction qui associe à chaque assertion (état, formule, valeur booléenne) un sous-modèle qui sert d'evidence (témoignage ou contre-exemple) pour cette assertion.
Caractérisation de l'Evidence :
- L'article définit des conditions syntaxiques ($wts$ pour témoin, $ctr$ pour contre-exemple) basées sur les opérateurs temporels (EX, EU, EG, etc.).
- Il distingue les formules contraintes (où l'absence d'étiquetage rend le modèle incohérent) des formules non contraintes.
- Il établit que pour les formules non contraintes, les conditions $wts$ et $ctr$ sont nécessaires et suffisantes pour l'existence d'une preuve.
Minimisation et Naturalité :
- Evidence minimale : Recherche des modèles les plus petits (au sens de l'inclusion de sous-modèles $\sqsubseteq$ ) qui suffisent à prouver l'assertion. Cela implique souvent de supprimer des états inutiles et de fermer certains états pour bloquer les branches indésirables.
- Evidence naturelle : Pour améliorer la lisibilité, l'auteur introduit l'idée d'une "evidence naturelle". Bien qu'une preuve minimale formelle puisse omettre l'étiquetage de certains sous-formules intermédiaires (car techniquement superflu), l'ajout de ces informations rend la visualisation plus intuitive pour l'humain.
Visualisation :
- Utilisation d'un arbre de syntaxe abstraite (AST) affiché dans chaque état.
- Codage couleur : Vert (satisfait/1), Rouge (violé/0), Gris (non défini).
- États ouverts vs fermés : Représentés visuellement (par exemple, points pleins vs hachurés) pour indiquer si des transitions sortantes sont absentes.
- Evidence combinée : Au lieu de montrer des milliers de snapshots individuels, l'article propose de combiner les preuves pour une formule donnée sur tous les états en un seul modèle, réduisant ainsi la complexité visuelle.

3. Contributions Clés

Définition formelle de l'Evidence CTL : Un cadre unifié traitant les témoins et les contre-exemples comme des "evidence", avec une distinction rigoureuse basée sur les états fermés.
Caractérisation de l'Evidence Minimale : Des conditions précises (Tableau 2 de l'article) décrivant la structure minimale requise pour chaque opérateur temporel (EX, EU, EG) pour prouver une propriété.
- Exemple : Pour un contre-exemple de $EX \psi$ , l'état doit être fermé et tous ses successeurs doivent violer $\psi$ .
Concept d'États Fermés : L'introduction des états fermés permet de généraliser les preuves de contre-exemple au CTL complet, en encapsulant l'information négative (absence de transitions) de manière concise.
Evidence Naturelle et Combinée :
- Proposition d'une "evidence naturelle" qui, tout en restant minimale, inclut les étiquetages locaux pour une meilleure compréhension.
- Preuve de l'existence d'une evidence combinée unique pour une formule donnée sur l'ensemble des états d'un modèle, permettant une visualisation statique globale plutôt qu'une navigation interactive fastidieuse.
Implémentation et Outil : Développement d'un démonstrateur logiciel (disponible en tant qu'artefact) qui génère et visualise ces preuves, illustré par des exemples de jeux et de modèles Kripke.

4. Résultats

Théorèmes de Minimalité : L'article démontre que les conditions définies dans les tableaux (Table 1 et Table 2) caractérisent exactement les modèles minimaux (témoins et contre-exemples) pour les formules CTL.
Comparaison avec la Simulation : L'auteur montre que la notion classique de simulation (utilisée dans d'autres travaux) échoue ici car elle ne gère pas correctement les états fermés. Un modèle qui simule un contre-exemple pourrait en réalité satisfaire la propriété si les états "fermés" du contre-exemple sont ouverts dans le modèle simulateur.
Efficacité de la Visualisation : Les expériences montrent que l'approche combinée (une seule vue par opérateur temporel) et l'ajout d'informations locales (evidence naturelle) rendent les résultats de model checking beaucoup plus compréhensibles pour les humains que les listes de traces ou les graphes de preuve complexes.

5. Signification et Impact

Bridging the Gap : Ce travail comble le fossé entre la puissance expressive du CTL et la nécessité de résultats interprétables par l'humain. Il transforme un résultat booléen (Vrai/Faux) en une explication structurelle visuelle.
Nouveauté Conceptuelle : L'utilisation d'états fermés pour représenter l'absence de branches est une innovation importante qui permet de traiter le CTL complet de manière analogue aux logiques linéaires pour la génération de contre-exemples.
Applications Pratiques : La méthodologie est directement applicable aux outils de débogage de systèmes critiques (systèmes embarqués, protocoles de sécurité) où comprendre pourquoi une propriété échoue est aussi important que de savoir qu'elle échoue.
Perspectives Futures : L'article ouvre la voie à l'application de ces concepts à des logiques plus expressives (comme le $\mu$ -calcul ou CTL*) et à l'exploration de relations de simulation adaptées aux états fermés.

En résumé, Rensink propose une théorie rigoureuse et un outil pratique pour rendre la vérification de modèles CTL transparente et intuitive, en remplaçant la simple recherche de traces par la construction de preuves structurées minimales et visuellement riches.