Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous
We consider networks of processes that all execute the same finite-state protocol and communicate via a rendez-vous mechanism. When a process requests a rendez-vous, another process can respond to it and they both change their control states accordingly. We focus here on a specific semantics, called non-blocking, where the process requesting a rendez-vous can change its state even if no process can respond to it. In this context, we study the parameterised coverability problem of a configuration, which consists in determining whether there is an initial number of processes and an execution allowing to reach a configuration bigger than a given one. We show that this problem is EXPSPACE-complete and can be solved in polynomial time if the protocol is partitioned into two sets of states, the states from which a process can request a rendez-vous and the ones from which it can answer one. We also prove that the problem of the existence of an execution bringing all the processes in a final state is undecidable in our context. These two problems can be solved in polynomial time with the classical rendez-vous semantics.
Parameterised verification
Coverability
Counter machines
Theory of computation~Formal languages and automata theory
7:1-7:17
Regular Paper
https://arxiv.org/abs/2307.04546
Lucie
Guillou
Lucie Guillou
IRIF, CNRS, Université Paris Cité, France
Arnaud
Sangnier
Arnaud Sangnier
IRIF, CNRS, Université Paris Cité, France
Nathalie
Sznajder
Nathalie Sznajder
LIP6, CNRS, Sorbonne Université, France
10.4230/LIPIcs.CONCUR.2023.7
P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. General decidability theorems for infinite-state systems. In LICS'96, pages 313-321. IEEE Computer Society, 1996.
P. A. Abdulla, K. Cerans, B. Jonsson, and Y.-K. Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1-2):109-127, 2000.
K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307-309, 1986.
A. R. Balasubramanian, J. Esparza, and M. A. Raskin. Finding cut-offs in leaderless rendez-vous protocols is easy. In FOSSACS'21, volume 12650 of LNCS, pages 42-61. Springer, 2021.
G. Delzanno, J. F. Raskin, and L. Van Begin. Towards the automated verification of multithreaded java programs. In TACAS'02, volume 2280 of LNCS, pages 173-187. Springer, 2002.
G. Delzanno, A. Sangnier, R. Traverso, and G. Zavattaro. On the complexity of parameterized reachability in reconfigurable broadcast networks. In FSTTCS'12, volume 18 of LIPIcs, pages 289-300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012.
A. Durand-Gasselin, J. Esparza, P. Ganty, and R. Majumdar. Model checking parameterized asynchronous shared-memory systems. Formal Methods in System Design, 50(2-3):140-167, 2017.
J. Esparza. Decidability and complexity of petri net problems - An introduction. In Advanced Course on Petri Nets, pages 374-428. Springer, 1998.
J. Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Ernst W. Mayr and Natacha Portier, editors, Proceedings of 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014), volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014.
J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In LICS'99, pages 352-359. IEEE Comp. Soc. Press, July 1999.
J. Esparza, P. Ganty, and R. Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV'13, volume 8044 of LNCS, pages 124-140. Springer-Verlag, 2013.
A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001.
S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992.
L. Guillou, A. Sangnier, and N. Sznajder. Safety analysis of parameterised networks with non-blocking rendez-vous, 2023. URL: https://arxiv.org/abs/2307.04546.
https://arxiv.org/abs/2307.04546
F. Horn and A. Sangnier. Deciding the existence of cut-off in parameterized rendez-vous networks. In CONCUR'20, volume 171 of LIPIcs, pages 46:1-46:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In FOCS'21, pages 1241-1252. IEEE, 2021.
R.J. Lipton. The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science). Department of Computer Science, Yale University, 1976.
Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967.
C. Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6:223-231, 1978.
J. F. Raskin and L. Van Begin. Petri nets with non-blocking arcs are difficult to analyze. In INFINITY'03, volume 98 of Electronic Notes in Theoretical Computer Science, pages 35-55. Elsevier, 2003.
Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode