Skip to Main content Skip to Navigation
Conference papers

Réification des accélérations pour la construction de Karp et Miller

Résumé : L'algorithme de Karp et Miller est basé sur une exploration de l’arbre d’accessibilité d’un réseau de Petri où on accélère les séquences de transitions à incidence positive.Les nœuds de l’arbre de Karp et Miller sont étiquetés par un ensemble d’ω-marquages représentant l’ensemble (potentiellement infini) de couverture Cover. Cet ensemble d’ω-marquages permet de décider la couverture d’un marquage ou la finitude de l’ensemble d’accessibilité. Les arcs de l’arbre de Karp et Miller sont étiquetés par des transitions mais la sémantique de celles-ci n’est pas toujours la sémantique de base ce qui rend la preuve de l’algorithme relativement compliquée. Nous introduisons ici trois nouveaux concepts :l’abstraction, l’accélération et la séquence d’exploration. En particulier, nous généralisons la définition des transitions auxω-transitions afin de pouvoir représenter une accélération par une ω-transition. La notion d’abstraction permet de simplifier grandement la preuve de correction de l’algorithme de Karp et Miller. D’autre part, au prix d’un surcoût minime en mémoire, évalué théoriquement, nous proposons une variante « accélérée » de l’algorithme de Karp et Miller avec un gain escompté en temps d’exécution et dont la preuve de correction se déduit très simplement de notre preuve de l’algorithme de Karp et Miller.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-02319755
Contributor : Igor Khmelnitsky <>
Submitted on : Friday, October 18, 2019 - 11:32:43 AM
Last modification on : Friday, April 30, 2021 - 10:05:13 AM
Long-term archiving on: : Sunday, January 19, 2020 - 1:46:43 PM

File

msr19.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02319755, version 1

Citation

Alain Finkel, Serge Haddad, Igor Khmelnitsky. Réification des accélérations pour la construction de Karp et Miller. MSR 2019 - 12ème Colloque sur la Modélisation des Systèmes Réactifs, Nov 2019, Angers, France. ⟨hal-02319755⟩

Share

Metrics

Record views

91

Files downloads

471