Réification des accélérations pour la construction de Karp et Miller - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

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.
Fichier principal
Vignette du fichier
msr19.pdf (522.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02319755 , version 1 (18-10-2019)

Identifiants

  • HAL Id : hal-02319755 , version 1

Citer

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⟩
51 Consultations
111 Téléchargements

Partager

Gmail Facebook X LinkedIn More