Les signaux

Dans le but de modéliser son comportement, un processus Signal est traduit en un système d'équations polynomiales sur les entiers modulo 3 : { -1, 0, 1} . Le principe est de coder les trois valeurs possibles d'un signal booléen A (i.e. present et true, present et false et absent) en une variable a de la manière suivante :

1. Un booléen présent et true est codé par la valeur 1
2. Un booléen présent et faux est codé par la valeur -1
3. Un booléen absent est codé par la valeur 0

Pour les signaux non-booléens dont la valeur ne peut pas être représentée,seule l'absence et la présence sont codées:

1. Un signal non booléen présent est codé par 1
2. Un signal non booléen absent est codé par 0

Par ce codage, un événement sur n signaux est représenté par un vecteur dans (F₃)ⁿ. De plus, la présence d'un signal est codée par la valeur 1. Par conséquent un signal A est synchrone avec un signal B si et seulement si ils satisfont l'équation a² = b².

Les processus primitifs

Chaque opérateur élémentaire du noyau Signal peut ainsi être codé sous forme équationnelle. Par exemple, C := A when B, signifiant : if b=1 then c=a else c=0, est réécrit c = a(b-b²).

Le délai $, qui est l'opérateur dynamique, est différent, car il requiert la mémorisation de la dernière valeur dans une variable d'état. Ainsi pour coder A := B$1 init A0, il est nécessaire d'introduire les trois équations suivantes:

L'équation (1) permet de calculer la nouvelle valeur x' de la variable d'état. Si b est présent, x' est égal à b (parceque (1-b²)=0 ); autrement x' est égal à la dernière valeur de b, mémorisé par x. L'équation (2) donne à a la dernière valeur de b (i.e. la valeur de x) et contraint l'horloge de a à être égale à celle de b. En effet, on a a²= x²b⁴ , et dans F₃ nous avons b³ = b , i.e. b⁴ = b² , ceci donne donc a²= x²b² ; Comme de plus x² = 1 (car x est toujours présent), et finalement a² = b² . L'équation (3) correspond à la valeur initiale de x, qui est la valeur initiale de a.

Certains opérateurs peuvent être codés de deux façons suivant le type des signaux. L'ensemble des codages est donné par la table suivante :

Les processus

En composant les différentes équations résultantes des différents processus élémentaires, tout programme Signal peut être traduit en un ensemble d'équations, appelé système dynamique polynomial. En utilisant ce codage, un processus est donc traduit en un système d'équations de la forme :

Ce système est constitué

• d'un ensemble de n variables X = { X₁,...,X_n} appelées variables d'états;
• d'un ensemble de m variables Y = { Y₁,...,Y_m} , appelées variables d'événements ,
• d'un ensemble de contraintes Q(X,Y)=0. Il est représenté par un vecteur [Q₁,..,Q_l], regroupant toutes les équations caractérisant l'aspect statique du système (invariant pour tout les instants t);
• d'une fonction d'évolution P(X,Y) de (F₃)^n+m dans (F₃)ⁿ. Cet ensemble regroupe toutes les équations concernant les variables d'états et caractérise l'aspect dynamique du système;
• d'un ensemble de n équations [Q₀₁,..,Q_0n] , appelées contraintes d'initialisation notées Q₀(X) = 0 et caractérisant l'initialisation des variables d'états du système. Quand la contrainte initiale n'est pas précisée, il s'agit d'un système dynamique polynomial pour lequel tous les états sont des états initiaux, ce qui revient à prendre Q₀ = 0 .

Les X proviennent de la traduction des signaux retardés, les Y représentent les signaux booléens et les horloges du programme. Le système dynamique décrit les suites de couples états / événements que peut produire le programme, c'est à dire les suites (x_i,y_i)_i telles que Q₀(x₀) = 0 . Ces suites sont appelées les trajectoires du système. Un couple x,y tel que Q(x,y) = 0 est dit admissible ; on dira aussi qu'un état x est admissible s'il existe un y tel que Q(x,y) = 0. Si x et x' sont deux états et qu'il existe un y tel que Q(x,y) = 0 et x' = (x,y), on dira que x' est un successeur de x et réciproquement que x est un prédécesseur de x'.

Exemple

Le programme Signal suivant,

est codé par un système dynamique polynomial comprenant les variables a, b, c et zc, correspondant respectivement aux événements A, B et aux signaux booléens C et ZC, et une variable d'état x, introduite par le delai. Le système obtenu est le suivant :

1. une équation d'évolution : x = -1,
2. une équation d'évolution : x' = c + (1-c²)*x
3. un système d'équations de contraintes : c = -zc, zc = x*c², a²= when c, b² = when zc

Système de transition résultant

Un système dynamique polynomial peut également être vu comme un système de transition fini. Les états initiaux de l'automate sont les solutions de l'équation Q₀(X) = 0 . Quand le système est dans l'état x de (F₃)ⁿ, tout événement y de (F₃)^m tels que Q(x,y))=0 constitue une transition qui peut être tirée. Dans ce cas le système évolue dans l'état x' tel que x'=P(x,y).