Système de transition d'états

Un système de transition d'états non étiqueté est un couple ${\displaystyle (S,\rightarrow )}$, où ${\displaystyle S}$ est l'ensemble des états et ${\displaystyle \rightarrow \subseteq S\times S}$ est la relation de transition. Si ${\displaystyle p}$ et ${\displaystyle q}$ sont deux états, ${\displaystyle (p,q)\in \rightarrow }$ signifie qu'il existe une transition de ${\displaystyle p}$ à ${\displaystyle q}$, et on l'écrit ${\displaystyle p\rightarrow q}$.

On ne fait aucune hypothèse a priori sur ${\displaystyle S}$ et ${\displaystyle \rightarrow }$, et ils peuvent être infinis, voire indénombrables.

Un système de transition d'états étiqueté est un triplet ${\displaystyle (S,\Lambda ,\rightarrow )}$, avec ${\displaystyle S}$ l'ensemble des états, ${\displaystyle \Lambda }$ un ensemble d'étiquettes et ${\displaystyle \rightarrow \subseteq S\times \Lambda \times S}$ la relation de transition. S'il existe une transition étiquetée par ${\displaystyle \lambda \in \Lambda }$ entre deux états ${\displaystyle p}$ et ${\displaystyle q}$, on écrit alors ${\displaystyle p{\xrightarrow {\lambda }}q}$.

Il est à noter que la définition de la relation de transition ne précise pas s'il s'agit d'une relation binaire :

• de ${\displaystyle S}$ dans ${\displaystyle \Lambda \times S}$ (cas non pertinent dans le cadre des systèmes de transition d'états) ;
• de ${\displaystyle S\times \Lambda }$ dans ${\displaystyle S}$ (cas des automates finis) ;
• de ${\displaystyle S\times \Lambda _{1}}$ dans ${\displaystyle \Lambda _{2}\times S}$ avec ${\displaystyle \Lambda =\Lambda _{1}\times \Lambda _{2}}$ (cas des transducteurs finis).

Dans le cas où ${\displaystyle S}$ et ${\displaystyle \Lambda }$ sont finis, on parle d'automate fini (ou machine à états finie). En général, on se donnera aussi une condition d'acceptation de mot d'entrée, qui sera souvent la donnée de deux parties de S qui seront les états initiaux et les états accepteurs.

Le système de transition est dit déterministe si par définition ${\displaystyle \rightarrow }$ est une fonction. L'expression système de transition non déterministe qualifie tous les systèmes de transition d'états quand on a besoin de préciser qu'on ne se retreint pas aux systèmes déterministes.

Les systèmes de transitions jouent un rôle important dans la reconnaissance des langages formels, notamment dans leur classification.

En vérification de modèles (en anglais : model checking), les systèmes de transitions d'états possèdent en plus une fonction d'étiquetage pour les états (voir par exemple structure de Kripke[1]).

Un système d'états-transitions non étiqueté est un système abstrait de réécriture (en)[2].