一句话：提出两种限制使带锁系统的分布式死锁避免控制器合成可判定，并刻画其精确复杂度。
本文研究带锁系统的分布式控制器合成问题：为各进程寻找局部控制器，使得全局系统不会死锁。无限制时该问题不可判定，即使三个进程各自使用固定数量的锁亦然。作者提出两种使问题可判定的限制。第一种限制每个进程最多使用两把锁，此时问题为 Σ₂^P-完全，并在若干附加假设下落入 PTIME；哲学家就餐问题满足这些假设。第二种限制是锁的嵌套使用，相应合成问题为 NEXPTIME-完全；饮酒哲学家问题属于此类。工作通过可判定性与复杂度分析，划定了分布式死锁避免控制器合成的可处理边界。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2204-12409,
title = {Distributed controller synthesis for deadlock avoidance},
author = {Hugo Gimbert and Corto Mascle and Anca Muscholl and Igor Walukiewicz},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:24)2025}
}