Spéc. & Vérif.

formelles

Spécifications et
vérifications formelles
Université d'Évry Paris-Saclay

Cours de Johan Arcile

 Model checking avec LTL

Pour vérifier formellement un système, on a besoin de :

[Link] formalisme de modélisation pour modéliser le

comportement du système;

[Link] formalisme de logique pour exprimer la propriété

qu’on souhaite vérifier;

[Link] méthode algorithmique pour répondre au

problème.
 Model checking avec LTL
Problème de la vérification de modèle (Model checking) :

Soit un modèle formel M et une propriété logique Φ;

Est-ce que le modèle satisfait la propriété ? (M ⊨ Φ ?)


M ⊨ Φ ssi t ⊨ Φ pour toute trace d’exécution t de M.


M ⊭ Φ, ssi il existe au moins une trace d’exécution t de M
telle que t ⊭ Φ.

Une telle trace est appelée contre-exemple.

 Model checking avec LTL
Exemple du ressort :

M: 1 2 3

∅ {e} {e,b}

➢
Φ=Fb

➢
Φ = G(F(¬e))
M⊨Φ?
➢
Φ = e ∨ (X e)
➢
Φ = G(F e)
 Model checking avec LTL
Exemple du ressort :

M: 1 2 3

∅ {e} {e,b}

➢
Φ=Fb Non, contre-exemple :
∀ i≥0, t(2i)=∅, t(2i+1)={e}

➢
Φ = G(F(¬e)) Non, contre-exemple :
M⊨Φ? t(0)=∅, t(1)={e}, ∀ i≥2, t(i)={e,b}

➢
Φ = e ∨ (X e) Oui, mais comment le prouver ?

➢
Φ = G(F e) Oui, mais comment le prouver ?
 Model checking avec LTL

M: 1 2 3 ➢
Φ = G(F e)

∅ {e} {e,b}

●
Si M ⊨ G(F e), alors (par transformation syntaxique)
M ⊨ ¬F(G (¬e))
●
Or, on peux prouver (par un contre-exemple) que M
⊭ F(G (¬e))
Contre-exemple : t(0)=∅, t(1)={e}, ∀ i≥2, t(i)={e,b}

M ⊭ F(G (¬e)) est il une preuve que M ⊨ ¬F(G (¬e)) ?

 Model checking avec LTL
M ⊭ F(G (¬e)) est il une preuve que M ⊨ ¬F(G (¬e)) ?

NON
M ⊨ Φ ⇒ M ⊭ ¬Φ mais M ⊭ ¬Φ ⇏ M ⊨ Φ

Pourquoi ?
 Model checking avec LTL
M ⊭ F(G (¬e)) est il une preuve que M ⊨ ¬F(G (¬e)) ?

NON
M ⊨ Φ ⇒ M ⊭ ¬Φ mais M ⊭ ¬Φ ⇏ M ⊨ Φ

Pourquoi ?

Φ et ¬Φ ne peuvent être vraies ensemble, mais elles

peuvent être fausses ensemble

M⊨Φ:
∀ t de M, t ⊨ Φ ≡ ∀ t de M, t ⊭ ¬Φ ⇒ ∃ t de M | t ⊭ ¬Φ

M ⊭ ¬Φ :
∃ t de M | t ⊭ ¬Φ ≡ ∃ t de M | t ⊨ Φ ⇏ ∀ t de M, t ⊨ Φ
 Model checking avec LTL
Exemple (non implication)

M: 1 2 3

∅ {e} {e,b}

M ⊭ G(F(¬e))
➢
Contre-exemple : t(0)=∅, t(1)={e}, ∀ i≥2, t(i)={e,b}

et

M ⊭ ¬(G(F(¬e)) ≡ F(G e)
➢
Contre-exemple : ∀ i≥0, t(2i)=∅, t(2i+1)={e}

On observe bien que M ⊭ G(F(¬e)) ⇏ M ⊨ ¬(G(F(¬e))

 Model checking avec LTL
Problématique

Soit M=(Q,q0,T,AP,L) une structure de Kripke et Φ une

formule LTL construite sur AP (les propositions atomiques de
M).

On veux vérifier que chaque trace d’exécution de M satifait Φ.


Problème : il peux exister une infinité d’exécutions
possibles !

Plutôt que de regarder chaque éléments d’un
ensemble infini (chaque trace), on va travailler sur
l’ensemble lui même.
 Model checking avec LTL
Langages

On note par Σω les mots infinis sur l’alphabet Σ


L’ensemble des traces d’exécutions de M est un
langage de mots infinis composé de lettres dans 2AP
( L(M) ⊆ (2AP)ω )

De même, on peux exprimer dans (2AP)ω toutes les
séquences infinies pour lesquelles Φ est satisfaite,
indépendamment de M. ( L(Φ) ⊆ (2AP)ω )

Ainsi, M ⊨ Φ est équivalent à L(M) ⊆ L(Φ)
 Model checking avec LTL
Exemple (inclusion des langages)

M: 1 2 Φ:Fp
∅ {p}

Mots de L(M) = Mots de L(Φ) =

•
∅ppp… ppp…
•
∅∅ppp… p∅∅∅...
•
∅...∅ppp… ∅...∅p∅∅∅...
•
∅∅∅… p∅p∅p∅…
... ...

Ici, le mot ∅∅∅… ∉ L(Φ), donc L(M) ⊊ L(Φ). Ce

mot est un contre-exemple prouvant que M ⊭ Φ.
 Langages ω-réguliers

●
Les langages de mots infinis que l’ont souhaite manipuler
sont appelés langages ω-réguliers

●
La où les langages réguliers sont des ensembles
(possiblement infinis) de mots finis, les langages ω-
réguliers sont des ensembles (possiblement infinis) de mots
infinis

●
Les langages ω-réguliers peuvent être exprimés par le
formalisme des expressions ω-régulières
 Expressions ω-régulières
Rappel

Une expression régulière (regex) est construite par :

●
les symboles d’un alphabet (tout a ∈ Σ)
●
le mot vide (ϵ)
●
les opérateurs de concaténation, de disjonction et de
l’étoile de Kleene (.,+,*)

Grammaire formelle des expressions régulières :

regex ≔ a | ϵ | regex . regex | regex + regex | regex *
 Expressions ω-régulières
Syntaxe
Grammaire formelle des expressions régulières :
regex ≔ a | ϵ | regex . regex | regex + regex | regex *

Une expression ω-régulière (ω-regex) est construite par

:
●
les expressions régulières (regex)
●
les opérateurs de concaténation, de disjonction et
d’itération infinie (.,+,ω)

Grammaire formelle des expressions ω-régulières :

ω-regex ≔ (regex) ω | regex . ω-regex | ω-regex + ω-regex
 Expressions ω-régulières
Sémantique
Grammaire formelle des expressions ω-régulières :
ω-regex ≔ (regex) ω | regex . ω-regex | ω-regex + ω-regex

regex ω signifie que l’on repète regex à l’infini, alors que

regex * signifie que l’on repète regex un nombre entier de
fois.

Formellement :

regex ω = regex ∞

regex * = ∪∀ i≥0, regex i = regex 0 + regex 1 + regex 2 + …

Intuitivement, une expression ω-régulière est une expression

régulière qui se termine par une répétition infinie.
 Expressions ω-régulières
Exemples

✔
(a+b)*.(b)ω ✗
(a+b)ω.(b)*

✔
(a)ω + (b)ω ✗
(a)ω.(b)ω

✔
a.(b)*.(ab)ω ✗
a.(b)* + (ab)ω

sont des ω-regex ne sont pas des ω-regex

 Expressions ω-régulières
Exemples
Exemple du ressort :

M: 1 2 3

∅ {e} {e,b}

L’alphabet du langage de M est composé de toutes les

étiquettes des états de M

L(M) = ((∅.{e}).(∅.{e})*({e,b})ω )+ (∅.{e})ω

 Expressions ω-régulières
Application au Model checking

Rappel : M ⊨ Φ est équivalent à L(M) ⊆ L(Φ)

M: 1 2 Φ:Fp
∅ {p}

L(M) = L(Φ) =
 Expressions ω-régulières
Application au Model checking

Rappel : M ⊨ Φ est équivalent à L(M) ⊆ L(Φ)

M: 1 2 Φ:Fp
∅ {p}

L(M) = ∅.(∅ *).({p}ω) + (∅ ω) L(Φ) = (∅ )*.{p}.({p} +∅ )ω

 Expressions ω-régulières
●
En général, sur un ensemble de proposition atomiques
AP, on peut généraliser le langage de Φ : F p avec L(Φ) =
(2AP ∩ ¬p)*.(2AP ∩ p).(2AP)ω

●
Pour simplifier la notation, on écrira Σ = 2AP, et Σp = 2AP ∩ p,
c’est à dire toutes les lettres de Σ telles que p est vraie.
●
Ainsi, on peux noter L(Φ) = (Σ¬p)*.Σp.(Σ)ω

●
On généralise cette notation à une formule booléene B :
ΣB = 2AP ∩ B
Par exemple Σ(p∧¬q)∨(¬p∧q) = 2AP ∩ (p∧¬q)∨(¬p∧q) = toutes
les lettres de Σ telles que soit p soit q sont vraies, mais
pas en même temps.
 Expressions ω-régulières
Exercice
G (¬ p)

pUq

GFp

F G (p∧¬q)

pRq
 Expressions ω-régulières
Exercice
G (¬ p)
➢
(Σ¬p)ω

pUq
➢
(Σp)*.Σq.(Σ)ω

GFp
➢
( (Σ¬p)*.Σp )ω

F G (p∧¬q)
➢
(Σ)*.(Σp∧¬q)ω

pRq
➢
(Σq)ω + (Σq)*.Σp∧q.(Σ)ω
 Expressions ω-régulières
Application au Model checking

Rappel : M ⊨ Φ est équivalent à L(M) ⊆ L(Φ)

M: 1 2 Φ:Fp
∅ {p}

L(M) = (∅ *).({p}ω) + (∅ ω) L(Φ) = (Σ¬p)*.Σp.(Σ)ω

Comment tester l’inclusion L(M) ⊆ L(Φ) ?

 Automates de Büchi
Comment tester l’inclusion L(M) ⊆ L(Φ) ?

Soit A et B deux ensembles, l’inclusion A ⊆ B est vraie ssi

l’intersection entre A et le complément de B est vide.
(A ∩ Bc = ∅)


Donc on a L(M) ⊆ L(Φ) ≡ L(M) ∩ (L(Φ))c = ∅

Or, (L(Φ))c = L(¬Φ)

Ainsi, M ⊨ Φ ≡ L(M) ⊆ L(Φ) ≡ L(M) ∩ L(¬Φ) = ∅
 Automates de Büchi
Comment tester l’inclusion L(M) ⊆ L(Φ) ?

Soit A et B deux ensembles, l’inclusion A ⊆ B est vraie ssi

l’intersection entre A et le complément de B est vide.
(A ∩ Bc = ∅)


Donc on a L(M) ⊆ L(Φ) ≡ L(M) ∩ (L(Φ))c = ∅

Or, (L(Φ))c = L(¬Φ)

Ainsi, M ⊨ Φ ≡ L(M) ⊆ L(Φ) ≡ L(M) ∩ L(¬Φ) = ∅

Pour construire cette intersection et vérifier si elle est

vide, on utilisera les automates qui reconnaissent les
langages ω-réguliers : les automates de Büchi
 Automates de Büchi
Syntaxe
Un automate de Büchi est noté A=(Σ,Q,q0,F,Δ) où
●
Σ est un ensemble de fini de symboles
●
Q est l’ensemble fini des états
●
q0 ∈ Q est l’état initial
●
F ⊆ Q est l’ensemble des états acceptants
●
Δ ⊆ Q × Σ × Q est l’ensemble fini des transitions

Syntaxiquement identiques aux automates finis, mais les états finaux

sont remplacés par des états acceptants.
 Automates de Büchi
Sémantique

●
Soit un alphabet Σ, on appelle mot une séquence
infinie des symboles de Σ.
●
Soit A=(Σ,Q,q0,F,Δ), un mot w=a1, a2, a3, … est
reconnu par A ssi il existe est une séquence infinie
d’états s1, s2, s3, … telle que
●
s1 = q 0
●
∀ i, (si,ai,si+1) ∈ Δ
●
∃ q ∈ F | sj = q pour un nombre infini de j
(c’est à dire que q est présent infiniement souvent)

●
On note L(A) le langage des mots reconnus par A. On
dit que A reconnait L(A).
 Automates de Büchi
Exemples
a,b b
✔
(a+b)*.(b)ω b

b
✔
(a)ω + (b)ω
a

b
a a b
✔
a.(b)*.(ab)
ω
a
 Automates de Büchi
Exemples
Exemple du ressort :

M: 1 2 3

∅ {e} {e,b}

L(M) = ((∅.{e}).(∅.{e})*({e,b})ω )+ (∅.{e})ω

Un automate de Büchi reconnaissant L(M) :

{e,b}
{e} {e}
∅
 Automates de Büchi
Exercice
G (¬ p)
➢
(Σ¬p)ω

pUq
➢
(Σp)*.Σq.(Σ)ω

GFp
➢
( (Σ¬p)*.Σp )ω

F G (p∧¬q)
➢
(Σ)*.(Σp∧¬q)ω

pRq
➢
(Σq)ω + (Σq)*.Σp∧q.(Σ)ω
 Automates de Büchi généralisés

●
Les automates de Büchi généralisés (GBA) sont
une généralisation syntaxique des automates de
Büchi qui permet d’exprimer les états acceptants non
pas dans un ensemble F, mais dans un ensemble
d’ensemble d’états {F1,F2,…,Fn}
●
Dans un GBA, un mot est reconu ssi il existe une
exécution correspondante telle qu’au moins un état
de chaque ensemble est présent infiniment souvent.
●
Un GBA est strictement aussi expressif qu’un
automate de Büchi : tout langage reconnu par l’un
peut l’être par l’autre.
 Automates de Büchi généralisés
Syntaxe

Un GBA est noté A=(Σ,Q,q0,F,Δ) où

●
Σ est un ensemble de fini de symboles
●
Q est l’ensemble fini des états
●
q0 ∈ Q est l’état initial
●
F = {F1,F2,…,Fn} ⊆ 2Q est l’ensemble des ensembles
d’états acceptants
●
Δ ⊆ Q × Σ × Q est l’ensemble fini des transitions

1) Tout automate de Büchi est un GBA à un seul

ensemble acceptant.

2) Soit un GBA A, il existe un automate de Büchi A’ tel

que L(A)=L(A’) et réciproquement.
 Automates de Büchi généralisés
Exemple

GF p ∧ GF q Σp Σ
Σ Σq
 Automates de Büchi généralisés
Intersection de GBAs
●
Soit deux GBA A1=(Σ, Q1, q01, F1 , Δ1) et A2=(Σ, Q2, q02,
F2, Δ2)

●
A1 ∩ A2 = (Σ, Q1 × Q2, (q01,q02), F , Δ) tel que
●
(q1,q2),a,(q1’,q2’) ∈ Δ ssi (q1,a,q1’) ∈ Δ1 et
(q2,a,q2’) ∈ Δ2
●
∀ f ∈ F1, f × Q2 ∈ F et ∀ f ∈ F2, Q1 × f ∈ F
●
L(A1 ∩ A2) = L(A1) ∩ L(A2)
 Automates de Büchi généralisés
Exemples (intersection)
b
a,b b
b 3
A1 : b A2 : 2
0 1
a 4

A1 ∩ A2 :
 Automates de Büchi généralisés
Exemples (intersection)
b
a,b b
b 3
A1 : b A2 : 2
0 1
a 4
a a
b a
b
0,2 0,3 0,4
A1 ∩ A2 : b
b
1,2 1,3 1,4
b
b
Pourquoi ne pas choisir F = F1 ∩ F2 ?
 Automates de Büchi généralisés
Exemples (intersection)

b b
A1 : 0 1 A2 : 2 3
a a

0,2 0,3
b
A1 ∩ A2 : a
1,2 1,3
 Automates de Büchi
Application au Model checking
M ⊨ Φ ≡ L(M) ⊆ L(Φ) ≡ L(M) ∩ L(¬Φ) = ∅

Φ:Fp
M: 1 2

∅ {p}
 Automates de Büchi
Application au Model checking
M ⊨ Φ ≡ L(M) ⊆ L(Φ) ≡ L(M) ∩ L(¬Φ) = ∅

Φ:Fp
M: 1 2

∅ {p} ¬Φ : ¬(F p) ≡ G ¬p
 Automates de Büchi
Application au Model checking
M ⊨ Φ ≡ L(M) ⊆ L(Φ) ≡ L(M) ∩ L(¬Φ) = ∅

Φ:Fp
M: 1 2

∅ {p} ¬Φ : ¬(F p) ≡ G ¬p

L(M) = (∅ *).({p}ω) + (∅ ω) L(¬Φ) = (Σ¬p)ω

 Automates de Büchi
Application au Model checking
M ⊨ Φ ≡ L(M) ⊆ L(Φ) ≡ L(M) ∩ L(¬Φ) = ∅

Φ:Fp
M: 1 2

∅ {p} ¬Φ : ¬(F p) ≡ G ¬p

L(M) = (∅ *).({p}ω) + (∅ ω) L(¬Φ) = (Σ¬p)ω

∅ p Σ¬p

∅ 2
0 1
 Automates de Büchi
Application au Model checking
M ⊨ Φ ≡ L(M) ⊆ L(Φ) ≡ L(M) ∩ L(¬Φ) = ∅

∅ p Σ¬p

L(M) ∅ L(Φ) 2
0 1

L(M) ∩ L(¬Φ) 0,2 ∅ 1,2

Cet automate reconnait au moins un mot, l’intersection n’est donc

pas vide ⇒ M ⊭ Φ. Tout mot de L(M) ∩ L(¬Φ) est un contre-
exemple prouvant l’insatisfiabilité de Φ sur M.