86 lines
2.1 KiB
Markdown
86 lines
2.1 KiB
Markdown
# 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) ...
|
|
```
|
|
|
|
## Sémantique
|
|
|
|
- S, q |= a uniquement si a in p(q) a appartiennt aux propositions de l'état q
|
|
- S, q |= AX phi uniquement si pour tout q' in Q tant que q -> delta q' ...
|
|
|
|
### Plus d'opérateurs
|
|
|
|
- AX B : à l'instant suivant, B forcément
|
|
- EX B : à l'instant suivant, B est possible
|
|
- B AU C : B est forcé jusqu'à C
|
|
- B EU C : B est possible jusqu'à C
|
|
|