Les programmes distribués sont une source de difficulté pour les méthodes formelles. Les interactions de plusieurs composantes provoquent une explosion combinatoire qui complexifie la vérification. Dans le cadre de la synthèse de contrôleurs, à cela s'ajoute le fait que les stratégies d'une composante ne peuvent tenir compte que d'une vision partielle du système. Ceci a mené à de nombreux résultats d'indécidabilité dans le domaine et des complexités très élevées dans les cas décidables. 
Dans cette thèse, nous proposons une approche permettant de décomposer les problèmes de vérification et de synthèse en instances locales aux processus. Cette approche mène à des résultats de décidabilité, et même dans certains cas à des algorithmes de complexités suffisamment basses pour envisager des applications. Nous montrons que cette méthode s'applique dans des systèmes distribués avec une communication restreinte entre les composantes : d'une part des systèmes où la communication se fait via la prise et le relâchement de locks, et d'autre part des systèmes où les processus communiquent par broadcast. De plus, nous utilisons cette approche dans des modèles a priori très différents, où le nombre de processus est constant, évolue dynamiquement, ou encore est paramétré.