LIPIcs.MFCS.2023.88.pdf
- Filesize: 0.85 MB
- 15 pages
Document
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems
Author
-
Part of:
Volume:
48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Mathematical Foundations of Computer Science (MFCS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-08-21
File
Document Identifiers
Acknowledgements
Many thanks to Nathalie Bertrand, Nicolas Markey and Ocan Sankur for their invaluable advice.
Cite AsGet BibTex
Nicolas Waldburger. Checking Presence Reachability Properties on Parameterized Shared-Memory Systems. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 88:1-88:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.MFCS.2023.88
https://doi.org/10.4230/LIPIcs.MFCS.2023.88
Abstract
We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by reading from and writing to a shared memory. Beyond the standard model with finitely many registers, we tackle round-based shared-memory systems with fresh registers at each round. In the latter model, both the number of processes and the number of registers are unbounded, making verification particularly challenging. The properties studied are generic presence reachability objectives, which subsume classical questions such as safety or synchronization by expressing the presence or absence of processes in some states. In the more general round-based setting, we establish that the parameterized verification of presence reachability properties is PSPACE-complete. Moreover, for the roundless model with finitely many registers, we prove that the complexity drops down to NP-complete and we provide several natural restrictions that make the problem solvable in polynomial time.
Subject Classification
ACM Subject Classification
- Theory of computation → Verification by model checking
- Theory of computation → Distributed algorithms
Keywords
- Verification
- Parameterized models
- Distributed algorithms
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Rojin Rezvan. Parameterized verification under TSO is PSPACE-complete. Proc. ACM Program. Lang., 4(POPL):26:1-26:29, 2020. URL: https://doi.org/10.1145/3371094.
- James Aspnes. Fast deterministic consensus in a noisy environment. Journal of Algorithms, 45(1):16-39, 2002. URL: https://doi.org/10.1016/S0196-6774(02)00220-1.
- A. R. Balasubramanian, Lucie Guillou, and Chana Weil-Kennedy. Erratum to parameterized analysis of reconfigurable broadcast networks, 2022. URL: https://www.model.in.tum.de/~weilkenn/erratum-fossacs22.pdf.
- A. R. Balasubramanian, Lucie Guillou, and Chana Weil-Kennedy. Parameterized analysis of reconfigurable broadcast networks (long version). CoRR, abs/2201.10432, 2022. URL: https://arxiv.org/abs/2201.10432.
- A. R. Balasubramanian and Chana Weil-Kennedy. Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent. In GandALF 2021, volume 346, pages 18-34, 2021. URL: https://doi.org/10.4204/EPTCS.346.2.
- Nathalie Bertrand, Nicolas Markey, Ocan Sankur, and Nicolas Waldburger. Parameterized safety verification of round-based shared-memory systems. In ICALP 2022, pages 113:1-113:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.113.
- Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. URL: https://doi.org/10.2200/S00658ED1V01Y201508DCT013.
- Patricia Bouyer, Nicolas Markey, Mickael Randour, Arnaud Sangnier, and Daniel Stan. Reachability in networks of register protocols under stochastic schedulers. In ICALP 2016, volume 55 of LIPIcs, pages 106:1-106:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.106.
- Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro. On the complexity of parameterized reachability in reconfigurable broadcast networks. In FSTTCS 2012, volume 18 of LIPIcs, pages 289-300. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2012.289.
- Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In STACS 2014, volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.STACS.2014.1.
- Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. Journal of the ACM, 63(1):10:1-10:48, 2016. URL: https://doi.org/10.1145/2842603.
- Paulin Fournier. Parameterized verification of networks of many identical processes. PhD thesis, University of Rennes 1, France, 2015. URL: https://tel.archives-ouvertes.fr/tel-01355847.
- Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. Journal of the ACM, 39(3):675-735, 1992. URL: https://doi.org/10.1145/146637.146681.
- Matthew Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS 2011, volume 13 of LIPIcs, pages 457-468. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2011.457.
- Michel Raynal and Julien Stainer. A simple asynchronous shared memory consensus algorithm based on omega and closing sets. In CISIS 2012, pages 357-364. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/CISIS.2012.198.