Vérification de réseaux de Petri avec états sous une sémantique d'ordres partiels

Résumé : Afin de munir le formalisme des MSG de compteurs, de timers et d'autres aspects, nous introduisons le modèle des réseaux de Petri avec états et une sémantique de processus non-branchants. Ce modèle est non seulement plus expressif que les MSG, mais il permet également des spécifications plus concises. Nous nous intéressons à trois problèmes de vérification classiques sur l'ensemble des marquages accessibles par les préfixes des processus : le caractère borné, la couverture et l'accessibilité. Nous montrons comment réduire ces problèmes au cas particulier des réseaux de Petri de telle sorte que tous les résultats de complexité et de décidabilité s'étendent des réseaux de Petri aux réseaux avec états sous la sémantique des processus. Nous introduisons aussi la notion de borne semi-structurelle afin de considérer des systèmes paramétrés. Cela consiste à fixer le marquage initial d'un sous-ensemble approprié de places, puis à vérifier que le système est borné quel que soit les valeurs des paramètres. Nous montrons comment un dépliage conduit à un problème plus simple à vérifier à l'aide de la Programmation Linéaire.
Type de document :
Documents associés à des manifestations scientifiques -- Hal-inria+
MSR 2013 - Modélisation des Systèmes Réactifs, 2013, Rennes, France
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00876642
Contributeur : Hervé Marchand <>
Soumis le : vendredi 25 octobre 2013 - 11:42:17
Dernière modification le : jeudi 18 janvier 2018 - 02:20:54
Document(s) archivé(s) le : vendredi 7 avril 2017 - 17:40:30

Fichier

Avellaneda.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00876642, version 1

Collections

Citation

Florent Avellaneda, Rémi Morin. Vérification de réseaux de Petri avec états sous une sémantique d'ordres partiels. MSR 2013 - Modélisation des Systèmes Réactifs, 2013, Rennes, France. 〈hal-00876642〉

Partager

Métriques

Consultations de la notice

117

Téléchargements de fichiers

1500