Document Open Access Logo

Distributed Local Strategies in Broadcast Networks

Authors Nathalie Bertrand, Paulin Fournier, Arnaud Sangnier

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.44.pdf
  • Filesize: 485 kB
  • 14 pages

Document Identifiers

Author Details

Nathalie Bertrand
Paulin Fournier
Arnaud Sangnier

Cite As Get BibTex

Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Distributed Local Strategies in Broadcast Networks. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 44-57, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.44

Abstract

We study the problems of reaching a specific control state, or converging to a set of target states, in networks with a parameterized number of identical processes communicating via broadcast. To reflect the distributed aspect of such networks, we restrict our attention to executions in which all the processes must follow the same local strategy that, given their past performed actions and received messages, provides the next action to be performed. We show that the reachability and target problems under such local strategies are NP-complete, assuming that the set of receivers is chosen non-deterministically at each step. On the other hand, these problems become undecidable when the communication topology is a clique. However, decidability can be regained for reachability under the additional assumption that all processes are bound to receive the broadcast messages.

Subject Classification

Keywords
  • Broadcast networks
  • parameterized verification
  • local strategies

Metrics

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

References

  1. Parosh A. Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput., 160(1-2):109-127, 2000. Google Scholar
  2. Benjamin Aminof, Swen Jacobs, Ayrat Khalimov, and Sasha Rubin. Parameterized model checking of token-passing systems. In Proc. of VMCAI'14, volume 8318 of LNCS, pages 262-281, 2014. Google Scholar
  3. Nathalie Bertrand, Paulin Fournier, and Arnaud Sangnier. Distributed local strategies in broadcast networks. Research report, Inria Rennes, July 2015. URL: https://hal.inria.fr/hal-01170796.
  4. Benedikt Bollig. Logic for communicating automata with parameterized topology. In Proc. of CSL-LICS'14, page 18. ACM, 2014. Google Scholar
  5. Benedikt Bollig, Paul Gastin, and Jana Schubert. Parameterized verification of communicating automata under context bounds. In Proc. of RP'14, volume 8762 of LNCS, pages 45-57, 2014. Google Scholar
  6. Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, and Helmut Veith. Verification by network decomposition. In Proc. of CONCUR'04, volume 3170 of LNCS, pages 276-291, 2004. Google Scholar
  7. Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, and Gianluigi Zavattaro. On the complexity of parameterized reachability in reconfigurable broadcast networks. In Proc. of FSTTCS'12, volume 18 of LIPIcs, pages 289-300. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  8. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. Parameterized verification of ad hoc networks. In Proc. of CONCUR'10, volume 6269 of LNCS, pages 313-327. Springer, 2010. Google Scholar
  9. Giorgio Delzanno, Arnaud Sangnier, and Gianluigi Zavattaro. On the power of cliques in the parameterized verification of ad hoc networks. In Proc. of FoSSaCS'11, volume 6604 of LNCS, pages 441-455. Springer, 2011. Google Scholar
  10. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Proc. of STACS'14, volume 25 of LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  11. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In Proc. of LICS'99, pages 352-359. IEEE Computer Society, 1999. Google Scholar
  12. Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In Proc. of CAV'13, volume 8044 of LNCS, pages 124-140, 2013. Google Scholar
  13. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. Google Scholar
  14. Steven M. German and A. Prasad Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. Google Scholar
  15. Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In Proc. of FOCS'90, pages 746-757. IEEE Computer Society, 1990. Google Scholar
  16. Sylvain Schmitz and Philippe Schnoebelen. The power of well-structured systems. In Proc. of CONCUR'13, volume 8052 of LNCS, pages 5-24. Springer, 2013. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact