Abstract FR:

Cette thèse porte sur la spécification logique de systèmes concurrents et la synthèse d'un modèle : les systèmes sont les réseaux de Petri non étiquetés et les spécifications sont des formules temporelles. Par l'introduction des réseaux de compteurs et de formules de " test à zéro " d'un compteur, nous réduisons le problème indécidable de la vacuité du langage d'une machine à deux compteurs à celui de la synthèse de réseau à partir d'une formule du Mu-Calcul. Nous affaiblissons la logique en le Nu-Calcul Conjonctif (NCC), et nous lui associons un reconnaisseur, les spécifications modales ; nous en exhibons une sous-classe pour laquelle la synthèse est décidable. Nous introduisons la théorie structurelle d'un réseau donné, exprimable en NCC, dont les modèles sont tous les réseaux qui contiennent le premier. Grâce à cette théorie, nous établissons l'indécidabilité de la synthèse pour le NCC par réduction du problème de l'exécution bornée d'une machine à compteurs.