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

    Consultation statistics

    This page has been seen 615 times.
    This article's PDF has been downloaded 158 times.