Complete verification lecture

content/conception_formelle/3_extention_logique/index.md

@@ -0,0 +1,145 @@
+---
+title: "Conception formelle : Extention de la logique"
+date: 2023-01-20
+tags: ["Bugs", "model-checking"]
+categories: ["Conception formelle", "Cours"]
+mathjax: true
+---
+
+## Rappel mathématique
+
+Soit \\(E\\) un ensemble dictret, \\(f\\) une fonction tel que \\(f: E \to E \\)
+et \\(E_1 \subseteq E_2\\) et \\(E_2 \subseteq E\\) :
+
+ * \\(f\\) est *monotone*  si et seulement si \\(E_1 \subseteq E_2) \implies
+   f(E_1) \subseteq f(E_2)\\)
+ * \\(f\\) est **antimonotone* si et seulement si \\(E_1 \subseteq E_2) \implies
+   f(E_1) \supseteq f(E_2)\\)
+ * \\(f\\) est augmentée si et seulement si \\(E_1 \subseteq f(E_1)\\)
+ * \\(f\\) est reduite siet seulement si \\(E_1) \supseteq f(E_2)\\)
+
+Soit \\(f_1, f_2: E \to E\\) deux fonctions monotones et \\(g_1, g_2: E \to E\\)
+deux fonctions antimonotone :
+
+ * \\(f_1(f_2(X))\\) est monotone
+ * \\(f_1(f_2(X))\\) est antimonotone
+ * \\(g_1(f_2(X))\\) est antimonotone
+ * \\(g_1(g_2(X))\\) est monotone
+
+### Propriété (fonction monotone croissante)
+
+Soit \\(f: E \to E\\) une fonction monotone croissante tel que \\(\emptyset 
+\subseteq f(\emptyset) \subseteq f^2(\emptyset) \subseteq ... \subseteq 
+f^n(\emptyset) \subseteq ... \subseteq E\\) avec \\(E\\) ensemble finis et
+discret : \\(\exists i / \forall n \le i; f^n(\emptyset) = f^i(\emptyset) \\)
+alors \\(f^i(\emptyset)\\) est la plus petite solution à l'équation \\(X = f(X)
+\\).
+
+Alors si \\(E\\) est un ensemble fini et discret et que \\(f: E \to E\\) est
+une fonction monotone croissante alors \\(X=f(X)\\) est **plus petit point fixe
+obtenu par itération**. \\(f(E) = E\\) alors \\(E\\) est aussi une solution de \\(
+X = f(X)\\)
+
+### Propriété (fonction monotone décroissante)
+
+Soit \\(f: E \to E\\) une fonction monotone décroissante tel que \\(E \supseteq
+f(E) \supseteq f^2(E) \subseteq ... \subseteq f^n(E) \subseteq ... \subseteq
+\emptyset\\) avec \\(E\\) ensemble finis et discret : \\(\exists i / \forall n
+\le i; f^n(\emptyset) = f^i(\emptyset) \\) alors \\(f^i(\emptyset)\\) est la
+plus petite solution à l'équation \\(X = f(X) \\).
+
+Et si \\(f: E \to E\\) est une fonction monotone décroissante, alors \\(X=f(X)
+\\) est **plus grand point fixe obtenu par itération**.\\(f(\emptyset) = 
+\emptyset\\) alors \\(\emptyset\\) est aussi une solution de \\(
+X = f(X)\\)
+
+## Extension de la logique de Dicky
+
+Soit : 
+
+ * \\(A\\) un graphe \\(G(S,T)\\)
+ * \\(f(X)\\) une formule logique sur \\(S\\) (*state*) ou \\(T\\) 
+   (*transition*)
+ * \\(S_1 \subseteq S\\) et \\(S_2 \subseteq S\\)
+ * \\(T_1 \subseteq S\\) et \\(T_2 \subseteq S\\)
+ * \\(X_1 \subseteq X\\) et \\(X_2 \subseteq X\\) avec \\(X = S\\) ou 
+   \\(X = T\\)
+ * \\(Y_1 \subseteq Y\\) et \\(Y_2 \subseteq Y\\) avec \\(Y = S\\) ou 
+   \\(Y = T\\)
+
+### Constantes et proposition élémentaires
+
+\\(F(X)\\) est une formule avec seulement \\(\emptyset_S, \emptyset_T, any_s,
+any_t, initial, ...\\). Si \\(f\\) est une constante et \\(f^2(X) = f(X)\\) 
+alors \\(f(X)\\) est la solution.
+
+### Les opérateurs logiques
+
+Soit \\(f(X)\\) une formule avec aussi `src`, `tgt`, `rsrc`, `rtgt` et \\(T\\),
+\\(S\\) tel que
+
+ * \\(T_1 \subseteq T_2 \implies src(T_1) \subseteq src(T_2)\\)
+ * \\(T_1 \subseteq T_2 \implies tgt(T_1) \subseteq tgt(T_2)\\)
+ * \\(S_1 \subseteq S_2 \implies rsrc(S_1) \subseteq rsrc(S_2)\\)
+ * \\(S_1 \subseteq S_2 \implies rtgt(S_1) \subseteq rtgt(S_2)\\)
+
+\\(f\\) est monotone alors la solution de \\(X = f(X)\\) peut être calculée par
+itération.
+
+### Opérateurs d'ensembles
+
+Soit \\(f(X)\\) une formule avec aussi \\( \cup, \cap, \setminus \\)
+(soustraction d'ensemble) :
+
+ * \\(X_1 \subseteq X_2, Y_1 \subseteq Y_2 \implies X_1 \cup Y_1 \subseteq X_2
+   \cup Y_2\\) (formule monotone)
+ * \\(X_1 \subseteq X_2, Y_1 \subseteq Y_2 \implies X_1 \cap Y_1 \subseteq X_2
+   \cap Y_2\\) (formule monotone)
+ * \\(X_1 \subseteq X_2, Y_1 \subseteq Y_2 \implies X_1 \setminus Y_1 ?
+   X_2  \setminus Y_2\\) ici deux cas de figures:
+   * \\(X_1 \subseteq X_2 \implies X_1 \setminus Y_1 \subseteq X_2 \setminus
+     Y_1\\) est une formule monotone.
+   * \\(Y_1 \subseteq Y_2 \implies X_1 \setminus X_2 \supseteq X_2 \setminus
+     Y_2\\) est une formule anti monotone.
+
+
+### Résultat
+
+Soit \\(f(X)\\) une formule. Si \\(X\\) apparaît derrière un nombre pair de
+soustrtactions, **alors \\(f\\) est monotone et \\(f(X)\\)** peut être calculé
+par itération :
+
+ * Si elle est croissante nous pouvons calculer le plus petit point fixe
+ * Si elle est décroissante nous pouvons caluler le plus grand point fixe
+
+Sinon **elle est antimonotone** et ne peut être calculée par itération. Alors
+nous ne pouvons pas savoir s'il existe une solution à \\(X = f(X)\\).
+
+### Exemple
+
+Prenons la formule \\(F(X) = dead_0 \ cup (src(rtgt(X)) \setminus src(rtgt(any_s
+\setminus X)))\\) :
+
+ * nous avons trois occurences de \\(X\\) après 0,0 et deux soustractions dans
+   l'expression, donc \\(f\\) est monotone.
+ * \\(f\\) est une fonction croissante, nous pouvons alos calculer le plus petit
+   point fixe par l'itération de \\(f^i(\emptyset_s)\\).
+
+La solution de cette équation représente le plus petit ensemble de
+configurations qu mène à un état puit.
+
+## Sur *ARC*
+
+\\( X -= f(X)\\) calcule le plus grand point fixe et \\( X += f(X)\\) le plus
+petit point fixe. Voici un exemple :
+
+``````
+with MyComponent do
+    // calculer les états puit 
+    dead := any_s - src(any_t - self_epsilon);
+
+    // trouver les transitions qui mène ces états : calcul du plus
+    // petit point fixe
+    deadlock += dead | (src(rtgt(deadlock)) - src(rtgt(any_s - deadlock)));
+done
+```