We apply model checking of knowledge properties to the design of distributed controllers that enforce global constraints on concurrent systems.The problem of synthesizing a distributed controller is, in general, undecidable, and the local knowledge of the processes may not directly suffice to control them to achieve the global constraint. We calculate when processes can decide, autonomously, to take or block an action so that the global constraint will not be violated. When the separate processes cannot make this decision alone, it may be possible to coordinate several processes in order to achieve more knowledge together and make combined decisions. A fixed coordination will severely degrade the concurrency; thus, the coordinations we use are temporary. Since the overhead for such coordinations is expensive, we strive to minimize their number, again using model checking. We show how this framework is applied to the design of controllers that guarantee a priority policy among transitions.