Systèmes de transition étiquetés (STE)

Exemple de l’ascenseur :

Exemple du distributeur de boissons :

q_{0} est vide :
Valeur de vérité de conjonction sur un ensemble vide : \forall e \in E : vrai (toujours vrai)
Valeur de vérité de disjonction sur un ensemble vide : \exists e \in E : faux (toujours faux)

Les STE peuvent être infinis.

• Etats infini
• Branchements finis (nombre de manières de quitter un état)

Par exemple :

• Etats infinis
• Branchements infinis
  

Disgression

Relation binaire des ensembles/domaines X et Y : \mathcal{R} \subseteq X \times Y avec \mathcal{R} la relation de X à Y.
Fonction : relation binaire, mais avec :

• Tous les éléments doivent être couverts (sinon c’est une fonction partielle)
• Un élément ne peux être lié qu’à un seul élément
  

Définition formelle

Un STE S est un tuple S = <Q, q_{0}, \text{Act}, \ra, AP, \mathcal{L}> tel que :

• Q est un ensemble d’états
• q_{0} \in Q est l’état initial
• \text{Act} est un ensemble fini d’actions
• \ra est un triplet (état, action état) : \subseteq Q \times \text{Act} \times Q
  Si j’ai (q, a, q') \in \ra, on écrit q \xrightarrow{a} q'
• AP est un ensemble de propositions atomiques
• \mathcal{L} : Q \mapsto \mathcal{P}(AP) (relation binaire de Q à \mathcal{P}(AP)) (\mathcal{P} est un powerset, aka toutes les étiquettes possibles)

Exemple

\begin{aligned} Q_{A} &= \{q_{0}, Q_{A}\} \\\\ q^{A}_{0} &= q_{0} \\\\ \text{Act}_{A} &= \{\text{aller en bas}, \text{aller en haut}\} \\\\ \ra_{A} &= \{(q_{0}, \text{aller en bas}, q_{1}), (q_{1}, \text{aller en haut}, q_{0})\} \\\\ AP &= \{\text{haut}, \text{bas}\} \\\\ \mathcal{L}(q_{0}) &= \{\text{haut}\}, \mathcal{L}(q_{A}) = \{\text{bas}\} \\\\ \end{aligned}

Communication

• Porte P et utilisateur U :
  

Pour obtenir un STE de système global, on fait un produit. Pour ce faire, on définit une table de synchronisation T^{P}_{u} (par abus de notation : T).
Le système global S = S_{u} \|_{T} S_{P}

• relation binaire avec chaque antécédent a au plus une image : une fonction partielle
  

Définition formelle

Soient S_{1} = <Q_{1}, q_{0}^{1}, \text{Act}_{1}, \ra_{1}, AP_{1}, \mathcal{L}_{1}> et S_{2} = <Q_{2}, q_{0}^{2}, \text{Act}_{2}, \ra_{2}, AP_{1}, \mathcal{L}_{2}>

Composition S = S_{1} \|_{T} S_{2} est un tuple S = <Q, Q_{0}, \text{Act}_{1}, \rightarrow, AP, \mathcal{L}> avec T : \text{Act}_{1} \cup \{-\} \times \text{Act}_{2} \cup \rightharpoondown \text{Act}_{U}\{\tau\}
où :

• Q \subseteq Q_{1} \times Q_{2}
• q_{0} = (q^{1}_{0}, q^{2}_{0})
• \text{Act} c’est un ensemble d’actions
• \ra \subseteq Q \times \text{Act}{\{\tau\}} \times Q tel que (q_{1}, q_{2}) \xrightarrow{\alpha \in \text{Act} \cup \{\tau\}} (q_{1}', q_{2}') si et seulement si :
  • q_{1} \xrightarrow{\alpha_{1} \in \text{Act}_{1}} q_{1} et q_{2} \xrightarrow{\alpha_{2} \in \text{Act}_{2}} q' et T(\alpha_{1},\alpha_{2)}= \alpha
  • q_{1} \xrightarrow{\alpha_{1} \in \text{Act}_{1}} q_{1} et q_{2} = q_{2}' et T(\alpha_{1}, -)= \alpha
  • q_{1} = q_{1}' et q_{2} \xrightarrow{\alpha_{2} \in \text{Act}_{2}} q_{2}' et T(-, \alpha_{2)}= \alpha
• AP = AP_{1} \cup AP_{2}
• \mathcal{L} = \mathcal{L}_{1}(q_{1}) \cup \mathcal{L}_{2}(q_{2}) pour tout q_{1} \in Q_{1} et q_{2} \in Q_{2}

Buffer à une place

Buffer à 2 places : B = B_{1} \|_{T} B_{2}

T : \text{Act}_{1} \cup \{-\} \times \text{Act}_{2} \cup \{-\} \rightharpoondown \text{Act} \cup \{\tau\}

Buffer à trois places : B \|_{T} B_{3}

(B_{1} \|_{T} B_{2}) \|_{T} B_{3} \equiv B_{1} \|_{T} B_{2} \|_{T} B_{3}