Propriété pour write :
G((\text{written} \wedge X(\neg \text{written})) \RA X(\neg \text{written}\ U\ \text{read}))

Si on a un written suivi d’un written, je ne peux pas encore written s’il n’y a pas un read.

Propriété pour read :

On peut faire deux lectures consécutives

à faire……..

En LTL

Vision d’un système comme l’ensemble des traces infinies à partir de son état initial.

CTL : Computational Tree Logic

Logique incomparable avec LTL, CTL n’est pas meilleur que LTL, juste différent (permet de comparer s’il y a pas de bissimilarité entre deux systèmes)

Syntaxe minimale

\varphi, \Psi ::= P|\neg \varphi|\varphi\wedge\Psi|EX\varphi|AX\varphi|E\varphi U\Psi|A\varphi U\Psi
avec parfois :

• E\varphi U\Psi \equiv \varphi EU \Psi
• A\varphi U\Psi \equiv \varphi AU \Psi

Equivalence LTL/CTL

F\varphi = TU\varphi

• aussi AF\varphi
• aussi EF \varphi
  G\varphi = \neg F \neg \varphi
• aussi AG\varphi
• aussi EG\varphi

Opérateur CTL

QT

• Q : quantificateur sur les chemins
• T : Opérateur Temporel

Sémantique

Rappel x \vDash y = x satisfait y.
Rappel x : y = x tel que y

Système de transitions étiquetées : S = <Q, q_{0}, \text{Act}, \ra, AP, \mathscr{L}>

• Exeq(q) : l’ensemble des exécutions infinies à partir de q \in Q.
• \forall \pi \in Exec(q). \pi=q_{0}q_{1} avec q_{0}=q et (q_{i}, q_{i+1})\ra (aussi écrit (q_{i}\ra q_{i+1})
• \pi(i) = q_{i}

On raisonne sur les états dans Q soit q\in Q.

• q\vDash P ssi P \in \mathscr{L}(q)
• q \vDash \varphi ssi q\nvDash \varphi
• q \vDash \varphi \wedge \Psi ssi q \vDash \varphi et q \vDash \Phi
• q\vDash EX\varphi ssi \exists(q, q') \in \ra : q' \vDash \varphi
• q \vDash AX\varphi ssi \forall(q, q')\in\ra:q'\vdash q
• q\vDash \varphi EU \Psi ssi \exists\pi\in Exec(q), (\exists i \geq 0 : q_{i} \vDash \Psi \wedge \forall j < i : q_{j} \vDash \varphi)
• q\vDash \varphi AU \Psi ssi \forall\pi\in Exec(q), \exists i \geq 0 : (q_{i} \vDash \Psi \wedge \forall 0 \leq j : q_{j} \vDash \varphi
• S\vDash \varphi ssi q_{0}\vDash \varphi

Exemple 1

AG_{P}

En LTL, ça correspond à G_{P}.

EG_{p}
En LTL, il n’y a pas d’équivalent.

EF_{P}

En LTL, cette propriété est inexplicable : c’est la reachability (inatteignable).

Exemple 2

AF_{P}

En LTL, c’est F_{P}

AFEG_{P}

Rappel : U = Until

pAU_{q}

Question du partiel de l’année dernière

QCM

• EGAX_{P} : il existe un chemin maximal tel que tous les successeurs satisfont P
• EFAX_{P} : il existe un chemin tel que j’ai un état qui satisfait tous les successeurs satisfont P
• EGEX_{P} : il existe un successeurs ou tous les successeurs satisfont P
• EX_{P} : Un sucesseur satisfait P

EF : je peux atteindre un état (reachability)

Exemple : Évaluer une formule CTL

\varphi = AG(a \RA ((EX_{c})EUb))

EX_{c} : il existe un chemin quelque soit satisfait c

S\vDash \overbrace{AG(a \RA \Psi)}^\varphi

Exemples de propriétés

• AG\varphi : Safety (G\varphi en LTL)
• AG(\varphi \RA AF\Psi) : Response (G(\varphi\RA F\Psi) en LTL)
• AGEF\varphi : Vivacité forte (Impossible en LTL )