Modélisation : modèle mathématique d’un système de manière formelle.

• Il faut vérifier une exclusion mutuelle quand on veut accéder à la section critique. (Nécessite)

• Absence de famine : raisonnement sur le futur, le programme peut accéder à la section critique (possibilité)

• Temporalité

• Ordre d’événements
  \RA Logiques temporelles

Dans ce cours, on verra LTL et CTL. (sans le passé).

LTL

Linear-time Temporal Logic

Propriétés évaluées sur des traces d’exécution infinies.

Syntaxe

\varphi, \Psi == P | \neg \varphi | \varphi \wedge \Psi | \varphi \vee \Psi | X \varphi | F \varphi | G \varphi | \varphi\ U\ \Psi

• X : next
• F : eventually (soit maintenant, soit dans le futur)
• G : globally (toujours)
• U : until (jusqu’à)

Sémantique

Interprétation sur des traces infinies (\omega word)
Soit S = <Q, q_{0}, \text{Act}, \ra, AP, \mathcal{L}> un STE.
Une trace infinie de S à partir d’un état s_{1} \in Q est de la forme
\rho = s_{0}, s_{1}, s_{2}... t_{q} s_{i} \xrightarrow{? \in \text{Act}} S_{i+1} pour tout i.

Notations : \rho(i) = S_{i}, \rho^{i} = S_{i}, S_{i+1}, \dots \rho_{i} = \dots, S_{i-1}, S_{i}
\text{Exeq}(q) toutes les traces infinies commençant à l’état q.

La sémantique est positionnelle.

• \rho_{i} \vDash P ssi \begin{aligned}\rho(i) \vDash P(?) \\\\ P \in \mathcal{L}(\rho)\end{aligned} (Rho i satisfait P si et seulement si l’état de départ satisfait P)
• \rho_{i} \vDash \neg \varphi ssi \rho_{i} \forall \varphi
• \rho_{i} \vDash \varphi \wedge \Psi ssi \rho_{i} \vDash \varphi et \rho_{i} \vDash \Psi
• \rho_{i} \vDash \varphi \vee \Psi ssi \rho_{i} \vDash \varphi ou \rho_{i} \vDash \Psi
• \rho_{i} \vDash X \varphi ssi \rho_{i+1} \vDash \varphi
  • 
• \rho_{i} \vDash F \varphi ssi \exists j \geqslant i : \rho_{ij} \vDash \varphi
  • 
• \rho_{i} \vDash G \varphi ssi \forall j \geqslant i : \rho_{ij} \vDash \varphi
  • 
• \rho_{i} \vDash \varphi\ U\ \Psi ssi \exists j \geqslant i : \rho_{ij} \vDash \varphi et \forall k \leqslant i \leqslant j : \rho_{k} \vDash \varphi
  • 

Syntaxe minimale

\varphi, \Psi == P | \neg \varphi | \varphi \wedge \Psi | X \varphi | \varphi\ U\ \Psi
F\varphi = T\ U\ \varphi
G\varphi = \neg F \neg \varphi

Remarques

1. On insiste sur les traces infinies

Exemple

\Psi = \neg X \varphi \Psi = X \neg \varphi
Traces infinies \Psi \Leftrightarrow \Psi'
Traces finies \Psi' \RA \Psi

2. S \vDash^{?} \varphi : Quand est-ce que S satisfait \varphi ?
   ssi \forall \rho \in \text{Exeq}(q_{0}) : \rho, 0 \vDash \varphi

Exemple

On reprend l’exemple du Buffer à la fin du cours précédent.
B \vDash v_{1} \wedge v_{2} B \nvDash G(v_{1} \wedge v_{2})
B \vDash P_{1} \RA v_{2} B \nvDash G(P_{1} \RA v_{2})

3. G\varphi formule de sûreté (safety, good things always happen, bad thing never happen)
   G(\neg\text{bug})
   F \varphi formule de liveness (a good thing eventually happen)

Exercice

Quelle est la relation entre ces trois propriétés ?

• \Psi_{1} = F(P \wedge P')
• \Psi_{2} = F P \wedge F P'
• \Psi_{3} = F(P \wedge F P')
  Il y a-t-il une équivalence ? Non aucune.
  
  \rho_{i} \vDash \Psi_{2} et \rho_{i} \vDash \Psi_{3} mais \rho_{i} \nvDash \Psi_{1}

\rho_{i} \vDash \Psi_{2} mais \rho_{i} \nvDash \Psi_{1} et \rho_{i} \nvDash \Psi_{3}

\rho_{i} \vDash \Psi_{1}, \rho_{i} \vDash \Psi_{2}, \rho_{i} \nvDash \Psi_{3}

Exercice

Vous atterrissez sur une planète N où : s’il pleut un jour, alors il pleuvra le lendemain.
Situation : il pleut
Que peut-on conclure ?

1. Il pleut tous les jours sur la planète N.
2. Il pleuvra demain sur la planète N.
3. Il a plu hier sur la planète N.
4. Il pleuvra tous les jours sur la planète N.

P proposition démontrant “il pleut sur la planète N” : (i le jour d’arrivée)
N \vDash G(P \vDash XP), N_{i} \vDash P

1. \varphi \wedge \Psi \RA GP donc faux
2. \varphi \wedge \Psi \RA (N_{i+1} \vDash P) donc vrai
3. \varphi \wedge \Psi \nRightarrow (N_{i+1} \vDash P) donc faux
4. \varphi \wedge \Psi \RA (N_{i} \vDash GP) donc vrai

Globally c’est sur la propriété, pas sur la trace