.

Méthodes Formelles
pour la Conception des Logiciels

Francesco Belardinelli

Laboratoire IBISC
Remerciements à Alessio Lomuscio et Joost-Pieter Katoen

16 novembre 2012
Pourquoi adopter des méthodes formelles ?

• Pourquoi dépenser du temps et de l’argent à l’avance ?

Pourquoi adopter des méthodes formelles ?

• Pourquoi dépenser du temps et de l’argent à l’avance ?

• Pourquoi fréquenter un cours en méthodes formelles ?
Pourquoi adopter des méthodes formelles ?

• Pourquoi dépenser du temps et de l’argent à l’avance ?

• Pourquoi fréquenter un cours en méthodes formelles ?
• Est-ce qu’on peut réparer un système quand/si il ne fonctionne pas ?
Pourquoi adopter des méthodes formelles ?

• Pourquoi dépenser du temps et de l’argent à l’avance ?

• Pourquoi fréquenter un cours en méthodes formelles ?
• Est-ce qu’on peut réparer un système quand/si il ne fonctionne pas ?

• Les fautes peuvent être coûteuses en termes de dégats causés et en termes

de profits/fonctionnalités manquants.
Pourquoi adopter des méthodes formelles ?

• Pourquoi dépenser du temps et de l’argent à l’avance ?

• Pourquoi fréquenter un cours en méthodes formelles ?
• Est-ce qu’on peut réparer un système quand/si il ne fonctionne pas ?

• Les fautes peuvent être coûteuses en termes de dégats causés et en termes

de profits/fonctionnalités manquants.
• La sécurité d’applications critiques nécessite vérification et validation.
Pourquoi adopter des méthodes formelles ?

• Pourquoi dépenser du temps et de l’argent à l’avance ?

• Pourquoi fréquenter un cours en méthodes formelles ?
• Est-ce qu’on peut réparer un système quand/si il ne fonctionne pas ?

• Les fautes peuvent être coûteuses en termes de dégats causés et en termes

de profits/fonctionnalités manquants.
• La sécurité d’applications critiques nécessite vérification et validation.
• Aujourd’hui, aucun système important n’est déployé sans une vérification et
une validation systématiques.
Échecs célèbres de Logiciels

1984 LSE Taurus (Transfer and Automated Registration of Uncertificated Stock).

Taurus a coûté £75m.
Il a fait £500m de dégats.
Finalment, il a été remplacé par CREST.
1985-87 Surdosage de radiations du Therac-25
Appareil de radiothérapie pour le traitement de malades de cancer
Au moins 6 cas de surdosage (≈ 100×dose)
Trois patients sont décédés
Source : erreur de conception dans le logiciel de contrôle (race condition)
1990 Panne du réseau téléphonique AT & T
Un problème à New York mène à 9h de coupure de courant dans la plupart
du réseau téléphonique des EUs
Coûts : plusieurs 100m de US$
Source : mauvaise interprétation d’une instruction break en C
1992 LASCAD (London Ambulance Service Computer-Aided Dispatch).
Attentes de 11h.
Jusqu’à 30 personnes auraient pu mourir.
Échecs célèbres de Logiciels

1993 Aéroport de Denver. Système de livraison des colis.

Les $186m de coût du système ont augmenté de $1m/j pendant les mois de
modifications et réparations.
1994 FDIV bug du Pentium (Floating point DIVision unit).
Certains division produisent des résultats incorrects (1 cas sur 9mrd)
4.195.835,0 * 3.145.727,0 / 3.145.727,0 = 4.195.579,0 ? ? ?
Unités retirées du marché. Perte ≈500m US$
Intel a commencé à investir en méthodes formelles.
1996 Lancement du Satellite Ariane 5 (vol 501)

Fig. : Ariane 5G V88/501, 4 Juin 1996 12 :34 :06 UTC

1996 Lancement du Satellite Ariane 5 (vol 501)

Fig. : Ariane 5G V88/501, 4 Juin 1996 12 :34 :43 UTC

Ariane 5

• Réutilisation de code, mais le module 5 était plus rapide au décollage que le

module 4.
• Panne du système de pilotage inertiel primaire et de secours.
• Cet erreur a engendré la conversion d’un nombre à 64-bit en un entier à
16-bit (des considérations d’efficacité avaient conduit à la désactivation de
ce contrôle !).
• Buses dirigées par des données fausses.
• Trajectoire du vol incorrecte.
• Autodestruction : module et charge perdus ! Coûts : plus de 500m US$.
Importance de l’Exactitude des Logiciels

L’intégration des TIC dans les différentes applications augmente rapidement :

• systèmes intégrés
• protocoles de communication et securité
• systèmes de transport
⇒ de manière croissante leur fiabilité dépend du logiciel !
Les défauts peuvent être mortels et extrêmement coûteux :
• produits objets de production de masse
• systèmes de securité critiques
Vérification Automatique

Dans ce cours on va découvrir des techniques pour la vérification automatique.

• Validation : Le processus d’évaluation du logiciel au cours ou à la fin du
processus de développement afin de déterminer s’il satisfait les exigences
spécifiées. [IEEE-STD-610]
C’est à dire, “construisons-nous le système correct” ?
• Vérification : le processus d’évaluation du logiciel pour déterminer si les
produits d’une phase de développement donnée satisfont les conditions
imposées au début de cette phase. [IEEE-STD-610].
C’est à dire, “construisons-nous le système correctement” ?
Techniques de Vérification du Logiciel

Peer reviewing :
• technique statique : inspection manuelle du code, pas d’exécution du
logiciel.
• détecte entre 31% et 93% de défauts avec une médiane de 60% environ.
• les erreurs subtiles (défauts de concurrence et dans l’algorithme) sont
difficiles à découvrir.
Testing :
• technique dynamique dans lequel le logiciel est exécuté.
• de 30% à 50% du coût des projets des logiciels est dédié au testing.
• plus de temps et d’efforts sont consacrés à la validation que au codage.
• densité de défauts acceptée : environ 1 défaut pour 1.000 lignes de code.
Méthodes Formelles

Description intuitive :
• les méthodes formelles sont les ”mathématiques appliquées à la
modélisation et l’analyse des systèmes TIC”.
Les méthodes formelles ont un grand potentiel pour :
• obtenir une intégration précoce de la vérification dans le processus de
conception du logiciel.
• fournir des techniques de vérification plus efficaces (couverture plus élevée)
• réduir le temps de vérification
Utilisation des méthodes formelles.
• Fortement recommandé par CEI, FAA et NASA pour les logiciels critiques.
• Exemple : ligne 14 du métro de Paris (Méthode B).
Techniques de Vérification Formelle pour la Propriété P

Méthodes déductives
• méthode : fournir une preuve formelle que P est vrai.
• outil : démonstrateur des théorèmes / assistant de preuve ou proof-checker
(Coq, Isabelle, Pandora)
• applicable si : le système se présente sous forme d’une théorie
mathématique (par exemple, tableaux)
Model-checking
• méthode : contrôle systématique de P dans tous les états
• outil : model checker (Spin, NuSMV, UppAal, . . . )
• applicable si : le système génère un modèle fini de comportements

Simulation ou testing basé sur modèles

• méthode : tester P en explorant les comportements possibles.
• applicable si : le système définit un modèle exécutable.
Simulation et Testing

Procédure de base :
• prendre un modèle (simulation) ou une réalisation (testing)
• introduir certains inputs (à savoir, des tests)
• observer la réaction et vérifier si cela est “désiré”
Inconvénients importants :
• le nombre de comportements possibles est très grand (voire infini)
• les comportements inexplorées peuvent contenir le bug fatal
À propos du testing . . .
• Le test / simulation peut montrer la présence d’erreurs, pas leur absence
Étapes de la Vérification Formelle

• Exactitude des programmes mathématiques (Turing, 1949)

• Technique basée sur la syntaxe pour les programmes séquentiels (Hoare,
1969)
I pour une donnée d’entrée, est-ce que un programme d’ordinateur génère la
sortie correcte ?
I fondée sur des règles de preuve compositionelles, exprimées dans la logique
des prédicats.
• Technique basée sur la syntaxe pour les programmes concurrents (Pnueli,
1977)
I elle manipule des propriétés concernant les états pendant la computation
I fondée sur des règles de preuve exprimées en logique temporelle
Vérification automatique de programmes concurrents
I approche basée sur les modèles au lieu des règles de preuve
I est-ce que le programme concurrent satisfait une propriété (logique) donnée ?
Plan du Cours

1. Spécification et Vérification.
2. Langages modaux : syntaxe, sémantique, exemples.
3. Vérification par model checking : théorie, pratique et limites.
Répartition du Cours

• Semaine 1
I Introduction au cours.
I Spécification par langages modaux - concepts de base, syntaxe, sémantique.
I Logiques temporelles - LTL, CTL. Expressivité.
I Exercices.

• Semaine 2
I Automates de Büchi finis et infinis.
I Formules comme automates.
I Systèmes comme automates.
I Exercices.

• Semaine 3
I Le problème du model checking.
I Produits de automates.
I Systèmes de transitions.
I Le model checker SPIN.
Matériaux d’étude

• Diapositives téléchargeables à partir du site

http ://www.ibisc.univ-evry.fr/˜belardinelli/
• Huth, Ryan ; Logic in Computer Science, CUP 2005. Chapitre 3.
• Baier, Katoen ; Principles of Model Checking, MIT Press 2008.
• Clarke, Grumberg, Peled ; Model Checking, MIT Press 2000.
Plus de Motivations pour le Cours

• Problème : concevoir un pilote automatique qui prend des mesures

d’évitement en proximité d’autres avions.
Plus de Motivations pour le Cours

• Problème : concevoir un pilote automatique qui prend des mesures

d’évitement en proximité d’autres avions.
• Solution ( ?) :
IF trajectoire de collision AND distance(avion) > 10km
THEN alerte(pilote)
ELSE IF trajectoire de collision AND distance(avion) < 2km
THEN monter(200m)
Plus de Motivations pour le Cours

• Problème : concevoir un pilote automatique qui prend des mesures

d’évitement en proximité d’autres avions.
• Solution ( ?) :
IF trajectoire de collision AND distance(avion) > 10km
THEN alerte(pilote)
ELSE IF trajectoire de collision AND distance(avion) < 2km
THEN monter(200m)
• Nous avons donc évité une collision à une altitude de X metres.
Plus de Motivations pour le Cours

• Problème : concevoir un pilote automatique qui prend des mesures

d’évitement en proximité d’autres avions.
• Solution ( ?) :
IF trajectoire de collision AND distance(avion) > 10km
THEN alerte(pilote)
ELSE IF trajectoire de collision AND distance(avion) < 2km
THEN monter(200m)
• Nous avons donc évité une collision à une altitude de X metres.
• Par ailleurs, si tous les avions utilisent le même système, nous avons conçu
un accident à 200 + X metres !
Cela vous paraı̂t impossible ?

• Bug du pilote automatique du F16 lors du franchissement de l’équateur

(tentative de renverser l’avion !).
• Système de controle du traffic aerien transféré des USA en GB (toutes les
latitudes à l’Est de Greenwich ne sont pas traitées !).
• Le pilote automatique du F16 s’est planté à des altitudes négatives (comme
découvert par l’aviation israélienne lors d’un survol de la Mer Morte !).
• Le système principal du F22 américain en panne lors du franchissement de
la ligne de changement de date (comme découvert en rendant des avions au
Japon en 2006).
• Logiciel principal de la navette spatiale NASA : 16 erreurs de niveau-1,
réduites à 8, aucune jamais rencontrée jusqu’à présent (dimension totale
400K).
Le Model Checking en Bref

• Nous voulons vérifier si un système S satisfait une propriété P.

• On construit un modèle MS “approprié” pour S, représentant toutes les
computations possibles de S.
• On définit une formule appropriée φP qui capture la propriété P.
• On vérifie automatiquement si φP est satisfaite par MS : MS |= φP .
Banal ? !
Consultez :
http ://www.acm.org/press-room/news-releases-2008/turing-award-07

(a) Edmund Clarke (b) Allen Emerson (c) Joseph Sifakis

(CMU, USA) (U. Texas à Austin, (IMAG Grenoble, F)
USA)

Justification du jury
• ”Pour leurs rôles dans le développement du model-checking dans une
technologie de vérification très efficace, largement adoptée dans les
industries des matériels informatiques et des logiciels”.
Une affaire d’université ? !
Consultez :

Fig. : Intel i7 Core

• Vérification formelle utilisée comme véhicule de validation primaire pour le

groupe d’exécution de base (core execution cluster), la composante
responsable du comportement fonctionnel de l’ensemble des
micro-instructions.
• Testing abandonné completement.
Quels sont les modèles ?

Systèmes de transitions :
• états marqués avec des propositions simple.
• relation de transition entre les états.
• transitions marqués par des actions pour faciliter la composition.
Expressivité
• les programmes sont des systèmes de transitions
• les programmes multi-thread sont des systèmes de transitions
• les processus communicants sont des systèmes de transitions
• les circuits sont des systèmes de transitions
• Quoi d’autre ?
Quelles sont les propriétés ?

Exemples des propriétés

• le système peut atteindre une situation de blocage ?
• Deux processus peuvent se trouver simultanément dans une situation
critique ?
• En cas de terminaison, est-ce que le programme fournit la sortie correcte ?
Logique temporelle
• Extension de la logique des propositions.
• Opérateurs modaux tels que  “Toujours” et  “éventuellement”
• Interprétée sur des séquences d’états (linéaire) . . .
• . . . ou sur des arbres d’états infinis (branchement)
La Procédure du Model Checking

• Phase de modélisation
I modéliser le système à l’étude
I comme test de cohérence, on peut d’abord effectuer quelques simulations
I formaliser la propriété à vérifier

• Phase d’exécution
I exécuter le model checker pour vérifier la validité de la propriété dans le

modèle
• Phase d’analyse
I propriété satisfaite ? ⇒ vérifier la propriété suivante (le cas échéant)
I propriété violée ? ⇒

1. analyser le contrexemple générée par simulation

2. affiner le modèle, le design du modèle ou la propriété . . . et répéter l’ensemble de
la procédure
I pas assez de mémoire ? ⇒ essayer de réduire le modèle et tester à nouveau
Les Pros du Model Checking

• largement applicable (hardware, logiciels, systèmes de protocoles, ...)

• permet une vérification partielle (uniquement les propriétés les plus
importantes)
• potentielment technologie ”pousser-le-bouton” (software-tools)
• intérêt industriel en hausse rapide
• en cas de violation des propriétés, un contre-exemple est fourni
• fondements mathématiques exacts et intéressant
• pas biaisé sur les scénarios les plus probables (comme le testing)
Les Inconvénients du Model Checking

• accent sur les applications basées sur les instruction de contrôle (moins sur
les données)
• le model checking est aussi “bon” que le modèle du système
• très puissant, en principe, mais difficile à maı̂triser et coûteux à utiliser à
l’échelle industrielle (étant donné la formation nécessaire).
• pour ces raisons utilisé maintenant principalement pour les systèmes
critiques.
• difficile à appliquer à des espaces d’états larges.
• aucune garantie quant à l’exhaustivité des résultats
• impossible de vérifier des généralisations

Néanmoins :
• de plus en plus les systèmes informatiques sont essentiels à nos vies :
tendance croissante dans l’analyse et vérification des systèmes.
• le model-checking est une technique efficace pour révéler les erreurs
potentiels de conception.
Exemples Saissants de Model Checking

• Sécurité : protocole Needham-Schroeder de cryptage

I erreur qui n’a été découvert pendant 17 ans

• Systèmes de transport
I modèle de train contenant 10476 états

• Model checkers pour C, Java et C++

I utilisé (et développé) par Microsoft, Digital, NASA
I domaine d’application : drivers de périphériques

• Barrage néerlandais anti-tempête dans la Nieuwe Waterweg

• Logiciel de la génération actuelle / prochaine de véhicules spatiaux
I NASA Mars Pathfinder, Deep Space-1, JPL LARS groupe
Cours en bref

Les objectifs du cours sont les suivants :

1. Apprendre à utiliser les logiques temporelles et d’autres langages de
spécification.
2. Comprendre comment construire des modèles symboliquement et
automatiquement.
3. Apprécier la programmation des modèles au moyen d’une variété de
langages.
4. Apprendre à faire ces contrôles de la manière la plus efficace possible.
5. Identifier les situations où le model checking ne doit pas être utilisé.
Cours 2 : Langages Modaux

La logique modale nous offre :

• Une façon naturelle de traiter les concepts temporels, connaissance,
croyance, Nécessité, Possibilité, etc.
• Une sémantique claire et naturelle.
• Un patrimoine de techniques pour prouver des résultats méta-logiques sur
les systèmes modaux : décidabilité, complétude, complexité computationelle,
etc.
Ceux-ci sont importants, mais nous ne les discuterons pas.
Toutes ces caractéristiques font des langages modaux un des formalismes de
choix pour la modèlisation des systèmes informatiques.
La logique modale est particulièrement utilisée dans le domaine des systèmes
distribués et des systèmes multi-agents (systèmes où les entités sont de nature
autonome).
Cette partie du cours

Le domaine de la logique modale est considérable, et il ne serait pas raisonnable

de viser à donner plus qu’un aperçu des techniques de base et de leurs
applications.
Ce que nous allons faire est :
• Etudier les notions de base syntaxiques et sémantiques.
• Explorer leurs applications dans la spécification des systèmes, notamment en
termes de logique temporelle et épistémique.
• Etudier une série d’exemples concrets en logique modale qui peuvent être
utilisés pour la spécification des systèmes.
Ce que cette partie du cours n’est pas

Ce cours ne demande pas des connaissainces préalables autres que la logique

propositionnelle.
Alors, nous n’explorerons pas de questions telles que :
• Bisimulations, complétude, incomplétude, indécidabilité.
• Produits des logiques modales, unions, combinaisons de logiques.
• Logiques pour la croyance et le désir. Logique dynamique, etc.

Tous ces sujets sont importants et intéressants - si quelqu’un parmi vous est
intéressé à des lectures ulterieures et/ou à des projets, contactez-moi pour des
renseignements.
Textes pour en savoir plus sur cette partie

Outre que ces notes, si vous êtes intéressés au sujet, vous pouvez consulter :
• Goldblatt ; Logics of Time and Computation. CSLI Publications, 1992.
Concis et réconnu. Très bonne introduction à la logique temporelle.
• Fagin, Halpern, Moses, Vardi ; Reasoning about Knowledge, MIT Press
1995.
Une des références principales pour tous ceux qui font de la recherche sur la
logique épistémique. Recommandé.
• Hughes & Cresswell ; A New Introduction to Modal Logic. Routledge 1996.
De nature plutôt philosophique. Aucun élément d’Informatique.
• Meyer & van der Hoek ; Epistemic Logic in Computer Science, CUP 1995.
Etude approfondie de la logique épistémique et ses applications.
• Blackburn, de Rijke, Venema ; Modal Logic. CUP 2001.
Une très bonne introduction à ce sujet. De nature mathématique. Exigeant.
Si vous êtes intéressés à faire de la recherche dans ce domaine ou simplement à
en connaı̂tre davantage, Blackburne, de Rijke & Venema est recommandé pour
les mathématiques de la logique modale, Fagin et al. est la référence pour ses
aspects informatiques.
Logique Temporelle LTL : Syntaxe et Sémantique

Lorsqu’on fait référence aux langages formels, il est toujours utile de séparer
deux concepts : la syntaxe et la sémantique.
• Syntaxe : façon dont nous écrivons les formules.
Elle définit le langage logique que nous utilisons dans l’écriture des formules.
• Sémantique : interprétation des formules construites selon la syntaxe.
Logique modale de base : Syntaxe et Sémantique
Definition (Syntaxe)
Soit P un ensemble de variables propositionnelles p, q, . . ., l’ensemble L des
formules de la logique modale propositionnelle est défini inductivement par :
• tous p ∈ L
• true ∈ L
• Si φ ∈ L, alors ¬φ ∈ L
• Si φ, ψ ∈ L, alors φ ∧ ψ ∈ L
• Si φ ∈ L, alors φ ∈ L
• Si φ ∈ L, alors φ ∈ L
• Si φ, ψ ∈ L, alors φUψ ∈ L
• Rien d’autre est en L

Notez que P peut être aussi grand qu’infini dénombrable (mais nous ne sommes
pas concernés avec ces questions dans ce cours).
Nous écrivons φ, ψ, . . . pour des formules arbitraires dans L, et p, q, . . . pour
des propositions atomiques dans P.
true est le symbole pour la vérité logique, le connecteur unaire ¬ signifie la
négation logique, alors que le connecteur binaire ∧ représente la conjunction
logique.
Logique Temporelle LTL : Syntaxe et Sémantique

D’après la Définition 1, l’ensemble L des formules que nous utilisons est une
extension du calcul des propositions par l’opérateur , que nous appelons box,
l’opérateur (next), et l’opérateur U (until).
Exercice
Soit P = {p, q} un ensemble de variables propositionnelles, quelles parmi les
suivantes sont des formules modales ?
• pφ ∧ q
• p ∧ q
• ¬¬q
• ¬∧p
• ¬q ∧ ¬φ
Abréviations

Il est parfois pratique d’utiliser d’autres connecteurs qu’on peut définir à partir
de la Définition 1.
• false pour la formule ¬true
• φ ∨ ψ signifie ¬(¬φ ∧ ¬ψ)
• φ → ψ signifie ¬φ ∨ ψ, c’est à dire, ¬(φ ∧ ¬ψ)
• φ signifie ¬¬φ

Notez que nous utilisons les parenthèse ( et ) pour desambiguer les formules à
chaque fois qu’il est nécessaire.
La plupart de ces abréviations vient de la logique propositionnelle : ∨ est la
disjunction logique, alors que → représente l’implication logique. L’opérateur
modal  est le dual de  et il est lu comme “diamant”.
Modalités - lectures

Bien qu’on puisse développer toute la théorie modale sans référence à la

signification des modalités, ce n’est pas la façon dont elle a été développée.
Ici, on se concentre sur quelques-unes parmi les significations modales du box,
particulièrment temporelles, mais il en existe d’autres.

Signification de  Lecture de  Lecture de 

Temporelle toujours dans le futur φ parfois dans le futur φ
Aléthique il est nécessaire que φ il est possible que φ
Epistémique il est connu que φ il est cohérent
avec notre connaissance que φ
Doxastique il est cru que φ il est cohérent
avec notre croyance que φ
Déontique il est obligatoire que φ il est permis que φ
Provabilité φ est un theorème ¬φ n’est pas un theorème
Modalités - lectures

Autres exemples :
Epistémique φ on sait qu’on sait φ
Epistémique   φ on sait qu’il est possible que φ
Mais la plupart des propriétés que nous allons étudier concerne l’évolution
temporelle.
Considerez la lecture des formules suivantes d’une façon temporelle :
φ → φ si φ est vraie maintenant, alors elle sera toujours vraie
φ → φ si φ est toujours vraie, alors elle sera vraie parfois dans le futur
D’autres opérateurs temporels sont possibles. On les verra dans la suite.
Notez l’expressivité des combinaisons d’opérateurs avec des interprétations
différentes !
Par exemple, on lit T K φ comme “l’agent saura toujours que φ” si on donne
une lecture temporelle à la première modalité et une lecture épistémique à la
deuxième.
On va explorer certains de ces aspects vers la fin du cours.
Sémantique des Mondes Possibles

Compte tenu de la Définition 1, nous savons maintenant comment construire des

formules du langage logique.
Maintenant, on va discuter la notion de vérité.
Etant donnée une situation, ou un système, certaines formules seront vraies,
d’autres seront fausses.
Par exemple, “à l’instant suivant votre logiciel Vista va se planter” sera fausse
dans une situation dans laquelle à l’instant suivant votre logiciel Vista est encore
functionnant.
D’autres formules seront vraies ; il se peut que “votre logiciel XP va se bloquer
dans 10 minutes”.
Celles-ci seront appellées vérités contingentes.
D’autres formules apparaissent nécessairement vraies (ou forcément fausses). Par
exemple, on considère une interprétation temporelle des modalités et la formule
p → p, où on lit p comme “ton logiciel XP est functionnant”.
Alors, on lira la formule p → p comme “si toujours dans l’avenir votre logiciel
XP functionne, alors dans un certain moment dans l’avenir votre logiciel XP est
functionnant”, qui semble en accord avec notre intuition sur le flux du temps.
Donc, il faut être prudent avec les différentes notions de vérité. Notre approche
sera d’exprimer ces concepts de manière formelle. Nous faisons abstraction de
différentes lectures des modalités et présentons des définitions formelles.
Structures de Kripke

Une bonne sémantique doit être simple et intuitive, mais en même temps, elle
doit être capable d’accueillir toutes les différentes lectures des modalités.
Il n’existe pas une seule sémantique pour la logique modale, et même la question
a reçu beaucoup d’attention dans le passé.
Ici on présente la sémantique des mondes possibles telle qu’elle a été définie par
S. Kripke à la fin des années 50 (basée sur les idées de Tarski et Johnson, début
des années 50, mais aussi de Leibniz, XVIII siècle).
Definition (Structure)
Une structure de Kripke F est un couple F = (W , R) tel que
• W 6= ∅ est un ensemble de mondes possibles,
• R ⊆ W × W est une rélation définie sur W .

Nous indiquerons les éléments de W avec w , w 0 , . . . .

Ceux-ci sont aussi appelés états, ou points.
Structures de Kripke

Exercice
Définez les structures de Kripke de certains structures mathématique (et non)
que vous connaissez. Dessinez-les aussi !
Par exemple :
• (N, suc), l’ensemble des nombres naturels avec la rélation de successeur est
une structure de Kripke.
• ({w }, ∅) est une structure de Kripke.
• (Z, suc), l’ensemble des nombres entiers avec la rélation de successeur est
une structure de Kripke.
• (N, <), l’ensemble des nombres naturels avec la rélation de “mineur que”
est une structure de Kripke.
• Chaque arbre fini et infini est une structure de Kripke.
Modèles de Kripke

Le structures de Kripke sont des structures sans évaluation, c’est à dire, on ne

peut pas évaluer des formules.
Pour faire ça, on a besoin des modèles de Kripke.
Definition (Modèle)
Un modèle de Kripke M est un couple M = (F , π) tel que
• F est une structure de Kripke
• π : P → 2W est une évaluation des propositions atomiques1

Intuitivement, π(p) = {w1 , w2 } représente la situation où p est vraie dans w1 ,

w2 , et p est fausse dans W \ {w1 , w2 }.
Par abus de notation, on indiquera souvent un modèle M comme une triple
M = (W , R, π), où (W , R) est la structure correspondante.

1
Soit A un ensemble, 2A est l’ensemble des parties de A, à savoir, l’ensemble contenant tous les
sous-ensembles de A. Par exemple, si A = {1, 2}, alors 2A = {∅, {1}, {2}, {1, 2}}.
Modèles de Kripke

L’intuition à la base de la sémantique des mondes possibles (ou sémantique de

Kripke) est qu’une formule qui est “peut-être vraie” est vraie dans quelques
mondes, et peut-être fausse dans des autres.
Definition (Chemin)
Un chemin dans un modèle M est une séquence infinie d’états ρ = w0 , w1 , . . . tel
que wi Rwi+1 pour tous i ≥ 0.
Si ρ = w0 , w1 , . . ., alors ρ(i) = wi , wi+1 , . . . pour i ≥ 0.
Nous avons maintenant tous les ingrédients pour définir formellement la
satisfaction d’une formule dans le langage logique de Définition 1.
Modèles de Kripke

La notion de satisfaction sur les modèles de Kripke est définie comme il suit :
Definition (Satisfaction)
La satisfaction d’une formule φ ∈ L dans un chemin ρ = w0 , w1 , . . . d’un modèle
M, formellement (M, ρ) |= φ, est définie inductivement comme il suit :
(M, ρ) |= true
(M, ρ) |= p ssi w0 ∈ π(p)
(M, ρ) |= ¬φ ssi (M, ρ) 6|= φ
(M, ρ) |= φ ∧ ψ ssi (M, ρ) |= φ et (M, ρ) |= ψ
(M, ρ) |= φ ssi pour tous i ≥ 0, (M, ρ(i)) |= φ
(M, ρ) |= φ ssi (M, ρ(1)) |= φ
(M, ρ) |= φUψ ssi il exists i ≥ 0 tel que (M, ρ(j)) |= ψ
et pour tous 0 ≤ i < j, (M, ρ(i)) |= φ

On lit (M, ρ) |= φ comme “φ est vraie dans ρ, dans le modèle M”.

La notion de satisfaction pour les autres connecteurs logiques peut être définie à
partir des abréviations.
Modèles de Kripke

Exercice
Vérifier que les abréviations introduites ci-dessus donnent les résultats entendus.
Par exemple,

(M, ρ) |= φ ∨ ψ ssi (M, ρ) |= φ ou (M, ρ) |= ψ

(M, ρ) |= φ ssi il existe i ≥ 0 tel que (M, ρ(i)) |= φ

Solution
(M, ρ) |= φ ∨ ψ ssi (M, ρ) |= ¬(¬φ ∧ ¬ψ)
ssi (M, ρ) 6|= ¬φ ∧ ¬ψ
ssi (M, ρ) 6|= ¬φ ou (M, ρ) 6|= ¬ψ
ssi (M, ρ) |= φ ou (M, ρ) |= ψ
Modèles de Kripke

Une formule φ ∈ L est vraie dans un état w d’un modèle M, formellement

(M, w ) |= φ, ssi pour tous chemin ρ, si ρ(0) = w alors (M, ρ) |= φ.
Definition (Validité)
Une formule φ ∈ L est valide dans un modèle M, formellement M |= φ, ssi
(M, w0 ) |= φ, où w0 est l’état initial.
Exercices

Exercice
Soit M un modèle de Kripke, construit sur un ensemble de variables
propositionnelles P = {p, q} comme il suit :
• M = {w1 , w2 , w3 , w4 }
• R = {(w2 , w1 ), (w3 , w2 ), (w4 , w2 ), (w4 , w3 ), (w3 , w3 )}
• π(p) = {w2 , w4 } ; π(q) = {w2 , w3 , w4 }

Contrôlez si les formules suivantes sont satisfaites

• (M, w4 ) |= p
• (M, w4 ) |= p
• (M, w3 ) |= p
• (M, w3 ) |= (q → ¬p) → (¬p ∧ ¬q)
• (M, w2 ) |= false
• (M, w2 ) |= false
• (M, w1 ) |= true ∧ false
• (M, w2 ) |= true ∨ false
Resumé du Model Checking
Systèmes de transitions

• Modèle pour décrire le comportement des systèmes.

• Graphes où les noeuds représentent les états et les flèches modelent les
transitions.
• état :
I La couleur courante d’un feu de circulation.
I Les valeurs courantes des variables de programme + le compteur du
programme
I La valeur courante de l’ensemble des registres avec les valeurs des bits
d’entrée.
• Transition : (”changement d’état”)
I Le passage d’une couleur à l’autre
I L’exécution d’une instruction de programme
I La modification des registres et des bits d’output pour une nouvelle input.
Systèmes de transitions

Un système de transitions TS est une tuple (S, Act, →, I , AP, L) où

• S est un ensemble d’états
• Act est un ensemble d’actions
• →⊆ S × Act × S est une relation de transition
• I ⊆ S est un ensemble d’ètats initiaux
• AP est un ensemble des propositions atomiques
• L : S → 2AP est une fonction de marcage

S et Act sont ou finis ou infinis dénombrable.

α
→ s 0 à la place de (s, α, s 0 ) ∈→
Notation : s −
Un Distributeur Automatique des Boissons

payer

prendre sprite prendre bière

insert coin

τ
sprite selectionner bière
τ

ètats ? actions ? transitions ? états initiaux ?

Le Model Checking des Systèmes de Transitions

Dans le cours on a vu :
• la logique temporelle LTL
• les automates de Buchi
Maintenant, considèrez le problème suivant :

Donnés un système fini des transitions TS et une formule φ de LTL : retournez

“oui” si TS |= φ, et “no” (plus un contre-exemple) si TS 6|= φ.
Premier Tentative

TS |= φ si et seulement si Exécutions(TS) ⊆ Mots(φ), où Mots(φ) = Lω (Aφ )

si et seulement si Exécutions(TS) ∩Lω (Aφ ) = ∅

• Mais la complémentation des NBA est exponentielle sur le nombres d’états.

• Si A a n états, alors A a c n états dans le cas le pire.
• On utilise le fact que Lω (Aφ ) = Lω (A¬φ ) !
Observation

TS |= φ ssi Exécutions(TS) ⊆ Mots(φ)

ssi Exécutions(TS) ∩((2AP )ω \ Mots(φ)) = ∅
ssi Exécutions(TS) ∩ Mots(¬φ) = ∅, où Mots(¬φ) = Lω (A¬φ )
ssi TS ⊗ A¬φ |= ¬F

Le model checking de LTL est alors reduit à un contrôle de persistance.

Model Checking pour les Automates de Büchi

TS |= φ ssi Exéc(TS) ⊆ Mots(φ)

Definition
Si TS = (S, Act, →, I , AP, L) est un système de transitions où Act = ∅, alors
l’automate de Büchi ATS = (QTS , ITS , δTS , ΣTS , FTS ) correspondant à TS est tel
que
• QTS = S = FTS
• ITS = I
• ΣTS = 2AP
• s ∈ δTS (s, a) ssi s → s 0 et L(s) = a

ATS |= φ ssi Exéc(ATS ) ⊆ Mots(φ), où Exéc(ATS ) = Lω (ATS ) et Mots(φ) = Lω (Aφ )

ssi Lω (ATS ) ∩ ((2AP )ω \ Lω (Aφ ) = ∅
ssi Lω (ATS ) ∩ Lω (Aφ ) = ∅
ssi Lω (ATS ) ∩ Lω (Aφ ) = ∅
ssi Lω (ATS ) ∩ Lω (A¬φ ) = ∅
ssi Lω (ATS × A¬φ ) = ∅

Le model checking de LTL est alors reduit à contrôler que Lω (ATS × A¬φ ) est
vide.
Automates de Büchi Finis
Definition
Un automate de Buchi fini est une tuple A = (Q, I , δ, Σ, F ) où :
• Q est ensemble fini d’états
• I ⊆ Q est un ensemble des états initiaux
• δ : Q × Σ → 2Q est une fonction de transition
• Σ est un alphabet fini
• F ⊆ Q est un ensemble d’états d’acceptation.

Un automate de Buchi fini est déterministe si

1. |I | = 1
2. pour tous s ∈ Q, a ∈ Σ, |δ(s, a)| ≤ 1

α
α e1 e2 β

Fig. : A1
Automates de Büchi Finis

• Un mot fini m est une séquence fini a0 , . . . , an de symboles de Σ.

• Σ∗ est l’ensemble de tous mots finis.
• Une exécution ρ sur un mot fini m = a0 , . . . , an est une séquence fini
s0 , . . . , sn+1 d’états dans Q tel que (i) s0 ∈ I et (ii) pour tous i < n,
si+1 ∈ δ(si , ai ).
• Les automates non-déterministe peuvent avoir plusieurs exécution pour
chaque mot donné.
• Une exécution ρ = s0 , . . . , sn sur un mot fini m accepte m ssi sn ∈ F .
• Un mot m est accepté par un FBA A ssi il y a une exécution ρ dans A qui
accepte m.
• L(A) est l’ensemble des mots finis acceptés par le FBA A.
• On a que L(A1 ) = (β ∗ α)∗ .
Produit de FBA

Theorem
Si A1 et A2 sont des FBA, alors il existe un FBA A tel que
L(A) = L(A1 ) ∩ L(A2 ).

Démonstration.
Soit Ai = (Qi , Ii , δi , Σ, Fi ) pour i = 1, 2. Définez A = (Q, I , δ, Σ, F ) tel que
• Q = Q1 × Q2
• I = I1 × I2
• δ((s1 , s2 ), a) = δ1 (s1 , a) × δ2 (s2 , a)
• F = F1 × F2

On peut contrôler que L(A) = L(A1 ) ∩ L(A2 ).

On dit que A = A1 × A2 est le produit des FBA A1 et A2 .
Produit de FBA

α α
α e1 e2 β β s1 s2 α

β β

(a) A1 (b) A2

• L(A1 ) = (αβ ∗ )∗
• L(A2 ) = (β ∗ (αα∗ β)∗ β ∗ )∗
Produit de FBA

α α
α e1 e2 β β s1 s2 α

β β

(a) A1 (b) A2

• L(A1 ) = (αβ ∗ )∗
• L(A2 ) = (β ∗ (αα∗ β)∗ β ∗ )∗

α
e1 , s 1 e1 , s2 α
α
β α
β
β e2 , s 1 e2 , s2
β

Fig. : A1 × A2
Automates de Büchi Finis

Theorem
Si A est un FBA déterministe, alors il existe un FBA A tel que
L(A) = Σω \ L(A) = L(A).

Démonstration.
Si A = (Q, I , δ, Σ, F ), alors A = (Q, I , δ, Σ, Q \ F ). On peut contrôler que
L(A) = Σω \ L(A).

Theorem
Si A est un FBA non-déterministe, alors il existe un FBA déterministe Ad tel
que L(Ad ) = L(A).

Démonstration.
Si A = (Q, I , δ, Σ, F ), alors Ad = (Qd , Id , δd , Σd , Fd ) est tel que
• Qd = 2Q
• Id = {I }
• δd (S, a) = {s 0 ∈ Q | s 0 ∈ δ(s, a) pour quelque s ∈ S}
On peut contrôler que Ad est déterministe et L(Ad ) = L(A).
La dimension |Qd | = 2|Q| de Ad est exponentielle dans la dimensions |Q| de
A
Automates de Büchi

Definition
Un automate de Buchi est une tuple A = (Q, I , δ, Σ, F ) où Q, I , δ, Σ, et F sont
definis comme pour les FBA.
Automate de Buchi déterministe : même definition que pour les FBA.
• Un mot infini m est une séquence infini a0 , . . . , an , . . . de symboles de Σ.
• Σω est l’ensemble de tous mots infinis.
• Une exécution ρ sur un mot infini m = a0 , . . . , an , . . . est une séquence
infini s0 , . . . , sn , . . . d’états dans Q tel que (i) s0 ∈ I et (ii) pour tous i < n,
si+1 ∈ δ(si , ai ).
• Les BA non-déterministe peuvent avoir plusieurs exécution pour chaque mot
donné.
• lim(ρ) ⊆ Q est l’ensemble d’états qui apparaissent infiniment souvent dans
ρ.
• Une exécution ρ sur un mot fini m accepte m ssi lim(ρ) ∩ F 6= ∅.
• Un mot m est accepté par un BA A ssi il y a une exécution ρ dans A qui
accepte m.
• Lω (A) est l’ensemble des mots infinis accepté par le BA A.
FBA et BA

α α
s t α s t

(a) A (b) A0

équivalence finie 6⇒ ω-équivalence

L(A) = L(A0 ), mais Lω (A) 6= Lω (A0 )

α α
s t s t
α α

(c) A (d) A0

ω-équivalence 6⇒ équivalence finie

Lω (A) = Lω (A0 ), mais L(A) 6= L(A0 )
Produit des BA

Theorem
Si A1 et A2 sont des BA, alors il existe un BA A tel que
L(A) = L(A1 ) ∩ L(A2 ).

Démonstration.
Soit Ai = (Qi , Ii , δi , Σ, Fi ) pour i = 1, 2. Définez A = (Q, I , δ, Σ, F) tel que :
• Q = Q1 × Q2 × {1, 2}
• I = I1 × I2 × {1}
• (t1 , t2 , i) ∈ δ((s1 , s2 , j), a) si t1 ∈ δ1 (s1 , a) et t2 ∈ δ2 (s2 , a) et
I j = i ; ou
I j = 1, s ∈ F et i = 2 ; ou
1 1
I j = 2, s ∈ F et i = 1
2 2

• F = F1 × Q2 × {1}
On peut verifier que L(A) = L(A1 ) ∩ L(A2 ).
Produit de BA

α α
e3 e4 s3 s4
α α

(e) A3 (f) A4

• Lω (A3 ) = Lω (A4 ) = αω
Produit de BA

α α
e3 e4 s3 s4
α α

(i) A3 (j) A4

• Lω (A3 ) = Lω (A4 ) = αω

e3 , s 3 e4 , s3 e3 , s3 , 1 e4 , s 3 , 1 e3 , s3 , 2 e4 , s 3 , 2

α α α α

e4 , s 4 e3 , s4 e4 , s4 , 1 e3 , s 4 , 1 e4 , s4 , 2 e3 , s 4 , 2

(k) A3 ×FBA A4 (l) A3 ×BA A4

Automates de Büchi
Theorem
Si A est un BA, alors il existe un BA A tel que L(A) = Σω \ L(A).
La dimension |A| de A est exponentielle dans la dimensions |A| de A.
Theorem
Il y a un BA non-déterministe A qui accepte le langage Γ = (0 + 1)∗ 1ω , mais Γ
n’est pas accepté par un BA déterministe.
Démonstration.
Définez A = (Q, I , δ, Σ, F ) tel que
• Q = {s, t}
• I = {s}
• Σ = {0, 1}
• δ(s, 0) = δ(s, 1) = {s, t}, δ(t, 1) = {t}, δ(t, 0) = ∅
• F = {t}
On peut vérifier que L(A) = Γ.
1
0
s t
1

0 1
Automates de Büchi

Theorem
Le problème du langage vide pour les BA est décidable en temps linéaire.

Démonstration.
Soit A = (Q, I , δ, Σ, F ) un BA. Pour s, t ∈ S on dit que
• t est lié directement à s si il y a a ∈ Σ tel que t ∈ δ(s, a) ;
• t est lié à s s’il y a une séquence s1 , . . . , sm telle que (i) s1 = s, (ii) sm = t,
et (iii) pour tous 1 ≤ i < m, si+1 est lié directement à si .
Le langage L(A) n’est pas vide ssi il y a des états s ∈ I et t ∈ F tels que (i) s
est lié a t, et (ii) t est lié a so-même.
Un algorithme peut trouver une décomposition du graphe en composants
fortement connexes (algorithm de Tarjan).
L(A) est non vide ssi à partir d’un composant qui intersecte I non-trivialment, il
est possible de parvenir à un composant non-trivial qui intersecte F
non-trivialment.
Automates de Büchi

Theorem
Pour chaque formule φ ∈ LTL, Lω (Aφ ) = Lω (A¬φ ).

Démonstration.
m ∈ Lω (Aφ ) ssi m ∈ Lω (Aφ )
ssi m ∈ (2AP )ω et m ∈
/ Lω (Aφ )
ssi m ∈ (2AP )ω et ρm |6 = φ
ssi m ∈ (2AP )ω et ρm |= ¬φ
ssi m ∈ Lω (A¬φ )
Infiniment Souvent Vert ?

¬ green
green
{red} {red}
q0 q1
s0 s1 s0 s1 ¬ green

{green} {green} green ¬ green

(m) TS (n) ATS (o) A¬green

Infiniment Souvent Vert ?

¬ green
green
{red} {red}
q0 q1
s0 s1 s0 s1 ¬ green

{green} {green} green ¬ green

(a) TS (b) ATS (c) A¬green

s0 , q0 ,1 s0 , q1 , 1 s0 , q0 ,2 s0 , q1 , 2

s1 , q0 , 1 s1 , q1 , 1 s1 , q0 , 2 s1 , q1 , 2

Fig. : ATS × A¬green

Infiniment Souvent Vert ?

∅ {red} ∅ {red}
s2 s0 s1 s2 s0 s1
{green} {red} {green}

(a) TS (b) ATS

Infiniment Souvent Vert ?

∅ {red} ∅ {red}
s2 s0 s1 s2 s0 s1
{green} {red} {green}

(a) TS (b) ATS

s2 , q0 ,1 s2 , q1 , 1 s2 , q0 ,2 s2 , q1 , 2

s0 , q0 ,1 s0 , q1 , 1 s0 , q0 ,2 s0 , q1 , 2

s1 , q0 , 1 s1 , q1 , 1 s1 , q0 , 2 s1 , q1 , 2

Fig. : ATS × A¬green

Complexité

Theorem
Vérifier si un automate de Büchi A satisfait une formule φ de LTL est fait en
temps O(|A| · 2O(|φ|) ) ou en espace O(log |A| + |φ|).
Systèmes de transitions

Un système de transitions TS est une tuple (S, Act, →, I , AP, L) où

• S est un ensemble d’états
• Act est un ensemble d’actions
• →⊆ S × Act × S est une relation de transition
• I ⊆ S est un ensemble d’ètats initiaux
• AP est un ensemble des propositions atomiques
• L : S → 2AP est une fonction de marcage

S et Act sont ou finis ou infinis dénombrable.

α
→ s 0 à la place de (s, α, s 0 ) ∈→
Notation : s −
Un Distributeur Automatique des Boissons

payer

prendre sprite prendre bière

insert coin

τ
sprite selectionner bière
τ

ètats ? actions ? transitions ? états initiaux ?

Exécutions

a
• Un état s est final s’il n’y a pas de a ∈ Act, s 0 ∈ S tels que s −
→ s 0.
• Un fragment fini ρ d’une éxécution de TS est une séquence alternante
d’états et actions qui termine par un état :
αi+1
ρ = s0 α1 s1 α2 s2 . . . αn sn tel que si −−−→ si+1 pour tous 0 ≤ i < n

• Un fragment infini ρ d’une éxécution de TS est une séquence alternante

d’états et actions :
αi+1
ρ = s0 α1 s1 α2 s2 α3 s3 . . . tel que si −−−→ si+1 pour tous 0 ≤ i

• Une exécution de TS est un fragment d’exécution initial et maximal.

• Un fragment maximal d’exécution est ou fini terminant dans un état final,
ou infini.
• Un fragment d’exécution est initial si s0 ∈ I .
Exemples d’Exécutions

mon. τ p sprite mon. τ p sprite

ρ1 = → sprite −−−−→ payer −−−→ select −
payer −−−→ select − → sprite −−−−→ . . .
τ p sprite mon. τ p biere
ρ2 = select −
→ sprite −−−−→ payer −−−→ select −
→ biere −
−−−
→ ...
mon. τ p sprite mon. τ
ρ = → sprite −−−−→ payer −−−→ select −
payer −−−→ select − → sprite

• Les fragments d’éxécution ρ1 et ρ sont initiaux, pas ρ2 .

• ρ n’est pas maximal comme il ne termine pas dans un état final.
• Si on suppose que ρ1 et ρ2 sont infinis, alors ils sont maximaux.
Etats Attenaibles

L’état s ∈ S est attenaible dans TS s’il existe un fragment d’exécution initial et

fini tel que
α1 α2 αn
s0 −→ s1 −→ . . . −→ sn = s
Attain(TS) est l’ensemble de tous états attenaibles dans TS.
Modélisation des Circuits

x = 0, r = 0 x = 1, r = 0

x = 0, r = 1 x = 1, r = 1

• Représentation du système de transition d’un circuit.

• x est la variables d’entrée, y la variable de sortie, et r le registre.
• ¬(x ⊕ r ) est la fonction de sortie et x ∨ r est la fonction d’évaluation du
registre.
Propositions Atomiques

Considèrez deux possibles marcages des états :

• Soit AP = {x, y , r },
I L(x = 0, r = 1) = {r } et L(x = 1, r = 1) = {x, r , y }
I L(x = 0, r = 0) = {y } et L(x = 1, r = 0) = {x}
I Exemple de propriété : “une fois que le registre est un, il reste un”

• Soit AP = {x, y }. Les valutations des régistres sont désormais “invisibles”.

I L(x = 0, r = 1) = ∅ et L(x = 1, r = 1) = {x, y }
I L(x = 0, r = 0) = {y } et L(x = 1, r = 0) = {x}
I Exemple de propriété : “le bit y de sortie est changé infiniment souvent”
Systèmes de Transitions 6= Automates Finis

Contrairement aux automates finis, dans un système de transition :

• il n’y a pas des états d’acceptation
• l’ensemble d’états et d’actions peut être infini dénombrable
• on peut avoir des ramifications infinies
• les actions peuvent être sujets de synchronisation
• le non-déterminisme a un rôle différent
Les systèmes de transitions sont appropriées pour le comportement des systèmes
réactifs.
Exercices

• Katoen 1.1
Synchronisation Parallèle

Donnés TS1 = (Si , Act, →i , Ii , APi , Li ) et Act × Act → Act, (α, β) → α ∗ β

TS1 ⊗ TS2 = (S1 × S2 , Act, →, I1 × I2 , AP1 ∪ AP2 , L)

où L est défini comme auparavant et → est défini par la regle suivante
α β
→ s10
s1 − → s20
s2 −
α∗β
(s1 , s2 ) −−→ (s10 , s20 )
Synchronisation Parallèle

0 00 01

1 10 11

(a) TS1 (b) TS2

000 100 101 001 110

010 111 011

Fig. : TS1 ⊗ TS2

Observation

TS |= φ ssi Exé(TS) ⊆ Mots(φ)

ssi Exéc(TS) ∩((2AP )ω \ Mots(φ)) = ∅
ssi Exéc(TS) ∩ Mots(¬φ) = ∅, où Mots(¬φ) = Lω (A¬φ )
ssi Exéc(TS) ∩Lω (A¬φ )
ssi TS ⊗ A¬φ |= ¬F

Le model checking de LTL est alors reduit à un contrôle de persistance.

Produit Synchronisé

Definition
Donnés un système de transitions TS = (S, Act, →, I , AP, L) sans états finaux
et un BA non-bloquant A = (Q, Σ, δ, I , F ) tel que Σ = 2AP , définez

TS1 ⊗ A = (S 0 , Act, →0 , I 0 , AP 0 , L0 )

où
• S0 = S × Q
• AP 0 = Q
• L0 (hs, qi) = {q}
• →0 est la relation la plus petite definie par

α L(t)
s−
→t q −−→ p
α 0
(s, q) −
→ (t, p)
L(s0 )
• I 0 = {hs0 , qi | s0 ∈ I et il y a q0 ∈ I tel que q0 −
−−→ q}
Vérification des propriétés en LTL

Soient
• TS un système de transitions sans états finaux sur AP
• φ une propriéte en LTL
Les propositions suivantes sont équivalentes :
1. TS |= φ
2. Exéc(TS) ∩ Lω (A) = ∅
3. TS ⊗ A |= ¬F
où F sont les états finaux de A.
⇒ vérifier des propriétés en LTL est reduit à un contrôle de persistance !
Infiniment Souvent Vert ?

¬ green
green

{red} {green} q0 q1
¬ green
s0 s1
green ¬ green

(a) TS (b) A¬green

Infiniment Souvent Vert ?

¬ green
green

{red} {green} q0 q1
¬ green
s0 s1
green ¬ green

(a) TS (b) A¬green

s0 , q0 s0 , q1

s1 , q0 s1 , q1

Fig. : TS ⊗ A¬green
Infiniment Souvent Vert ?

¬ green
green

∅ {red} {green} q0 q1
¬ green
s2 s0 s1
green ¬ green

(a) TS (b) A¬green

Infiniment Souvent Vert ?

¬ green
green

∅ {red} {green} q0 q1
¬ green
s2 s0 s1
green ¬ green

(a) TS (b) A¬green

s2 , q0 s0 , q0 s1 , q0

s2 , q1 s0 , q1 s1 , q1

Fig. : TS ⊗ A¬green
Contrôle de Persistance

• Objectif : établir si TS |= ¬F

• L’état s soit attainable in TS et s |= F
I TS a un fragment initial qui termine en s

• Si s est dans en cycle...

I ce fragment d’exécution peut être prolongé par un’exécution infinie
I ... en traversant le cycle qui contient s infiniment souvent

⇒ TS peut visiter l’état s infiniment souvent. Alors, TS 6|= ¬F

• Si on ne trouve pas un tel s, alors TS |= ¬F
Contrôle de Persistance et Découverte des Cycles

Soient
• TS un système de transitions sans états finaux sur AP
• φ une formule propositionelle sur AP
Les propositions suivantes sont équivalentes :
1. TS 6|= φ
2. il existe s ∈ Attain(S) tel que s 6|= φ et s est dans un cycle du graphe
G (TS) de TS
Découverte des Cycles

Comment trouver des cycles attainables qui contienent des états pour ¬F ?
• Alternative 1 :
I calculez les components fortement connexes (SCC) dans G (TS)
I contrôlez qu’un des ces SCC est attainable d’un état initial
I ... qui contient un état pour ¬F
I ”finalement toujours F” est réfuté ssi un tel SCC est trouvé
• Alternative 2 :
I utilisez une recherche en profondeur
I plus adéquat pour l’algorithm de vérification ”on-the-fly”
I plus facile pour produire des contrexemples
Un Algorithme en Profondeur en Deux Phases

1. Déterminez tous les états pour ¬F qui sont attainable de quelque état
initial
I ça est fait par une recherche en profondeur standard
2. Pour chaque état pour ¬F , on contrôle s’il appartient à un cycle
I on commence une recherche en profondeur de s
I on contrôle pour tous les états attainables de s s’il y a un parcours jusqu’à s.

• Complexity temporelle : O(N (|¬F˙ | + N + M))

I où N est le nombre d’états et M le nombre des transitions
I les fragments attainable par K états pour ¬F sont recherchés K fois.