Dans la première partie de cette thèse, nous présentons une implémentation du langage fp2 ayant pour modèle les réseaux de Petri. Fp2 est un langage de programmation parallèle base sur la réécriture de termes et les spécifications algébriques. Nous donnons une nouvelle sémantique a fp2, de la famille des sémantiques du vrai parallélisme, et prouvons la correction de cette sémantique par rapport a la sémantique interleaving du langage. Le modèle utilise, les réseaux de Petri, et la nouvelle sémantique donnée au langage permettent une représentation plus compacte de programmes complexes, évitant les problèmes d'explosion combinatoire rencontres avec les implémentations précédentes. Nous évaluons le gain de notre approche, et proposons plusieurs schémas d'interprétation du langage, bases sur cette nouvelle sémantique. La seconde partie de ce travail concerne la définition d'une nouvelle famille d'équivalences comportementales pour les réseaux de Petri. Alors que les équivalences proposées jusqu'alors sont définies entre les marquages, c'est-a-dire entre les états globaux du réseau, nous définissons une relation entre les places du réseau, reprenant une idée proposée par olderog. De nouvelles équivalences, les bisimulations de places, sont proposées a partir de cette définition. Un algorithme efficace (polynomial) permettant de calculer la plus grande bisimulation de places sur un réseau est propose. Nous montrons comment simplifier un réseau en le quotientant par cette plus grande bisimulation, obtenant ainsi un représentant canonique d'une classe d'équivalence de réseaux bisimilaires de places. L'étude de ces équivalences est ensuite étendue aux réseaux avec actions internes
Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00343578 |
Date | 10 May 1993 |
Creators | Autant, Cyril |
Source Sets | CCSD theses-EN-ligne, France |
Language | French |
Detected Language | French |
Type | PhD thesis |
Page generated in 0.0017 seconds