Reachability in Distributed Memory Automata

Authors Benedikt Bollig, Fedor Ryabinin, Arnaud Sangnier

Thumbnail PDF


  • Filesize: 0.62 MB
  • 16 pages

Document Identifiers

Author Details

Benedikt Bollig
  • CNRS, LSV, ENS Paris-Saclay, Université Paris-Saclay, Gif-sur-Yvette, France
Fedor Ryabinin
  • IMDEA Software Institue, Madrid, Spain
Arnaud Sangnier
  • IRIF, Université de Paris, CNRS, France

Cite AsGet 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)


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
  • Distributed algorithms
  • Atomic snapshot objects
  • Register automata
  • Reachability


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


  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. Wan Fokkink. Distributed Algorithms: An Intuitive Approach. MIT Press, 2013. Google Scholar
  10. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. Google Scholar
  11. Dexter Kozen. Lower bounds for natural proof systems. In FOCS'77, pages 254-266. IEEE Computer Society, 1977. Google Scholar
  12. Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996. Google Scholar
  13. 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. Google Scholar