We consider the distributed control synthesis problem for systems with locks. The goal is to find local controllers so that the global system does not deadlock. With no restriction this problem is undecidable even for three processes each using a fixed number of locks. We propose two restrictions that make distributed control decidable. The first one is to allow each process to use at most two locks. The problem then becomes Sigma2P-complete, and even in PTIME under some additional assumptions. The dining philosophers problem satisfies these assumptions. The second restriction is a nested usage of locks. In this case the synthesis problem is NEXPTIME-complete. The drinking philosophers problem falls in this case.

翻译：本文研究带锁系统的分布式控制综合问题，目标是通过设计局部控制器来确保全局系统不发生死锁。若无约束条件，即使每个进程仅使用固定数量的锁，该问题在三个进程的情况下也是不可判定的。我们提出了两种使分布式控制可判定的约束方案。第一种方案限制每个进程最多使用两个锁，此时问题具有Sigma2P完全复杂度，在特定附加假设下甚至存在多项式时间解法。哲学家就餐问题即满足此类假设。第二种方案要求锁的使用具有嵌套结构，此时综合问题具有NEXPTIME完全复杂度。饮酒哲学家问题属于此类情形。