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

Question 3

Pour toute exécution infinie $\pi$ de $S$, il existe un état $s$ satisfaisant $p$ et tous les états suivants $s$ dans $\pi$ satisfait $p$

Quantifier sur les traces (“Pour toute exécution infinie”), donc exprimable en LTL.

• en LTL : $FGp$
• en CTL : non exprimable

Question 4

Question 5

• $pEUq$ : $p$ jusqu’à ce que j’ai $q$ : vrai
• $pAUq$ : pour tous les chemins, tout va bien : vrai
• $EFEGp$ : il existe un chemin tel que dans ce chemin je trouve un état, tel que dans ce chemin je trouve un état à partir duquel je satisfais toujours $p$ : vrai
• $EFAFp$ : il existe un chemin dans lequel j’ai qu’un seul chemin et à partir de celui-ci je vais pouvoir toujours satisfaire $p$ dans le futur : vrai
• $AFEFp$ : pour tous les chemins, il existe un état qui peut satisfait $p$ dans le futur : vrai

Exercices

Question 1

• le réseau est borné (oui, car graphe de marquage)
• le réseau est vivant (non, on ne connait pas les transitions, uniquement le graphe)
• le réseau est quasi vivant (on ne connait toujours pas les transitions)
• le réseau est sans blocage (on n’a pas de CFC pendante et triviale)
• le réseau est pas réinitialisable (car 2 CFC, et non 1)

Question 2

Quelque soit l’état accessible de $S$, il existe une manière de satisfaire la proposition $p$ à partir de cet état (maintenant ou dans le futur).

Indice : quantification sur les états, donc CTL faisable.

En CTL : $AGEFp$
En LTL : pas exprimable

Question 3

$S\vDash AFAGp$ (CTL)

• $S\overset{?}{\vDash} FGp$ (LTL)

Question 4

• $F\ M(P_{2})\geq2$

Question 5

• est-il borné ? Non, $P_{3}$ ne l’est pas. Supposons $\exists k \in \N$ tel que $\forall M \in \mathcal{A}(k, M_{0}), M(P_{2}) \leq k$
• est-il réinitialisable ? (si on tire $P_{3}$ vers $t_{3}$ autant qu’il faut, on peut revenir au marquage initial)
• $M(P_{3}) > 0 \RA X\ M(P_{3}) = 0$ (parce que au marquage initiale, la propriété initiale est fausse)
• $G(M(P_{3}) = 0 \RA X(M(P_{4}) = 1 \vee M(P_{1}) = 1))$
• $G(M(P_{3}) = 0 \RA X(M(P_{4}) = 1 \vee M(P_{2}) = 1))$