{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:19:08Z","timestamp":1743099548446,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572302"},{"type":"electronic","value":"9783031572319"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>\nWe consider the parameterized verification of networks of agents which communicate through unreliable broadcasts. In this model, agents have local registers whose values are unordered and initially distinct and may therefore be thought of as identifiers. When an agent broadcasts a message, it appends to the message the value stored in one of its registers. Upon reception, an agent can store the received value or test it for equality against one of its own registers. We consider the coverability problem, where one asks whether a given state of the system may be reached by at least one agent. We establish that this problem is decidable, although non-primitive recursive. We contrast this with the undecidability of the closely related target problem where all agents must synchronize on a given state. On the other hand, we show that the coverability problem is NP-complete when each agent only has one register.<\/jats:p>","DOI":"10.1007\/978-3-031-57231-9_12","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T18:01:54Z","timestamp":1712340114000},"page":"250-270","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parameterized Broadcast Networks with Registers: from NP to the Frontiers of Decidability"],"prefix":"10.1007","author":[{"given":"Lucie","family":"Guillou","sequence":"first","affiliation":[]},{"given":"Corto","family":"Mascle","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Waldburger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of dynamic register automata. In: 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014. LIPIcs, vol.\u00a029, pp. 653\u2013665. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2014). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2014.653","DOI":"10.4230\/LIPIcs.FSTTCS.2014.653"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Kara, A., Rezine, O.: Verification of buffered dynamic register automata. In: Networked Systems, NETYS 2015. Lecture Notes in Computer Science, vol.\u00a09466, pp. 15\u201331. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-26850-7_2","DOI":"10.1007\/978-3-319-26850-7_2"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91\u2013101 (1996). https:\/\/doi.org\/10.1006\/inco.1996.0053","DOI":"10.1006\/inco.1996.0053"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Balasubramanian, A.R., Bertrand, N., Markey, N.: Parameterized verification of synchronization in constrained reconfigurable broadcast networks. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018. Lecture Notes in Computer Science, vol. 10806, pp. 38\u201354. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_3","DOI":"10.1007\/978-3-319-89963-3_3"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Balasubramanian, A.R., Guillou, L., Weil-Kennedy, C.: Parameterized analysis of reconfigurable broadcast networks. In: Foundations of Software Science and Computation Structures, FoSSaCS 2022. Lecture Notes in Computer Science, vol. 13242, pp. 61\u201380. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99253-8_4","DOI":"10.1007\/978-3-030-99253-8_4"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Bollig, B., Ryabinin, F., Sangnier, A.: Reachability in distributed memory automata. In: Annual Conference on Computer Science Logic, CSL 2021. LIPIcs, vol.\u00a0183, pp. 13:1\u201313:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2021.13","DOI":"10.4230\/LIPIcs.CSL.2021.13"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. Journal of the ACM 30(2), 323\u2013342 (1983). https:\/\/doi.org\/10.1145\/322374.322380","DOI":"10.1145\/322374.322380"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Chambart, P., Schnoebelen, P.: The ordinal recursive complexity of lossychannel systems. In: Annual IEEE Symposium on Logic in Computer Science,LICS 2008. pp. 205\u2013216. IEEE Computer Society (2008).https:\/\/doi.org\/10.1109\/LICS.2008.47","DOI":"10.1109\/LICS.2008.47"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Chini, P., Meyer, R., Saivasan, P.: Liveness in broadcast networks. Computing 104(10), 2203\u20132223 (2022). https:\/\/doi.org\/10.1007\/s00607-021-00986-y","DOI":"10.1007\/s00607-021-00986-y"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcast networks of register automata. In: Reachability Problems , RP 2013. Lecture Notes in Computer Science, vol.\u00a08169, pp. 109\u2013121. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-41036-9_11","DOI":"10.1007\/978-3-642-41036-9_11"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity ofparameterized reachability in reconfigurable broadcast networks. In: IARCSAnnual Conference on Foundations of Software Technology and TheoreticalComputer Science, FSTTCS 2012. LIPIcs, vol.\u00a018, pp. 289\u2013300. SchlossDagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012).https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.289","DOI":"10.4230\/LIPIcs.FSTTCS.2012.289"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: CONCUR 2010. Lecture Notes in Computer Science, vol.\u00a06269, pp. 313\u2013327. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-15375-4_22","DOI":"10.1007\/978-3-642-15375-4_22"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Annual IEEE Symposium on Logic in Computer Science, LICS 1998. pp. 70\u201380. IEEE Computer Society (1998). https:\/\/doi.org\/10.1109\/LICS.1998.705644","DOI":"10.1109\/LICS.1998.705644"},{"key":"12_CR14","doi-asserted-by":"publisher","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999. pp. 352\u2013359. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/LICS.1999.782630","DOI":"10.1109\/LICS.1999.782630"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Haddad, S., Schmitz, S., Schnoebelen, P.: The ordinal-recursive complexity of timed-arc petri nets, data nets, and other enriched nets. In: Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. pp. 355\u2013364. IEEE Computer Society (2012). https:\/\/doi.org\/10.1109\/LICS.2012.46","DOI":"10.1109\/LICS.2012.46"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society s3-2(1), 326\u2013336 (1952). https:\/\/doi.org\/10.1112\/plms\/s3-2.1.326","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Lasota, S.: Decidability border for petri nets with data: WQO dichotomy conjecture. In: Kordon, F., Moldt, D. (eds.) Application and Theory of Petri Nets and Concurrency - 37th International Conference, PETRI NETS 2016, Toru\u0144, Poland, June 19-24, 2016. Proceedings. Lecture Notes in Computer Science, vol.\u00a09698, pp. 20\u201336. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-39086-4_3, https:\/\/doi.org\/10.1007\/978-3-319-39086-4_3","DOI":"10.1007\/978-3-319-39086-4_3"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Lazic, R., Newcomb, T.C., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Informaticae 88(3), 251\u2013274 (2008). https:\/\/doi.org\/10.1007\/978-3-540-73094-1_19","DOI":"10.1007\/978-3-540-73094-1_19"},{"key":"12_CR19","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall, Inc., USA (1967)"},{"key":"12_CR20","unstructured":"Rezine, O.: Verification of networks of communicating processes: Reachability problems and decidability issues. Ph.D. thesis, Uppsala University, Sweden (2017)"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Rosa-Velardo, F.: Ordinal recursive complexity of unordered data nets. Information and Computation 254, 41\u201358 (2017). https:\/\/doi.org\/10.1016\/j.ic.2017.02.002","DOI":"10.1016\/j.ic.2017.02.002"},{"key":"12_CR22","unstructured":"Sangnier, A.: Erratum to parameterized verification of broadcast networks of register automata (2023), https:\/\/www.irif.fr\/~sangnier\/publications.html"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Schmitz, S.: Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory 8(1), 3:1\u20133:36 (2016). https:\/\/doi.org\/10.1145\/2858784","DOI":"10.1145\/2858784"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Schmitz, S., Schnoebelen, P.: Multiply-recursive upper bounds with Higman\u2019s lemma. In: International Colloquium on Automata, Languages and Programming, ICALP 2011. Lecture Notes in Computer Science, vol.\u00a06756, pp. 441\u2013452. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22012-8_35","DOI":"10.1007\/978-3-642-22012-8_35"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D\u2019Argenio, P.R., Melgratti, H.C. (eds.) CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a08052, pp.5\u201324. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_2","DOI":"10.1007\/978-3-642-40184-8_2"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251\u2013261 (2002). https:\/\/doi.org\/10.1016\/S0020-0190(01)00337-4","DOI":"10.1016\/S0020-0190(01)00337-4"}],"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-031-57231-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T16:04:04Z","timestamp":1714752244000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57231-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572302","9783031572319"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57231-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","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":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/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":"79","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":"24","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)"}}]}}