ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

lA retenir sur la Logique:

C’est quoi la logique, les éléments, la syntaxe et la sémantique de la logique;

Les différents types: Propositionnels, prédicats et la logique temporelle (LT),

Pourquoi on a besoin de la logique temporelle

1. Definition
La logique est un ensemble de mots fini ou infinis formés à partir d’un ensemble fini
d’alphabet. Autrement dit la logique est un langage pour la spécification et la représentation
des connaissances. On distingue différents classes de logique.
2. Les différentes classes de la logique

a. Logique des Propositions

Mots de base ; les mots de base sont des variables propositionnelle (ensemble de formules
atomiques) V={Q, P, R, …}, d’un ensemble de connecteurs {∨, ∧, ¬, ⇒, ⇔}et aussi d’une
parenthèse ouvrante et d’une parenthèse fermante {(,)}

L’operateur unaire
1. La négation, ¬
Exemple:
‘Pierre n’est pas content.’
p : Pierre est content

L’operateur binaire

2. La conjonction, ∧
Exemple: ‘Pierre est content et Marie est triste.’
p : Pierre est content
q : Marie est triste

3. La disjonction, ∨
Exemple:
‘il va pleuvoir ou il va neiger’
p : il va pleuvoir
q : il va neige

4. Le conditionnel, →
Exemple: ‘Si Pierre est content alors Marie est triste.’
p : Pierre est content
q : Marie est triste

Syntaxe: règles pour former les formules appartenant à la logique des propositions (LP),

1
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

P est une variable propositionnelle

La formule suivante (P∧Q) appartient à la logique des propositions LP

Exemple : Les expressions suivantes sont-elles des formules ?

p oui c’est une formule

pq non
(p ∨ q) oui
(p ∨ q non
¬p oui
(¬p) non
¬((p → q) ∨ (p ∧ r )) oui
¬(p¬q) non
Exercice1 corrigé : En notant M et C les affirmations suivantes :
M = « Jean est fort en Maths »,
C = « Jean est fort en Chimie »,
Représenter les affirmations qui suivent sous forme symbolique, à l’aide des lettres M et C et
des connecteurs usuels.
1. « Jean est fort en Maths mais faible en Chimie »
2. « Jean n’est fort ni en Maths ni en Chimie »
3. « Jean est fort en Maths ou il est à la fois fort en Chimie et faible en Maths »
4. « Jean est fort en Maths s’il est fort en Chimie »
5. « Jean est fort en Chimie et en Maths ou il est fort en Chimie et faible en Maths »

Réponses :
1.M ∧(￢C) ;

2. (￢M)∧(￢C) ;

3.M ∨(￢M ∧C) ;

4. C ⇒ M ;

5. (M ∧C)∨(￢M ∧C).

Exercice 2 corrigé : Construire les tables de vérité des formules propositionnelles suivantes :
1. (￢p) ∧ q
2. (￢p) ⇒ (p ∨ q)
3. ￢ ((￢p) ∧ (￢q))

2
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

4. (p ∧ q) ⇒ (￢q)
5. (p ⇒ q) ∨ (q ⇒ p)
6. (p ⇒ (￢q)) ∨ (q ⇒ (￢p))
7. (p ∨ (￢q)) ∧ ((￢p) ∨ q)
8. p ⇒ ((￢p) ⇒ p)

Réponse :

p q 1 2 3 4 5 6 7 8
F F F F F V V V V V
F V V V V V V V F V
V F F V V V V V F V
V V F V V F V F V V

Revoir la logique des propositions et la logique des prédicats ;;;;;;;;;

La Logique Temporelle (LT)

Introduction à la Logique Temporelle (LT)
➢ Pourquoi on fait appel à la logique temporelle?
Réponse : On a besoin de la logique temporelle pour la spécification des systèmes, ou
bien tout simplement pour exprimer et spécifier les propriétés d’un système au cours
du temps.
➢ Pourquoi on n’utilise pas la logique classique (propositionnelle et de prédicats)?
Réponse : parce-que les deux logiques sont insuffisantes pour spécifier les propriétés
d’un système au cours du temps. On les utilise juste pour exprimer et spécifier des
propriétés d’un système à l’instant donné
Par exemple : Soit un feu de circulation de trois variables propositionnelles R, O et V
suivant (R : Rouge, O : Orange et V : Vert)

1. 2. 3. 4.

3
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

Exprimer les propriétés de ce feu en utilisant la logique des propositions.

Oui c’est faisable d’exprimer la situation de chaque événement à l’instant donné (ca veut dire
une situation instantanée).
✓ ¬R ∧ ¬V ∧ O 2. R ∧V ∧ O 3. ¬R ∧V ∧¬ O 4. ¬V∧R∧¬ O
Remarque: on peut exprimer une situation instantanée par une expression
propositionnelle en basant sur les connecteurs classiques (∧¬ ⇔ ∨……. ) et les variables
des propositions (proposition atomique).

Comment dire que précède ? Comment dire que le système ne reste pas

toujours sur ? alors on a besoin de faire apparaître le temps

Dans ce chapitre, on s’interesse à la logique temporelle pour exprimer les proprieties d’un
systeme (systeme réactif). Les proprieties sont des contraintes ou des éxigences qui
imposent le systéme, elles sont verifiées sur un modéle (les automates de Buchi,
structure de kripke, des reseaus de petri……..etc) d’une maniére synchrone.

1. La logique temporelle est une extension de la logique des propositions. Elle est utilisée
pour décrire des propriétés, c’est donc un langage de description.
2. Ce type de logique a besoin de la logique classique+Opérateur dédiés au temps
(Opérateurs temporels) pour évaluer et étudier le comportement d’un système au
cours du temps.
3. Les opérateurs temporels permettent d'exprimer l'évolution d'un système au cours du
temps, tels que : toujours, jusqu'à, un jour, . . . . ..Ces operateurs associent une valeur
de vérité non pas à un état, mais à une séquence d'états, représentant l'évolution d'un
système au cours du temps. On distingue deux types d’opérateurs temporels :
❖ Les connecteurs temporels sont :
✓ X : Next (suivant)
✓ F : Futur (un jour)
✓ G: Globaly (toujours)
✓ U : Until (jusqu’à)
❖ Les quantificateurs de chemins sont:
✓ A : tous les chemins
✓ E : exsistentiel

4
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

Le langage de la logique temporelle: l’alphabet se compose de :

➢ propositions atomiques : les propositions atomiques sont écrites en logique des
propositions, elles sont utilisées pour caractériser les états.
➢ Les opérateurs logiques
Grace aux propositions atomiques on écrit les propriétés d’un système en logique temporelle
en basant sur les operateurs du temps.

On distingue deux approches de la logique temporelle (LT) : Logiques temporelles

linéaires(LTL) ou arborescentes (CTL):
• Temps linéaire : propriétés des séquences d’exécutions (futur déterminé) •
• Temps arborescent : propriétés de l’arbre d’exécutions (tous les futurs possibles)

I. La logique temporelle linéaire (Linear Temporel Logic :LTL)

1. Combinateurs temporels (Combinateurs sur une exécution ou un seul chemin):

En parlant de la logique temporelle linéaire propositionnelle LTLP (PLTL)

❖ Temps est linéaire

❖ Logique propositionnelle + opérateurs temporels
Soit P une proposition atomique, on écrit :

Next (Suivant): ⃝ p = Xp signifié que l’état suivant vérifie la propriété P.

Finally (inévitablement p): ⃟ p= Fp énonce qu’un état futur vérifie P (présent ou

futur).

Globally (Toujours p): ⃞p=GP signifié que tous les états futurs vérifient P.
Autrement dit : « il y aura toujours P» ou «P sera toujours vraie ».

5
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

Soient deux propositions atomiques p et q

Until (jusqu’à): PUq Signifie que : «P est vraie jusqu’à ce que q le soit ». C’est-à-dire
q sera vrai un jour, en attendant P restera vraie.

La dualité entre les combinateurs G et F

▪ GFP se lit : « toujours, il y aura un jour un état, tel que P sera vraie un nombre infini
de fois le long de l’exécution considérée». On dit : «P sera vraie infiniment souvent»

▪ FGP se lit : « à partir d’un certain moment, P sera toujours vraie ».

Dans cette partie du chapitre nous voyons comment créer des formules LTL à une
execution quelconque. La trace d’une execution va étre un chemin infini composé
d’ensembles de propositions atomiques (c’est à dire de construire la syntaxe de LTL).
On dit qu’une propriété quelconque est une formule de LTL si la trace (mot infini) d’une
execution satisfait cette formule.

L’emboitement de F et G est très fréquemment utilisé pour exprimer des propriétés de

répétition.

Syntaxiquement:
ɸ:=true|pi| p1∧p2|¬ p1 |Xp | p1U p2|Fp |Gp | …

En commencant par:

1. True: le mot true est toujours une formule de LTL (chaque execution satisfait
True), aussi vrai par tout. En d’autres termes chaque mot infini sur l’ensemble de
puissance des propositions atomiques satisfait True
2. Proposition: une proposition pi est une formule de LTL si pi présente dans la 1er
lettre du mot infini considéré tel que piЄAP ( la formule pi est vérifiée à la position
initial de la trace).
3. la formule P1∧ p2
p1∧p2 est dit une formule de chemin de LTL si p1 et p2 présente dans la 1er lettre du
mot considéré (l’état courant).

6
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

Exemple : Exécution d’un mot infini

Deux propositions atomiques AP={P1, p2} (p1 et p2 sont des formules de LTL)

Dans cette trace p1 est une formule de LTL car la 1er lettre du mot contient p1 alors ce mot
entier est dit satifaire p1.

Dans cette trace p2 est également une formule de LTL car la 1er lettre du mot contient p2
alors ce mot entier est dit satifaire p2.

Dans cette trace p1∧p2 est une formule de LTL car la 1er lettre du mot contient p1 et p2 alors
ce mot entier est dit satifaire p1∧p2 ca veut dire la formule p1∧p2 est vrai le long de chemin
infini ou d’une execution.

X (p1∧p2) est satisfaite par cette trace car l’état suivant contient p1 et p2
On a p1∧ p2 est une formule de LTL alors X (p1 ∧p2) est aussi une formule de LTL.
XXXp2 est vraie car p2 présente dans l’état 4 d’une trace d’exécution.

Ce X est un chemin de sauter à l’interiéur d’une trace pendant l’étape l’exécution si on ecrit
une seule fois X, cela nous permet de sauter une seule fois(l’état prochain de l’état
courant). Pour aller plus loin en utilisant plusieurs fois l’opérateur X ou l’opérateur U.

Qaund on parle de LTL, on travaille sur un alphabet fini ∑= 2AP, la formule LTL est
construite en utilisant par exp: AP={P1, p2}
Avec ∑={{}, {P1}, {p2}, {P1, p2}} on aura quatre combinaisons.

❖ Les lettres de ∑ comme formules atomiques: p1 est une formule de LTL de

base
❖ Les operateurs booléens classiques {∨, ∧, ¬, ⇒, ⇔}: (p1∨p2) ∧ ¬ p2 est
une formule de LTL.
❖ Les operateurs temporels unaires sont: X, F, G: (X p1 ∨ p2) ∧ X¬X p2 est
une formule de LTL(un operateur temporel unaire est celui qui prend un
seul argument comme la negation).

❖ Les operateurs temporels binaires comme: U: (Xp1∨p1) U p1 est une

formule de LTL.

7
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

Ordre de priorité
X comme la negation (revoir les régles de priorité classique)
U comme la conjonction, la disjonction,le conditionnel…………, on est obligé de
parenthèsé ce qui n’est pas priorité.

2. La syntaxe et la sémantique de la logique PLTL

Definition: La logique temporelle linéare (linear Temporel Logic: LTL). Quelle que soit la
logique utilisée: la syntaxe correspond aux règles utilisées pour écrire des formules
correctes et la sémantique donne la signification de formules bien formée. La sémantique
est utilisée pour décider si une formule bien formée est vrai ou non sur un système donné.

La syntaxe de LTL
Les propositions atomiques sont des formules LTLP
:
➢ true et false;
➢ une variable propositionnelle p; .
➢ Des formules complexes sont construites avec les connecteurs de la logique
propositionnelle et des connecteurs temporels;
o Connecteurs propositionnels : ¬p, p ∧ q, p∨ q, p ⇒ q, p⇔ q

o Connecteurs temporels: p1 Uq, G p, F p, X p

Sémantique de LTL(traces)
La définition de la satisfaction d’une formule PLTL ϕ dans un modèle donné σ: s0, s1, s2, ….
est basée sur la validité d’une proposition p à la position i de la séquence σ, i≥ 0 qu’on note par
: (σ, i) |= p.
Une formule de LTL s’interprète sur une position i d’une exécution infinie partant de l’´etat
Courant: σ : s0 → s1 → s2 …….. Pour i ≥ 0, on note σ(i) le ieme état de σ (donc ici si). La
sémantique de LTL est alors définie comme montré ci-dessous. σ est un mot infini sur
l'alphabet 2Ap.

σ |= T comme cité précédemment le mot true est toujours une formule de LTL et tjrs vrai
σ, i |= P ssi P est dans l’ensemble des propositions et p présente dans l’état courant (p ∈ σ (0))
σ, i |= ￢ϕ ssi il n’est pas vrai que σ, i|= ϕ (σ |= ¬p si pas σ |= p)
σ, i |= ϕ1∧ ϕ2 ssi σ, i |= ϕ1 et σ, i |= ϕ2
σ, i |= ϕ1 ∨ ϕ2 ssi σ, i |= ϕ1 ou σ, i |= ϕ2
σ, i |= Xϕ ssi σ, i + 1 |= ϕ1 et i< |σ|
σ, i |= Fϕ ssi il existe j≥i tel que ( σ, j) |= ϕ
σ, i |= Gϕ ssi pour tout j≥i , tel que ( σ, j) |= ϕ
σ, i |= ϕ1U ϕ2 ssi il existe j tel que i≤ j ≤ |σ| et σ, j |=ϕ2 et pour tout k tel que, i ≤ k < j on a σ,
k |= ϕ1.

Interprétation sur une séquence d’états σ = σ0σ1σ2, …

8
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

I 0 1 2 3 4 5 6
x 1 3 2 4 3 5 4
x>3 F F F T F T T
G( x>3) F F F F F T T

I 0 1 2 3 4 5 6
x 1 2 3 4 5 6 7
X=4 F F F T F F F
F( x=4) T T T T F F F

3. Quelques equivalences en LTL

Soient deux propositions atomiques p1 et p2:
1) Gp1⇔¬F ¬p1
2) ¬Gp1⇔F ¬p1
3) ¬Fp1⇔G ¬p1
4) Fp1⇔¬G ¬p1
5) F(p1∨ p2) ⇔ (Fp1)∨ (Fp2)
6) G(p1∧p2) ⇔ (Gp1) ∧ (Gp2)
7) FG(p1∧p2) ⇔(FGp1) ∧ (FGp2)
8) GF(p1∨ p2) ⇔(GFp1)∨ (GFp2)
9) p1U (p2∨ p3) ⇔( p1U p2)∨ (p1U p3)
10) (p1∧ p2)U p3 ⇔( p1U p3)∨ (p2U p3)

Notes: Quelle que soit la logique utilisée:

1. La syntaxe correspond aux règles utilisées pour écrire des formules bien formées.
2. La sémantique donne la signification de formules bien formée.
3. La sémantique est utilisée pour décider si une formule bien formée est vrai ou non
sur un système.
4. Les formules de LTL sont toutes des formules de chemin

II. La logique temporelle arborescente (Computation Tres Logic :CTL)

1. Quantification sur l’ensemble des exécutions ou sur plusieurs chemins):

En parlant de la logique temporelle arborescente CTL.

A partir d’un état, plusieurs futurs sont possibles. Cela donne une arborescence des
comportements. Dans ce cas, la logique temporelle introduit : les quantificateurs de chemins
A et E qui permettent une quantification sur toutes les exécutions.

9
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

-AP : énonce que toutes les exécutions partant de l’état courant satisfont P ou bien tous les
chemins futurs vérifient la propriété. (∀p: pour tous les chemins,p est vérifiée).

- E P: énonce qu’il existe au moins une exécution partant de l’état courant, qui satisfait P
ou bien certain chemins futurs vérifient la propriété (∃p : il existe un chemin pour lequel
p est vérifiée) On passe d’une vue chemin par chemin (LTL) à une vue arborescente.

Attention de ne pas confondre AP avec G P

A P : signifie que toutes les exécutions possibles maintenant, satisfont P.

G P : signifie qu’à tout instant de l’exécution considérée, P est vérifiée.

11
L’équivalence entre A et E:

• A P⩧¬ E ¬ P
• E P ⩧¬ A ¬ P

L’équivalence entre F et G

• Fp⩧trueUp
• Gp⩧¬ trueU¬ p

[Link] combinaison entre A, E, G et F

❖ Transformations directe:

AGp: énonce que p est toujours vraie on a AGp=¬EF¬p

AFp: énonce qu’on aura p, quelque soit l’exécution retenue on a AFp= ¬ E¬ Fp
EGp: énonce qu’il existe une éxecution le long de laquelle p est toujours vraie on a
EGp=E¬ F¬p.
EFp: énonce qu’il est possible d’avoir p suivant une des exécutions.

Transformations indirecte (par équivalence):

EGp=¬(A true Up) il existe une exécution ou p est toujours vraie

EFp= E trueUp il existe au moins un p vraie dans le futur
AGp=¬(E trueU¬p) dans toutes exécutions p est toujours vraie.
AFp=A true Up dans toutes exécutions p est vraie dans le futur
En ulistrant ces formules avec des arbres d’exécutions…..

10
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

.2. La combinaison entre A, E, X et U

EXred:
AX(red):
AredUblue:
EredUblue:
En ulistrant ces formules avec des arbres d’exécutions…..

2. La syntaxe et la sémantique de la logique CTL

Deux formules pour CTL*: La logique temporelle arborescente star CTL* regroupe les
deux types de logiques CTL et LTL. Cette logique dispose de formule d’état et de formule
de chemin. Les formules étatiques sont formées par un ensemble de régles True, ɸ1 ∧ ɸ2
|¬ ɸ1 ….……
Formule d’état

ɸ:=True|pi| ɸ1∧ɸ2|¬ ɸ1 | ɸ1U ɸ2|A|E

avec pi ∈ AP , ɸ1 et ɸ2 sont des formules d’état et  formule de chemin. Signification de la

syntaxe de formules d’état

➢ Chaque état satisfait True

➢ Un état satisfait pi si cet état est etiqueté par pi
➢ Un état satisfait ɸ1∧ɸ2 si cet état est etiqueté par ɸ1et ɸ2
➢ Un état satisfait NON ɸ1 si cet état ne satisfait ɸ1

11
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

➢ Un état satisfait E s’il existe un chemin commence par cet état satisfait la formule

➢ Un état satisfait A si tout les chemins commence par cet état satisfait la formule 
Formule de chemin

:=ɸ| 1∧2|¬ 1| 1U 2|F1|G1|X1

ɸ cette formule d’état peut etre considérée comme formule de chemin si l’état courant
satisfait ɸ.
1 et 2 sont des formules de chemin donc 1∧2 est aussi formule de chemin, le NON
d’une formule de chemin est une formule de chemin.
Ici X d’une formule de chemin, G, F et until sont des formules de chemin.

Maintenant: Comment éliminer certaines reglés de la syntaxe de CTL* pour obtenir un

sous ensemble restreint de CTL. Les formules obtenues pour CTL auront aussi un
algorithme de model checking efficace.

Passage de CTL* vers CTL

o La syntaxe de CTL
Toute proposition atomique est une formule CTL
Si P1 et P2 sont des formules CTL alors ┐P1, P1∧P2, AXp1, EXp1, A(p1Up2), E(p1U p2) sont des
formules CTL
Les éléments suivants sont des formules atomiques de la CTL:
➢ true et false;
➢ une variable propositionnelle;
➢ Des formules complexes sont construites avec les connecteurs de la logique
propositionnelle et des connecteurs temporels.

• connecteurs propositionnels : ¬p, p ∧ q, p ∨ q, p ⇒ q, p ⇔ q,

•connecteurs temporels : tous les chemins : A(p U q), AGp, AFp, AXp
• connecteurs temporels : existe un chemin : E(p U q), EGp, EFp, EX p on les appels la
forme normale existentielle de CTL (seront détailés par la suite dans le chapitreIV).
a. Formule d’état
ɸ:=true|pi| ɸ1∧ɸ2|¬ ɸ1 | ɸ1U ɸ2|A|E
avec pi ∈ AP et aussi une formule d’état, ɸ1 et ɸ2 sont des formules d’état et  formule de
chemin

b. Formule de chemin
Ici on a remplacé la formule de chemin  par la formule d’état ɸ et éliminer les trois
1ere régles de CTL*
12
ChapitreIII: Formalisme pour la spécification des propriétés d’un système 2024/2025

:= ….partie à supprimer…………ɸ1Uɸ 2|Fɸ1|G ɸ1|X ɸ1

❖ Quelques Formules qu’on peut ou non exprimer par les régles de CTL:

Formule de CTL Formule de non CTL

1. p AFGp1
2. EFp1 Ap1
3. EFAGP1 EGFp1
4. AXp1 A(Fp1∧Gp2)
5. AFp1 ∧AGp2 A(p1U(Gp2))
6. A(p1U(EGp2))

Rq:
➢ L’intersection entre LTL et CTL est non vide
➢ Toute formule de LTL et CTL peut-etre s’exprimer par les régles de CTL*
➢ CTL* combine les avantages de CTL et de LTL, et est donc plus expressif, mais
aussi plus complexe.

13