Title | ||
---|---|---|
Le problème de couverture pour les réseaux de Petri: résultats classiques et développements récents |
Abstract | ||
---|---|---|
RÉSUMÉ. Les réseaux de Petri sont une classe bien étudiée de modèles propres à représenter les comportements de systèmes informatiques concurrents. Dans ce cadre, le problème de cou- verture (étant donné un marquage m, existe-t-il un marquage accessible qui assigne à chaque place du réseau au moins autant de jetons que m ?) est de tout premier intérêt, car de nom- breuses propriétés de sûreté (toutes les exécutions du système resteront-elles dans un ensemble de bons états ?) peuvent y être ramenées. De nombreux travaux ont récemment été consacrés à l'étude d'algorithmes efficaces pour résoudre le problème de couverture. Dans cet article, nous survolons plusieurs de ces travaux classiques ou récents: l'algorithme de Karp et Miller et un algorithme efficace en pratique, qui résolvent le problème de couverture en calculant un ensemble de couverture du réseau; l'approche « en arrière » d'Abdulla et al.; et l'approche « en avant » Expand, Enlarge and Check. Finalement, nous terminons l'article en présentant une nouvelle approche combinant les forces des méthodes « en avant » et « en arrière ». ABSTRACT. Petri nets are a widespread class of models to represent behaviours of concurrent systems. An important problem on Petri nets is the coverability problem (does there exist a reachable marking that assigns to each place at least as many tokens as a given marking m ?), mainly because many safety properties (does the systems always stay inside a set of good be- haviours ?) can be reduced to it. Many recent works have been devoted to the study of efficient algorithms to decide the coverability problem. In this paper, we survey several of these classical or recent works: the Karp and Miller algorithm, and an efficient algorithm, that both solve the coverability problem by computing the coverability set of the net; the "backward" approach of Abdulla et al.; and the Expand, Enlarge and Check "forward" approach. We close the paper by discussing a new method combining the strength of the forward and backward methods. |
Year | DOI | Venue |
---|---|---|
2009 | 10.3166/tsi.28.1107-1142 | Technique et Science Informatiques |
Keywords | Field | DocType |
problème de couverture keywords:petri nets,coverability problem,by discussing a new method combining the strength of the forward and backward me thods. mots-clés :réseaux de petri | Computer science,Algorithm,Humanities,Database | Journal |
Volume | Issue | Citations |
28 | 9 | 1 |
PageRank | References | Authors |
0.35 | 22 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Pierre Ganty | 1 | 242 | 20.29 |
Gilles Geeraerts | 2 | 126 | 15.95 |
Jean-François Raskin | 3 | 1735 | 100.15 |
Laurent Van Begin | 4 | 194 | 11.15 |