Ordre bien fondé sur les états

Ordre bien fondé sur les états

Un état d’accueil d’an système est un état qu’il est toujours possible d’atteindre, quelle que soit l’évolution de ce système. Ce concept a été introduit par Keller[3G] pour les systèmes de transitions, et il a proposé le concept de norme (inspiré de Floyd) comme outil de preuve. Une norme est une fonction à valeurs entières définie sur les états, qui vaut zéro sur l’état d’accueil et qu’il est toujours possible de faire décroître. La notion d’espace d’accueil est une généralisation de celle d’état d’accueil due à Memmi[42,43]: au lieu de pouvoir toujours atteindre un état fixé, on peut toujours atteindre un état appartenant à un ensemble fixé (c-à-d, un état vérifiant une certaine propriété). La vérification d’espace d’accueil joue un rôle essentiel dans l’analyse des réseaux de Petri car il s’agit de montrer qu’on peut toujours atteindre une certaine propriété: cette notion est utile dans la preuve de propriétés temporelles des systèmes. Memmi avait donné une autre méthode de preuve que la norme: preuve par raffinements successifs qui consiste en des réductions successives d’un espace con­ tenant tous les marquages accessibles pour arriver à l’espace donné. Dans sa thèse, Johnen[35] a étudié la décidabilité et la vérification automatique des es­ paces d’accueil (utilisant des techniques de réécriture), et a proposé un algorithme qui est une formalisation et une automatisation de cette méthode. Cet algorithme prend en entrée l’espace global G (contenant tous les marquages accessibles) défini par des équations linéaires des marquages (égalités et inégalités) et l’espace E .

Nous visons à munir les espaces d’accueil de méthodes de preuve composi- tionnelles. Nous proposons un nouveau concept de norme qui réunit ces deux méthodes: nous conservons la notion de norme qui est une fonction sur les mar­ quages, mais en plus, ces normes peuvent représenter le passage d’un ensemble d’états à un autre et donc un pas de la preuve par raffinements successifs: une norme qui prouve l’existence de l’espace d’accueil est la composition de ces normes. Ainsi ces normes sont munies d’opérateurs de composition qui permettent de les construire par raffinements successifs, et en plus, de construire la norme d’une composition de réseaux en composant leurs normes (dans certaines conditions). Dans la première section, la définition d’un espace d’accueil est rappelée, et nous donnons une caractérisation de cette propriété en termes d’ordre bien fondé. Dans la deuxième section, nous définissons un nouveau concept de norme, avec un cas particulier: les normes linéaires. Ces normes sont des applications de La troisième section présente les opérations de composition de normes. La première est l’ordonnancement de normes, qui correspond à la preuve d’espace d’accueil par réductions successives d’un espace global. La deuxième opération est la somme de norme, qui permet de montrer que l’intersection de deux espaces d’accueil en est un, si une certaine condition « d’indépendance » est vérifiée. La quatrième section est consacrée à la vérification hiérarchique des normes. Nous définissons la preuve d’une norme et la composition de ces preuves. Une méthode de réutilisation de preuve dans la vérification de normes est illustrée par des exemples au moyen de ces notions.

D’autre part, les espaces d’accueil sont utilisables dans la preuve de certaines relations synchroniques. Si on veut prouver que les occurrences de deux transitions a et b forment un langage de parenthèses dont le niveau d’imbrication est borné par n, il suffit d’ajouter une place p entre a et 6, de montrer que p est implicite et bornée par n, puis que E = {M; M(p) = 0} est un espace d’accueil. Dans tous les cas, un pas de preuve d’espace d’accueil consiste à montrer qu’il existe une séquence menant d’un ensemble d’états à un autre ensemble d’états d’ordre strictement inférieur. Le concept de norme que nous définissons représente ce pas de preuve, et répond au souci d’avoir un outil maniable de preuve qui se prête à la composition. Notons que la norme est définie pour un réseau non marqué, et que c’est uniquement une relation d’accessibilité. Pour ordonner les états, nous considérons des normes qui sont des applications à valeurs dans N* muni de l’ordre lexicographique. Le choix de cet ordre est justifié par la définition des normes linéaires et les compositions de normes définies dans la suite.