net

surete/02_kripke.md

@@ -71,3 +71,16 @@ GFA : FA se produira forcément
  |
 ( )->(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
+