Notes
Notes
vérification et de validation
notes de cours
Michael Blondin
30 novembre 2023
Avant-propos
cb
Cette œuvre est mise à disposition selon les termes de la licence
Creative Commons Attribution 4.0 International.
Légende
Observation.
Remarque.
Les passages compris dans une région colorée sans bordure comme celle-ci
correspondent à du contenu qui ne sera pas nécessairement présenté en classe,
mais qui peut aider à une compréhension plus approfondie.
Les exercices marqués par « ⋆ » sont considérés plus avancés que les autres.
Les exercices marqués par « ⋆⋆ » sont difficiles ou dépassent le cadre du cours.
L’icône « » dans la marge fournit un lien vers des fichiers associés au passage.
L’icône « ? » dans la marge fournit un lien vers la solution de l’exercice
iii
Table des matières
1 Systèmes de transition 1
1.1 Prédécesseurs et successeurs . . . . . . . . . . . . . . . . . . . . 3
1.2 Chemins et exécutions . . . . . . . . . . . . . . . . . . . . . . . 4
1.3 Structures de Kripke . . . . . . . . . . . . . . . . . . . . . . . . 5
1.4 Explosion combinatoire . . . . . . . . . . . . . . . . . . . . . . . 6
1.5 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
3 Langages ω-réguliers 27
3.1 Expressions ω-régulières . . . . . . . . . . . . . . . . . . . . . . 27
3.1.1 Expressions régulières . . . . . . . . . . . . . . . . . . . 27
3.1.2 Syntaxe . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
iv
TABLE DES MATIÈRES v
3.1.3 Sémantique . . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2 Automates de Büchi . . . . . . . . . . . . . . . . . . . . . . . . 29
3.2.1 Langage d’un automate . . . . . . . . . . . . . . . . . . 30
3.2.2 Déterminisme et expressivité . . . . . . . . . . . . . . . 32
3.3 Intersection d’automates de Büchi . . . . . . . . . . . . . . . . . 32
3.3.1 Construction à partir d’un exemple . . . . . . . . . . . . 33
3.3.2 Construction générale . . . . . . . . . . . . . . . . . . . 35
3.4 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
8 Systèmes à pile 85
8.1 Systèmes à pile . . . . . . . . . . . . . . . . . . . . . . . . . . . 86
8.2 Calcul des prédécesseurs . . . . . . . . . . . . . . . . . . . . . . 87
8.3 Vérification à l’aide de système à pile . . . . . . . . . . . . . . . 91
8.4 Autre exemple: analyse de code intermédiaire . . . . . . . . . . 92
8.5 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
9 Systèmes à compteurs 97
9.1 Réseaux de Petri . . . . . . . . . . . . . . . . . . . . . . . . . . 97
9.2 Modélisation de systèmes concurrents . . . . . . . . . . . . . . 99
9.3 Vérification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
9.3.1 Graphes de couverture . . . . . . . . . . . . . . . . . . . 101
9.3.2 Algorithme arrière . . . . . . . . . . . . . . . . . . . . . 103
9.4 Exercices . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
Bibliographie 171
Index 174
1
Systèmes de transition
Exemple.
s0 s1 s2
1
CHAPITRE 1. SYSTÈMES DE TRANSITION 2
Exemple.
Considérons les deux processus suivants qui sont exécutés de façon concur-
rente et qui partagent une variable booléenne tour ∈ {0, 1}:
P0 (): P1 ():
boucler: boucler:
a: attendre(tour == 0) a: attendre(tour == 1)
b: tour = 1 b: tour = 0
a, b, 0 a, a, 0 b, b, 1
b, b, 0 b, a, 0 b, a, 1
a, a, 1 a, b, 1
Remarque.
La plupart du temps, nous allons omettre les états d’un système de tran-
sition qui ne sont pas accessibles à partir d’un état initial; comme ceux
plus pâles à l’exemple précédent. Toutefois, notons que déterminer si un
état est accessible ou non possède un coût algorithmique.
CHAPITRE 1. SYSTÈMES DE TRANSITION 3
Exemple.
f0
b0 b1
f0 f1 f1
m0 m1 m1 m1
f1
m1 m1
Ce système est infini puisque, par exemple, cette exécution infinie génère
une pile de profondeur arbitrairement grande:
Post(s) := {t ∈ S : s −
→ t},
Pre(s) := {t ∈ S : t −
→ s}.
∗
Nous écrivons s −→ t lorsque l’état t est accessible à partir de l’état s en zéro,
∗
une ou plusieurs transitions. En termes plus techniques, − → est la fermeture
∗
réflexive et transitive de −
→. En particulier, notons que s − → s pour tout s ∈ S.
∗
Si s −
→ t, nous disons que s est un prédécesseur de t, et que t est un suc-
cesseur de s. L’ensemble des successeurs et prédécesseurs d’un état s ∈ S sont
respectivement dénotés:
∗
Post∗ (s) := {t ∈ S : s −
→ t},
∗
Pre∗ (s) := {t ∈ S : t −
→ s}.
Exemple.
Remarque.
Exemple.
ρ n’est pas initial puisque s1 n’est pas initial. De plus, ρ n’est pas maximal
puisque Post(s2 ) ̸= ∅. En fait, T1 ne possède aucun état terminal.
Exemple.
s0 s1 s2 s3 s4
La première propriété est ambiguë car il n’est pas clair si « suivie d’une
réponse » permet l’occurrence d’une réponse en même temps qu’une de-
mande.
Si cela est permis, alors la propriété est satisfaite par T4 puisque lors-
qu’une demande est faite en s0 , elle est forcément suivie d’une réponse
en s1 , et lorsqu’une demande est faite en s4 , elle est suivie au même mo-
ment d’une réponse. Si cela n’est pas permis, alors la propriété n’est pas
satisfaite puisque la deuxième demande de l’exécution suivante n’est pas
suivie d’une demande:
ρ := s0 s1 s4 s3 s2 s3 s2 · · · .
1.5 Exercices
1.1) Considérons la structure de Kripke T suivante: ?
{p, q} {p} ∅ ∅ {p, q}
s0 s1 s2 s3 s4
s5 s6
{q} {p}
a) Décrivez Post(s), Pre(s), Post∗ (s) et Pre∗ (s) pour chaque état s.
b) Donnez la plus courte exécution de T .
c) Donnez une exécution de T qui satisfait toujours p.
d) Donnez une exécution de T qui satisfait p infiniment souvent et qui
ne satisfait pas q infiniment souvent.
boucler
1 tant que x ̸= faux
rien faire
2 /* section critique */
3 x ← vrai
4 /* section non critique */
c) Soient T1 = (S1 , −
→1 , I1 , E1 ) et T2 = (S2 , −
→2 , I2 , E2 ) des systèmes de
transition étiquetés. Le produit asynchrone T1 ∥ T2 est le système de
transition étiqueté obtenu en composant T1 et T2 avec une synchroni-
sation faite uniquement sur leurs étiquettes communes. Construisez
le produit asynchrone des deux systèmes modélisés précédemment.
Plus formellement, T1 ∥ T2 := (S, −
→, I, E) où S := S1 × S2 , I :=
I1 × I2 , E := E1 ∪ E2 , et
→ (s′1 , s′2 ) ⇐⇒ (e ∈ E1 ∩ E2 ∧ s1 −
→ s′1 ∧ s2 −
→ s′2 ) ∨
e déf e e
(s1 , s2 ) −
→ s′1 ∧ s2 = s′2 ) ∨
e
(e ∈ E1 ∩ E2 ∧ s1 −
(e ∈ E1 ∩ E2 ∧ s1 = s′1 ∧ s2 −
→ s′2 ).
e
CHAPITRE 1. SYSTÈMES DE TRANSITION 8
Processus 0 Processus 1
répéter répéter
nc0 : b0 ← 1 nc1 : b1 ← 1
t0 : tant que b1 = 1: rien t1 : si b0 = 1 alors
c0 : b0 ← 0 q1 : b1 ← 0
q1′ : tant que b0 = 1: rien
aller à nc1
c1 : b1 ← 0
2.1 Syntaxe
Soit AP un ensemble de propositions atomiques. La syntaxe de la logique tem-
porelle linéaire (LTL) sur AP est définie par la grammaire suivante:
φ ::= vrai | p | φ ∧ φ | ¬φ | Xφ | φ U φ
où p ∈ AP. Autrement dit, l’ensemble des formules LTL sur AP est défini récur-
sivement par ces règles:
— vrai est une formule LTL;
— Si p ∈ AP, alors p est une formule LTL;
— Si φ1 et φ2 sont des formules LTL, alors φ1 ∧ φ2 est une formule LTL;
— Si φ est une formule LTL, alors ¬φ est une formule LTL;
9
CHAPITRE 2. LOGIQUE TEMPORELLE LINÉAIRE (LTL) 10
Remarque.
Remarque.
2.3 Sémantique
Nous associons un sens formel aux formules LTL. Celles-ci raisonnent sur des sé-
quences infinies qui représenteront les exécutions d’un système. Formellement,
un mot infini sur un alphabet fini Σ est une fonction σ : N → Σ que nous consi-
dérons comme une séquence infinie σ(0)σ(1)σ(2) · · · . Nous écrivons Σω pour
dénoter l’ensemble des mots infinis sur Σ. Pour tous mots finis u ∈ Σ∗ et v ∈ Σ+ ,
nous dénotons par uv ω le mot infini uvvv · · · , donc u suivi de v répété infiniment
souvent. Pour tous σ ∈ Σω et i ∈ N, nous définissons σ[i..] := σ(i)σ(i + 1) · · · .
Autrement dit, σ[i..] est le suffixe infini de σ obtenu en débutant à l’indice i.
CHAPITRE 2. LOGIQUE TEMPORELLE LINÉAIRE (LTL) 11
Exemple.
Dans le but de raisonner sur les exécutions de structures de Kripke, nous uti-
liserons l’alphabet Σ = 2AP . Ainsi, une lettre est ici un ensemble de propositions
atomiques et non une unique proposition (cela peut paraître contre-intuitif!)
Exemple.
Le mot infini ∅{p}{p, q}ω sur alphabet 2{p,q} correspond à une exécution
où ni p, ni q ne sont vraies au premier moment; où seulement p est vraie
au second moment; et où p et q sont vraies pour toujours par la suite.
σ |= vrai
déf
σ |= p ⇐⇒ p ∈ σ(0)
déf
σ |= φ1 ∧ φ2 ⇐⇒ σ |= φ1 ∧ σ |= φ2
déf
σ |= ¬φ ⇐⇒ σ ̸|= φ
déf
σ |= Xφ ⇐⇒ σ[1..] |= φ
déf
σ |= φ1 U φ2 ⇐⇒ ∃j ≥ 0 : (σ[j..] |= φ2 ) ∧ (∀0 ≤ i < j : σ[i..] |= φ1 ).
p p p p p p p
Gp:
Exemple.
Nous avons:
σ |= p, σ ̸|= q,
σ ̸|= Xp, σ ̸|= Xq,
σ |= ¬Xp, σ |= ¬Xq,
σ ̸|= p U q, σ |= q U p,
σ |= GFp, σ ̸|= FGp,
σ |= G(q → Fp), σ |= FG(p ⊕ q).
Démonstration.
(a)
σ |= Fφ ⇐⇒ σ |= vrai U φ (par déf. de F)
⇐⇒ ∃j ≥ 0 : (σ[j..] |= φ) ∧ (∀0 ≤ i < j : σ[i..] |= vrai) (par déf. de U)
⇐⇒ ∃j ≥ 0 : σ[j..] |= φ (par déf. de vrai).
(b)
σ |= Gφ ⇐⇒ σ |= ¬F¬φ (par déf. de G)
⇐⇒ ¬(σ |= F¬φ) (par déf. de ¬)
⇐⇒ ¬(∃j ≥ 0 : σ[j..] |= ¬φ) (par (a))
⇐⇒ ¬(∃j ≥ 0 : ¬(σ[j..] |= φ)) (par déf. de ¬)
⇐⇒ ∀j ≥ 0 : ¬(¬(σ[j..] |= φ)) (loi de De Morgan)
⇐⇒ ∀j ≥ 0 : σ[j..] |= φ (double négation).
2.4 Équivalences
L’ensemble des mots qui satisfont une formule LTL φ sur AP se dénote par:
{ ω
}
JφK := σ ∈ (2AP ) : σ |= φ .
2.4.1 Distributivité
Les opérateurs temporels se distribuent ainsi sur les opérateurs logiques:
X(φ1 ∨ φ2 ) ≡ Xφ1 ∨ Xφ2 ,
X(φ1 ∧ φ2 ) ≡ Xφ1 ∧ Xφ2 ,
F(φ1 ∨ φ2 ) ≡ Fφ1 ∨ Fφ2 ,
G(φ1 ∧ φ2 ) ≡ Gφ1 ∧ Gφ2 ,
(φ1 ∧ φ2 ) U ψ, ≡ (φ1 U ψ) ∧ (φ2 U ψ),
ψ U (φ1 ∨ φ2 ), ≡ (ψ U φ1 ) ∨ (ψ U φ2 ).
CHAPITRE 2. LOGIQUE TEMPORELLE LINÉAIRE (LTL) 14
Remarque.
σ |= G(p ∨ q),
σ ̸|= Gp ∨ Gq.
2.4.2 Dualité
La négation interagit de cette façon avec les opérateurs temporels:
¬Xφ ≡ X¬φ,
¬Fφ ≡ G¬φ,
¬Gφ ≡ F¬φ.
2.4.3 Idempotence
Les opérateurs temporels satisfont ces règles d’idempotence:
FFφ ≡ Fφ,
GGφ ≡ Gφ,
φ1 U (φ1 U φ2 ) ≡ φ1 U φ2 .
2.4.4 Absorption
Les opérateurs temporels satisfont ces règles d’absorption:
FGFφ ≡ GFφ,
GFGφ ≡ FGφ.
Ainsi, il n’existe que quatre combinaisons des opérateurs F et G: {F, G, FG, GF}.
Ceux-ci spécifient respectivement « éventuellement », « toujours », » éventuelle-
ment toujours » et « infiniment souvent ».
Kripke T = (S, −
→, I, AP, L). La trace d’une exécution infinie s0 s1 · · · de T est
définie par
trace(s0 s1 · · · ) := L(s0 )L(s1 ) · · · .
Autrement dit, la trace d’une exécution est obtenue en remplaçant chaque état
par son étiquette qui indique les propositions atomiques qu’il satisfait.
L’ensemble des traces de T est dénoté
Traces(T ) ⊆ JφK.
Exemple.
T |= p, T |= GFp,
T ̸|= Gp, T ̸|= (¬q) U q.
{p} {p, q}
s0 s2
∅
s1
Notons qu’il est possible qu’une propriété et sa négation ne soient pas satis-
faites par un système. Par exemple, pour la structure de Kripke de la figure 2.2,
nous avons T ̸|= p ∧ q et T ̸|= ¬(p ∧ q) puisque toute exécution qui débute en s0
ne satisfait pas p ∧ q et toute exécution qui débute en s2 ne satisfait pas ¬(p ∧ q).
En particulier, il faut donc tenir compte de tous les états initiaux.
Exemple.
⊕ r1 ¬
∧ s
¬ r2 ¬
Nous spécifions ensuite que la sortie vaut 1 au plus une fois par cycle de
taille trois:
φ≤1 := G(s → (X¬s ∧ XX¬s)).
La formule ψ = s ∧ φ≥1 ∧ φ≤1 spécifie que la sortie de C évolue bien de la
façon suivante: 1, 0, 0, 1, 0, 0, . . .. Notons que C satisfait φ si et seulement
si ses registres sont initialisés à r1 = 0 et r2 = 0.
2.6.1 Invariants
Un invariant est une propriété qui doit être satisfaite à tout moment d’une exé-
cution. En LTL, un invariant s’écrit sous la forme « Gφ », où φ est une formule
propositionnelle. Par exemple, l’exclusion mutuelle de deux processus est un in-
variant qui s’écrit sous la forme G¬(c1 ∧ c2 ). Une telle propriété peut être dé-
montrée ou infirmée à l’aide d’un parcours de graphe sur la structure de Kripke.
De plus, un témoin de l’invalidité d’un invariant peut être identifié algorithmi-
quement, par exemple à l’aide d’un parcours en profondeur où l’on utilise une
pile afin de stocker un chemin qui mène à un état qui enfreint la propriété (par
ex. voir [BK08, algo. 4, p. 110]). Ainsi, on peut automatiser la vérification d’un
CHAPITRE 2. LOGIQUE TEMPORELLE LINÉAIRE (LTL) 17
2.6.2 Sûreté
Informellement, une propriété de sûreté est une propriété qui indique que « rien
de mauvais ne se produit ». Une propriété de sûreté qui n’est pas satisfaite peut
être réfutée par un préfixe fini d’une trace. Par exemple, reconsidérons la struc-
ture de Kripke T illustrée à la figure 2.2 et la propriété φ = G(p∨q). La structure
T ne satisfait pas φ tel que démontré par la « trace finie »: {p, q}{p}∅. En effet,
ni p, ni q sont vraies à la troisième position, donc la suite n’a pas d’importance.
En particulier, les invariants sont des propriétés de sûreté.
Formellement, nous disons qu’une propriété φ sur AP est une propriété de
sûreté si tout mot infini σ ̸∈ JφK satisfait:
En mots, cela signifie que si un mot infini σ enfreint φ, alors il doit posséder un
préfixe fini qui enfreint φ peu importe la façon dont on l’étend. Intuitivement,
ce préfixe σ[0..i] est celui qui « témoigne » de l’erreur.
2.6.3 Vivacité
Informellement, une propriété de vivacité est une propriété dont les bons com-
portements se manifestent « vers l’infini ». Contrairement aux propriétés de sû-
reté, une propriété de vivacité ne peut pas être réfutée à l’aide d’un préfixe fini.
Voici quelques exemples de propriétés de vivacité:
(a) GFp: p est satisfaite infiniment souvent;
(b) FGp: p est éventuellement toujours satisfaite (propriété de persistance);
(c) G(p → Fq): lorsque p est satisfaite, q est éventuellement satisfaite.
Afin d’illustrer la vivacité, considérons la propriété (a). Si elle est enfreinte
par un système T , on ne peut pas s’en convaincre à l’aide d’un préfixe fini w. Par
exemple, considérons w = ∅∅{q}∅. Bien que w ne contienne aucune occurrence
de p, il est possible qu’après quatre transitions, T visite infiniment souvent p. En
fait, ici on ne peut même pas se convaincre que T satisfait la propriété à l’aide
d’un préfixe fini. Par exemple, bien que w′ := {p}{p, q}{p} visite p plusieurs
fois, il y a peut-être moyen de compléter w′ dans T sans plus jamais visiter p.
Formellement, nous disons qu’une propriété φ sur AP est une propriété de
vivacité si pour tout mot fini w ∈ (2AP )∗ , il existe un mot infini σ ∈ (2AP )ω tel
que wσ ∈ JφK. Plus informellement, cela signifie que toute « trace finie » w peut
être étendue de telle sorte à satisfaire φ.
CHAPITRE 2. LOGIQUE TEMPORELLE LINÉAIRE (LTL) 18
2.7 Équité
Certaines propriétés d’un système concurrent peuvent parfois être trivialement
enfreintes en raison d’exécutions inéquitables qui priorisent systématiquement
certains processus. Par exemple, considérons un système constitué de n proces-
sus P1 , P2 , . . . , Pn . Pour tout 1 ≤ i ≤ n, définissons les propositions atomiques:
pi := Pi peut exécuter une instruction,
qi := Pi exécute une instruction.
Considérons la trace σ := {p1 , q1 , p2 }ω . Cette trace correspond à une exécution
où seules les instructions du processus P1 sont exécutées, bien que les instruc-
tions du processus P2 soient exécutables. En particulier, nous avons:
σ |= FG(p2 ∧ ¬q2 ).
Autrement dit, à partir d’un certain point, le processus P2 est toujours exécu-
table, mais n’est jamais exécuté. En pratique, cela pourrait correspondre à un
ordonnanceur qui ignore complètement un processus pour aucune raison va-
lable. Normalement, ce type de comportement n’est pas réaliste et il faut donc
faire l’hypothèse d’une certaine notion d’« équité » entre les processus. Nous
survolons deux telles notions d’équité.
Autrement dit, σ est faiblement équitable ssi pour chaque processus Pi , ce n’est
pas le cas qu’éventuellement celui-ci est toujours exécutable et jamais exécuté.
Il est possible de spécifier que toutes les traces faiblement équitables d’un
système doivent satisfaire une propriété ψ, et d’ignorer les traces non équitables
avec cette formule: ( n )
∧
¬φi → ψ.
i=1
Ainsi, la vérification d’une propriété ψ, sous hypothèse que les exécutions sont
faiblement équitables, ne requiert pas de machinerie supplémentaire. En effet,
la formule résultante est également une formule LTL.
Notons que:
¬φi = ¬FG(pi ∧ ¬qi ) (par définition de φi )
≡ ¬(FGpi ∧ FG¬qi ) (par distributivité de FG, voir exercice 2.9))
≡ ¬FGpi ∨ ¬FG¬qi (par la loi de De Morgan)
≡ ¬FGpi ∨ GFqi (par dualité)
≡ FGpi → GFqi (par défininition de →).
CHAPITRE 2. LOGIQUE TEMPORELLE LINÉAIRE (LTL) 19
Ainsi, de façon équivalente, qui est celle utilisée dans d’autres ouvrages comme
le manuel de référence [BK08], une trace σ est faiblement équitable ssi:
∧
n
σ |= (FGpi → GFqi ).
i=1
Équité forte. Considérons la trace ({p1 , q1 , p2 }{p1 , q1 })ω . Cette trace est fai-
blement équitable (vérifiez-le!) Toutefois, bien que le processus P2 soit exécu-
table infiniment souvent, il n’est jamais exécuté. La notion d’équité faible peut
être raffinée afin d’éliminer ce type de traces. Posons φ′i := (GFpi ∧ FG¬qi ) pour
tout 1 ≤ i ≤ n. Nous disons qu’une trace σ est fortement équitable ssi
∧
n
σ |= ¬φ′i .
i=1
Autrement dit, une trace n’est pas fortement équitable ssi un processus est exé-
cutable infiniment souvent, mais n’est exécuté qu’un nombre fini de fois.
Comme dans le cas de l’équité faible, la vérification d’une propriété ψ, sous
hypothèse que les exécutions sont fortement équitables, ne ∧requiert pas de ma-
chinerie supplémentaire; il suffit de considérer la formule ( i=1 ¬φ′i ) → ψ.
n
Notons que:
Ainsi, de façon équivalente, qui est celle utilisée par d’autres ouvrages comme
le manuel de référence [BK08], une trace σ est fortement équitable ssi:
∧
n
σ |= (GFpi → GFqi ).
i=1
Remarque.
par des assertions ou des formules LTL (avec ou sans équité). Le développe-
ment de cet outil a débuté en 1980 dans le « groupe Unix » de Bell Labs. Spin
est maintenu à jour et distribué sous licence libre. Le langage Promela supporte
des types booléens et entiers, les tableaux, les structures, les canaux de commu-
nication (finis ou de type rendez-vous), les processus (avec identités), les blocs
atomiques, différents types de flôt de contrôles (boucle, sélection, saut, etc.) Sa
syntaxe s’apparente à celle de C, à l’exception notable de l’ajout du non déter-
minisme qui permet de modéliser des comportements imprévisibles. À l’interne,
Spin convertit le code Promela vers une structure de Kripke.
Par exemple, reconsidérons l’algorithme d’exclusion mutuelle de Lamport à
deux processus tel qu’introduit au début du cours:
Processus A Processus B
init
{
atomic
{
run A()
run B()
}
}
proctype A()
{
do
:: true ->
enter:
x = true
wait:
do
:: y -> skip
:: else -> break
od
CHAPITRE 2. LOGIQUE TEMPORELLE LINÉAIRE (LTL) 21
critical:
skip
leave:
x = false
od
}
proctype B()
{
do
:: true ->
enter:
y = true
wait:
if
:: x ->
y = false
do
:: x -> skip
:: else -> break
od
goto enter
φ1 := ¬(F(« A est dans sa section critique » ∧ « B est dans sa section critique »))
φ2 := G(« B désire entrer dans sa section critique » →
F « B est dans sa section critique »)
1. ⟨A, NA ⟩B
2. ⟨NA , NB ⟩A
♂ ♂
Alice 3. ⟨NB ⟩B Bob
1. ⟨A, NA ⟩E 2. ⟨A, NA ⟩B
4. ⟨NA , NB ⟩A 3. ⟨NA , NB ⟩A
♂ 5. ⟨NB ⟩E
♂ 6. ⟨NB ⟩B
♂
Alice Eve Bob
2.10 Exercices
2.1) Soit AP = {vert, jaune, rouge} l’ensemble où chaque proposition atomique ?
indique si un feu de circulation est allumé ou non. Dites en français ce que
spécifient ces formules LTL:
a) F(vert ∧ ¬jaune ∧ ¬rouge)
b) G(rouge → ¬X vert)
c) G(rouge → (rouge U X(jaune ∧ X(jaune U vert))))
(tiré en partie de [BK08, ex. 5.4])
φ R ψ: ou
ψ ∧ ¬φ ψ ∧ ¬φ ψ ∧ ¬φ ψ ∧ ¬φ ψ ∧ ¬φ ψ ∧ ¬φ
a) ∅ω d) {r}∅{p, q, s}ω
b) {p, q, r, s}ω e) {r}∅({p, q}{r, s})ω
c) {p, q}ω f) {r}∅{p}{q, r}({p, s}∅)ω
s0 s1 s2
s3 s4 s5
{p, q, r} {q} ∅
Dans les deux premiers chapitres, nous avons vu comment modéliser différents
systèmes à l’aide de structures de Kripke, et comment spécifier leurs propriétés
en logique temporelle linéaire. Une question demeure: comment vérifier systé-
matiquement qu’une structure de Kripke satisfait une propriété LTL? Autrement
dit, comment faire le pont afin de tester algorithmiquement si Traces(T ) ⊆ JφK?
Dans cette optique, observons que Traces(T ) et JφK sont tous deux des sous-
ensembles de Σω où Σ := 2AP , donc des langages de mots infinis sur l’alphabet
Σ. Nous chercherons donc à représenter ces langages symboliquement par des
automates. Ceux-ci serviront de structures de données pouvant être manipulées
algorithmiquement.
Il est bien connu que les langages reconnus par les automates finis (déter-
ministes ou non) correspondent précisément aux langages décrits par les ex-
pressions régulières. Ces formalismes opèrent sur des mots finis. Dans notre
contexte, nous devons plutôt raisonner sur des mots infinis. Nous introduisons
donc les expressions ω-régulières, puis les automates de Büchi, qui étendent
naturellement ces formalismes au cas infini.
r ::= r∗ | (r · r) | (r + r) | a | ε
27
CHAPITRE 3. LANGAGES ω-RÉGULIERS 28
L(a) := {a},
L(ε) := {ε}.
3.1.2 Syntaxe
La syntaxe des expressions ω-régulières sur alphabet Σ est définie par cette gram-
maire, où a ∈ Σ:
s ::= rω | (r · s) | (s + s)
r ::= r∗ | (r · r) | (r + r) | a | ε
Exemple.
3.1.3 Sémantique
Nous associons un langage L(s) ⊆ Σω à chaque expression ω-régulière s, défini
récursivement par:
L(rω ) := {w0 w1 · · · : wi ∈ L(r) pour tout i ∈ N},
L(r · s) := {wσ : w ∈ L(r), σ ∈ L(s)},
L(s + s′ ) := L(s) ∪ L(s′ ).
Ainsi, l’opérateur rω est une variante de l’opérateur r∗ où plutôt que de conca-
téner des mots de L(r) un nombre fini de fois, on en concatène une infinité.
Nous disons qu’un langage est ω-régulier s’il peut être décrit par une expres-
sion ω-régulière.
Exemples.
Exemple.
A: B: q a
a
a
p q a, b p
a
r b
Exemple.
Exemples.
A: B:
a, b, c a, b a, b, c a, b
a
a, b a, b
C: D: b b
a
b, c
b, c
a
a
a c
b
a, c a, b, c
met de les combiner afin d’obtenir une représentation de leurs mots communs.
Pour y arriver, il suffit de construire un automate qui accepte l’intersection de
leurs langages. Nous montrons donc comment construire un automate de Bü-
chi, nommé A∩B, tel que L(A∩B) = L(A)∩L(B). Autrement dit, cet automate
acceptera précisément les mots acceptés par A et B.
A: B:
a b a b
a b
p q r s
a a
a
a
p, r q, r
a
b
a
q, s b
a
a
a
a
a
p, r, A q, r, A p, r, B q, r, B
a
b b
q, s, A q, s, B
b
A = (QA , Σ, δA , Q0,A , FA ), et
B = (QB , Σ, δB , Q0,B , FB ).
Q := QA × QB × {A, B},
Q0 := Q0,A × Q0,B × {A},
F := FA × QB × {A}.
a
La fonction de transition δ est définie par la règle suivante. Si qA −
→ rA dans
a
A, et qB −
→ rB dans B, alors nous ajoutons à A ∩ B la transition:
B si I = A et qA ∈ FA ,
a ′ ′
(qA , qB , I) −
→ (rA , rB , I ) où I := A si I = B et qB ∈ FB ,
I sinon.
Exemple.
a, b, c r
b b
a
p, s, A q, s, A
a
a, b
r, t, A r, s, B a, b
c
c c a, b
a, b
r, t, B r, s, A
c
3.4 Exercices
3.1) Donnez une expression ω-régulière et un automate de Büchi pour chacun ?
de ces langages:
a) L ⊆ {a, b}ω tel que σ ∈ L ssi le nombre de a entre deux b est pair;
b) Comme en (a) mais sur alphabet {a, b, c};
c) L ⊆ {a, b, c}ω tel que σ ∈ L ssi σ ne contient aucun b qui suit immé-
diatement un a.
a a, c
a
p q r s t
b b
3.9) Qu’en est-il des états acceptants? Autrement dit, est-ce toujours possible ?
d’obtenir un automate de Büchi équivalent avec un seul état acceptant?
3.10) ⋆ Montrez qu’il n’existe pas d’automate de Büchi déterministe qui accepte ?
le langage des mots avec un nombre fini de b sur alphabet Σ := {a, b};
autrement dit, le langage décrit par (a + b)∗ aω .
CHAPITRE 3. LANGAGES ω-RÉGULIERS 38
(p, a, q) ∈ δ ′ ⇐⇒ (p, a, q) ∈
/ δ.
Exemple.
ω
JGpK = ({p} + {p, q}) ,
| {z }
occurrence de p
∗
JGFpK = ((∅ + {q}) ({p} + {p, q}))ω ,
| {z } | {z }
pas de p occurrence de p
∗
Jp U qK = ({p} + {p, q}) ({q} + {p, q}) Σω .
| {z } | {z }
occurrence de p occurrence de q
39
CHAPITRE 4. VÉRIFICATION ALGORITHMIQUE DE FORMULES LTL 40
Fp: Gp:
{p}, {p, q}
GFp: p U q:
∅, {q}
Théorème 1. Pour toute formule LTL φ sur AP, il est possible de construire un
automate de Büchi Aφ de 2O(|φ|) états tel que L(Aφ ) = JφK. De plus, certaines
familles de formules requièrent un nombre exponentiel d’états.
δ(q, a) := {r ∈ Q : q −
→ r et L(q) = a} pour tous q ∈ Q, a ∈ 2AP .
Exemple.
T: AT :
{p} {p, q} {p}
s0 s2 s0 s2
{p, q}
{p}
{∅} {p} ∅
s1 s1
Observation.
Bien que tous les états de l’automate AT soient acceptants, cela ne si-
gnifie pas qu’il accepte forcément tous les mots. En effet, les transitions
sortantes d’un état sont toutes étiquetées par la même lettre. En particu-
lier, nous avons ∅ω ̸∈ L(AT ) dans l’exemple précédent.
T |= φ ⇐⇒ Traces(T ) ⊆ JφK
⇐⇒ Traces(T ) ∩ JφK =∅
⇐⇒ Traces(T ) ∩ J¬φK =∅
⇐⇒ L(AT ) ∩ L(A¬φ ) = ∅.
Rappelons que nous avons vu, à la section 3.3, un algorithme qui peut pro-
duire un automate B tel L(B) = L(AT )∩L(A¬φ ). Ainsi, la vérification de T |= φ
se réduit au problème qui consiste à déterminer si L(B) = ∅. Voyons comment
résoudre ce problème algorithmiquement.
CHAPITRE 4. VÉRIFICATION ALGORITHMIQUE DE FORMULES LTL 43
4.3.1 Lassos
Nous présentons d’abord une condition suffisante et nécessaire afin de détermi-
ner si le langage d’un automate de Büchi est vide. Soit B = (Q, Σ, δ, Q0 , F ) un
automate de Büchi. Un lasso de B est une séquence de la forme
u v
q0 −−−→ r −−−→ r,
Puisque F est fini, il existe forcément deux indices i < j tels que qi = qj ∈ F .
Nous obtenons donc le lasso suivant:
v0 v1 ···vi−1 vi vi+1 ···vj−1
q0 −−−−−−−→ qi −−−−−−−−→ qi .
vn
u1 um
q0 r
v1 v2
Exemple.
1 14 2 13 3 12 6 7
b
a
q0 q1 q2 q6 b
a
a b a a a
a, b b
q3 q4 q5
10 11 4 9 5 8
CHAPITRE 4. VÉRIFICATION ALGORITHMIQUE DE FORMULES LTL 46
Suite à cette première fouille, les états acceptants sont ordonnés par
[q5 , q3 , q0 ] car leur exploration a respectivement terminé aux moments
[8, 11, 14]. La deuxième exploration à partir de q5 visite [q5 , q6 ] et ainsi
aucun cycle n’est identifié. La seconde exploration à partir de q3 visite
[q4 , q5 , q2 , q1 , q3 ] et ainsi un cycle de q3 vers lui-même est découvert. Par
conséquent, l’algorithme identifie un lasso de la forme
∗ +
q0 −
→ q3 −
→ q3 .
Remarquons que les lettres sur les transitions ne jouent aucun rôle. De
plus, d’autres ordres d’exploration sont possibles selon l’ordre dans le-
quel les successeurs immédiats d’un état sont considérés.
2. Voir [EB23, chapitre 12], par exemple, pour une preuve formelle que cet algorithme fonc-
tionne, ainsi qu’une présentation d’autres algorithmes de détection de lasso.
CHAPITRE 4. VÉRIFICATION ALGORITHMIQUE DE FORMULES LTL 47
devient inactif lorsque tous les sommets de sa composante ont été entièrement
traités (ce qui est équivalent à dire que la racine a été entièrement traitée).
La procédure, décrite à algorithme 4, procède ainsi:
— On lance l’exploration à partir d’un état initial q0 ∈ Q0 ;
— Si un nouvel état inactif q est découvert, alors q devient actif et la racine
de sa propre composante;
— Si un état actif q est redécouvert à partir d’un état p, alors p, q et tous les
sommets de rang supérieur à q sur le dessus de la pile font partie de la
même composante fortement connexe; on procède donc à leur fusion;
— Lors d’une fusion, si on rencontre une racine acceptante x, alors un lasso a
été identifé; en effet, cela signifie qu’à partir de q0 ∈ Q0 on peut atteindre
p ∈ Q et que la composante fortement connexe de p contient au moins
une transition et un état acceptant x ∈ F .
Exemple.
a, b b
q3 q4 q5
graphe actif C
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 })]
a, b b
q3 q4 q5
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 }); (q1 , {q1 })]
a, b b
q3 q4 q5
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 }); (q1 , {q1 }); (q2 , {q2 })]
a, b b
q3 q4 q5
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 }); (q1 , {q1 , q2 })]
a, b b
q3 q4 q5
CHAPITRE 4. VÉRIFICATION ALGORITHMIQUE DE FORMULES LTL 49
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 }); (q1 , {q1 , q2 }); (q4 , {q4 })]
a, b b
q3 q4 q5
b
a
q0 q1 q2 q6 b
a b
a
a a a
[(q0 , {q0 }); (q1 , {q1 , q2 }); (q4 , {q4 });
q3
a, b
q4
b
q5
(q5 , {q5 })]
b
a
q0 q1 q2 q6 b
a b
a
a a a
[(q0 , {q0 }); (q1 , {q1 , q2 }); (q4 , {q4 });
q3
a, b
q4
b
q5
(q5 , {q5 }); (q6 , {q6 })]
b
a
q0 q1 q2 q6 b
a b
a
a a a
[(q0 , {q0 }); (q1 , {q1 , q2 }); (q4 , {q4 });
q3
a, b
q4
b
q5
(q5 , {q5 })]
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 }); (q1 , {q1 , q2 }); (q4 , {q4 })]
a, b b
q3 q4 q5
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 }); (q1 , {q1 , q2 , q4 })]
a, b b
q3 q4 q5
b
a
q0 q1 q2 q6 b
a
a b a a a
[(q0 , {q0 }); (q1 , {q1 , q2 , q4 }); (q3 , {q3 })]
a, b b
q3 q4 q5
b
q0
a
q1
a
q2 q6 b [(q0 , {q0 }); (q1 , {q1 , q2 , q3 , q4 })]
a b a a a
a, b b
q3 q4 q5
lasso détecté via q3
4.4 Sommaire
L’approche algorithmique complète est schématisée à la figure 4.2.
Remarquons que la construction de T , AT et AT ∩ Aφ , ainsi que le test du
vide peuvent être être effectués simultanément à la volée. En effet, imaginons
qu’un modèle soit fourni dans un langage de description comme Promela. Un
outil de vérification comme Spin peut tester si L(AT ∩Aφ ) = ∅ en exécutant, par
exemple, l’algorithme 4 qui génère les états de AT ∩ Aφ au besoin, où les états
internes de AT sont eux-mêmes obtenus à la volée à partir du code Promela.
CHAPITRE 4. VÉRIFICATION ALGORITHMIQUE DE FORMULES LTL 50
Système Propriété
Structure de Kripke T
Calculer AT ∩ A¬φ
L(AT ∩ A¬φ ) = ∅?
oui non
Cela permet d’identifier des erreurs sans avoir à construire la structure et les
automates en entier. Dans le cas où aucune erreur n’est identifiée, on explore
tout l’espace. Cependant, il existe des techniques plus sophistiquées comme la
réduction par ordre partiel qui permet de réduire le nombre d’états.
Remarque.
4.5 Exercices
4.1) Donnez une expression ω-régulière et un automate de Büchi pour ces for- ?
mules LTL sur AP = {p, q}:
a) Xp e) p ∨ q
b) FGp
f) G(p → Fq)
c) G(p U q)
d) p U (Xq) g) G[(X¬p) → (F(p ∧ q))]
q2
c a
a b
q0 q1 q3
a
b q6 b a
c
a b
q5 q4 q7 q8
b
Remarque.
a q a
p
b r b
p, Xp p, ¬Xp
Observation.
Cela montre que le problème de vérification est NP-difficile.
5
Logique temporelle arborescente (CTL)
s0 s2 s0
{p} ∅ {p, q}
∅
s0 s1 s2
s1
{p} ∅ {p, q} {p, q} {p}
s0 s1 s2 s2 s0
54
CHAPITRE 5. LOGIQUE TEMPORELLE ARBORESCENTE (CTL) 55
Exemple.
5.1 Syntaxe
Soit AP un ensemble de propositions atomiques. La syntaxe de la logique tem-
porelle arborescente (CTL) sur AP est définie à partir de cette grammaire:
Φ ::= vrai | p | (Φ ∧ Φ) | ¬Φ | ∃φ | ∀φ
φ ::= XΦ | (Φ U Φ)
où p ∈ AP. Nous disons qu’une telle formule Φ est une formule d’état et qu’une
telle formule φ est une formule de chemin. Une formule CTL est une formule
d’état. Ainsi, les formules de chemin ne sont qu’un concept intermédiaire pour
définir les formules CTL.
Comme pour LTL, les opérateurs logiques ∨, →, ↔ et ⊕ se définissent natu-
rellement à partir de ∧ et ¬. Nous introduisons des opérateurs supplémentaires
qui seront utiles afin de modéliser des propriétés:
∃FΦ := ∃(vrai U Φ)
∀FΦ := ∀(vrai U Φ)
∃GΦ := ¬∀F¬Φ
∀GΦ := ¬∃F¬Φ
Exemple.
Remarque.
5.2 Sémantique
Contrairement à LTL, la sémantique d’une formule CTL dépend d’un système,
et donc pas seulement de AP. Soit T = (S, − →, I, AP, L) une structure de Kripke.
Nous associons un sens formel aux formules CTL en fonction de T . Les formules
d’état sont interprétées sur les états S et les formules de chemin sur les chemins
infinis de T .
Pour tout état s ∈ S, nous disons que:
s |= vrai,
déf
s |= p ⇐⇒ p ∈ L(s),
déf
s |= ¬Φ ⇐⇒ ¬(s |= Φ),
déf
s |= Φ1 ∧ Φ2 ⇐⇒ (s |= Φ1 ) ∧ (s |= Φ2 ),
déf
s |= ∃φ ⇐⇒ σ |= φ pour un certain chemin infini de T débutant en s,
déf
s |= ∀φ ⇐⇒ σ |= φ pour tout chemin infini de T débutant en s.
Remarque.
L’intuition derrière la sémantique des formules CTL est illustrée à la figure 5.2.
CHAPITRE 5. LOGIQUE TEMPORELLE ARBORESCENTE (CTL) 57
Exemple.
Exemple.
s0 s1 s3
{q}
s2
Nous avons:
5.4 Équivalences
Nous disons que deux formules CTL Φ1 et Φ2 sont équivalentes, dénoté Φ1 ≡
Φ2 , si JΦ1 K = JΦ2 K pour toute structure de Kripke. Ainsi, deux formules sont
équivalentes si elles ne peuvent pas être distinguées par une structure de Kripke.
Nous répertorions quelques équivalences entre formules CTL qui peuvent
simplifier la spécification ou l’analyse de propriétés.
5.4.1 Distributivité
Les opérateurs temporels quantifiés se distribuent de cette façon sur les opéra-
teurs logiques:
avons:
Remarque.
5.4.2 Dualité
La négation interagit de cette façon avec les opérateurs temporels quantifiés:
¬∃XΦ ≡ ∀X¬Φ,
¬∀XΦ ≡ ∃X¬Φ,
¬∃GΦ ≡ ∀F¬Φ,
¬∀GΦ ≡ ∃F¬Φ.
5.4.3 Idempotence
Les opérateurs temporels quantifiés satisfont ces règles d’idempotence:
∀G ∀GΦ ≡ ∀GΦ,
∀F ∀FΦ ≡ ∀FΦ,
∃G ∃GΦ ≡ ∃GΦ,
∃F ∃FΦ ≡ ∃FΦ.
CHAPITRE 5. LOGIQUE TEMPORELLE ARBORESCENTE (CTL) 60
5.5 Exercices
5.1) Considérons la structure de Kripke illustrée à l’exemple de la section 5.3. ?
Satisfait-elle ces formules?
a) ∃(p U (¬p ∧ ∃(¬p U q)));
b) ∃(p U (¬p ∧ ∀(¬p U q)));
c) ∀(p U (¬p ∧ ∃(¬p U q)));
d) ∀(p U (¬p ∧ ∀(¬p U q))).
5.2) Montrez que ces formules CTL ne sont généralement pas équivalentes: ?
a) ∀F(Φ1 ∨ Φ2 ) ̸≡ (∀FΦ1 ) ∨ (∀FΦ2 ),
b) ∃G(Φ1 ∧ Φ2 ) ̸≡ (∃GΦ1 ) ∧ (∃GΦ2 ),
c) ¬∃(Φ1 U Φ2 ) ̸≡ ∀((¬Φ1 ) U (¬Φ2 )).
5.4) Nous disons qu’une formule LTL φ et une formule CTL Φ sont équivalentes, ?
dénoté φ ≡ Φ, lorsque T |= φ ⇐⇒ T |= Φ pour toute structure de Kripke
T . Montrez que ces formules ne sont pas équivalentes:
a) φ := FGp et Φ := ∀F∀Gp
b) φ := FXp et Φ := ∀F∀Xp
{p} {p, q}
s0 s1
s2 s3
{q} ∅
a) ∀F∃Gp
b) ∀G∃X∀F(p ∧ q)
c) ∃[(¬(p ∧ q)) U (∀Xp)]
6
Vérification algorithmique de formules CTL
1. JpK, 5. J∃G¬rK,
2. JqK, 6. J∃XpK,
3. JrK, 7. J∃(q U (∃G¬r))K,
4. J¬rK, 8. JΦK.
Autrement dit, nous procéderons par induction structurelle sur l’arbre syn-
taxique de Φ, c.-à-d. en calculant l’ensemble d’états de chacun de ces sommets
récursivement (du bas vers le haut):
p q ∃G¬r
¬r
61
CHAPITRE 6. VÉRIFICATION ALGORITHMIQUE DE FORMULES CTL 62
∃FΦ ≡ ∃(vrai U Φ)
∀XΦ ≡ ¬∃X¬Φ
∀FΦ ≡ ¬∃G¬Φ
∀GΦ ≡ ¬∃(vrai U ¬Φ)
∀(Φ1 U Φ2 ) ≡ (¬∃G¬Φ2 ) ∧ (¬∃(¬Φ2 U (¬Φ1 ∧ ¬Φ2 )))
Exemple.
JvraiK = S,
JpK = {s ∈ S : p ∈ L(s)},
JΦ1 ∧ Φ2 K = JΦ1 K ∩ JΦ2 K,
J¬ΦK = S \ JΦK.
Démonstration. Montrons d’abord que T est bien défini, c.-à-d. qu’il existe bien
un plus grand ensemble. Pour ce faire, il suffit de démontrer que les ensembles
qui satisfont la propriété sont clos sous union. Soient T1 , T2 ⊆ JΦK tels que
s ∈ T1 =⇒ Post(s) ∩ T1 ̸= ∅,
s ∈ T2 =⇒ Post(s) ∩ T2 ̸= ∅.
T ′ ⊆ JΦK et s ∈ T ′ =⇒ Post(s) ∩ T ′ ̸= ∅.
Exemple.
s1 s3 s5 s7
s1 s3 s5 s7
s1 s3 s5 s7
Exemple.
s1 s3 s5 s7
s1 s3 s5 s7
s1 s3 s5 s7
s1 s3 s5 s7
s1 s3 s5 s7
6.2.5 Optimisations
Il est possible d’adapter l’algorithme 7 afin d’opérer directement sur une formule
CTL générale, plutôt que de la mettre en forme normale existentielle. De plus,
chaque étape s’implémente en temps linéaire plutôt que quadratique. Ainsi, la
vérification d’une formule CTL Φ requiert un temps de O((|S| + |− →|) · |Φ|) dans
le pire cas. En particulier, pour une formule de taille constante, la vérification
s’effectue en temps linéaire.
Nous présentons deux telles optimisations afin d’illustrer les idées générales.
Voyons d’abord comment calculer J∃GΦK en temps linéaire à partir de JΦK. Soit
CHAPITRE 6. VÉRIFICATION ALGORITHMIQUE DE FORMULES CTL 68
GΦ le graphe induit par la structure de Kripke restreinte à ses états qui appar-
tiennent à JΦK. Remarquons que
Exemple.
s1 s3 s1
{q} {p}
Voyons maintenant comment gérer une formule de la forme ∀GΦ sans passer
par la forme normale existentielle. Rappelons que s |= ∀GΦ ssi tous les chemins
qui débutent dans l’état s satisfont Φ. Ainsi, on peut initialement considérer tous
les états de JΦK, puis itérativement raffiner l’ensemble en retirant les états qui
possèdent au moins un successeur qui n’en fait pas partie. Cette procédure est
décrite à l’algorithme 8.
Exemple.
s1 s3 s5
s1 s3 s5
s1 s3 s5
6.2.6 Outils
Il existe un certain nombre d’outils de vérifications pour CTL. En particulier, le
logiciel de vérification NuSMV, développé conjointement à l’Université Carnegie-
Mellon, de Gênes et de Trente, permet de vérifier des spécifications CTL (et LTL)
de systèmes finis dans un langage de description de haut niveau. NuSMV est un
descendant de SMV, un outil de vérification historique qui a notamment per-
mis de vérifier formellement des composantes matérielles de grande taille et
d’identifier des bogues dans le standard IEEE Future+.
Voici un exemple de modélisation d’une structure de Kripke et de la propriété
∀X(p ∧ ∃(p U q)):
MODULE main
VAR
etat : {s0, s1, s2, s3};
ASSIGN
init(etat) := s0;
next(etat) :=
case
etat = s0 : {s1, s2};
etat = s1 : s3;
etat = s2 : {s0, s1, s2};
etat = s3 : s2;
esac;
DEFINE
p := etat = s0 | etat = s1 | etat = s2;
q := etat = s1;
SPEC
AX (p & E [p U q])
niveau afin de décrire des structures plus complexes, qui sont ensuite converties
en structures de Kripke à l’interne (comme pour Spin et Promela).
Remarque.
6.3 Exercices
6.1) Calculer algorithmiquement les états de la structure de Kripke ci-dessous ?
qui satisfont ces propriétés:
a) Φ1 := ∃F(p ↔ r ∧ p ⊕ q)
b) Φ2 := ∃Gq
c) ∀X(¬Φ1 ∨ ¬Φ2 )
{r} ∅
s6 s7
{p, q, r} {p}
s0 s3
s4 s5
{q} {p, r}
s2 s1
{q, r} {p, q}
6.7) Comme pour LTL, certaines spécifications ne font du sens en pratique que ?
sous hypothèse d’une notion d’équité. Contrairement à LTL, il est générale-
ment impossible de spécifier directement l’équité en CTL. Une vérification
qui tient compte de l’équité requiert donc de nouveaux algorithmes.
Soient S1 , . . . , Sn ⊆ S des ensembles d’états. Nous disons qu’un chemin
infini s0 s1 · · · est équitable s’il visite chaque ensemble Si infiniment sou-
vent. De plus, nous disons que:
CHAPITRE 6. VÉRIFICATION ALGORITHMIQUE DE FORMULES CTL 73
Au chapitre 6, nous avons vu qu’il est possible de vérifier qu’un système T satis-
fait une spécification CTL Φ en temps polynomial, plus précisément O((#états+
#transitions)·|Φ|). Toutefois, les algorithmes de vérification manipulent des en-
sembles d’états souvent gigantesques dû à l’explosion combinatoire causée par
le passage d’un modèle de haut niveau vers une structure de Kripke. Ainsi, une
représentation « énumérative », où tous les éléments d’un ensemble sont explici-
tement stockés, s’avère peu efficace en pratique. Dans ce chapitre, nous voyons
une structure de données qui représente des ensembles d’états de façon symbo-
lique. Une telle représentation permet de réduire la quantité de données tout
en offrant généralement de bonnes propriétés algorithmiques. Elle est utilisée
à l’interne, par exemple, par l’outil de vérification NuSMV. Ce chapitre se base
fortement sur l’excellente présentation de [And98]. En particulier, nous suivons
donc sa terminologie anglophone afin d’en faciliter sa lecture.
x1
x2 x2
x3 x3 x3 x3
1 1 0 0 1 1 0 1
Figure 7.1 – Arbre de décision de l’expression booléenne (x1 ∨¬x2 )∧(¬x2 ∨x3 ).
Une arête tiretée (resp. pleine) sortant d’un sommet xi indique la décision où la
variable xi prend la valeur faux (resp. vrai). Les sommets 0 et 1 correspondent
respectivement aux valeurs booléennes faux et vrai.
74
CHAPITRE 7. VÉRIFICATION SYMBOLIQUE: DIAGRAMMES DE DÉCISION
BINAIRE 75
À titre d’exemple, considérons une structure de Kripke dont l’ensemble des
états est S = {s0 , s1 , . . . , s7 }, et telle que JpK = {s0 , s1 , s4 , s5 , s7 }. Chaque état
de S peut être représenté par la représentation binaire de son indice. Ainsi,
JpK = {000, 001, 100, 101, 111}
= {x1 x2 x3 ∈ {0, 1}3 : (x1 ∨ ¬x2 ) ∧ (¬x2 ∨ x3 )}.
L’ensemble JpK se représente donc symboliquement par l’expression (x1 ∨¬x2 )∧
(¬x2 ∨ x3 ), ou alternativement par l’arbre de décision illustré à la figure 7.1.
Ces deux représentations ne sont pas pratiques parce que d’une part les ex-
pressions booléennes souffrent d’une complexité calculatoire élevée, et d’autre
part de tels arbres de décision sont de taille 2n où n est le nombre de variables.
Cependant, un arbre de décision contient généralement une grande quantité de
redondance. Par exemple, l’arbre de la figure 7.1 possède plusieurs occurrences
des sommets 0 et 1, deux sous-arbres isomorphes étiquetés par x3 , en plus de
choix inutiles: par ex. lorsque x1 = x2 = faux, le résultat est vrai indépendam-
ment de la valeur de x3 .
x1
x2 x2
x3
0 1
5
x1
4 3
x2 x2
2
x3
0 1
Figure 7.3 – Exemple d’un BDD sur trois variables x1 < x2 < x3 .
Exemple.
f0 = faux ≡ ∅,
f1 = vrai ≡ {000, 001, 010, 011, 100, 101, 110, 111},
f2 = x3 ≡ {001, 011, 101, 111},
f3 = ¬x2 ∨ x3 ≡ {000, 001, 100, 101, 011, 111},
f4 = ¬x2 ≡ {000, 001, 100, 101},
f5 = (x1 ∨ ¬x2 ) ∧ (¬x2 ∨ x3 ) ≡ {000, 001, 100, 101, 111}.
Il est possible de démontrer que les BDDs offrent une représentation cano-
nique des fonctions booléennes. Autrement dit, chaque fonction booléenne est
représentée par un unique BDD (pour un ordre fixe des variables). Ainsi:
Lemme 1. Soit t une fonction booléenne sur les variables ordonnées x1 < x2 <
· · · < xn . Il existe un unique sommet de BDD tel que fu = t.
CHAPITRE 7. VÉRIFICATION SYMBOLIQUE: DIAGRAMMES DE DÉCISION
BINAIRE 77
Remarque.
⃝
4
x3
0 1
Figure 7.4 – Haut gauche: arbre d’appel de build(x1 ∨ ¬x2 ); haut droite: arbre
d’appel de build(¬x2 ∨ x3 ); où x1 < x2 < x3 , et chaque nombre encerclé
indique la valeur retournée par l’appel. Bas: BDD résultant des deux appels.
et hi(u1 ) ⃝ hi(u2 ). Comme deux chemins ne font pas nécessairement des re-
quêtes simultanément aux mêmes variables, certains appels doivent « mettre
un côté en attente » pour que l’autre côté « le ratrappe ».
⃝
6
⃝
6 x1
(3, 5)
⃝
3
⃝
2 ⃝
5 x1
⃝
2 ⃝
5
(2, 5) (1, 5)
x2 x2
⃝
1 ⃝
0 ⃝
1 ⃝
4
⃝
4
(1, 1) (0, 4) (1, 1) (1, 4) x3
⃝
0 ⃝
0 ⃝
0 ⃝
1
(0, 0) (0, 1) (1, 0) (1, 1) 0 1
Figure 7.5 – Gauche: arbre d’appel de apply∧(3, 5) sur le BDD de la figure 7.4;
droite: BDD résultant où f6 = f3 ∧ f5 .
{q} {p, q}
s0 s1
s3 s2
∅ {q}
Post(M ) = {t : ∃s (s, t) ∈ (−
→ ∩ (M × S))},
Pre(M ) = {s : ∃t (s, t) ∈ (−
→ ∩ (S × M ))}.
Notons que J∃XpK = Pre(JpK). Ainsi, nous devons calculer l’ensemble:
{s : ∃t (s, t) ∈ (−
→ ∩ (S × JpK))}.
CHAPITRE 7. VÉRIFICATION SYMBOLIQUE: DIAGRAMMES DE DÉCISION
BINAIRE 82
La représentation ensembliste de −→ ainsi que l’ensemble S × JpK = {0001,
0101, 1001, 1101} sont représentés respectivement par les sommets 8 (rayé) et
3 (plein) du BDD de la figure 7.7. Ces sommets s’obtiennent avec deux appels à
build. L’ensemble −→ ∩ (S ×JpK) est représenté par le sommet 9 de la figure 7.7.
Ce sommet est obtenu par un appel à apply∧(3, 8).
⃝
8
x1
⃝
6
x2
⃝
9
x1
⃝
3 ⃝
5 ⃝
7
x3 x3 x3
⃝
10
x1
⃝
2 ⃝
4
x4 x4
⃝
11
x1
Figure 7.7 – BDD partiel obtenu lors de la vérification de T |= ∃Xp. Les arêtes
vers le sommet 0 sont omises par souci de lisibilité.
T |= ∃Xp ⇐⇒ I ⊆ PreJpK
⇐⇒ I ∩ PreJpK = ∅.
7.2) Montrez maintenant que l’ordre des variables peut avoir un impact expo- ?
nentiel sur le nombre de sommets.
s0 s2
s1 s3
{p, q} {q, r}
Dans ce chapitre, nous voyons comment vérifier des systèmes qui font des ap-
pels récursifs ou possèdent une forme de pile. Il n’est pas possible de modéliser
de tels systèmes par une structure de Kripke finie puisqu’une pile peut générale-
ment avoir une taille arbitraire. Néanmoins, il s’avère possible de les représenter
symboliquement à l’aide d’une variante des automates à pile.
Par exemple, considérons le programme suivant constitué de deux fonctions
et d’une variable booléenne globale x:
bool x ∈ {faux,vrai}
foo(): bar():
f0 : x = ¬x: b0 : si x: foo()
f1 : si x: foo() b1 : retourner
sinon: bar()
f2 : retourner
Il n’est pas immédiatement clair si la pile d’appel peut devenir infinie ou non à
partir d’un appel initial à foo. Ainsi, sans en avoir la certitude, nous ne pouvons
pas utiliser les méthodes de vérification présentées jusqu’ici. Le programme peut
plutôt être modélisé à l’aide de ce diagramme:
f0 −
→ f1
f1 −
→ b0 f 2 f1 −
→ f0 f2
f2 −
→ ε f2 −
→ ε
x0 x1
b0 −
→ b1 b0 −
→ f 0 b1
b1 −
→ ε b1 −
→ ε
f0 −
→ f1
85
CHAPITRE 8. SYSTÈMES À PILE 86
par b0 , et on effectue un retour vers f2 (plus tard). Le mot vide ε indique que
l’exécution locale se complète et que rien n’est mis sur la pile d’appel, par ex.
« b1 −
→ ε » représente un retour de la fonction bar.
Ce type de modélisation s’étend également aux variables locales. Par exemple,
considérons ce programme:
bool g ∈ {faux,vrai}
main(l): foo():
m0 : si l: foo() f0 : g = ¬g
m1 : assert(g == l) f1 : si ¬g:
m2 : retourner foo()
f2 : foo()
f3 : retourner
(m0 , ℓ0 ) −
→ (m1 , ℓ0 ) (m0 , ℓ0 ) −
→ (m1 , ℓ0 )
(m0 , ℓ1 ) −
→ f0 (m1 , ℓ1 ) (m0 , ℓ1 ) −
→ f0 (m1 , ℓ1 )
(m1 , ℓ0 ) −
→ (m2 , ℓ0 ) f0 −
→ f1 (m1 , ℓ0 ) −
→ ⊥
(m1 , ℓ1 ) −
→ ⊥ (m1 , ℓ1 ) −
→ (m2 , ℓ1 )
(m2 , ℓ0 ) −
→ ε g0 g1 (m2 , ℓ0 ) −
→ ε
(m2 , ℓ1 ) −
→ ε (m2 , ℓ1 ) −
→ ε
f1 −
→ f0 f2 f0 −
→ f1 f1 −
→ f3
f2 −
→ f0 f3 f2 −
→ f0 f3
f3 −
→ ε f3 −
→ ε
→ ⟨p′ , w′ ⟩
i
⟨p, w⟩ −
où
Autrement dit, un P-automate A est un automate fini classique dont les états
initiaux sont ceux de P et dont l’alphabet est celui de la pile de P. Le langage
accepté par A représente le contenu possible de la pile de P. Afin d’éviter toute
ambiguïté, nous ajoutons parfois un indice à « − → » afin de mettre l’emphase sur
le système dont nous faisons référence, par ex. − →A pour A.
Formellement, nous disons que le P-automate A accepte une configuration
⟨p, w⟩ ∈ P × Γ∗ ssi p ∈ P et il existe q ∈ F tel que
w
p−
→A q.
L’ensemble des configurations acceptées par A est dénoté par Conf(A). Par
exemple, le haut de la figure 8.1 illustre un système à pile P (gauche) et un
P-automate A (droite) où Conf(A) = {⟨p, aa⟩}.
P: A:
a a
p b−
→ε p s t
a−
→ ba
c−
→b q q
b−
→ ca
r r
b
B: a
a a
p s t
b
c q b
Figure 8.1 – Exemple de P-automate B tel que Conf(B) = Pre∗ (A) calculé à
partir d’un système à pile P et d’un P-automate A.
a−
→w w
Si p −−−−→P p′ et p′ −
→B q, alors (p, a, q) peut être ajoutée à B.
Exemple.
c−
→b
r −−−→ p
⃝
2 b (r, c, p)
p −
→ p
b−
→ca
q −−−−→ r
⃝
3 ca (q, b, s)
r −→ s
a−
→ba
p −−−−→ q
⃝
4 ba (p, a, t)
q −→ t
b−
→ca
b −−−−→ r
⃝
5 ca (q, b, t)
r −→ t
main(): foo():
m0 : y = ¬y: f0 : x = ¬y
m1 : si y: f1 : si x: foo()
foo()
sinon:
main()
m2 : assert(x ̸= y)
m0 −
→ m1 m1 −
→ f0 m2
m1 −
→ m0 m2
m2 −
→ ε
m2 −
→ ⊥ x0 , y 0 x0 , y 1
f0 −
→ f1
f1 −
→ ε m0 −
→ m1
f1 −
→ ε
f0 −
→ f1 f0 −
→ f1
m1 −
→ m0 m2 m0 −
→ m1 m1 −
→ f0 m2
m2 −
→ ε x1 , y 0 x1 , y 1 m2 −
→ ⊥
f0 −
→ f1
m0 −
→ m1 f1 −
→ f0
f1 −
→ f0
x0 , y 0 Γ x1 , y 0
⊥ ⊥
⊥ ⊥
x0 , y 1 x1 , y 1
0 0 0 null ? null
−
→ 0 −
→ −
→ 0 −
→ −
→ ? −
→ ···
.. .. ..
. .. . .. . ..
. . .
CHAPITRE 8. SYSTÈMES À PILE 93
τ−
→ τ où τ ∈ Γ
τ−
→ sτ τ−
→ sτ τ−
→ aτ
où τ ∈ Γ où τ ∈ Γ s−
→ε s−
→s où τ ∈ Γ
p0 p1 p2 p3 p4 p5
sconst_0 sconst_0 smul aconst_null goto -2
L’instruction smul cause une erreur (au sens du typage) si l’on peut atteindre
une configuration de cet ensemble:
p0 p1 p2 p3 p4 p5
τ ∈ Γ \ {s}
τ ∈ Γ \ {s}
Γ
Remarque.
8.5 Exercices
8.1) Reconsidérons ce programme non déterministe du chapitre 1: ?
8.3) Nous pouvons associer une structure de Kripke infinie à un système à pile: ?
les états sont les configurations et les transitions dictent l’évolution entre
les configurations. Considérons une variante où la fonction d’étiquetage
L est de la forme L : (P × Γ) → 2AP , plutôt que de (P × Γ∗ ) → 2AP . En
mots, cela signifie qu’une proposition atomique attachée à une configura-
tion ⟨q, aw⟩ ne peut raisonner que sur son état q et la lettre a au dessus de
sa pile. Donnez une formule LTL, et la façon dont vous assignez les pro-
positions atomiques, pour ces propriétés du programme de la section 8.3:
a) une trace exécute foo infiniment souvent;
b) le programme termine;
c) chaque fois que foo est exécutée, main l’est éventuellement aussi;
d) à partir d’un certain point, x = y.
8.6) Notre modélisation à la section 8.4 suppose que seuls deux entiers de ?
type « short » (16 bits) peuvent être additionnés par l’instruction smul.
Supposons qu’elle supporte aussi des entiers de type « byte » (8 bits) qui
sont convertis à l’interne sur 16 bits. Adaptez P et A pour en tenir compte.
8.7) Donnez un système à pile pour ces programmes (tirés de [Fé19, p. 65]):
— sconst_0; goto 3; goto -2; sconst_0; smul
CHAPITRE 8. SYSTÈMES À PILE 96
8.8) ⋆⋆ (Cet « exercice » est ardu et sert d’abord à présenter une preuve, omise
dans le chapitre, aux lectrices et lecteurs intéressé·e·s; tentez d’abord l’inclu-
sion de droite qui est la plus simple) ?
Complétez cette partie de l’esquisse de preuve du théorème 2:
Au chapitre 8, nous avons introduit une forme d’infinité à nos systèmes: une
pile. En général, l’ajout d’une seconde pile à un système rend la vérification al-
gorithmique impossible car cela mène à un formalisme Turing-complet. 1 Pour
le cas particulier d’un alphabet muni d’une seule lettre, une pile correspond à
un compteur non négatif: empiler consiste à incrémenter et dépiler consiste à
décrémenter. Contrairement aux piles, l’ajout de plusieurs compteurs ne mène
pas immédiatement à un formalisme Turing-complet. Les compteurs sont éga-
lement pratiques afin de, par ex., dénombrer le nombre de ressources actuelles
d’un système. Nous poursuivons ainsi notre excursion dans le domaine des sys-
tèmes infinis en considérant les réseaux de Petri, un formalisme qui peut être
vu comme une extension des graphes (ou des automates) avec des compteurs.
Les réseaux de Petri permettent de modéliser des systèmes variés allant des
programmes concurrents aux systèmes biologiques, chimiques ou d’affaires.
1. Rappelons que par le théorème de Rice, il est impossible de vérifier une propriété sémantique
d’une machine de Turing. En particulier, il n’existe aucun algorithme qui résout le problème d’arrêt
qui consiste à déterminer si un programme termine sur une entrée donnée.
97
CHAPITRE 9. SYSTÈMES À COMPTEURS 98
Exemple.
F (s, p) = 0, F (t, p) = 4,
F (s, q) = 2, F (t, q) = 1.
s
2
p q
4 3
t
Figure 9.1 – Un exemple de réseau de Petri marqué par (1, 1). Les places
et les transitions sont représentées respectivement par des cercles et des
carrés. Les arcs représentent la fonction de flot.
mk = m′ .
t t t
m = m0 −→
1
m1 −→
2
· · · −→
k
Exemple.
∗
Dans le réseau de la figure 9.1, nous avons (1, 1) −
→ (3, 3) puisque
s t s
(1, 1) −
→ (0, 3) −
→ (4, 1) −
→ (3, 3).
CHAPITRE 9. SYSTÈMES À COMPTEURS 99
x = faux
tant que ?:
lancer proc()
proc():
p0 : si ¬x: x = vrai sinon: goto p0
p1 : tant que ¬x: pass
p2 : // code
p0 p1 p2
¬x x
p0 p1 p2
¬x x
9.3 Vérification
Nous formalisons les problèmes de vérification sous-jacents aux deux exemples:
Problème d’accessibilité
Entrée: réseau de Petri N = (P, T, F ) et marquages m, m′ ∈ NP
∗
Question: → m′ ?
m−
Problème de couverture
Entrée: réseau de Petri N = (P, T, F ) et marquages m, m′ ∈ NP
∗
Question: existe-t-il m′′ ∈ NP tel que m −
→ m′′ et m′′ ≥ m′ ?
CHAPITRE 9. SYSTÈMES À COMPTEURS 101
Ces deux problèmes sont décidables; autrement dit, ils sont tous deux so-
lubles à l’aide d’un algorithme.
Remarque.
Bien que ces deux problèmes soient décidables, leur complexité est co-
lossale: non récursive primitive [ST77, May81, Kos82, Lam92, Ler12,
CLL+ 19, Ler21, CO21] et EXPSPACE-complet [Lip76, Rac78], respecti-
vement. Cela n’empêche toutefois pas de les résoudre en pratique.
p0 p1
s
3
t
(1, 1) (1, 1)
s t s t
(1, 2) (1, ω)
s t s t
(1, 3) (3, 0)
(1, 1). En itérant la séquence st, nous pouvons donc faire croître arbitrairement
la deuxième place. Nous remplaçons donc ce marquage par le marquage étendu
(1, ω), que nous appelons son accélération. Le symbole « ω » n’indique pas que
toutes les valeurs sont atteignables, mais bien que la place peut contenir autant
de jetons que désiré. Ainsi, en inspectant les ancêtres d’un marquage lors de
son ajout, nous obtenons un graphe fini qui capture la forme des marquages
couvrables, comme celui du côté droite de la figure 9.5.
La procédure de calcul d’un graphe de couverture est décrite à l’algorithme 15.
La proposition suivante explique comment déterminer si un marquage m′
est couvrable à l’aide d’un graphe de couverture:
Proposition 10. Soit N = (P, T, F ) un réseau de Petri, et soient deux marquages
m, m′ ∈ NP . Soit G un graphe de couverture calculé par cover(N , m). Le mar-
quage m′ est couvrable à partir de m si et seulement si G possède un marquage
m′′ tel que m′′ ≥ m′ .
Notons que l’algorithme termine bel et bien sur toute entrée et qu’ainsi un
graphe de couverture est nécessairement fini:
Comme le chemin est infini et que P est fini, il existe des indices i0 < i1 < · · ·
tels que Jmi0 K = Jmi1 K = · · · . Ainsi, par le lemme de Dickson, il existe j, k ∈ N
tels que j < k et mij ≤ mik . Notons que mij ̸= mik , puisqu’autrement le
chemin ne serait pas simple. Ainsi, mij (p) < mik (p) pour au moins une place
p ∈ P . Si mik (p) = ω, alors Jmij K ̸= Jmik K, ce qui est une contradiction. Nous
avons donc mik (p) ∈ N. Cela implique que mik aurait dû être accéléré par son
ancêtre mij , ce qui n’est pas le cas puisque Jmij K = Jmik K.
Nous disons que X ⊆ N est clos par le haut si ↑X = X. Une base d’un ensemble
P
clos par le haut X est un ensemble B tel que ↑B = X. Une base B est minimale
si ce n’est pas le cas qu’il existe x, y ∈ B tels que x ≥ y et x ̸= y. Autrement dit,
B est minimale si tous ses éléments sont incomparables. La figure 9.6 donne un
exemple d’ensemble clos par le haut et de base minimale.
Figure 9.6 – Illustration d’un ensemble clos par le haut (cercles). Sa base mi-
nimale {(1, 2), (3, 1)} est représentée par des carrés.
m
≤
∗
k → m′′
−
≤
m′
CHAPITRE 9. SYSTÈMES À COMPTEURS 105
∗
Ainsi, par monotonicité, il existe un marquage m′′′ tel que m −
→ m′′′ et m′′′ ≥
′′ ′
m ≥ m . Informellement, la « monotonicité » signifie qu’un plus grand bud-
get de jetons permet de déclencher (au moins) autant de transitions. Nous
concluons donc que m peut couvrir m′ .
L’algorithme arrière cherche à calculer une représentation de ↑Pre∗ (↑m′ ).
Par exemple, considérons le réseau de Petri illustré à la figure 9.7 avec m′ =
(0, 2). L’algorithme arrière débute avec l’ensemble ↑m′ , puis calcule itérative-
ment les prédécesseurs immédiats de chacun de ses marquages jusqu’à ce que
l’ensemble se stabilise:
0 — —
3 ensemble inchangé
Puisque les ensembles clos par le haut sont infinis, cette procédure n’est pas,
à priori, effective. Pour qu’elle le soit, nous devons être en mesure de:
— représenter les ensembles clos par le haut symboliquement;
— calculer les prédécesseurs immédiats de tous les marquages d’un ensemble
clos par le haut.
Le premier point est rendu possible par cette observation:
Proposition 13. Tout ensemble X ⊆ NP clos par le haut a une base finie.
CHAPITRE 9. SYSTÈMES À COMPTEURS 106
p1 p2
t2
4 5
2
t1
Pour le second point, nous calculons pour chaque élément de la base et pour
chaque transition, le plus petit marquage pouvant le couvrir sous cette transi-
tion. Formellement, soit t ∈ T une transition et m ∈ NP un marquage. Le plus
petit marquage pouvant couvrir m en déclechant t est le marquage mt tel que
mt (p) := max(F (p, t), m(p) + F (p, t) − F (t, p)) pour tout p ∈ P.
| {z } | {z }
« budget nécessaire » « déclenchement arrière »
9.4 Exercices
9.1) Calculez un graphe de couverture de ce réseau de Petri à partir de (1, 0, 0, 0): ?
t1 p3
p1 t3 p4
t2 p2
t4
9.2) Exécutez l’algorithme arrière sur ce réseau de Petri à partir de (0, 1, 1): ?
p2
t1 t3
p1 t2 p3
9.3) Montrez que l’ordre dans lequel on construit un graphe de couverture peut ?
avoir une incidence sur sa taille. Considérez ce réseau de Petri:
t1
p1 p2
t3
t2
CHAPITRE 9. SYSTÈMES À COMPTEURS 109
Remarque.
t
→ m′ et k ≥ m
9.4) Montrez la propriété de monotonicité, c.-à-d. que m − ?
′ ′ t ′
implique l’existence de k ≥ m tel que k −
→k.
9.5) Considérons une variable entière x de n bits qui peut être incrémentée.
a) Modélisez x à l’aide de 8 places pour n = 3, puis généralisez.
b) Modélisez x à l’aide de 6 places pour n = 3, puis généralisez.
c) Modélisez le test « x == 0 ».
d) En supposant que x est signée et représentée sous complément à
deux, modélisez le test « x > 0 ».
9.7) Dans le jeu de société Century: La route des épices, chaque personne pos- ?
sède des unités de quatre types d’épices ordonnés comme suit:
17 13 16
ii. le nombre de tours minimal afin d’acheter toutes les cartes points.
b) Répondez à nouveau, en supposant maintenant qu’il est interdit de
posséder plus de dix unités d’épices (ce qui est le cas dans le jeu).
c) ⋆ Déterminez une séquence minimale pour les cartes ci-dessus, en
supposant qu’on débute avec trois unités de curcuma.
10
Systèmes probabilistes
Nous supposons pour le reste du chapitre qu’une chaîne de Markov est finie.
Les notions de chemins, d’exécutions, de successeurs et de prédécesseurs s’ap-
pliquent directement à une chaîne de Markov: nous considérons le système de
transition qu’il induit en ignorant la valeur précise des probabilités. Pour facili-
ter la présentation, nous supposerons qu’une chaîne de Markov ne possède pas
d’état terminal (c.-à-d. sans successeur immédiat).
112
CHAPITRE 10. SYSTÈMES PROBABILISTES 113
Exemple.
Considérons la figure 10.1 qui illustre une chaîne de Markov, sans pro-
positions atomiques. Celle-ci modélise un système de communication
simple qui tente d’envoyer un message à répétition sur un canal non
fiable.
1 départ
1 1
1/10
Afin de raisonner sur les propriétés d’une chaîne de Markov M, nous devons
lui associer un espace de probabilité. À cette fin, nous associons à chaque chemin
fini ρ = s0 s1 · · · sn de M, ce cylindre et cette valeur:
Proposition 14. Les ensembles engendrés par la notation LTL sont mesurables.
Exemple.
Dans le cas général indiqué par « ? », un état s atteint l’ensemble B en plus d’une
étape, ou en exactement une étape. Ainsi:
∑ ∑
P(s |= FB) = P(s, s′ ) · P(s′ |= FB) + P(s, s′ ).
s′ ∈S\B s′ ∈B
Exemple.
Exemple.
Exemple.
2. Une telle chaîne est dite ergodique ou irréductible dans le jargon mathématique.
CHAPITRE 10. SYSTÈMES PROBABILISTES 118
P(FGp) = P(FGA)
= P(FA′ ) (où A′ := {s4 , s5 })
= 3/4 · P(s0 |= FA′ ) + 1/4 · P(s5 |= FA′ ) (selon init)
= 3/4 · P(s0 |= FA′ ) + 1/4 (car s5 ∈ A′ )
= 3/4 · x(s0 ) + 1/4 (où (I − A) · x = b).
s |= vrai,
déf
s |= p ⇐⇒ p ∈ L(s),
déf
s |= ¬Φ ⇐⇒ ¬(s |= Φ),
déf
s |= Φ1 ∧ Φ2 ⇐⇒ (s |= Φ1 ) ∧ (s |= Φ2 ),
déf
s |= PI (φ) ⇐⇒ P(s |= φ) ∈ I.
Notons que la sémantique de l’opérateur PI est bien définie car toute formule
de chemin donne lieu à un événement:
Proposition 16. Pour toute formule de chemin φ et tout état s, P(s |= φ) est bien
définie, c.-à-d. que cet ensemble est mesurable:
Exemple.
10.4.2 Vérification
Le problème de vérification PCTL consiste à déterminer si un état s satisfait une
formule d’état Φ. Cela se détermine en temps O(poly(|M|) · |Φ| · m), où m est le
plus grand exposant qui apparaît sur un opérateur U≤n (ou 1 s’il n’y en a pas).
CHAPITRE 10. SYSTÈMES PROBABILISTES 120
Ainsi, JPI (XΦ)K s’obtient en évaluant chaque probabilité avec (10.2) et en conser-
vant les états dont la valeur appartenant à I.
Nous savons comment calculer P(s |= JΦ1 K U JΦ2 K) par le théorème 4. Ainsi,
comme pour l’opérateur X, il suffit d’évaluer les probabilités et de préserver les
états dont la valeur appartient à l’intervalle I.
Exemple.
10.5 Outils
La vérification formelle de chaînes de Markov (et de processus de décision mar-
koviens) est supportée par des outils comme PRISM [KNP11] et Storm [HJK+ 20].
Par exemple, la chaîne de Markov de la figure 10.1 se modélise avec PRISM:
dtmc
module systeme
// 0 = départ, 1 = envoyer, 2 = succès, 3 = échec
etat : [0..3] init 0;
// Propositions atomiques
label "envoyer" = (etat = 1);
label "succes" = (etat = 2);
P>=1 [ F "succes" ]
P>=1 [ G "envoyer" => P>=0.99 [ F<=3 "succes" ] ]
PRISM peut aussi performer des analyses quantitatives. Par exemple, nous
pouvons calculer l’espérance du nombre d’envois effectués avant un succès, en
ajoutant ce bloc de code:
puis en effectuant cette requête qui retourne (une approximation de) 10/9:
R{"nombre_envois"}=? [ F "succes" ]
CHAPITRE 10. SYSTÈMES PROBABILISTES 123
10.6 Exercices
10.1) Soit M la chaîne de Markov de la figure 10.2. ?
a) Calculez P(s0 |= Fs2 ) à l’aide d’une somme exhaustive des chemins.
b) Calculez P(GFp).
c) Calculez P(p U q).
d) Calculez P(G(p ∨ q)).
e) Calculez P(XX¬q).
10.2) Cette fonction de Knuth et Yao cherche à simuler un dé à six faces à l’aide ?
d’une pièce non biaisée:
from random import randint
def lancer_de():
x = randint(0, 1)
while True:
y = randint(0, 1)
z = randint(0, 1)
if not(x == y == z):
break
---
1/2 1/2
1 1 1 1 1 1
CHAPITRE 10. SYSTÈMES PROBABILISTES 124
(adapté de [BK08])
10.3) Nous disons qu’une formule CTL Φ et qu’une formule PCTL Φ′ sont équi- ?
valentes lorsque JΦK = JΦ′ K pour toute structure de Kripke. Montrez que
ces formules ne sont pas équivalentes à l’aide de contre-exemples:
a) Φ := ∀Fp et Φ′ := P=1 (Fp)
b) Φ := ∃Gp et Φ′ := P>0 (Gp)
10.6) ⋆ Dites pourquoi l’ensemble A := {ρ : inf(ρ) est une CFC terminale} dé-
fini à la proposition 15 est un événement.
{pIP } u 1
(adapté de [BK08])
, → ,
, → ,
, → ,
q, q → q, q pour q ∈ {, , }.
Si tous les agents se stabilisent dans le même état, alors le jeu se termine.
Calculez la probabilité que le jeu se termine dans un certain état lorsque
a) il y a initialement trois agents distincts;
b) il y a initialement deux , un et un .
Solutions des exercices
Cette section présente des solutions à certains des exercices du document. Dans
certains cas, il ne s’agit que d’ébauches de solutions.
126
SOLUTIONS DES EXERCICES 127
Chapitre 1
1.1)
a) Par ex. pour s = s2 :
Post(s2 ) = {s1 , s2 , s3 },
Pre(s2 ) = {s1 , s2 },
Post∗ (s2 ) = {s1 , s2 , . . . , s6 },
Pre∗ (s2 ) = {s0 , s1 , s2 }.
b) s0 −
→ s1 −
→ s2 −
→ s3 −
→ s4 .
c) Par ex. s0 −
→ s0 −
→ s0 −
→ ···.
d) Par ex. s0 −
→ s1 −
→ s2 −
→ s1 −
→ · · · ou s0 −
→ s5 −
→ s6 −
→ s6 −
→ ···
1.2)
a)
x = vrai x = faux
x ← faux
xv xf
x ← vrai
x ← vrai x ← faux
b)
x = vrai
noncrit
c)
SOLUTIONS DES EXERCICES 128
noncrit
x = vrai
crit x ← vrai
1, xv 2, xv 3, xv 4, xv
x ← vrai
x = faux crit
1, xf 2, xf 3, xf 4, xf
noncrit
b1 = 1
b0 ← 1 b1 = 0
nc0 t0 c0 b0 ← 0 b0 ← 1
b0 = 0 b0 = 1
b0 ← 1
b0 ← 0
0 1
b0 ← 0
b1 ← 0
b0 = 1 q1′ q1
b1 ← 0 b1 ← 1
b1 = 0 b1 = 1
b0 = 0 b0 = 1
b1 ← 1
b1 ← 1 b0 = 0 0 1
nc1 t1 c1
b1 ← 0
b1 ← 0
0, 0, nc0 , q1′
b0 = 0 b0 ← 0
b0 ← 0 b1 ← 0
1, 0, c0 , nc1 1, 1, c0 , q1 1, 0, c0 , q1′ b0 ← 1
b1 = 0 b1 ← 1 b0 ← 0
b0 = 1
b0 = 1
b0 ← 0 b0 ← 1 b1 ← 0
1, 0, t0 , nc1 1, 1, c0 , t1 0, 1, nc0 , q1
b0 ← 1
b1 = 0
b1 ← 1
b0 = 1 b1 ← 0
0, 0, nc0 , nc1 1, 1, t0 , t1 1, 1, t0 , q1 1, 0, t0 , q1′
b0 ← 1 b1 = 1 b1 = 1 b1 = 1
b1 ← 1
0, 1, nc0 , t1 1, 1, t0 , c1
b1 ← 0
b1 ← 0 b1 = 1
b0 = 0 b0 ← 1
0, 1, nc0 , c1
1.5) Supposons que ce ne soit pas le cas. Puisque T est fini et que le chemin est
infini, il existe une composante fortement connexe C ⊆ S visitée infini-
ment souvent. En particulier, il existe donc un état si ∈ C visité infiniment
souvent. Par hypothèse, {si , si+1 . . .} ̸⊆ C. Ainsi, il existe un indice j > i
tel que sj ̸∈ C. Puisque si est visité infiniment souvent, il existe un indice
k > j tel que sk = si .
∗ ∗
Ainsi, si −
→ sj −→ si , ce qui implique la contradiction sj ∈ C.
1.6)
pour i ∈ [1..n]
xi ← 0
boucler
pour i ∈ [1..n]
xi ← 1 − xi
si xi = 1 alors quitter bloc si
SOLUTIONS DES EXERCICES 130
Chapitre 2
2.1)
a) À un certain point, seul le feu vert est allumé.
b) On ne peut pas immédiatement passer du rouge au vert.
c) Lorsque le feu rouge est allumé, c’est aussi éventuellement le cas du
jaune, puis du vert.
2.2) Il existe bien des solutions (une infinité), en voici des exemples:
a) — satisfait: ∅{vert}∅ω
— ne satisfait pas: ({vert, jaune}{rouge})ω
b) — satisfait: ({rouge}{rouge}{vert})ω
— ne satisfait pas: {rouge}({rouge}{vert})ω
c) — satisfait: {rouge}{jaune}{vert}∅ω
— ne satisfait pas: {rouge}{jaune, vert}∅ω
2.3)
a)
b) GF rouge
c) ¬F ((rouge ∧ ¬vert) ∧ X ((¬jaune) U (¬rouge ∧ vert)))
2.4)
a) G(d → Fr) ou G(d → XFr) (selon l’interpétation de « suivie »)
b) FG d
c) F(d ∧ r)
d) GF r
2.5)
a)
σ |= F(φ1 ∨ φ2 )
⇐⇒ ∃j ≥ 0 : σ[j..] |= (φ1 ∨ φ2 ) (par déf. de F)
⇐⇒ ∃j ≥ 0 : (σ[j..] |= φ1 ) ∨ (σ[j..] |= φ2 ) (par déf. de ∨)
⇐⇒ (∃j ≥ 0 : σ[j..] |= φ1 ) ∨ (∃j ≥ 0 : σ[j..] |= φ2 ) (par distributivité)
⇐⇒ (σ |= Fφ1 ) ∨ (σ |= Fφ2 ) (par déf. de F)
SOLUTIONS DES EXERCICES 131
b)
2.6) φ W ψ := (φ U ψ) ∨ (Gφ)
2.8)
a) Oui, nous avons bien (φ ∨ ψ) U ψ ≡ φ U ψ. La formule de droite im-
plique celle de gauche puisqu’elle est syntaxiquement plus restrictive.
De plus, celle de gauche implique celle de droite car en choisissant
la première position qui satisfait ψ, toutes les positions précédentes
satisfont forcément φ.
Plus formellement, soit σ |= (φ ∨ ψ) U ψ. Il existe j ∈ N tel que
ce qui implie σ |= φ U ψ.
b) Non, par exemple, pour σ := {p}ω :
σ |= p U (p ∨ q),
σ ̸|= p U q.
σ |= ¬(p U q),
σ ̸|= (¬p) U (¬q).
Xψ Xψ Xφ
SOLUTIONS DES EXERCICES 132
Plus formellement:
σ |= X(φ U ψ) ⇐⇒ σ[1..] |= φ U ψ
⇐⇒ ∃j(∀0 ≤ i < j : (σ[1..])[i..] |= φ) ∧ (σ[1..])[j..] |= ψ
⇐⇒ ∃j(∀0 ≤ i < j : (σ[i..])[1..] |= φ) ∧ (σ[j..])[1..] |= ψ
⇐⇒ ∃j(∀0 ≤ i < j : σ[i..] |= Xφ) ∧ (σ[j..]) |= Xψ
⇐⇒ σ |= (Xφ) U (Xψ).
2.9) Si σ |= FG(φ1 ∧φ2 ), alors il existe un point à partir duquel tous les suffixes
de σ satisfont φ1 ∧ φ2 , et par conséquent σ |= FGφ1 et σ |= FGφ2 .
L’autre direction est moins évidente. Supposons que σ |= FGφ1 et σ |=
FGφ2 . Cela signifie qu’il existe un point i à partir duquel tous les suffixes
de σ satisfont φ1 , et un autre point j à partir duquel tous les suffixes de σ
satisfont φ2 . Par conséquent, à partir du point max(i, j), tous les suffixes
de σ satisfont à la fois φ1 et φ2 .
2.10)
2.11)
(a–b)
chan c = [1] of { bit };
byte crit = 0;
init
{
atomic
{
run process(0)
run process(1)
}
}
proctype process(bit i)
{
SOLUTIONS DES EXERCICES 133
request:
c ! i
wait:
c ? i
critical:
atomic
{
crit++
assert(crit == 1)
}
noncritical:
atomic
{
crit--
goto request
}
}
(c–d)
processus(i):
tant que vrai
/* section non critique */
c?1
/* section critique */
c!1
chan c = [1] of { bit };
init
{
atomic
{
c ! 1
run process(0)
run process(1)
}
}
proctype process(bit i)
{
noncritical:
skip
SOLUTIONS DES EXERCICES 134
wait:
c ? 1
critical:
skip
leave:
atomic
{
c ! 1
goto noncritical
}
}
#define ev_enter ([](wait0 -> <> crit0) && [](wait1 -> <> crit1))
2.12)
a) Oui. f) Non.
b) Non. g) Oui.
c) Non. h) Oui.
d) Oui. i) Oui.
e) Oui. j) Non.
Chapitre 3
3.1)
sans b un seul b plusieurs b infinité de b
z}|{ z }| { z }| { z }| {
a) aω + a∗ baω + a∗ (b(aa)∗ )∗ aω + a∗ (b(aa)∗ )ω ou a∗ (b + aa)ω
a b
a
b
a
b)
sans b un seul b
z }| { z }| {
(a + c)ω + (a + c)∗ b(a + c)ω +
(a + c)∗ (b(c + ac∗ ac∗ ))∗ (a + c)ω + (a + c)∗ (b(c + ac∗ ac∗ ))ω
| {z } | {z }
plusieurs b infinité de b
a, c b, c c
a
b
b, c a, c
a
c
3.2) a) Oui, les deux décrivent {σ ∈ {a, b} : σ contient une infinité de a et b}
ω
Remarque.
3.5) En les mettant simplement l’un à côté de l’autre, puisque plusieurs états
initiaux sont permis.
SOLUTIONS DES EXERCICES 136
3.6) Non, par exemple l’automate ci-dessous accepte aω . En inversant son état
acceptant et son état non acceptant, l’automate accepte le même langage.
3.7)
p, s, A q, s, A q, s, B
a b a
c c
a
q, t, A r, t, A q, t, B r, t, B
a
3.8) Oui, il suffit d’ajouter un nouvel état ∪ q0 , d’en faire l’unique état initial, et
d’ajouter les transitions δ(q0 , a) := q∈Q0 δ(q, a).
3.11) Non. Par exemple, dans le cas suivant, L(A) = {a, b}ω = L(A′ ):
a b b a
b a
a b
SOLUTIONS DES EXERCICES 138
Chapitre 4
4.1) Posons Σ := 2AP .
a) ∅({p} + {p, q})ω
Σ {p}, {p, q}
Σ
Σ {p}, {p, q}
{p}, {p, q}
{p}
{p}, {p, q} Σ
Σ {q}, {p, q}
{q}, {p, q}
∗
g) [(∅ + {p} + {q})∗ {p, q}] + [(∅ + {p} + {q})∗ {p, q}] Σ{p}ω
ω
∅, {p}, {q}
{p, q}
{p, q}
4.2)
a) Nous considérons l’algorithme 2 (détection linéaire par parcours post-
ordre). Après un premier parcours en profondeur, nous obtenons cet
étiquetage des états:
15 16
q2
c a
1 18 2 17 3 14
a b
q0 q1 q3
11 12
a
b q6 b a
c
a b
q5 q4 q7 q8
b
9 10 4 13 5 8 6 7
4.3)
a) ∅
b) Voici la construction pour Σ = {a, b, c} qui se généralise à un alpha-
bet arbitraire:
a b
b
p q
a
c b
a c
r
c
SOLUTIONS DES EXERCICES 141
4.4)
{p}
{p}
p, Xp p, ¬Xp
∅
∅ {p}
{p}
4.5) On peut utiliser la même idée que pour l’exercice 3.10). Afin d’obtenir une
contradiction, supposons qu’il existe un automate de Büchi déterministe
A = (Q, Σ, δ, {q0 }, F ) tel que L(A) = JFGpK. Remarquons que ∅{p}ω ∈
L(A). Il existe donc n1 ∈ N tel que ∅{p}n1 atteint un état acceptant q1 ∈ F
à partir de q0 . Le mot ∅{p}n1 ∅{p}ω est aussi accepté par A. Ainsi, il existe
n2 ∈ N tel que ∅{p}n1 ∅{p}n2 atteint un état acceptant q2 ∈ F à partir
de q0 . Puisque l’automate est déterministe, le préfixe commun à ces deux
mots traverse les mêmes états. Ainsi, nous avons:
∅{p}n1 ∅{p}n2
q0 −−−−→ q1 −−−−→ q2 .
Chapitre 5
5.1)
a) Oui, en prenant une trace de la forme {p}{q} · · · .
b) Oui. De s0 à s2 on obtient {p}{q} qui satisfait ∃p U ¬p. L’état s2 sa-
tisfait q, donc toute trace à partir de s2 satisfait trivialement ¬p U q.
c) Non, la trace ({p}{p, q})ω ne satisfait pas p U ¬p, donc ce n’est pas
nécessaire d’explorer le côté droit de la conjonction.
d) Non, cette propriété est plus forte que la précédente.
5.2) a) Cette structure de Kripke satisfait ∀F(p ∨ q), mais pas (∀Fp) ∨ (∀Fq):
{q} ∅ {p}
s2 s0 s1
b) Cette structure de Kripke satisfait (∃Gp) ∧ (∃Gq), mais pas ∃G(p ∧ q):
s2 s0 s1
{p} {q}
s0 s1
5.4)
a) Cette structure de Kripke satisfait FGp mais pas ∀F∀Gp:
s0 s1 s2
SOLUTIONS DES EXERCICES 143
5.6)
a) Oui.
b) Non.
c) Oui.
SOLUTIONS DES EXERCICES 144
Chapitre 6
6.1) Afin d’illustrer les étapes de calcul, ces solutions utilisent des ensembles
d’états comme propositions atomiques (par abus de notation):
a) ∃F{s4 , s5 } ≡ {s4 , s5 , s6 , s7 }
b) ∃G{s0 , s1 , s2 , s4 } ≡ {s0 , s2 , s4 }
c)
Ainsi:
f (n) = 3 · f (n − 1) + 2
= 3[3 · f (n − 2) + 2] + 2
= 32 · f (n − 2) + 8
= 32 · [3 · f (n − 3) + 2] + 8
= 33 · f (n − 3) + 26
= 33 · f (n − 3) + (33 − 1)
..
.
= 3i · f (n − i) + (3i − 1)
..
.
= 3n · f (n − n) + (3n − 1)
= 3n − 1.
Chapitre 7
7.1) Par exemple, le BDD ci-dessous calcule (x1 ∨ ¬x2 ) ∧ (¬x2 ∨ x3 ) sous l’ordre
x3 < x1 < x2 . Ce BDD possède trois sommets internes, alors que celui de
la figure 7.2 en possède quatre.
x3
x1 x2
⃝
5
⃝
5 x1
(x1 ∧ x3 ) ∨ x2 , 1) ⃝
2 ⃝
4
⃝
2 ⃝
4 x2 x2
(x2 , 2) (x3 ∨ x2 , 2)
⃝
0 ⃝
1 ⃝
3 ⃝
1
x3 ⃝
3
(faux, 3) (vrai, 3) (x3 , 3) (vrai, 3)
⃝
0 ⃝
1
(faux, 4) (vrai, 4) 0 1
⃝
7 ⃝
5
x1 x1
⃝
2 ⃝
4
⃝ ⃝
6 x2 x2 x2
7
(x1 ⊕ x2 , 1)
⃝
2 ⃝
6 x3 ⃝
3
(x2 , 2) (¬x2 , 2)
⃝
0 ⃝
1 ⃝
1 ⃝
0
(faux, 3) (vrai, 3) (vrai, 3) (faux, 3) 0 1
⃝
7 ⃝ ⃝
9
5
x1 x1 x1
⃝
2 ⃝
4
⃝
6 x2 x2 x2 ⃝
8 x2
⃝
9
(5, 7) x3 ⃝
3
⃝
2 ⃝
8
(2, 2) (4, 6)
⃝
0 ⃝1 ⃝
3 ⃝0 0 1
(0, 0) (1, 1) (3, 1) (1, 0)
⃝0 ⃝
1
(0, 1) (1, 1)
⃝
10 ⃝
7 ⃝ ⃝
9
5
x1 x1 x1 x1
⃝
2 ⃝
4
⃝
6 x2 x2 x2 ⃝
8 x2
x3 ⃝
3
0 1
Entrées : sommet u
Sorties : {x ∈ {0, 1}n : fu (x1 , . . . , xn ) = vrai}
sol(u):
sol'(u, i):
si u = 0 alors retourner ∅
sinon si u = 1 alors retourner {0, 1}n−i+1
sinon
ℓ ← var(u) − i
X0 ← sol'(lo(u), var(u) + 1)
X1 ← sol'(hi(u), var(u) + 1)
retourner {abc : a ∈ {0, 1}ℓ , b ∈ {0, 1}, c ∈ Xb }
retourner sol'(u, 1)
SOLUTIONS DES EXERCICES 149
c)
Entrées : sommet u
Sorties : x ∈ {0, 1}n tel que fu (x1 , . . . , xn ) = vrai
sat(u):
sat'(u, i):
si u = 0 alors retourner ⊥
sinon si u = 1 alors retourner 1n−i+1
sinon
ℓ ← var(u) − i
X1 ← sat'(hi(u), var(u) + 1)
si X1 ̸= ∅ alors
b ←1
c ← un élément de X1
sinon
X0 ← sat'(lo(u), var(u) + 1)
b ←0
c ← un élément de X0
retourner 1ℓ bc
retourner sat'(u, 1)
d)
Entrées : sommet u
Sorties : |{x ∈ {0, 1}n : fu (x1 , . . . , xn ) = vrai}|
count(u):
count'(u, i):
si u = 0 alors retourner 0
sinon si u = 1 alors retourner 2n−i+1
sinon
ℓ ← var(u) − i
c0 ← count'(lo(u), var(u) + 1)
c1 ← count'(hi(u), var(u) + 1)
retourner 2ℓ · (c0 + c1 )
retourner count'(u, 1)
⃝
5 ⃝
2
x1 x1
⃝
4 x2 x2 ⃝
3
⃝
5 ⃝
2 ⃝
6
x1 x1 x1
⃝
4 x2 x2 ⃝
3
d) Nous omettons les sommets déjà présents car ils ne sont pas utilisés:
SOLUTIONS DES EXERCICES 151
⃝
12
x1
⃝
10
x2
⃝
11
x3 x3 ⃝
9
⃝
8
x4 x4 ⃝
7
⃝
13 ⃝
2 ⃝
12 ⃝
18 ⃝
17
x3 x1 x1 x1 x1
⃝
10
x2 x2 ⃝
16
⃝
11 ⃝
14 ⃝
15
x3 x3 ⃝
9 x3 x3
⃝
8
x4 x4 ⃝
7
Chapitre 8
8.1)
a) Comme il n’y a pas de variables, le système n’a qu’un état p que nous
n’avons pas à illustrer. Les règles sont comme suit:
m0 −
→ f0 m1
m1 −
→ ε
f0 −
→ b0 f 1 | f 1
f1 −
→ ε
b0 −
→ f 0 b1
b1 −
→ ε | b2
b2 −
→ b0
m0
p q
8.3) Étiquetons chaque configuration dans l’état (xi , yj ) avec la lettre a sur
le dessus de la pile par la proposition atomique p(xi ,yj ),a . Posons φa :=
∨
i,j∈{0,1} p(xi ,yj ),a .
a) GFφf0
b) Fφε (en supposant que les configurations terminales bouclent sur
elles-mêmes afin que les exécutions soient infinies)
SOLUTIONS DES EXERCICES 153
c) G(φf0 → Fφm0 )
∨
d) FG a∈Γ (p(x0 ,y0 ),a ∧ p(x1 ,y1 ),a )
8.4) Pour chaque état initial p0 qui possède des transitions entrantes, il suffit
de copier p0 par un état p′0 , de rediriger les transitions qui entrent dans p0
vers p′0 , et de copier les transitions sortantes de p0 à p′0 . Le nombre d’états
et transitions ajoutés est linéaire.
a−
→a
i−
→i
s−
→s
a−
→ sa a−
→ sa a−
→ aa
i−
→ si i−
→ si i−
→ ai
s−
→ ss s−
→ ss s−
→ε s−
→s s−
→ as
p0 p1 p2 p3 p4 p5
sconst_0 sconst_0 smul aconst_null goto -2
Nous obtenons:
s
p0 p1 p2 p3 p4 p5
s
s
a, i
a, i
a, i a, i, s
a, i, s
a, i
a, i, s
τ−
→ τ où τ ∈ Γ
τ−
→ sτ τ−
→ sτ s−
→ε s−
→s τ−
→ aτ
où τ ∈ Γ où τ ∈ Γ b−
→ε b−
→s où τ ∈ Γ
p0 p1 p2 p3 p4 p5
sconst_0 sconst_0 smul aconst_null goto -2
8.8) ⋆⋆
Proposition 17. Conf(Bi ) ⊇ Prei (Conf(A)) pour tout i ∈ N.
p′ −
→Bi−1 p′′ −
→Bi−1 pf où p′ ∈ P , p′′ ∈ Q et pf ∈ F .
u v
→Bi p′′ −
a v
p− →Bi pf ,
→Bi r′ −
u a v
p−
→Bi−1 r − →Bi q,
w′′ ∗
— ∃ p′′ −−→A r et ⟨p, u⟩ −
→P ⟨p′′ , w′′ ⟩, et
w′ ∗
— ∃ p′ −→A q et ⟨r, av⟩ −
→P ⟨p′ , w′ ⟩.
Comme r ∈ P et aucune transition n’entre dans un état initial de A, nous
avons forcément w′′ = ε et nous pouvons donc simplifier par:
∗
— ⟨p, u⟩ −
→P ⟨r, ε⟩, et
w′ ∗
→P ⟨p′ , w′ ⟩.
— p′ −→A q et ⟨r, av⟩ −
Par conséquent:
∗ ∗
⟨p, w⟩ = ⟨p, uav⟩ − →P ⟨p′ , w′ ⟩.
→P ⟨r, av⟩ −
w′ ∗
Ainsi, p′ −→A q et ⟨p, w⟩ −
→P ⟨p′ , w′ ⟩ comme désiré.
SOLUTIONS DES EXERCICES 156
Chapitre 9
9.1)
t2 1, 0, 0, 0 t3
0, 1, 0, 0 0, 0, 1, 1
t1
t2 1, 0, 0, ω t3
0, 1, 0, ω t4 t1 0, 0, 1, ω
9.2)
→ (m′ + d) = k′ ≥ m′ .
t
k = (m + d) −
9.7) Les actions se modélisent à l’aide d’un réseau de Petri. Une carte d’amé-
lioration se modélise comme suit:
SOLUTIONS DES EXERCICES 157
2 2 2 2 2 2
3
Afin de modéliser le fait qu’une carte marchand est mise de côté lorsqu’elle
est jouée, il suffit d’ajouter deux places pour chaque carte: une qui indique
qu’elle est libre, et l’autre qui indique qu’elle est de côté. Chaque transition
est enrichie comme suit:
libre de côté
2
17
2
17
disponible 2
score
13
REPRENDRE
(3, 0, 1, 0) (0, 1, 2, 0) (2, 1, 2, 0) (1, 2, 1, 1) (2, 3, 2, 0) (0, 1, 0, 0) (0, 1, 0, 0)
16
REPRENDRE REPRENDRE
(1, 1, 3, 1) (0, 2, 2, 2) (1, 3, 3, 1) (0, 0, 2, 0) (2, 0, 2, 0) (2, 0, 3, 0) (2, 0, 3, 0)
17
Chapitre 10
10.1)
a) Nous avons:
P(s0 |= Fs2 )
∞
∑ ∞
∑
= ((1/2) · (1/4))i · (1/2) + (1/2) · ((1/4) · (1/2))i · (1/2)
i=0 i=0
∞
∑ ∞
∑
= (1/2) · (1/8)i + (1/4) · (1/8)i
i=0 i=0
= (1/2) · (1/(1 − 1/8)) + (1/4) · (1/(1 − 1/8))
= (3/4) · (8/7)
= 6/7.
P(G(p ∨ q)) = init(s0 ) · P(s0 |= G(p ∨ q)) + init(s5 ) · P(s5 |= G(p ∨ q))
= init(s0 ) · (1 − P(s0 |= F(¬p ∧ ¬q))) +
init(s5 ) · (1 − P(s5 |= F(¬p ∧ ¬q)))
= (3/4) · (1 − 4/7) + (1/4) · (1 − 0)
= 4/7
= 0,571428.
P(XX(p ∨ ¬q)
= init(s0 ) · (1/2 · 1/4 + 1/2 · 1/2 + 1/2 · 1/4) + init(s5 ) · (1/2 · 1/4)
= 3/4 · (1/2 · 1/4 + 1/2 · 1/2 + 1/2 · 1/4) + 1/4 · (1/2 · 1/4)
= 13/32
= 0,40625.
10.2)
∧
a) 1≤k≤6 P=1/6 (F pk ), où AP := {pk : 1 ≤ k ≤ 6} et la proposition pi
est associée au ième état du bas (à partir de la gauche).
SOLUTIONS DES EXERCICES 162
10.3)
a)
∅ {p}
s0 s1
b)
{p} ∅
s0 s1
10.7)
a) P=1 (F pIP )
b) P≥1/2 ((¬pIP ) U≤2 pIP )
SOLUTIONS DES EXERCICES 163
c) P=0 (F p⊥ )
d) P>0 (G P>0 (F p? ))
e) P=1 (G(pIP → P=1 (G pIP )))
10.8)
a) Nous obtenons cette chaîne de Markov:
1/3 1/3 1
2/3 2/3
1/3
1/3 1/3 1
1/3 1/3 1
1/3
2/3 2/3
1/3
1/3 1/6
1/3 1/6 1/6 1/2
1/3 1/6
1/6 1/2 1/2 1/3 1/2 1
1/3 1/2 1
1/6
2/3 1/2 1/2
1/3 1/2 1
Nous avons:
3 i
∞
∑ ∞
∑
P( |= F ) = (1/6)j · (1/3)
i=1 j=0
∞ (
∑ )i
3
= (6/5 · 1/3)
i=1
∞
∑ i
= (8/125)
i=1
∞
∑ i
= (8/125) − 1
i=0
= (125/117) − 1
= 8/117.
SOLUTIONS DES EXERCICES 165
P( |= FG )
= P( |= F )
∞ (
∑ )i
3
= P( |= F ) + (6/5 · 1/3) · 6/5 · 1/6
i=0
∑∞
= P( |= F ) + (8/125)i · 6/5 · 1/6
i=0
= P( |= F ) + 125/117 · 6/5 · 1/6
= P( |= F ) + 25/117
= 8/117 + 25/117
= 33/117.
Par conséquent:
P( |= FG )
= 1 − (P( |= FG ) + P( |= FG ))
= 1 − (33/117 + 60/117)
= 24/117.
Les fiches des pages suivantes résument le contenu de chacun des chapitres.
Elles peuvent être imprimées recto-verso, ou bien au recto seulement afin d’être
découpées et pliées en deux. À l’ordinateur, il est possible de cliquer sur la plu-
part des puces « ▶ » pour accéder à la section du contenu correspondant.
166
1. Systèmes de transition
Systèmes de transition Chemins et exécutions
▶ Modélise formellement un système concret ▶ Chemin fini: s0 −
→ s1 −
→ s2 −
→ s1
▶ États: ensemble S (sommets) ▶ Chemin infini: s1 −
→ s2 −
→ s1 −
→ s2 −
→ ···
▶ Relation de transition: −
→ ⊆ S × S (arcs) ▶ Ch. maximal: ne peut être étendu, par ex. s0 −
→ s1 −
→ s2 −
→ s3
▶ États initiaux: I ⊆ S (où S peut débuter) ▶ Exécution: chemin maximal qui débute par un état initial
Structures de Kripke
s0 s1 s2 s3 ▶ Décrit les propriétés des états d’un système
▶ Système de transition (S, −
→, I)
Prédécesseurs et successeurs ▶ Propositions atomiques AP
▶ Successeurs immédiats: Post(s1 ) = {s2 } ▶ Fonction d’étiquetage L : S → 2AP
▶ Prédécesseurs immédiats: Pre(s1 ) = {s0 , s2 } ▶ Exemple: si AP = {p, q, r} et L(s1 ) = {p, q}, alors s1 satisfait
p et q, mais pas r
▶ Successeurs: Post∗ (s1 ) = {s1 , s2 , s3 }
Explosion combinatoire
▶ Prédécesseurs: Pre∗ (s1 ) = {s0 , s1 , s2 }
▶ Nombre d’états peut croître rapidement, par ex. O(2n )
▶ États terminaux: s3 car Post(s3 ) = ∅
▶ Existe techniques pour surmonter ce problème
3. Langages ω-réguliers
Expressions ω-régulières ▶ Exemple: mots tels que #a = ∞, #b = ∞ et #c ̸= ∞:
▶ Décrivent: les langages ω-réguliers de mots infinis a, b, c a, b
▶ Syntaxe: a
a, b
s ::= rω | (r · s) | (s + s)
r ::= r∗ | (r · r) | (r + r) | a | ε b
∅, {q} 10 11 4 9 5 8
Structure de Kripke T
▶ Exemple: {p, q}
Automate de Büchi AT Automate de Büchi A¬φ
T: {p} AT :
{p}
Calculer AT ∩ A¬φ
s0 s1 {p, q} s0 s1
oui non
L(AT ∩ A¬φ ) = ∅? Erreur (lasso)
{p, q} Pas d’erreur
Logique propositionnelle s s s
▶ Règles récursives:
JvraiK = S,
Optimisations
JpK = {s ∈ S : p ∈ L(s)}, ▶ Autres opérateurs: ∀ et F s’implémentent directement; néces-
saire pour obtenir un algorithme polynomial
JΦ1 ∧ Φ2 K = JΦ1 K ∩ JΦ2 K,
▶ Points fixes: temps linéaire si calculs directs sans raffinements
J¬ΦK = S \ JΦK. itératifs; par ex. calcul de composantes fortement connexes
7. Vérification symbolique : diagrammes de décision binaire
▶ les chemins respectent l’ordre des variables ▶ Complexité: polynomiale sauf pour build ⃝
6
x2
▶ sommets uniques et non redondants (lo(u) ̸= hi(u)) ⃝
9
Vérification x1
⃝
3 ⃝ ⃝
5 7
▶ Canonicité: pas deux BDDs pour la même fonction booléenne ▶ État: représenté par identifiant binaire ⃝
10
x3 x3 x3
x1
⃝
▶ Transition: paire d’identifiants binaires
2 ⃝
4
x1 ⃝
x4 x4
x1 11
x2 x2
▶ Logique prop.: manipulation de BDD
1
x3 x3 x3 x3
→ x3
▶ Opérateurs temporels: via calculs de Post ou Pre sur BDD
1 1 0 0 1 1 0 1 0 1 ▶ Satisfiabilité: I ⊆ JΦK ⇔ I∩JΦK = ∅ ⇔ apply∧ (uI , uJΦK ) = 0
9. Systèmes infinis
Réseaux de Petri Graphes de couverture
▶ Déf.: places et transitions reliées par arcs pondérés ▶ Idée: construire Post∗ (m) mais accélérer avec ω si x < x′
▶ Marquage: nombre de jetons par place ▶ Test: m′ couvrable ssi le graphe contient un m′′ ≥ m′
▶ Déclenchement: si assez de jetons pour chaque arc entrant, ▶ Exemple: (1, 1)
s t
les retirer, et en ajouter de nouveaux selon les arcs sortants p0 p1
∗ s (0, 3) (2, 0)
▶ Successeurs: Post∗ (m) = {m′ ∈ NP : m −
→ m′ } t
3
∗
▶ Prédecesseurs: Pre∗ (m′ ) = {m ∈ NP : m −
→ m′ } t
s
(1, ω)
t
p1 p2 p1 p2
▶ Exemple: t t (0, ω) (ω, ω) s, t
t
2 2 Algorithme arrière
Modélisation ▶ Idée: construire ↑Pre∗ (↑m′ ) en déclenchant vers l’arrière
▶ Processus: comptés par les places ▶ Représentation: d’ensemble clos par le haut par base finie
▶ Exemple: si ¬x: x = vrai tant que ¬x:
▶ Test: m peut couvrir m′ ssi découvert
sinon: goto p0 pass // code
Accessibilité
▶ Problème: tester si m′ ∈ Post∗ (m)
¬x x
▶ Décidable mais plus compliqué
10. Systèmes probabilistes
Chaîne de Markov Accessibilité
▶ But: remplacer non-déterminisme par probabilités ▶ Accessibilité: événement de la forme A U B
▶ Déf.: struct. de Kripke avec proba. sur transitions / états init. ▶ Partition: S0 := J¬∃(A U B)K, S1 := B , S? := S \ (S0 ∪ S1 )
| {z } | {z } | {z }
▶ Représentation: probabilités = matrice P et vecteur init prob. nulle prob. = 1 prob. à déterminer
▶ Événements: exéc. inf. décrites par préfixes finis (cylindres) CTL probabiliste (PCTL)
▶ Probabilité: somme du produit des transitions de cylindres ▶ Syntaxe: comme CTL, mais ∃ / ∀ deviennent PI , et ajout U≤n
∑∞ ▶ PI (φ): proba. de φ dans intervalle I?
▶ Exemple: P(F succès) = i=0 1 · ((1/10) · 1)i · (9/10) = 1
▶ Outils: PRISM/Storm (PCTL, analyse quantitative, etc.) ▶ U≤n : côté droit satisfait en ≤ n étapes?
▶ Vérification: calcul récursif + éval. proba. d’accessibilité
Bibliographie
171
BIBLIOGRAPHIE 172
F, 10 déterminisme, 32
G, 10
U, 9 équité, 18
X, 9 équité faible, 18
équité forte, 19
absorption, 14 explosion combinatoire, 6
accessibilité, 100 expression
Algorithme ω-régulière, 27, 28
de Lamport, 20 régulière, 27
algorithme arrière, 103 expressivité, 32
automate, 86 exécution, 4
automate de Büchi, 29
Finally, 10
base, 103 fonction d’étiquetage, 5
BDD, 74 forme normale
bytecode, 92 existentielle, 62
chemin, 4 Globally, 10
initial, 4 graphe de couverture, 101
maximal, 4
clôture par le haut, 103 idempotence, 14, 59
code intermédiaire, 92 Infer, 70
composante fortement connexe, 67 intersection, 32
couverture, 100 invariant, 16
cryptographie, 22
Java, 92
CTL, 54, 92
langage, 30
diagramme de décision binaire, 74
ω-régulier, 29
distributivité, 13, 58
régulier, 27
dualité, 14, 59
lasso, 43
déclenchement, 97
logique temporelle arborescente, 54
174
INDEX 175
syntaxe, 55 tautologie, 13
sémantique, 56 trace, 14
équivalence, 58 transition, 1, 30
logique temporelle linéaire, 9 types de propriétés, 16
syntaxe, 9
sémantique, 10 Until, 9
équivalence, 13
LTL, 9, 92 vivacité, 17
vérification, 42, 61
marquage, 97 vérification symbolique, 74, 80
mot
infini, 10 équité, 72
état, 1
Next, 9 terminal, 3
non déterminisme, 32
NuSMV, 70
persistance, 17
Petri, 97
point fixe, 65
problème d’accessibilité, 100
problème de couverture, 100
Promela, 19
proposition atomique, 5
propriétés
invariant, 16
persistance, 17
sûreté, 17
vivacité, 17
protocole
de Needham-Schroeder, 22
prédécesseur, 3, 87
récursion, 85
réseau de Petri, 97
SMV, 70
Spin, 19
structure de Kripke, 5
successeur, 3
successeurs, 91
sucre syntaxique, 10
système
à pile, 86
système de transition, 1
système infini, 97
sûreté, 17