Name
Abstract | ||
|---|---|---|
This paper investigates the deadlock prevention problem for Petri nets (PN), in which the control is performed by appropriately setting time constraints on transitions, in terms of firing intervals. We show that this time based deadlock prevention (TBDP) problem is decidable for bounded PN and can be formalised as a parametric model checking problem. However, in this context, the parametric model checking faces a severe state explosion problem. To deal with this limitation, we propose a symbolic approach that abstracts firing order constraints and bypasses the use of parameter domains with their associated very costly operations. Both approaches can handle, as an input model, a (time) PN with controllable/uncontrollable transitions. In such a case, they expose whether or not the firing intervals of the controllable transitions of the input model can be restricted so as to force the deadlock freeness (i.e., there is no marking with no enabled transitions). |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1016/j.automatica.2021.110119 | Automatica |
Keywords | DocType | Volume |
Petri net,Time petri net,Deadlock prevention,Time based deadlock prevention,Supervisory control | Journal | 137 |
Issue | ISSN | Citations |
1 | 0005-1098 | 0 |
PageRank | References | Authors |
0.34 | 0 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| H. Boucheneb | 1 | 17 | 3.46 |
| Kamel Barkaoui | 2 | 536 | 76.60 |
| Qian Xing | 3 | 0 | 0.34 |
| KuangZe Wang | 4 | 0 | 0.34 |
| GaiYun Liu | 5 | 70 | 5.40 |
| ZhiWu Li | 6 | 1863 | 113.66 |