CTL vs LTL
Expressivité
EFp
EFp n’est pas exprimable en LTL. (= je peux trouver un chemin qui peut satisfaire p à un certain état) mais sa négation est exprimable : \neg EFp est G\neg p (= quel que soit le chemin, j’ai \neg p).
La négation de G\neg p est Fp qui est plus forte que EFp.
\RA la négation du chemin est différente dans CTL que dans LTL.
AGEFp
AGEFp n’est pas exprimable en LTL. (= pour tout les chemins, pour tout les états, j’ai un chemin à partir duquel je peux faire p) avec (AG = tous les chemins et tous les états)
Exemple
- S \vDash Fp
- S \nvDash AGEFp
donc (AGEFp)_{CTL} \RA (FP)_{CTL} (avec \RA = implique)
FGp (propriété de stabilité)
(pour tous les chemins, je vais trouver un chemin sur lequel p est vrai et restera toujours vrai
Tentative 1 de transformation : AFAGp
Pour tous les chemins, je trouverais un état à partir duquel tous les états satisfont p
S \vDash FGp, en dépliant :
S \nvDash AFAGp
Donc : (AFAGp)_{CTL} \RA (FGp)_{CTL}
Tentative 2 de transformation : AFEGp
S' \vDash AFEGp
S' \nvDash FGp
Donc : (FGp)_{LTL} \RA (AFEGp)_{CTL}
Conclusion
En terme d’expressivité, LTL et CTL sont incomparables !
Pouvoir de distinction
- Propriété LTL : FXp : S_{1} et S_{2} indistinguable, car S_{1}\vDash FXp et S_{2}\vDash FXp
- Propriété CTL : AFAXp (pour tous les chemins, j’ai un état sur lequel tous les successeurs satisfont p): S_{1} et S_{2} deviennent distinguables, parce que S_{1}\vDash AFAXp mais S_{2} \nvDash AFAXp
Théorème
CTL distingue tous systèmes non bisimillaires.
CTL a un pouvoir de distinction plus fort que celui de LTL.
Systèmes différents mais indistinguable par CTL
ils sont bissimilaires
Réseaux de Petri
- Pre(P_{4}, t_{3}) = 1
- Pre(P_{7}, t_{3}) = 0
Définition formelle 1
Syntaxe d’un réseau de Petri
Un réseau de Petri R est un typle R = <P, T, Pre, Post> où :
- P est un ensemble fini de places
- T est un ensemble fini de transitions avec P\cap T = \varnothing
- Pre : P\times T \ra \N
- Post : T \times P \ra \N
Un réseau de Petri marqué est un tuple <R, M> où :
- R est un réseau de Petri
- M : P \ra \N (fonction qui est définie pour toutes les places, qui renvoie un entier) avec comme notation : M\in \N^{|P|} \sim \N^{P}
Sémantique
-
Une transition T est dîte sensibilisée (ou franchissable) ssi : \forall p : M(p) \geq \text{Pre}(p, t)
On écrit alors M[t > -
Le tir (franchissement) d’une transition correspond à l’obtention d’un nouveau marquage M' : \forall p : M'(p) = M(p) - \text{Pre}(p, t) + \text{Post}(t, p)
On note alors M[t > M'
Définition formelle 2
Syntaxe d’un réseau de Petri
R = <P, T> où :
- P est un ensemble fini de places
- T \subset \N^{P} \times \N^{P} est un ensemble fini de transitions
Notation
On note t={}^{\bullet}{}t, t^{\bullet} \in T avec {}^{\bullet}{}t l’incidence arrière et t^{\bullet} l’incidence avant
Sémantique
t\in T
M[t> ssi M \leq {}^{\bullet}{}t (comparaison de vecteurs éléments à éléments)
M[t>M' \RA M' = M-{}^{\bullet}{}t + t^{\bullet}
Graphe de marquages
Soit <R, M> un réseau de Petri marqué et M_{0} son marquage initial.
Le graphe de marquages accessibles depuis M_{0} : \mathcal{A}(R, M_{0}) est donné par l’algorithme suivant :
\mathcal{A}_{0}=\{M_{0}\}
\mathcal{A}_{i}=\{M\in\N^{P}\ |\ \exists M' \in \mathcal{A}_{i-1}\quad \exists t\in T : M'[t>M\}
\mathcal{A}(R, M_{0})= \cup_{i\geq 0}\mathcal{A}_{i}
[0]\xrightarrow{t}[1]\xrightarrow{t}[2]\xrightarrow{t}[3]\xrightarrow{t}\dots
R_{1} est non-borné \RA graphe de marquages infini
Définition
Un réseau de Petri marqué <R, M_{0}> est borné ssi \forall p \in P. p est bornée.
Une place p est bornée : \exists k\in \N \forall M \in \mathcal{A}(R, M_{0}) : M_{p}\leq k
Exercice : Le pont scandinave
Sur Tina (nd pour lancer l’interface graphique)
On a quatre personnes qui veulent traverser un pont
La capacité du pont est de deux personnes.
Les personnes ont une lampe torche.
Il faut une lampe pour traverser le pont.
Il faut y aller à deux et l’un doit revenir avec la torche pour faire passer les suivants.
La personne A traverse en 10 minutes.
La personne B traverse en cinq minutes.
La personne C traverse en deux minutes.
La personne D traverse en une minute.
- Quel est le temps minimal de la traversée ?
Modéliser le temps par des jetons, aka 1 minutes = 1 jeton, 5 minutes = 5 jetons.
C et D traversent : 2 minutes
C revient avec la lampe : 4 minutes
A et B traversent : 14 minutes
D revient avec la lampe : 15 minutes
C et D traversent : 17 minutes