From 8034cef538466afd3935d23a29f8cae2d18594e9 Mon Sep 17 00:00:00 2001
From: JOLIMAITRE Matthieu <matthieu@imagevo.fr>
Date: Mon, 26 Feb 2024 16:09:47 +0100
Subject: [PATCH] =?UTF-8?q?surete=20op=C3=A9rateurs=20temporelle?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 surete/02_kripke.md | 69 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)

diff --git a/surete/02_kripke.md b/surete/02_kripke.md
index 6ebe4df..6f192db 100644
--- a/surete/02_kripke.md
+++ b/surete/02_kripke.md
@@ -2,3 +2,72 @@
 
 - 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) ...
+```