# Synthèse de cours : PPC
###### tags: `PPC` `synthèse`

## Algèbre de processus
### Résumé du chapitre
Les algèbres de processus sont une famille de langages formels permettant de modéliser les systèmes (informatiques) concurrents ou distribués.
Les expressions du langages sont interprétés comme un système de transition étiqueté ou LTS (*Labelled Transition System*). Entre ces deux modèles la bisimilarité est utilisée comme une sémantique d'équivalence.
### Syntaxe et représentations graphiques
Le langage CCS a été créé en 1980 et sert à décrire des processus parallèle.

Sa syntaxe est :
$$
P::=0 \ \textbf{|} \
\alpha.P_1 \ \textbf{|} \
A \ \textbf{|} \
P_1+P_2 \ \textbf{|} \
P_1|P_2 \ \textbf{|} \
P_1[b/a] \ \textbf{|} \
P_1 \text{\ } a
$$
- $0$ est le processus inactif
- $\alpha.P_1$ symbolise l'action $\alpha$ sur $P_1$
- $A=^{def}P_1$ est utlisé pour signifié que $A$ pointe sur $P_1$
- $P_1+P_2$ Signifie que l'on peut avancer le process soit via $P_1$ soit via $P_2$
- $P_1|P_2$ Signifie que les deux processus peuvent exister simultanément
- $P_1[b/a]$ Signifie que dans $P_1$ les action $a$ sont renommées $b$
- $P_1 \text{\ } a$ C'est le process $P_1$ sans $a$

### Equivalence structurelle entre processus
Dans le calcul des systèmes de communication (CCS), la congruence structurelle joue ce rôle en rendant, par exemple, la composition parallèle **commutative et associative**. Sans elle, le système serait lourd à utiliser et à raisonner, et il est possible de prouver que ce changement est inoffensif dans un sens technique précis.

La congurence structurelle (notée : ≡) de processus sur $P$ est déterminée par équations suivantes :

### Sémantique opérationnelle entre processus
#### Sémantique de réactions
Les réactions en CCS sont dictées par 5 règles :
- **TAU** : $\frac{}{\tau.P+M \rightarrow P}$ On a effectué l'action $\tau$ et il n'y avait pas d'action a effectuer sur le processus M, il ne reste donc que P.
- **REACT** : $\frac{}{(a.P+M)|(\bar{a}.Q+N) \rightarrow P|Q}$ En effectuant l'action $a$ on enclenche l'action $\bar{a}$ et il reste $P$ et $Q$ car il n'y a rien à faire sur les processus $M$ et $N$
- **PAR** : $\frac{P\rightarrow P'}{P|Q \rightarrow P'|Q}$ On a effectué des actions dans $P$ et devient donc $P'$ partout où il existe
- **RES** : $\frac{P\rightarrow P'}{\nu a P \rightarrow \nu a P'}$ $a$ est protégé des modifications dans P (a vérifier)
- **STRUCT** $\frac{P\rightarrow P'}{Q\rightarrow Q'}$ si $P \equiv Q$ et $P' \equiv Q'$ car il y a une congruence entre eux donc une modification de l'un impliquera la même modification dans l'autre

##### Congruence de processus
Un contexte est une expression dans laquelle il y'a un "trou" une place libre pour un processus.
Par exemple les contextes élémentaires :
$$
\alpha.[ \ ]+M;\\ \nu a \ [ \ ];\\ [ \ ] | P;\\ P | [ \ ];
$$

Deux processus peuvent être congrus si et seulement si ils sont équivalent dans le même contexte.

#### Sémantique de transitions : LTS
Un LTS va servir a montrer tous le dérouler d'une expression. Il est régit par un certain nombre de règles formelles.

Grossièrement l'idée est :
- Une transition est possible entre deux états $P' \rightarrow^\alpha P''$ si on peut inférer à partir des règles de transitions, comprendre qu'une transition existe si une règle de transition existe la concernant
##### Règles de transitions formelles

##### Exemple
$P \equiv a.b+a.c+a.d$
En LTS :

graph TD
P[a.b+a.c+a.d]
empty[N/A]

P -->|a| b -->|b| empty
P -->|a| c -->|c| empty
P -->|a| d -->|d| empty

On voit bien ici le processus en entier avec toutes ses possibilités aux différentes étapes.
On arrive donc ici à une opération vide, on peut en conclure que $P \equiv \emptyset$.
Cela peut aussi permettre de comparer deux expressions:
$Q \equiv a.(b+c+d)$
En LTS :

graph TD
Q

Q --> |a| Q_[b+c+d]
Q_ -->|b| empty[N/A]
Q_ -->|c| empty[N/A]
Q_ -->|d| empty[N/A]

On voit ici que malgré le même résultats $P \equiv \emptyset$ et $Q \equiv \emptyset$ les deux epxressions n'ont pas le même LTS et ne sont donc pas équivalents.
## Bisimulation et points fixes
### Résumé du chapitre

### Rappel équivalence entre processus

Soit deux processus $P$ et $Q$.

Le but étant de trouver si $P$ est équivalent à $Q$, c'est à dire, de prouver si le processus $Q$ peut remplacer le processus $P$
Les relations d'équivalence entre ces processus $P$ et $Q$ peuvent être décrites ci-dessous :

### 1. $P = Q$
**Proposition:** $P$ et $Q$ sont équivalent s'ils s'écrivent de la même manière.

**Exemple :** $P = a.b.c$ et $Q = a.b.c$

Cette équivalence **est trop forte.**
**Car** $P = a | b$ et $Q = b | a$ devraient être équivalent

### 2. $P \equiv Q$
**Proposition:** $P$ et $Q$ sont équivalent s'ils sont congrus entre eux. (Par les rêgles de congruences)

**Exemple :** $P = a.b|\bar{a}$ et $Q = \bar{a}|a.b$ (Équivalence structurelle par la règle **PAR**)

Cette équivalence **est trop forte.**
**Car** $P =a | b$ et $Q = a.b + b.a$ devraient être équivalent

### 3. LTS( P) = LTS(Q)
**Proposition:** $P$ et $Q$ sont équivalent s'ils ont les mêmes LTS

**Exemple:** $P = a|b$ et $Q = a.b + b.a$ (Même LTS)


$P = a.b.a.b.P$ et $Q = a.b.Q$ (Pas le même LTS, même comportement)

Cette équivalence **est trop forte**.
**Car** $P = a.b.a.b.P$ et $Q = a.b.Q$ devraient être équivalent.

### 4. Même trace, même comportement
**Proposition** $P$ et $Q$ sont équivalent s'ils ont les mêmes comportements.

**Exemple** $P = a.b.a.b.P$ et $Q = a.b.Q$

Cette équivalence **est trop faible**.
**Car** $P = p.(bt.\bar t + bc.\bar c)$ et $Q = p.bt.\bar t + p.bc.\bar c$ ont les mêmes traces **MAIS** ne marchent pas en tout contexte.


Il y a non-determinisme avec $Q$.

Du point de vue de l'utilisateur, s'il insère une pièce avec $Q$, c'est la machine qui choisit s'il peut appuyer sur $bt$ ou $bc$. Ce qui n'est pas le cas avec $P$. Et l'on ne veut pas de ça.

#### Équivalence de trace
Soit $LTS(P) = <Q,T>$
#### Trace forte (STR)
$P=_{STR}Q$ si str$(P)$ = str$(Q)$

$str(P) =def \{<α_1, ..., α_n>|∃q_1, .., q_n ∈ Q : P \xrightarrow[]{α_1}q_1 \xrightarrow[]{α_2} ... \xrightarrow[]{α_n} q_n\}$

Plus simplement => Transition α sans $\tau$
#### Trace faible (TR)
$P=_{TR}Q$ si tr$(P)$ = tr$(Q)$

$tr(P) =def \{<α_1, ..., α_n>|∃q_1, .., q_n ∈ Q : P \xrightarrow[]{\tau}^* \xrightarrow[]{α_1} \xrightarrow[]{\tau}^* q_1 ...\xrightarrow[]{\tau}^* \xrightarrow[]{α_n} \xrightarrow[]{\tau}^* q_n\}$

Plus simplement => Transition α avec 0 ou plusieurs $\tau$

#### Exemple

**Trace forte:** STR($P$) = { <$a, b, \bar a$>, <$a, \bar a, b$>, <$\bar a, a, b$> }

**Trace faible:** TR($P$) = STR($P$) $\cup$ { <$b$> }

Il nous faut une relation d'équivalence qui soit plus fine que (1,2 et 3) mais plus forte que (4).

Ce qui introduit la notion de **bisimilarité**

### Bisimulation (forte)

### Bisimulation faible

La double flèche indique une transition $\tau$

### Bisimulation comme un point fixe

## Exemple 1 bisimulation

Soit $P= a.\bar a.P$ et $Q = a.\bar a.Q | \bar a$.
Montrons que $P \sim Q$

#### LTS

Supposons qu'il existe R bisumulation t.q $P R Q$

$Q \xrightarrow[]{\bar a} a.\bar a.Q$ et $P \not\xrightarrow[]{a}$ donc $R$ n'est pas une bisimulation donc $P \not\sim Q$

## Exemple 2 bisimulation

Soit $P = a.b$ et $Q = a.b + a.b$

Montrons que $P \sim Q$

**LTS**

$P$ et $Q$ n'ont pas les mêmes LTS.

$R = \{ (P_0, Q_0), (P_1, Q_1), (P_2, Q_2)\}$

Pour montrer que $R$ est une bisimulation, il faut montrer que $P$ et $Q$ respectent le jeu de la bisimulation tels que:

$P_0 \xrightarrow[]{a} P_1$ et $Q_0 \xrightarrow[]{a} Q_1$ et $P_1 R Q_1$
$Q_0 \xrightarrow[]{red(a)} Q_1$ et $P_0 \xrightarrow[]{a} P_1$ et $Q_1 R P_1$
$Q_0 \xrightarrow[]{blue(a)} Q_1$ et $P_0 \xrightarrow[]{a} P_1$ et $Q_1 R P_1$
$P_1 \xrightarrow[]{a} P_2$ et $Q_1 \xrightarrow[]{a} Q_2$ et $P_2 R Q_2$
$Q_1 \xrightarrow[]{a} Q_2$ et $P_1 \xrightarrow[]{a} P_2$ et $Q_2 R P_2$

Alors $P \sim Q$

## Hennessy-Milner Logic
### Résumé du chapitre
Permet de voir un terme de CCS comme une spécification, exprimée par des propriétés vérifiables. (En explorant l'espace des états du processus)

### Définition
L'ensemble $M$ des formules HML sur un ensemble d'Act

$F,G ::=tt | ff | F∧G | F∨G | ⟨a⟩F | [a]F$

avec a ∈ Act, tt = vrai,ff =faux

### Notation
C'est une logique modale avec :
**Possiblement**
⟨a⟩F : Il est possible de s’engager dans une action a et satisfaire F
**Nécessairement**
[a]F : Peut importe comme on s’engage dans une action a, F sera nécessairement satisfaite

### Exemple

$⟨.a.⟩\{S1, R1\} = \{S, R\}$
$[.a.]\{S1, R1\} = \{S1, S2, R, R1\}$
$<.b.> \{S1,R1\} = \{R1\}$
$[.b.]\{S1, R1\} = \{S, R, R1\}$

## Algèbres de processus temporels
### Résumé du chapitre

## $\pi$ calcul
### Résumé du chapitre

### Syntaxe
* **$a\langle x \rangle .P$** : Le processus envoie un nom $x$ sur le canal $a$, puis continue avec P
* **$a(x).P$** : Le processus reçoie un nom $x$ sur le canal $a$, puis continue avec P $\to$ P peut utiliser $x$ $\to$ lie $x$ dans $P$
* **$!P$** : réplication de P $\to$ $!P \equiv !P | P$ ...
* **$(\nu a) \ P$** lie $a$ dans $P$ $\to$ les noms liés sont distincts deux à deux et sont distincts des noms libres

### Bisimulation Barbue
* $P \downarrow_{a}$ signifie "P peut recevoir un message sur a"
* $P \downarrow_{\bar{a}}$ signifie "P peut envoyer un message sur a"
* On note $\mu$ pour $a$ ou $\bar{a}$ désignant les entrées et les sorties (mais pas $\tau$)


### Equivalence Barbue
Si les 2 processus ont les mêmes entrées et sorties alors on fait que des $\tau$.
Equivalence Barbue représentée par : $\simeq$
$\to P \simeq Q$ si $\forall R, P | R$ est bisimilaire à $Q | R$

#### Théorème de Caractérisation
$P \simeq Q$ si et seulement si $P \sim Q$

### Exemple

### Typage
#### Typage simple
Le typage en $\pi$ calcul est assuré par un ensemble règles que voici :

**Explication :**
- (Nil) : S'il n'y a rien a typer ne type rien
- (Out) : Dans le cas d'une expression $\overline{a} \langle v \rangle.P$ On va typer $v : T$ car il est émis et donc pas vide et $a:\#(T)$ car c'un canal gérant une varaible de type $T$. Et P on le laisse pour après.
- (Par) : On traite $P_1$ et $P_2$ en parallèles.
- (In) :
- (Rep) :
- (Res) :

##### Exemple
Ex : $p(x,y).(\overline{x} \langle y \rangle | \overline{y} \langle 3 \rangle)$
Donc ici nous avons:
- $y: \#Nat$
- $x:\#(\#Nat)$
- $p:\#(\#(\#Nat), \# Nat)$ car nous avons inclus dans $p$ les types de $x$ & $y$
#### Deng-Sangiorgi (Système des poids)
Cet ajout au système de typage vise a vérifier la terminaison possible d'un programme.
En résumé cela vise a ajouter a chaque type un "poids" une valeur arbitraire.

Et cela selon ces règles :

En résumé pour chaque type on va associer une valeur qui doit respecter deux règles simples (spécifiée dans Rep) :

Dans un programme $a(x).P$ :
- $P$ a un poids de $n$
- $a(x)$ a un poids $k$

Si elles mènent a une situation de non sens on peut considérer que le programme ne se termine pas.

Controle des réplications:

$!a^k(x).P$ avec $\vdash P: n$ requiert k > n.
Avec $\Gamma \vdash P: n$ le niveau maximum d'un output dans l'état courant.

##### Exemple
Ex: $c(x).\overline{x} \langle 8 \rangle$

Types :
- $x: \#^2 Nat$ assimilé a $n$
- $c:\#^1(\# ^2 Nat)$ assimilé a $k$

Donc ici comme $2>1$ c'est bon.


## UPAAL
**Exemple avec le diner chic**

### UI
Arc

- **Séléction :**
- **Garde :** Condition de passage par l'arc.
- **Sync :** Si *?* alors va chercher a récupérer sur le canal précdant le *?*. Ici c'est le canal *fg*. Si *!* alors on émet sur le canal.
- **Mise à jour :** Element a mettre à jour quand on passe sur l'arc

### Déclaration globale :

// Place global declarations here.
chan get_f, put_c, put_f, ch, fg, st;
urgent chan get_c;

int [0,1] libre;

const int M = 10;
int [0,M] mets;

### Schémas
**Client :**

**Serveur :**

**Cuillère :**

**Fourchette :**