Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf

Résumé : Pour la vérification formelle des systèmes dynamiques concurrents ou coopérants modélisés à l’aide des réseaux de Petri, la méthode du dépliage est utilisée pour endiguer le phénomène bien connu de l’explosion combinatoire. Une extension de la méthode aux réseaux de Petri temporels à modèle sous-jacent non sauf est présentée. Le dépliage obtenu est simplement un préfixe de celui du réseau de Petri ordinaire sous-jacent au réseau temporel. Pour une certaine classe de réseaux temporels, un préfixe fini capturant l’espace d’état et le langage temporisé découle du calcul d’un ensemble fini de processus finis réalisables. Les contraintes temporelles quantitatives associées à ces processus peuvent servir à valider plus efficacement les spécifications temporelles d’un système temps réel dur.
Type de document :
Article dans une revue
Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, INRIA, 2011, 14, pp.185-203
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01299417
Contributeur : Coordination Episciences Iam <>
Soumis le : jeudi 7 avril 2016 - 16:12:14
Dernière modification le : mercredi 16 mai 2018 - 11:48:03
Document(s) archivé(s) le : lundi 14 novembre 2016 - 21:13:28

Fichier

Vol.14.pp.185-203.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : hal-01299417, version 1

Collections

Citation

M. Sogbohossou, D. Delfieu. Dépliage des réseaux de Petri temporels à modèle sous-jacent non sauf. Revue Africaine de la Recherche en Informatique et Mathématiques Appliquées, INRIA, 2011, 14, pp.185-203. 〈hal-01299417〉

Partager

Métriques

Consultations de la notice

134

Téléchargements de fichiers

186