Chapitre III LTL

Exo 1 (page 27)
---------------
                  0  | 1  | 2  | 3  |  4  | 5 ....
                 _________________________________
*	    q	  V    V    V     F    F    F
*	    p	  F    F    F    V     F    F
        q U p     V    V    V    V     F    F
*        [] -Q    f    f    F    v     v    v
      <> [] ¬q    V    V    V    V     V    V
    <> (q U p)    V    V    V    V     F    F
  <> ¬ (q U p)    V    V    V    V     V    V
 *  [] (q U p)    F    F    F    F     F    F       
  ¬ [] (q U p)    V    V    V    V     V    V
*   [] ¬ (q U p)  F    F    F    F     V    V
  ¬ [] ¬ (q U p) ...

======================
 
Exemple de Specification LTL

1Exclusion Mutuelle
Jamais plus de deux processus en train de travailler en même temps

2 Absence de Famine
Un processus en attente sera au bout d’un temps fini
dans l’état travail

3 Temps d’utilisation de la ressource borné
Un processus dans l’état travail sera au bout d’un temps fini dans
un état non travail

4 La ressource n’est accordée qu’aux processus l’ayant demandée
Pour un process donné : l’état attente précède toujours
l’état travail