Distributed controller synthesis for deadlock avoidance
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2022
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911143194263552 |
|---|---|
| author | Gimbert, Hugo Mascle, Corto Muscholl, Anca Walukiewicz, Igor |
| author_facet | Gimbert, Hugo Mascle, Corto Muscholl, Anca Walukiewicz, Igor |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2204_12409 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Distributed controller synthesis for deadlock avoidance Gimbert, Hugo Mascle, Corto Muscholl, Anca Walukiewicz, Igor Logic in Computer Science 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. |
| title | Distributed controller synthesis for deadlock avoidance |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2204.12409 |