Sujet : Dépliage de réseaux de Petri généraux.



Responsable : Jean-Michel Couvreur et Pascal Weil
Téléphone : 05 40 00 69 34 & 05 40 00 69 28

e-mail : couvreur@labri.fr et weil@labri.fr

Présentation du sujet : Une des causes principales du problème de l'explosion combinatoire de la vérification de systèmes est la représentation de la concurrence par entrelacement. Des méthodes (ensembles persistants) évitent d'explorer l'ensemble de l'espace d'états lors de la vérification en opérant des réductions basées sur la sémantique de l'ordre partiel du système tout en préservant certaines propriétés de l'entrelacement. Une autre approche consiste à réaliser la vérification directement sur une représentation explicite de l'ordre partiel. Les processus arborescents (ou dépliages) proposent une sémantique arborescente de l'ordre partiel pour les réseaux de Petri. McMillan a montré comment les processus arborescents peuvent être efficacement employés pour la détection des inter-blocages et le problème de l'accessibilité dans le cas des réseaux de Petri dont l'espace d'états est fini. Il a décrit la construction d'un processus arborescent fini contenant l'ensemble des états accessibles. Récemment, nous avons généralisé cette technique aux réseaux Petri généraux.
L'objectif du projet est d'implémenter cette nouvelle technique et d'en évaluer l'efficacité.

Mot-clés : Model-checking, dépliages, réseaux de Petri.

Références :

Commentaires éventuels :