Réseaux de Petri stochastiques bien formés

Définition

(Réseaux ordonnés)

Un réseau bien formé est un réseau ordonné si il vérie les mêmes contraintes qu’un réseau régulier excepté le fait qu’il peut faire intervenir la fonction successeur (!XCi ) mais pas la fonction de diusion. Les fonctions autorisées sur une classe sont donc :XCi et !XCi.

Le graphe symbolique d’accessibilité

La puissance du modèle réseau de Petri bien formé provient de ce qu’il autorise la dénition et le calcul automatique d’une version réduite du graphe d’accessibilité à partir de la dénition même du réseau sans le calculer préalablement.
Le schéma de la démarche [9] est le suivant :
dénition de classes d’états identiques à une symétrie de couleur près : les marquages symboliques ;
dénition d’une représentation unique de ces marquages symboliques, appelée représentation canonique ;
dénition d’une règle de franchissement symbolique fondée sur ces représentations : un franchissement symbolique d’un marquage symbolique vers un autre condense un ensemble de franchissements ordinaires.
On construit ainsi, le graphe symbolique d’accessibilité qui est une version condensée du graphe d’accessibilité du réseau.
Pour la version stochastique du modèle (SWN), ce graphe dénit une agrégation markovienne de la CTMC du réseau. Cette agrégation permet de retrouver les probabilités à l’équilibre des états ordinaires.
Ces propriétés sont fondées sur les symétries du système modélisé qui se traduisent dans la structure régulière des éléments qui constituent le modèle.
La formalisation de ces symétries est la notion de permutation de couleur. Un permutation doit laisser stables les sous-classes statiques et être compatible avec l’opérateur successeur. Le lecteur pourra consulter les références [2, 9] pour plus de détails sur les permutations.
Les WN mettent en avant les symétries du système modélisé. L’idée du graphe de marquage symbolique (GMS) est de prendre en compte ces symétries dans la construction de l’ensemble des marquages accessibles an d’en obtenir une représentation compacte [2, 7]. Cette représentation repose sur les concepts de marquage symbolique et de franchissement symbolique que nous dénissons dans la suite.

Représentation d’un marquage symbolique

Dans le cas général, il n’existe pas de méthode eective pour choisir la représentation d’un marquage symbolique. Si l’on choisit d’utiliser un marquage quelconque de la classe comme représentant (par exemple le premier rencontré), alors pour chaque nouveau marquage construit, il faut tester (à l’aide de l’ensemble des symétries ξ) s’il est équivalent à un autre marquage.
Ce test est généralement très coûteux à eectuer. On propose alors d’utiliser pour une classe d’équivalence de marquages une représentation générique [2]. Le concept de représentation canonique est utilisé pour garantir l’unicité de la représentation générique et le test d’équivalence entre les marquages peut alors être remplacé par un test d’égalité. La représentation choisie utilise le fait que les valeurs de couleurs d’un marquage symbolique ne sont pas très importantes mais plutôt la distribution des valeurs dans les places.
Ces représentations sont utilisées dans les outils pour pouvoir manipuler les marquages symboliques. Ce sont des descriptions de haut niveau puisqu’elles indiquent, pour chacun des marquages du marquage symbolique ce que doit être le marquage coloré pour chaque place.

Définition 

(Graphe symbolique d’accessibilité)

Le graphe symbolique d’accessibilité (Symbolic Reachability Graph, SRG) d’un WN est le graphe dont les noeuds sont les éléments de l’ensemble symbolique d’accessibilité et les arcs les franchissements symboliques.
Un arc dans le graphe symbolique d’accessibilité (appelé franchissement symbolique) représente un ensemble de franchissements des instances de transition toutes franchissables dans chaque marquage ordinaire du marquage symbolique. Avec des systèmes présentant plusieurs entités ayant un comportement identique, le SRG fournit une représentation réduite du graphe d’accessibilité du réseau coloré.
Nous pouvons maintenant donner la dénition des réseaux de Petri stochastiques bien formés.

Réseaux de Petri stochastiques bien formés (SWN)

Sémantique stochastique d’un réseau de Petri bien formé

L’introduction d’une sémantique stochastique pour un réseau de Petri bien formé vise trois objectifs :
être consistante avec la sémantique stochastique des réseaux de Petri,
permettre à l’utilisateur de la spécier au niveau du réseau bien formé,
préserver la symétrie de telle sorte que le graphe symbolique d’accessibilité (GAS) (Symbolic Reachability Graph, SRG) puisse servir de support à une évaluation quantitative.
La manière la plus simple consiste à dénir la sémantique stochastique comme étant celle du réseau de Petri (stochastique) déplié. Ceci sut à assurer une définition cohérente d’une extension stochastique des réseaux de Petri bien formés.
Un réseau stochastique bien formé (Stochastic Well formed Net, SWN ) est un réseau bien formé dont les transitions possèdent un attribut supplémentaire qui correspond à un délai de franchissement. Le délai de franchissement associé à une transition peut être soit distribué suivant une loi exponentielle (transition temporisée), soit nul (transition immédiate). La politique de choix de la transition à franchir sera celle du plus court délai tiré si aucune transition immédiate n’est franchissable et une sélection probabiliste conditionnée par le poids des transitions immédiates franchissables sinon ; par contre le choix de la politique de mémoire est sans importance ici puisque nous utilisons des lois exponentielles et immédiates.
Rappelons que les SW N autorisent des dépendances des paramètres stochastiques vis à vis du marquage courant. Nous pouvons simuler alors une politique innite-server par une politique single-server en utilisant le fait que le minimum de k variables aléatoires exponentielles de taux λ est une variable aléatoire de taux k.λ.

Définition des réseaux de Petri stochastiques bien formés

An de formaliser la restriction des dépendances fonctionnelles, nous introduisons la notion de domaine de sous-classes statiques correspondant à un domaine de couleurs et l’image d’une couleur dans le domaine correspondant.
Ceci permettra de dénir des taux de franchissement en ne tenant compte que des projections de l’instance de franchissement et du marquage courant sur les sous-classes statiques. Dénition 2.1.17 (Graphe symbolique d’accessibilité) Le graphe symbolique d’accessibilité (Symbolic Reachability Graph, SRG) d’un WN est le graphe dont les noeuds sont les éléments de l’ensemble symbolique d’accessibilité et les arcs les franchissements symboliques.
Un arc dans le graphe symbolique d’accessibilité (appelé franchissement symbolique) représente un ensemble de franchissements des instances de transition toutes franchissables dans chaque marquage ordinaire du marquage symbolique. Avec des systèmes présentant plusieurs entités ayant un comportement identique, le SRG fournit une représentation réduite du graphe d’accessibilité du réseau coloré.
Nous pouvons maintenant donner la dénition des réseaux de Petri stochastiques bien formés. Réseaux de Petri stochastiques bien formés (SWN)

Sémantique stochastique d’un réseau de Petri bien formé

L’introduction d’une sémantique stochastique pour un réseau de Petri bien formé vise trois objectifs :
être consistante avec la sémantique stochastique des réseaux de Petri,
permettre à l’utilisateur de la spécier au niveau du réseau bien formé,
préserver la symétrie de telle sorte que le graphe symbolique d’accessibilité (GAS) (Symbolic Reachability Graph, SRG) puisse servir de support à une évaluation quantitative.
La manière la plus simple consiste à dénir la sémantique stochastique comme étant celle du réseau de Petri (stochastique) déplié. Ceci sut à assurer une dénition cohérente d’une extension stochastique des réseaux de Petri bien formés.
Un réseau stochastique bien formé (Stochastic Well formed Net, SWN ) est un réseau bien formé dont les transitions possèdent un attribut supplémentaire qui correspond à un délai de franchissement. Le délai de franchissement associé à une transition peut être soit distribué suivant une loi exponentielle (transition temporisée), soit nul (transition immédiate). La politique de choix de la transition à franchir sera celle du plus court délai tiré si aucune transition immédiate n’est franchissable et une sélection probabiliste conditionnée par le poids des transitions immédiates franchissables sinon ; par contre le choix de la politique de mémoire est sans importance ici puisque nous utilisons des loisexponentielles et immédiates.
Rappelons que les SW N autorisent des dépendances des paramètres stochastiques vis à vis du marquage courant. Nous pouvons simuler alors une politique innite-server par une politique single-server en utilisant le fait que le minimum de k variables aléatoires exponentielles de taux λ est une variable aléatoire de taux k.λ.

Définition des réseaux de Petri stochastiques bien formés

An de formaliser la restriction des dépendances fonctionnelles, nous introduisons la notion de domaine de sous-classes statiques correspondant à un domaine de couleurs et l’image d’une couleur dans le domaine correspondant.
Ceci permettra de dénir des taux de franchissement en ne tenant compte que des projections de l’instance de franchissement et du marquage courant sur les sous-classes statiques.