Modèles formels pour l'informatique quantique

6.2.2 Sémantique opérationnelle de Basic LOTOS

La sémantique opérationnelle du langage Basic LOTOS est donnée par l'ensemble des règles d'inférence suivantes :

1.

2.		exit-->.stop

3. (a) E4E'

E[]F4E'

E4E'

(b)- F[]E4E'

{8

4. (a)i.E|[L]|FE4E'aELU'|[L]}|F ii. E4E'a/ELU{8} F|[L]|E4F|[L]|E' -->.F'a/ELU{8} (b)Ea -->.E',F a E|[L]|F4E'|[L]|F'

5. (a) (b)

E4E'a/EL hideLinE4hideLinE' E4E'aEL hideLinE4hideLinE'

a6=8

6. (a) E4E'

(b)

E>>F-E'>>F E4E^'a6=8 E>>F4E'>>F E4E^'a

7. (a) 8
E[>F-E'[>F

_(b)E4E'a6=8 E[>F4E' (c)F4F'a 8

E[>F4F'

6.3 Q-LOTOS

on va introduire une technique Q-LOTOS pour (Quantum Language of Temporal Ordering Specification) de description formelle pour la spécification des intéractions quantiques

6.3.1 Syntaxe de Q-LOTOS

La syntaxe de Q-LOTOS est une extension de celle de Basic LOTOS avec l'introduction des actions quantique (actions sur desinformations quantiques). Soit :

- P l'ensemble de processus quantiques

56

chapitre6 : Q-LOTOS

- G l'ensemble d'actions classiques. Q est l'ensemble d'actions quantiques - 8 action particulière qui désignée la terminisation avec succés

- r action particulière qui désignée une action silencieuse

- L c G un sous-ensemble (pouvant être vide) quelconque de G

- M c Q un sous-ensemble quelconque de Q

avec l'ensemble de toutes les actions est désigné par Act où :

Act = G U Q U {r,8}.

Dans ce qui suit, nous supposons toujours que M est un ensemble fini de Q et est un super-opérateur sur HM quand [M] ou _M est rencontré.

VM c Q, M =def ® IH_Q- où IH_Q- est l'opérateur d'identité de HQ-M

La syntaxe formelle du Q-LOTOS est donnée par:

P : := stop exit X[L] [M];P á;P r;P P[]P P |[M]|P |

hide L in P P >> P P[> P

où á E Q U G et M c Q U G.

Il est semblable à la syntaxe de Basic LOTOS, et les seules différences entre eux sont :

- La clause [M]; P de la définition ci-dessus nous permet d'effectuer des opérations quantiques sur certains processus quantiques.

- La clause q; P : Processus qui réalise l'action quantique q, puis se transforme en P. "Pré-fixage par une action quantique".

- La clause E1 [M] E2 : E1 et E2 s'exécutent en paralléle et se synchronisent sur les portes quantiques qi E M et la porte 8. "Composition paralléle".

6.3.2 Sémantique Opérationnelle

La sémantique opérationnelle du langage Q-LOTOS est donnée par l'ensemble des règles d'inférence suivantes :

chapitre6 : Q-LOTOS

1.

2.

3.

exit ^ä +stop

á;E^á+E

î[M];E^î[M1

+ îM (E)

4. 57

(a) Eá+E'

E^á+E'

(b) F[]Eá+E'

E^á+E'a/ELU{ä}

5. (a)2. E|[L]|Fá+E'|[L]|F

ii . F|[L]|Eá+F|[L]|E'

b Eá+E',F$F'a/ELU{ä} () E|[L]|Fá+E'|[L]|F'

E^á+E'a/ELU{ä}

4. (a)i.

E^á+E'a/EMU{ä}

ii.

E|[M]|F^á+E'|[M]|F E^á+E'a/EMU{ä}

F|[M]|E^á+F|[M]|E'

+F'a/EMU{ä}

(b)Eá +E',F á

E|[M]|F^á+E'|[M]|F'

7. (a) Eá+E'a/EL
hideLinE^á+hideLinE' E^á+E'aEL

(b)

hideLinE+ô hideLinE'

E^ä+E^'

8. (a) E>>F+aE'>>F

E^á+E'ä

(9. (b) a E»F-+TE'»F
) Eá+E'a6=ä a) E[>Fá+E'[>F _(b)E^á+E'a6=ä

E[>F^á+E'

_(c)F^á+F'a6=ä E[>F^á+F'