| 12345678910111213141516171819 |
- 2 propr. :
- - correction partielle : « tout procédé terminé est dans son état final » <-> square (dead => finished)
- [] <> =>
- - terminaison : « toute exécution se termine » <-> square diamond dead
- rappel LTL-SE :
- - variante de LTL pour traiter de façon homogène les propositions d'états et
- propositions de transitions
- - structures de kripke
- P : P vraie au départ de chemin (pour l'état initial)
- square P : P vraie tout le long du chemin
- diamond P : P vraie une fois au moins le long du chemin
- P U Q : Q sera vraie dans le futur et P est vraie jusqu'à cet instant
- square diamond P : P vraie infiniment souvent
|
