1.1 KiB
Proprieta` del modello
Ogni modello successivamente mostrato rispetta le seguenti proprieta`:
-
Mutua esclusione (safety): garantisce che al piu` un solo processo e` nella sezione critica ad ogni istante
G (¬cₚ∨¬cq) -
Assenza di deadlock (liveness): ogni qualvolta un processo e` in attesa di entrare nella sezione critica, eventualmente verra` concesso ad un processo di entrare nella sezione critica
G(wₚ → F(cₚ∨cq) -
Assenza di starvation individuale (strong fairness): ogni qualvolta un processo e` in attesa di entrare nella sezione critica, eventualmente gli verra` concesso
GFcₚ
Possiamo convertire queste tre formule LTL in formule equivalenti CTL anteponendo l'operatore di stato A:
| AG (¬cₚ∨¬cq) |
| AG(wₚ → AF(cₚ∨cq) |
| AGAFcₚ |
Benche` non tutte le formule LTL possono essere convertite in una formula CTL equivalente anteponendo ad ogni operatore temporale l'operatore di stato A, per queste tre proprieta` possiamo
[ ] Correggi LTL E CTL dell'ultima. [ ] Chiedi a galla` se e` giusto in termini di liveness safety e fairness