Informatique C

Notations et définitions.

Pour un ensemble fini $E$, on note $2^E$ son ensemble des parties, $E^*$ l’ensemble des mots finis sur $E$ et $E^\omega$ l’ensemble des mots infinis sur $E$.

Le mot vide est noté $\epsilon$.

Les positions commencent à $0$.

Pour un mot $u$, la notation $|u|_a$ désigne le nombre d’occurrences de la lettre $a$, éventuellement infini.

Un système de transitions est un quadruplet $T=(S,A,D,\delta)$.

Les ensembles $S$ et $A$ sont finis.

Pour chaque $s\in S$, l’ensemble $D(s)\subset A$ contient les actions exécutables depuis $s$.

Pour chaque $\alpha\in D(s)$, l’état obtenu est $\delta(s,\alpha)$.

La notation $s\xrightarrow{u}s'$ signifie que le mot fini $u\in A^*$ décrit une exécution de $s$ à $s'$.

En particulier, $s\xrightarrow{\epsilon}s$.

Un état $s$ est terminal lorsque $D(s)=\varnothing$.

Une exécution infinie détermine une suite d’états $(s_i)_{i\in\mathbb{N}}$, appelée sa trace.

Une propriété de trace est un ensemble $P\subset S^\omega$.

La relation $s\models P$ signifie que toutes les exécutions infinies issues de $s$ ont leur trace dans $P$.

Elle est donc vraie lorsqu’aucune exécution infinie ne part de $s$.

Un ensemble $I\subset S$ est invariant lorsque toute transition issue de $I$ reste dans $I$.

Une propriété $P\subset S^\omega$ est une propriété de sûreté lorsque toute trace hors de $P$ possède un préfixe fini qu’aucune continuation infinie ne peut rendre compatible avec $P$.

Un tel préfixe est dit interdit.

Il est minimal si aucun de ses préfixes stricts n’est interdit.

On note $\widehat P$ l’ensemble des préfixes interdits minimaux.

La propriété est dite régulière lorsque $\widehat P$ est un langage régulier.

On utilisera le résultat admis suivant : une trace satisfait une propriété de sûreté exactement lorsqu’aucun de ses préfixes n’est dans $\widehat P$.

Pour les programmes OCaml, les représentations sont :

Le type action est supposé défini.

Les états sont les entiers de 0 à size - 1.

La liste next s contient les couples action et état successeur, sans répétition d’action.

Son obtention est supposée de coût constant.

Les comparaisons d’états et d’actions ont également un coût constant.