Structure de kripke

ensemble de variables propositionnelles pour chaque état
ensemble d'état

[ c.f. intro ]

Table de vérité

listes des état des variables propositionnelles possibles

Logique Temporelle Linéaire

propriétés linéaires, rigides, s'applique sans laisser d'options possibles

si l'utilisateur n'ouvre pas la porte, la machine va démarrer le lavage
la porte reste déverrouillée jusqu'au démarrage du lavage

opérateurs de temporalité

X(next) A : à l'instant suivant, A
A U(until) B : A jusqu'à B

exemple :

si l'utilisateur n'ouvre pas la porte, la machine va démarrer le lavage
- (X F) => (X D)
la porte reste déverrouillée jusqu'au démarrage du lavage
- (not V) U (D)

Trace

Un état du système : s = L
Une trace est une suite infinie d'état : pi e L^N
Les états du système le long de la trace : pi_1, pi_2, ...

Satisfaction

...

plus d'opérateurs

'jamais' et 'toujours' sont difficile à formuler en terme d'opérateurs de temporalité X, U

G(always) A = not(True U (not A)) : A est toujours vrai
F(eventually) A = True U A : A devient éventuellement vrai

dans une trace :

FA : A peut se produire dans un état suivant
 |
( )->( )->(A)->( ) ...


GA : A se produira forcément dans tous les états suivants
 |
(A)->(A)->(A)->(A) ...


FGA : GA peut se produire
 |    il peut se produire dans un état suivant que ...
 |       A se produira forcément dans tous les états suivants
 |
( )->( )->(A)->(A) ...


GFA : FA se produira forcément
 |    il se produira forcément dans tous les états suivants que ...
 |       A peut se produira dans un état suivant
 |
( )->(A)->( )->(A) ...

1.7 KiB Raw Blame History