Réseaux de Petri à Paramètres Discrets

With the aim of increasing the modelling capability of Petri nets, wesuggest that models involve parameters to represent the weights of arcs, or the number of tokensin places. We consider the property of coverability of markings. Two general questions arise,the universal and the existential one: “Is there a parameter value for which the property issatisfied?” and “Does the property hold for all possible values of the parameters”. We showthat these issues are undecidable in the general case. Therefore, we also define subclasses ofparameterised nets, depending on whether the parameters are used on places, input or outputarcs of transitions. For some classes, we prove that universal and existential coverability becomedecidable, making these classes more usable in practice. To complete this study, we prove thatthose problems are ExpSpace-complete. We also address a problem of parameter synthesis,that is computing the set of values for the parameters such that a given marking is coverablein the instantiated net. Restricting parameters to only input weights (preT-PPNs) provides adownward-closed structure to the solution set. We therefore invoke a result for the representationof upward closed set from Valk and Jantzen. The condition to use this procedure is equivalentto decide the universal coverability. We also propose an adaptation of this reasoning to thecase of parameters used only as output weights (postT-PPNs). In this case, the condition touse this procedure can be reduced to the decidability of the existential coverability. Finally,we broaden this study by establishing decision frontiers through the study of existential anduniversal reachability.Afin de permettre une modélisation plus souple des systèmes, nous proposons d’étendre les réseaux de Petri par des paramètres discrets représentant le poids des arcsou le nombre de jetons présents dans les places. Dans ce modèle, tout problème de décision peutêtre décliné sous deux versions, une universelle, demandant si la propriété considérée est vraiequelles que soient les valeurs que prennent les paramètres et une existentielle, qui s’interroge surl’existence d’une valeur pour les paramètres telle que la propriété soit satisfaite. Concernantla couverture, nous montrons que ces deux problèmes sont indécidables dans le cas général.Nous introduisons donc des sous classes syntaxiques basées sur la restriction des paramètres auxplaces, aux arcs en sortie ou aux arcs en entrée des transitions. Dans ces différents cas, nousmontrons que la couverture existentielle et universelle sont décidables et EXPSPACE-complètes.Nous étudions alors le problème de la synthèse de paramètres qui s’intéresse à calculer l’ensembledes valeurs de paramètres telles que la propriété considérée soit vraie. Sur les sous classes introduites, concernant la couverture, nous montrons que les ensembles solutions à la synthèseont des structures fermée supérieurement (cas des arcs de sortie) et fermée inférieurement (casdes arcs d’entrée). Nous prouvons alors que ces ensembles se calculent par un algorithme dela littérature, proposé par Valk et Jantzen, dont les conditions d’application se réduisent auxproblèmes de décision étudiés précédemment. Enfin nous étudions les frontières de décision ennous intéressant aux versions paramétrées de l’accessibilité pour ces sous classes