---
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
```