Hugo Gimbert ; Corto Mascle ; Anca Muscholl ; Igor Walukiewicz - Distributed controller synthesis for deadlock avoidance

lmcs:10965 - Logical Methods in Computer Science, September 3, 2025, Volume 21, Issue 3 - https://doi.org/10.46298/lmcs-21(3:24)2025
Distributed controller synthesis for deadlock avoidanceArticle

Authors: Hugo Gimbert ; Corto Mascle ; Anca Muscholl ; Igor Walukiewicz

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.


Volume: Volume 21, Issue 3
Published on: September 3, 2025
Accepted on: May 12, 2025
Submitted on: February 15, 2023
Keywords: Logic in Computer Science
Funding:
    Source : OpenAIRE Graph
  • FoRmal mEthods for the Design of Distributed Algorithms; Funder: French National Research Agency (ANR); Code: ANR-17-CE40-0013

Consultation statistics

This page has been seen 856 times.
This article's PDF has been downloaded 346 times.