Document Open Access Logo

Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous

Authors Lucie Guillou, Arnaud Sangnier, Nathalie Sznajder

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2023.7.pdf
  • Filesize: 0.89 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Parameterised verification
  • Coverability
  • Counter machines

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Safety Analysis of Parameterised Networks with Non-Blocking Rendez-Vous. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.7

Author Details

Lucie Guillou
  • IRIF, CNRS, Université Paris Cité, France
Arnaud Sangnier
  • IRIF, CNRS, Université Paris Cité, France
Nathalie Sznajder
  • LIP6, CNRS, Sorbonne Université, France

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22(6):307-309, 1986. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. J. Esparza. Decidability and complexity of petri net problems - An introduction. In Advanced Course on Petri Nets, pages 374-428. Springer, 1998. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. A. Finkel and P. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. Google Scholar
  13. S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992. Google Scholar
  14. 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.
  15. 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. Google Scholar
  16. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In FOCS'21, pages 1241-1252. IEEE, 2021. Google Scholar
  17. R.J. Lipton. The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science). Department of Computer Science, Yale University, 1976. Google Scholar
  18. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967. Google Scholar
  19. C. Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6:223-231, 1978. Google Scholar
  20. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact