Distributed controller synthesis for deadlock avoidance

2022/04/26 by Gimbert, Hugo, Corto Mascle, Mascle, Corto +4 · 1 citation
Computer Science · Engineering · #Petri Nets in System Modeling #Formal Methods in Verification #Stability and Control of Uncertain Systems

paper · doi:10.48550/arxiv.2204.12409

Abstract

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 Σ₂^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.

Cited by

• On Reconfigurable Bisimulation, with an Application to the Distributed Synthesis Problem

Related

• Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory (Full Version)
• Distributed synthesis for acyclic architectures
• Model-checking lock-sharing systems against regular constraints
• Distributed and Constrained H₂ Control Design via System Level Synthesis and Dual Consensus ADMM
• Design of Distributed Controller for Discrete-Time Systems Via the Integration of Extended LMI and Clique-Wise Decomposition