Laboratoire d'Informatique de Grenoble

Résumé
Dans le cadre de la vérification des systèmes concurrents, nous étudions les réseaux de Petri et une de leurs extensions, les NUPN (acronyme anglais de « réseaux de Petri à unités imbriquées »), qui leur apportent modularité et hiérarchie par une structure en processus séquentiels, imbriqués sous la forme d’un arbre.

Nous proposons diverses techniques permettant de résoudre plusieurs questions relatives aux réseaux de Petri et aux NUPN. D'abord, nous exposons des approches pour décider efficacement l'isomorphisme des réseaux de Petri et des NUPN. Puis, nous définissons des algorithmes pour détecter les places mortes et les transitions mortes, ce qui permet l'élimination du code mort, ainsi que des algorithmes pour détecter les places concurrentes, qui donnent des informations sur la concurrence des réseaux. Enfin, nous abordons la traduction automatisée des réseaux de Petri en réseaux d'automates communicants, en NUPN avec des processus imbriqués, ou en différentes algèbres de processus. Ces algorithmes ont été implantés et testés sur de grandes collections de réseaux d’origine académique, industrielle, ou provenant de compétitions internationales.