LIPIcs.CSL.2021.13.pdf
- Filesize: 0.62 MB
- 16 pages
Document
Reachability in Distributed Memory Automata
Authors
-
Part of:
Volume:
29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2021-01-13
Cite As Get BibTex
Benedikt Bollig, Fedor Ryabinin, and Arnaud Sangnier. Reachability in Distributed Memory Automata. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.13
Abstract
We introduce Distributed Memory Automata, a model of register automata suitable to capture some features of distributed algorithms designed for shared-memory systems. In this model, each participant owns a local register and a shared register and has the ability to change its local value, to write it in the global memory and to test atomically the number of occurrences of its value in the shared memory, up to some threshold. We show that the control-state reachability problem for Distributed Memory Automata is Pspace-complete for a fixed number of participants and is in Pspace when the number of participants is not fixed a priori.
Subject Classification
ACM Subject Classification
- Theory of computation → Concurrency
Keywords
- Distributed algorithms
- Atomic snapshot objects
- Register automata
- Reachability
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
C. Aiswarya, Benedikt Bollig, and Paul Gastin. An automata-theoretic approach to the verification of distributed algorithms. Inf. Comput., 259(Part 3):305-327, 2018.
-
Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. In Erzsébet Csuhaj-Varjú and Zoltán Ésik, editors, Fundamentals of Computation Theory, 16th International Symposium, FCT 2007, volume 4639 of Lecture Notes in Computer Science, pages 88-99. Springer, 2007.
-
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.
-
Mikolaj Bojanczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Log., 12(4):27:1-27:26, 2011.
-
Benedikt Bollig, Patricia Bouyer, and Fabian Reiter. Identifiers in registers - describing network algorithms with logic. In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, volume 11425 of Lecture Notes in Computer Science, pages 115-132. Springer, 2019.
-
Armando Castañeda, Sergio Rajsbaum, and Michel Raynal. The renaming problem in shared memory systems: An introduction. Comput. Sci. Rev., 5(3):229-251, 2011.
-
Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009.
-
Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Ernst W. Mayr and Natacha Portier, editors, 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.
-
Wan Fokkink. Distributed Algorithms: An Intuitive Approach. MIT Press, 2013.
-
Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994.
-
Dexter Kozen. Lower bounds for natural proof systems. In FOCS'77, pages 254-266. IEEE Computer Society, 1977.
-
Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996.
-
Nikos Tzevelekos. Fresh-register automata. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, pages 295-306. ACM, 2011.