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
reinit-nonviv

viv-non-reinit

Bornée et vivant

Sans rapport
vivant-nonbornee

Quand non borné, alors pas de graphe de marquage

bornée-nonvivant

Borné et réinitialisable

Sans rapport
nonborné-reinit
bornee-noreinit

Non bornée et bloquant

non-bornée-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.
graphe_cfc