Distributed programs are a cause of difficulty for formal methods. The interactions of multiple components lead to a combinatorial explosion, which complicates verification. In the context of controller synthesis, this is further compounded by the fact that the strategies of one component can only take into account a partial view of the system. This has led to numerous undecidability results in the field and very high complexities in decidable cases.
In this thesis, we propose an approach that allows the decomposition of verification and synthesis problems into local instances for individual processes. This approach leads to decidability results, and in some cases, to algorithms with low enough complexity to consider practical applications. We show that this method applies to distributed systems with restricted communication between components: on the one hand, systems where communication is limited to the acquisition and release of locks, and on the other hand, systems where processes communicate via broadcast. Moreover, we apply this approach to models that are quite different, where the number of processes is constant, evolves dynamically, or is parameterised.