Abstract FR:

Nous avons etudie des extensions du modele des reseaux de petri dans le cadre des methodes formelles de verification de systemes paralleles et distribues. Dans le modele standard des reseaux de petri, les transitions incrementent ou decrementent les places. Notre etude porte principalement sur les modeles permettant aussi l'utilisation : _ d'arcs de mise a zero ou reset (qui vident une place) _ d'arcs de transfert (qui transferent le contenu d'une place vers une autre place) _ d'arcs g-post (qui ajoutent a une place p(m) jetons, ou p est un polynome a coefficients non negatifs et m est le marquage courant du reseau) araki-kasami et valk ont montre que l'accessibilite est indecidable pour toutes ces extensions. Pour cinq grandes classes de reseaux, nous avons elargi l'etude a plusieurs autres problemes classiques : la terminaison, la couverture, le caractere borne du reseau ou d'une place, le caractere structurellement borne, le blocage, la vivacite et la t-vivacite. Nous avons dresse une hierarchie detaillee qui a permis de separer (ou regrouper) les classes de reseaux et/ou les problemes. En particulier nous avons mis en evidence de grandes classes de reseaux partiellement analysables. Par exemple, la couverture est decidable pour les reseaux de petri avec reset pour lesquels il n'est pourtant pas possible d'appliquer l'algorithme classique de construction d'un arbre de couverture. Par ailleurs nous avons affine les frontieres entre ce qui est decidable et ce qui ne l'est pas. Par exemple, trois arcs reset suffisent a rendre le caractere borne du reseau indecidable.