Modèle mathématique sous-jacent

Afin de raisonner sur des systèmes dynamiques polynomiaux, il est nécessaire d'utiliser des notions élémentaires d'algèbre. L'idée est de convertir des propriétés exprimées à l'aide d'ensemble d'états ou d'événements en propriétés équationnelles équivalentes. Par la suite, la méthode classique utilisée est de remplacer ces systèmes d'équations par des idéaux de polynômes. On peut alors traduire les propriétés des ensembles par des propriétés sur les idéaux. L'intérêt des équations est de représenter de manière compacte les ensembles manipulés avec un ensemble de méthodes bien établies. Les opérations ensemblistes sont donc remplaçées par des calculs algébriques pour lesquels des algorithmes efficaces ont été implémentés.

Vérification de propriétés

Propriété de vivacité.
On dit qu'un système est vivant si et seulement si il n'est pas jamais en ``dead-lock''. Un état x sera un état mort ou bloquant s'il n'existe pas d'événement admissible dans l'état x . Une trajectoire comportant un état mort est nécessairement finie. Un système vivace implique que toutes les trajectoires de celui-ci sont infinies. En terme de systèmes dynamiques polynomiaux, cette définition peut se décrire de la manière suivante:

Définition: Un système est vivace, si et seulement si pour tous les couples (x,y) tq Q(x,y)=0, P(x,y) est un état qui admet encore des transitions admissibles.

Propriétés de sécurité
Informellement,une propriété de sécurité décrit le fait que de "mauvaises choses" ne peuvent pas se produire. Dans notre cas, cette sorte de propriété couvre la classe des propriétés, décrivant un ensemble de bons états, qui restent invariants. La définition suivante rappelle la définition d'un ensemble d'états invariant.

Définition Un ensemble d'états E est invariant vis à vis d'un système dynamique polynomial, si et seulement si pour chaque état x de E et pour tout événement y admissible dans l'état x, l'état x'= P(x,y) appartient à E.

Un ensemble d'états est dit invariant sous-contrôle pour un système dynamique si et seulement si il est possible de le ``piloter'' en réalisant un choix sur les événements, de manière à rester dans l'ensemble des ``bons états''. Ainsi :
Définition Un ensemble d'états E est invariant sous-contrôle vis à vis d'un système dynamique polynomial, si et seulement si pour chaque état x de E il existe un événement y admissible dans l'état x, tel que l'état x'= P(x,y) appartient à E.

D'autres classes de propriétés peuvent se déduire à partir des propriétés d'invariance et d'invariance sous contrôle.

Propriété d'atteignabilité

Définition Un sous-ensemble F d'états est accessible pour un système dynamique, si et seulement si chaque état x de F peut être atteint à partir des états initiaux du système dynamique considéré (ie, il existe une trajectoire partant des états initiaux qui atteint x).

Définition : Un ensemble d'états F est attractif vis à vis d'un autre ensemble d'états E , si et seulement si, chaque trajectoire du système initialisée dans un état de E atteint l'ensemble F.

Nous avons donné un apercu des méthodes liées à la vérification de propriétés d'états pouvant être réalisées sur les systèmes dynamiques polynomiaux. Cette liste de propriétés n'est cependant pas exhaustive. Il est ainsi possible, en utilisant les mêmes méthodes algébriques d'exprimer des formules CTL , ainsi que des formules propositionelles de mu-calcul.