Reconfiguration and Message Losses in Parameterized Broadcast Networks

Authors Nathalie Bertrand , Patricia Bouyer , Anirban Majumdar



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.32.pdf
  • Filesize: 0.58 MB
  • 15 pages

Document Identifiers

Author Details

Nathalie Bertrand
  • Univ. Rennes, Inria, CNRS, IRISA - Rennes, France
Patricia Bouyer
  • LSV, CNRS & ENS Paris-Saclay, Univ. Paris-Saclay - Cachan, France
Anirban Majumdar
  • Univ. Rennes, Inria, CNRS, IRISA - Rennes, France
  • LSV, CNRS & ENS Paris-Saclay, Univ. Paris-Saclay - Cachan, France

Cite AsGet BibTex

Nathalie Bertrand, Patricia Bouyer, and Anirban Majumdar. Reconfiguration and Message Losses in Parameterized Broadcast Networks. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 32:1-32:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.32

Abstract

Broadcast networks allow one to model networks of identical nodes communicating through message broadcasts. Their parameterized verification aims at proving a property holds for any number of nodes, under any communication topology, and on all possible executions. We focus on the coverability problem which dually asks whether there exists an execution that visits a configuration exhibiting some given state of the broadcast protocol. Coverability is known to be undecidable for static networks, i.e. when the number of nodes and communication topology is fixed along executions. In contrast, it is decidable in PTIME when the communication topology may change arbitrarily along executions, that is for reconfigurable networks. Surprisingly, no lower nor upper bounds on the minimal number of nodes, or the minimal length of covering execution in reconfigurable networks, appear in the literature. In this paper we show tight bounds for cutoff and length, which happen to be linear and quadratic, respectively, in the number of states of the protocol. We also introduce an intermediary model with static communication topology and non-deterministic message losses upon sending. We show that the same tight bounds apply to lossy networks, although, reconfigurable executions may be linearly more succinct than lossy executions. Finally, we show NP-completeness for the natural optimisation problem associated with the cutoff.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • model checking
  • parameterized verification
  • broadcast networks

Metrics

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

References

  1. 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: http://dx.doi.org/10.2200/S00658ED1V01Y201508DCT013.
  2. Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro. On the Complexity of Parameterized Reachability in Reconfigurable Broadcast Networks. In Proceedings of the 32nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'12), volume 18 of Leibniz International Proceedings in Informatics, pages 289-300. Leibniz-Zentrum für Informatik, December 2012. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.289.
  3. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized Verification of Ad Hoc Networks. In Proceedings of the 21st International Conference on Concurrency Theory (CONCUR'10), volume 6269 of Lecture Notes in Computer Science, pages 313-327. Springer, September 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_22.
  4. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Verification of Ad Hoc Networks with Node and Communication Failures. In Proceedings of the 32nd International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE'12), volume 7273 of Lecture Notes in Computer Science. Springer, 2012. Google Scholar
  5. E. Allen Emerson and A. Prasad Sistla. Symmetry and model checking. Formal Methods in System Design, 9(1-2):105-131, August 1996. URL: http://dx.doi.org/10.1007/BF00625970.
  6. Javier Esparza. Keeping a Crowd Safe: On the Complexity of Parameterized Verification (Invited Talk). In Proceedings of the 31st Symposium on Theoretical Aspects of Computer Science (STACS'14), volume 25 of Leibniz International Proceedings in Informatics, pages 1-10. Leibniz-Zentrum für Informatik, March 2014. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2014.1.
  7. Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV'13), volume 8044 of Lecture Notes in Computer Science, pages 124-140. Springer, July 2013. URL: http://dx.doi.org/10.1007/978-3-642-39799-8_8.
  8. Steven M. German and A. Prasad Sistla. Reasoning about Systems with Many Processes. Journal of the ACM, 39(3):675-735, July 1992. URL: http://dx.doi.org/10.1145/146637.146681.
  9. Richard M. Karp. Reducibility among Combinatorial Problems. In Complexity of Computer Computations, The IBM Research Symposia Series, pages 85-103, 1972. Google Scholar
  10. Marvin Minsky. Computation: Finite and Infinite Machines. Prentice Hall International, 1967. Google Scholar
  11. Ichiro Suzuki. Proving Properties of a Ring of Finite-State Machines. Information Processing Letters, 28(4):213-214, 1988. URL: http://dx.doi.org/10.1016/0020-0190(88)90211-6.
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