论文标题
分布式控制器合成以避免僵局
Distributed controller synthesis for deadlock avoidance
论文作者
论文摘要
我们考虑带有锁的系统的分布式控制合成问题。目的是找到本地控制器，以使全球系统不会僵局。在没有限制的情况下，即使对于三个过程，都使用固定数量的锁，也无法确定。我们提出了两个使分布式控制可决定的限制。第一个是允许每个过程最多使用两个锁。然后，问题变成$σ_2^p $ - complete，甚至在ptime中，在一些其他假设下也是如此。用餐哲学家的问题满足了这些假设。第二个限制是锁的嵌套用法。在这种情况下，合成问题是nexptime-complete。在这种情况下，饮酒哲学家的问题落在。
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 $Σ_2^P$-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.
