Abstract FR:

Les reseaux de petri (en abrege, rdp) sont un modele eprouve pour l'etude des systemes distribues et concurrents, de meme que leur modele de base, les systemes de reseaux elementaires. Ils permettent en particulier une representation correcte des relations causales entre differentes actions d'un systeme. Cette these est consacree a l'etude des comportements de ces deux types de reseaux. Le comportement concurrent d'un reseau est decrit par l'ensemble des mots partiels associes a ses executions concurrentes, les comportements sequentiels par les langages finitaires ou infinitaires qui lui sont associes. Nous prouvons la definissabilite dans la logique monadique du second ordre de buchi des comportements concurrents et sequentiels (finis et infinis) des systemes de reseaux elementaires. Pour des rdp, nous definissons une extension naturelle de cette logique et obtenons la definissabilite de tous leurs comportements dans celle-ci. Dans le cas sequentiel, nous montrons que la reciproque est vraie: les formules existentielles de ces deux logiques peuvent etre utilisees comme langage de specification. On peut de plus construire automatiquement le reseau a partir de la formule qui specifie son comportement. Nous indiquons pourquoi ceci n'est pas possible dans le cas concurrent. Les preuves de ces resultats concernant les rdp reposent sur une propriete structurelle: apres avoir introduit la notion de rdp normalise, nous exhibons un algorithme de normalisation qui preserve tous les types de comportements (sequentiel fini et indefini, concurrent). Nous etudions egalement des proprietes de cloture des classes de reseaux pour un type de comportement donne. Nous montrons notamment que le complement du langage d'un rdp a etiquetage deterministe est toujours un langage de rdp, alors que la classe des langages de tous les rdp n'est pas close par complementation