Abstract FR:

Cette thèse présente un formalisme logique pour la synthèse de contrôleurs des systèmes à événements discrets. Ce formalisme est obtenu par quantification des propositions atomiques dans les formules de la logique Mu-calcul. Cette approche logique permet la spécification formelle et uniforme de divers problèmes de contrôle. Différents critères de contrôle, comme la permissivité maximale, sont requis de manière simple. La synthèse de contrôleurs est obtenue par vérification des spécifications, en utilisant la théorie des automates d'arbres ainsi que la théorie des jeux de parité.