{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:48:49Z","timestamp":1742964529103,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030992521"},{"type":"electronic","value":"9783030992538"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reconfigurable broadcast networks (RBN) are a model of distributed computation in which agents can broadcast messages to other agents using some underlying communication topology which can change arbitrarily over the course of executions. In this paper, we conduct <jats:italic>parameterized analysis<\/jats:italic> of RBN. We consider cubes, (infinite) sets of configurations in the form of lower and upper bounds on the number of agents in each state, and we show that we can evaluate boolean combinations over cubes and reachability sets of cubes in . In particular, reachability from a cube to another cube is a -complete problem.<\/jats:p><jats:p>To prove the upper bound for this parameterized analysis, we prove some structural properties about the reachability sets and the <jats:italic>symbolic graph<\/jats:italic> abstraction of RBN, which might be of independent interest. We justify this claim by providing two applications of these results. First, we show that the almost-sure coverability problem is -complete for RBN, thereby closing a complexity gap from a previous paper\u00a0[3]. Second, we define a computation model using RBN, \u00e0 la population protocols, called RBN protocols. We characterize precisely the set of predicates that can be computed by such protocols.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_4","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"61-80","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Parameterized Analysis of Reconfigurable Broadcast Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7258-5445","authenticated-orcid":false,"given":"A. R.","family":"Balasubramanian","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6101-2895","authenticated-orcid":false,"given":"Lucie","family":"Guillou","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1351-8824","authenticated-orcid":false,"given":"Chana","family":"Weil-Kennedy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Angluin, D., Aspnes, J., Diamadi, Z., Fischer, M.J., Peralta, R.: Computation in networks of passively mobile finite-state sensors. Distributed Comput. 18(4), 235\u2013253 (2006). https:\/\/doi.org\/10.1007\/s00446-005-0138-3","key":"4_CR1","DOI":"10.1007\/s00446-005-0138-3"},{"doi-asserted-by":"publisher","unstructured":"Angluin, D., Aspnes, J., Eisenstat, D., Ruppert, E.: The computational power of population protocols. Distributed Comput. 20(4), 279\u2013304 (2007). https:\/\/doi.org\/10.1007\/s00446-007-0040-2","key":"4_CR2","DOI":"10.1007\/s00446-007-0040-2"},{"doi-asserted-by":"publisher","unstructured":"Balasubramanian, A.R., Weil-Kennedy, C.: Reconfigurable broadcast networks and asynchronous shared-memory systems are equivalent. In: Ganty, P., Bresolin, D. (eds.) Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2021, Padua, Italy, 20-22 September 2021. EPTCS, vol.\u00a0346, pp. 18\u201334 (2021). https:\/\/doi.org\/10.4204\/EPTCS.346.2","key":"4_CR3","DOI":"10.4204\/EPTCS.346.2"},{"doi-asserted-by":"publisher","unstructured":"Bertrand, N., Fournier, P.: Parameterized verification of many identical probabilistic timed processes. In: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS. pp. 501\u2013513 (2013). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2013.501","key":"4_CR4","DOI":"10.4230\/LIPIcs.FSTTCS.2013.501"},{"doi-asserted-by":"publisher","unstructured":"Bertrand, N., Fournier, P., Sangnier, A.: Playing with probabilities in reconfigurable broadcast networks. In: Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS. pp. 134\u2013148 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54830-7_9","key":"4_CR5","DOI":"10.1007\/978-3-642-54830-7_9"},{"doi-asserted-by":"publisher","unstructured":"Bouyer, P., Markey, N., Randour, M., Sangnier, A., Stan, D.: Reachability in networks of register protocols under stochastic schedulers. In: Chatzigiannakis, I., Mitzenmacher, M., Rabani, Y., Sangiorgi, D. (eds.) 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy. LIPIcs, vol.\u00a055, pp. 106:1\u2013106:14. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2016). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2016.106","key":"4_CR6","DOI":"10.4230\/LIPIcs.ICALP.2016.106"},{"doi-asserted-by":"publisher","unstructured":"Chini, P., Meyer, R., Saivasan, P.: Liveness in broadcast networks. In: Atig, M.F., Schwarzmann, A.A. (eds.) Networked Systems - 7th International Conference, NETYS 2019, Marrakech, Morocco, June 19-21, 2019, Revised Selected Papers. Lecture Notes in Computer Science, vol. 11704, pp. 52\u201366. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31277-0_4","key":"4_CR7","DOI":"10.1007\/978-3-030-31277-0_4"},{"doi-asserted-by":"publisher","unstructured":"Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: D\u2019Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2012, December 15-17, 2012, Hyderabad, India. LIPIcs, vol.\u00a018, pp. 289\u2013300. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012), https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.289","key":"4_CR8","DOI":"10.4230\/LIPIcs.FSTTCS.2012.289"},{"unstructured":"Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. Long version (2012), https:\/\/www.irif.fr\/~sangnier\/publis\/DSTZ-FSTTCS12-long.pdf","key":"4_CR9"},{"doi-asserted-by":"publisher","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06269, pp. 313\u2013327. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_22","key":"4_CR10","DOI":"10.1007\/978-3-642-15375-4_22"},{"doi-asserted-by":"publisher","unstructured":"Esparza, J., Ganty, P., Majumdar, R., Weil-Kennedy, C.: Verification of immediate observation population protocols. In: CONCUR. LIPIcs, vol.\u00a0118, pp. 31:1\u201331:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2018). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2018.31","key":"4_CR11","DOI":"10.4230\/LIPIcs.CONCUR.2018.31"},{"doi-asserted-by":"publisher","unstructured":"Esparza, J., Jaax, S., Raskin, M.A., Weil-Kennedy, C.: The complexity of verifying population protocols. Distributed Comput. 34(2), 133\u2013177 (2021). https:\/\/doi.org\/10.1007\/s00446-021-00390-x","key":"4_CR12","DOI":"10.1007\/s00446-021-00390-x"},{"doi-asserted-by":"publisher","unstructured":"Esparza, J., Raskin, M.A., Weil-Kennedy, C.: Parameterized analysis of immediate observation petri nets. In: Donatelli, S., Haar, S. (eds.) Application and Theory of Petri Nets and Concurrency - 40th International Conference, PETRI NETS 2019, Aachen, Germany, June 23-28, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11522, pp. 365\u2013385. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-21571-2_20","key":"4_CR13","DOI":"10.1007\/978-3-030-21571-2_20"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:05:00Z","timestamp":1648497900000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}