Modalité de contrôle : 1 partiel (sur Moodle) + 1 examen
Documents autorisés
21 novembre le partiel
Second partiel pour le dernier ou avant dernier cours
19/12/2024 examen final à 11 h 45, durée : 1h ; amphi 4C
Pas de seconde session
ancien cours

Plan

2 parties :

• Modélisation : STE (Systèmes réseaux étiquetés), Réseaux de Petri
• Spécification : Logique temporelle

Un système informatique doit répondre à des exigences.

• Comment garantir que le système répond aux exigences ? En faisant des tests
• Comment faire des tests parfaits ? Impossible
  Exemple : Toyota UA (Unattendented Acceleration)

Il faut donc une contrepartie mathématique pour

• Système Informatique
  • $\RA$ modèle mathématiques $M$ (STE, Réseau de Petri, …)
• Exigences
  • $\RA$ Propriétés $\mathcal{P}$ (Logiques)

$\RA$ $\forall P \in \mathcal{P} : M \models P$ “Model Checking” (technique de vérification formelle)

Systèmes de transition étiquetés (STE)

Exemple de l’ascenseur :

Exemple du distributeur de boissons :

$q_{0}$ est vide :
Valeur de vérité de conjonction sur un ensemble vide : $\forall e \in E :$ vrai (toujours vrai)
Valeur de vérité de disjonction sur un ensemble vide : $\exists e \in E :$ faux (toujours faux)

Les STE peuvent être infinis.

• Etats infini
• Branchements finis (nombre de manières de quitter un état)

Par exemple :

• Etats infinis
• Branchements infinis
  

Disgression

Relation binaire des ensembles/domaines $X$ et $Y$ : $\mathcal{R} \subseteq X \times Y$ avec $\mathcal{R}$ la relation de $X$ à $Y$.
Fonction : relation binaire, mais avec :

• Tous les éléments doivent être couverts (sinon c’est une fonction partielle)
• Un élément ne peux être lié qu’à un seul élément
  

Définition formelle

Un STE $S$ est un tuple $S = <Q, q_{0}, \text{Act}, \ra, AP, \mathcal{L}>$ tel que :

• $Q$ est un ensemble d’états
• $q_{0} \in Q$ est l’état initial
• $\text{Act}$ est un ensemble fini d’actions
• $\ra$ est un triplet (état, action état) : $\subseteq Q \times \text{Act} \times Q$
  Si j’ai $(q, a, q') \in \ra$, on écrit $q \xrightarrow{a} q'$
• $AP$ est un ensemble de propositions atomiques
• $\mathcal{L} : Q \mapsto \mathcal{P}(AP)$ (relation binaire de $Q$ à $\mathcal{P}(AP)$) ($\mathcal{P}$ est un powerset, aka toutes les étiquettes possibles)

Exemple

$$\begin{aligned} Q_{A} &= \{q_{0}, Q_{A}\} \\\\ q^{A}_{0} &= q_{0} \\\\ \text{Act}_{A} &= \{\text{aller en bas}, \text{aller en haut}\} \\\\ \ra_{A} &= \{(q_{0}, \text{aller en bas}, q_{1}), (q_{1}, \text{aller en haut}, q_{0})\} \\\\ AP &= \{\text{haut}, \text{bas}\} \\\\ \mathcal{L}(q_{0}) &= \{\text{haut}\}, \mathcal{L}(q_{A}) = \{\text{bas}\} \\\\ \end{aligned}$$

Communication

• Porte $P$ et utilisateur $U$ :
  

Pour obtenir un STE de système global, on fait un produit. Pour ce faire, on définit une table de synchronisation $T^{P}_{u}$ (par abus de notation : $T$).
Le système global $S = S_{u} \|_{T} S_{P}$

• relation binaire avec chaque antécédent a au plus une image : une fonction partielle
  

Définition formelle

Soient $S_{1} = <Q_{1}, q_{0}^{1}, \text{Act}_{1}, \ra_{1}, AP_{1}, \mathcal{L}_{1}>$ et $S_{2} = <Q_{2}, q_{0}^{2}, \text{Act}_{2}, \ra_{2}, AP_{1}, \mathcal{L}_{2}>$

Composition $S = S_{1} \|_{T} S_{2}$ est un tuple $S = <Q, Q_{0}, \text{Act}_{1}, \rightarrow, AP, \mathcal{L}>$ avec $T : \text{Act}_{1} \cup \{-\} \times \text{Act}_{2} \cup \rightharpoondown \text{Act}_{U}\{\tau\}$
où :

• $Q \subseteq Q_{1} \times Q_{2}$
• $q_{0} = (q^{1}_{0}, q^{2}_{0})$
• $\text{Act}$ c’est un ensemble d’actions
• $\ra \subseteq Q \times \text{Act}{\{\tau\}} \times Q$ tel que $(q_{1}, q_{2}) \xrightarrow{\alpha \in \text{Act} \cup \{\tau\}} (q_{1}', q_{2}')$ si et seulement si :
  • $q_{1} \xrightarrow{\alpha_{1} \in \text{Act}_{1}} q_{1}$ et $q_{2} \xrightarrow{\alpha_{2} \in \text{Act}_{2}} q'$ et $T(\alpha_{1},\alpha_{2)}= \alpha$
  • $q_{1} \xrightarrow{\alpha_{1} \in \text{Act}_{1}} q_{1}$ et $q_{2} = q_{2}'$ et $T(\alpha_{1}, -)= \alpha$
  • $q_{1} = q_{1}'$ et $q_{2} \xrightarrow{\alpha_{2} \in \text{Act}_{2}} q_{2}'$ et $T(-, \alpha_{2)}= \alpha$
• $AP = AP_{1} \cup AP_{2}$
• $\mathcal{L} = \mathcal{L}_{1}(q_{1}) \cup \mathcal{L}_{2}(q_{2})$ pour tout $q_{1} \in Q_{1}$ et $q_{2} \in Q_{2}$

Buffer à une place

Buffer à 2 places : $B = B_{1} \|_{T} B_{2}$

$T : \text{Act}_{1} \cup \{-\} \times \text{Act}_{2} \cup \{-\} \rightharpoondown \text{Act} \cup \{\tau\}$

Buffer à trois places : $B \|_{T} B_{3}$

$$(B_{1} \|_{T} B_{2}) \|_{T} B_{3} \equiv B_{1} \|_{T} B_{2} \|_{T} B_{3}$$

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

Modélisation

Exemple

$$S = (P_{1} \| P_{2} \| B)_{T}$$

Table de synchronisation

Act$_{B}$ $\cup$ {-}	Act$_{P_{1}}$ $\cup$ {-}	Act$_{P_{2}}$ $\cup$ {-}	Act$_{S}$ $\cup$ {$\tau$}
isTrue	-	isTrue	$\tau$
isFalse	isFalse	-	$\tau$
setTrue	setTrue	-	$\tau$
setFalse	-	setFalse	$\tau$
-	wr	-	$\omega$
-	-	rd	r

LTE

• $S \vDash$ written $\RA$ (XX read)

• $S \nvDash$ G (written $\RA$ (XX read))

• $S \vDash$ G (written $\RA$ F read) : propriété de réponse (propriété importante dans les systèmes réactifs)

On recherche de la fairness (càd un équilibre entre les lectures et écritures) ; ces propriétés ne spécifient pas la fairness.

Graphes de programmes

Définition

Syntaxe

Un graphe de programme est un tuple
$< L, l_{0}, \longleftrightarrow,$ Val$_{0}>$ sur un ensemble de variables
Var = EVar $\cup$ BVar

• EVar ensemble fini de variables entières
• BVar ensemble fini de variable booléennes
• $L$ ensemble d’états de contrôle (locationss)
• $l_{0} \in L$ initial location (location d’états de contrôle initial)
• $\hookrightarrow$ $\subseteq$ $L \times \mathscr{C}(Var) \times \text{Op}(Var) \times L$ ($\mathscr{C}$ les conditions et $\text{Op}$ les opérations)
• Val$_{0}$ (définition formelle) : …
  • EVal (évaluation d’une variable entière) : Evar $\ra \Z$
  • BVal (évaluation d’un booléen) : BVar $\ra \mathbb{B}$
  • Val$(x) = \begin{cases}\text{Eval}(x) & \text{si } x \in \text{EVar} \\\\ \text{Bval}(x) & \text{si } x \in \text{BVar}\end{cases}$
  • Val$_{0}(x)$ est Val$(x)$ à l’état initial

Sémantique

Rappel : $\wedge$ = ET

La sémantique d’un graphe de programme $< L, l_{0}, \longleftrightarrow,$ Val$_{0}>$ sur Var est donné par un STE $< Q, q_{0},$ Act$, \rightarrow,$ AP$, \mathcal{L}>$ tel que :

• $Q = L \times$ Val
• $q_{0}$ = $(l_{0},$ Val$_{0})$
• Act = {$\tau$}
• $\rightarrow$ : $(l, v) \xrightarrow{\tau}(l', v')$ ssi $l \hookrightarrow l' \wedge v \vDash c \wedge v' =$ Op$(v)$
• (propositions atomiques) AP $= L \times \mathscr{C}$(Var)
• $\mathcal{L} : Q \ra$ AP tel que $q : q = (l, v) \rightarrow \mathcal{L}(q) = (l, C) \wedge v \vDash C$ (avec $C$ la condition)

Produit

• $g_{1} = <L_{1}, l_{0}^{1}, \hookrightarrow_{1},$ Val$_{0}^{1}>$ sur Var$_{1}$c
• $g_{2} = <L_{2}, l_{0}^{2}, \hookrightarrow_{2},$ Val$_{0}^{2}>$ sur Var$_{1}$c

Le produit $\mathbb{P}(g_{1,}g_{2}) = g_{1}||| g_{2}$ ($|||$ = interleaving, aka pas de synchronisation, chacun fait un pas après le tour de l’autre)
Syntaxe de $\mathbb{P}(g_{1,}g_{2}) = <L_{1 \times}L_{2}, (l_{0^{1},}l_{0}^{2}), \hookrightarrow,$ Val$_{0}>$ sur Var$_{1} \cup$ Var$_{2}$
$\mathbb{P}(g_{1,}g_{2})$ est défini ssi $\forall x \in$ Var$_{1} \cap$ Var$_{2} :$ Val$_{0}^{1}(x) =$ Val$_{0}^{2}(x)$

• $\hookrightarrow :(l_{1}, l_{2}) \ra (l_{1}', l_{2}')$ ssi $\begin{cases} l_{1} = l_{1}' et l_{2} \hookrightarrow_{2} l_{2}' \\\\ l_{2} = l_{2}' et l_{1} \hookrightarrow_{1} l_{1}' \end{cases}$

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 )

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.

1. 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

Ensemble des marquages accessibles $\mathcal{A}(R, M_{0})$

Pour l’instant, on a juste défini les sommets, on doit définir désormais les transitions

Définition (1) : Graphe de marquages (accessible)

Pour un réseau de Petri marqué $<R, M_{0}>$, le graphe des marquages accessibles $G(R, M_{0}) = <\mathcal{A}(R, M_{0}, \ra, L)>$

• $\mathcal{A}(R, M_{0})$ est l’ensemble des états
• $L$ est un ensemble de labels (noms) des transitions
• $\ra \subseteq \mathcal{A}(R, M_{0}) \times L \times \mathcal{A}(R, M_{0})$ tel que $\forall M_{1} M_{2} \text{ et } \forall t \in L \in \mathcal{A}(R, M_{0}) : M_{1} \xrightarrow{t} M_{2} \Leftrightarrow M_{1} [t M_{2}$

Définition (2)

$G(R, M_{0})$ est un STE : $<Q, q_{0},$ Act$, \ra,$ AP$, \mathcal{L}>$

• $Q = \mathcal{A}(R, M_{0})$
• $Q_{0} = M_{0}$
• Act = $T$ (noms de transitions)
• $\ra \subseteq Q \times$ Act $\times Q$ tel que $q\xrightarrow{t}q'$ ssi $q = M_{1}$ et $q' = M_{2}$ et celle de la définition (1)
• AP (propositions atomiques) : Cond$(M), M\in \N^{p}$
• $\mathcal{L} : Q \ra$ AP

Les “bonnes” propriétés d’un réseau de Petri

Dans $<R, M_{0}>$.

La vivacité

Transition vivace
Quel que soit mon marquage actuel, j’ai une manière de tirer la transition $t$ maintenant ou dans le futur.
“Possibilité de sensibilisé depuis n’importe quelle transition.”
Une transition $t$ est vivante si et seulement si $\forall M \in G(R, M_{0}) \exists\ \sigma \in L^{*}$ tel que $M\xrightarrow{\sigma}M' \wedge M'[t\rangle$

$\RA$ Un réseau qui ne se bloque pas $\neq$ un réseau vivant

Un réseau est vivant ssi toutes ses transitions sont vivantes.

Non-blocage

$<R, M_{0}>$ est sans blocage ssi si $\forall M\in G-R, M_{0} \exists t \in L : M[t\rangle$

Un non-blocage n’implique pas une vivacité.

Sans blocage et non vivant :
Réseau zombie : vivant, mais bloquant (mort-vivant) : $\RA$ il faut qu’il y ait au moins une transition.

Quasi-vivacité

Je peux sensibiliser ma transition au moins une fois.
Une transition quasi vivante $t$ est quasi-vivante ssi $\exists M \in G(R, M_{0}) : M[t\rangle$

Un réseau de Petri est quasi vivant ssi toutes ses transitions le sont.

Quasi vivant et bloquant :

Réinitialisibilité

Quel que soit le marquage accessible, il y a possibilité dans le marquage initiale $M_{0}$

Réseau de Petri : $R, M_0$ est réinitialisable si et seulement si :

Définition faible

$$\forall M \in G(R, M_{0}) \exists \sigma \in L^{*} : M \xrightarrow{\sigma} M_{0}$$
Dans ce cas, un réseau réinitialisable peut être bloqué sur son marquage initiale.

Définition forte

$L^{+}$ : Sigma non-vide

$$\forall M \in G(R, M_{0}) \exists \sigma \in L^{+} : M \xrightarrow{\sigma} M_{0}$$

Dans ce cas, un réseau réinitialisable est non bloquant.

Réseau borné

Place bornée
Une place $p$ est bornée ssi $\exists k \in \N$ tel que $\forall M \in G(R, M_{0}) : M(p) \leq k$

Un réseau de Petri est borné ssi toutes ses places le sont.

Réseau non borné, mais réinitialisable :

• Réseau borné ? Oui
• Réseau réinitialisable ? Oui
• Réseau vivant ? Non

Tina

Relations entre les propriétés

Vivant $\xRightarrow{?}$ sans-blocage

$(\xRightarrow{?})$ Sous hypothèse

Réinitialisable $\RA$ sans blocage

Fausse avec la définition faible
Vraie avec la définition forte

Réinitialisable et vivant

Sans rapport

Bornée et vivant

Sans rapport

Quand non borné, alors pas de graphe de marquage

Borné et réinitialisable

Sans rapport

Non bornée et bloquant

Réinitialisibilité en LTL (définition faible)

$$\begin{aligned} GF&(\forall p : M(p) = M(0)) \\\\ GF&(M = M_{0}) \end{aligned}$$

Analyse en Composantes fortement connexe (CFC)

Définition

Soit pour un graphe $G = <S, \ra>$ un graphe orienté et $C \subseteq S$ est appelée une composante fortement connexe (CFC, SCC - “Strongly Component Connexe” en anglais) ssi $\forall s, s' \in C, \exists \sigma, \sigma' \ra^{*} s\xrightarrow{\sigma}s' \wedge s'\xrightarrow{\sigma'}s$ (avec $\sigma$ des séquences)
Les CFC nous permettent de partionner un graphe de marquages modulo une relation d’équivalence $G\text{/}_{\sim CFC}: M\sim_{CGC}M'$ ssi $M$ et $M'$ appartiennt à la même CFC.

• Pendante : on ne peut pas en sortir
• Triviale : Contient un seul sommet sans boucle

Analyse en CFC

Soit $<R, M_{0}>$ un réseau de Petri marqué borné.

• $<R, M_{0}>$ est vivant ssi toute CFC pendante dans le $G(R, M_{0})\text{/}_{\sim CFC}$ contient toutes les transitions.
• $<R, M_{0}>$ est réinitialisable ssi $G(R, M_{0})\text{/}_{\sim CFC}$ contient une seule CFC (+ non triviale pour la définition forte).
• $<R, M_{0}>$ est bloquant ssi $G(R, M_{0})\text{/}_{\sim CFC}$ contient une CFC pendante et triviale.

$\mathcal{R}$ est vivant, non réinitialisable et non bloquant.

Correction partielle

Question 1

Acc = $EF_{p}$ (CTL)
Safe = $G(\neg p)$ (LTL)

Si $\nvDash$ Acc $\RA$ $S \vDash$ Safe : vrai

Question 2

$R, M_{0}$, $T \neq \varnothing$

• $R, M_{0}$ vivant $\RA$ $(R, M_{0})$ réinitialisable : faux
• $R, M_{0}$ vivant $\RA$ $(R, M_{0})$ sans blocage : vrai
• $R, M_{0}$ réinitialisable $\RA$ $(R, M_{0})$ borné : faux