{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T02:59:29Z","timestamp":1780628369113,"version":"3.54.1"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031614323","type":"print"},{"value":"9783031614330","type":"electronic"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-61433-0_14","type":"book-chapter","created":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T16:02:01Z","timestamp":1718208121000},"page":"291-311","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Safety Verification of\u00a0Wait-Only Non-Blocking Broadcast Protocols"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6101-2895","authenticated-orcid":false,"given":"Lucie","family":"Guillou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6731-0340","authenticated-orcid":false,"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4199-2443","authenticated-orcid":false,"given":"Nathalie","family":"Sznajder","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,6,13]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-662-48899-7_22","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B Aminof","year":"2015","unstructured":"Aminof, B., Rubin, S., Zuleger, F.: On the expressive power of communication primitives in parameterised systems. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 313\u2013328. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_22"},{"issue":"6","key":"14_CR2","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"KR Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307\u2013309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"14_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-030-71995-1_3","volume-title":"FOSSACS 2021","author":"AR Balasubramanian","year":"2021","unstructured":"Balasubramanian, A.R., Esparza, J., Raskin, M.A.: Finding cut-offs in leaderless rendez-vous protocols is easy. In: Kiefer, S., Tasson, C. (eds.) FOSSACS 2021. LNCS, vol. 12650, pp. 42\u201361. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71995-1_3"},{"key":"14_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-46002-0_13","volume-title":"TACAS\u201902","author":"G Delzanno","year":"2002","unstructured":"Delzanno, G., Raskin, J.F., Begin, L.V.: Towards the automated verification of multithreaded java programs. In: Katoen, J.P., Stevens, P. (eds.) TACAS\u201902. LNCS, vol. 2280, pp. 173\u2013187. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_13"},{"key":"14_CR5","unstructured":"Delzanno, G., Sangnier, A., Traverso, R., Zavattaro, G.: On the complexity of parameterized reachability in reconfigurable broadcast networks. In: FSTTCS 2012. LIPIcs, vol.\u00a018, pp. 289\u2013300. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"issue":"2\u20133","key":"14_CR6","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/s10703-016-0258-3","volume":"50","author":"A Durand-Gasselin","year":"2017","unstructured":"Durand-Gasselin, A., Esparza, J., Ganty, P., Majumdar, R.: Model checking parameterized asynchronous shared-memory systems. Formal Methods Syst. Des. 50(2\u20133), 140\u2013167 (2017)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Kahlon, V.: Model checking guarded protocols. In: (LICS 2003, pp. 361\u2013370. IEEE (2003)","DOI":"10.1109\/LICS.2003.1210076"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352\u2013359. IEEE Computer Soc. Press (1999)","DOI":"10.1109\/LICS.1999.782630"},{"issue":"3","key":"14_CR9","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM 39(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"14_CR10","unstructured":"Guillou, L., Sangnier, A., Sznajder, N.: Safety analysis of parameterised networks with non-blocking rendez-vous. In: CONCUR\u201923. LIPIcs, vol.\u00a0279, pp. 7:1\u20137:17. loss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023)"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Guillou, L., Sangnier, A., Sznajder, N.: Safety verification of wait-only non-blocking broadcast protocols (2024). https:\/\/doi.org\/10.48550\/arXiv.2403.18591","DOI":"10.48550\/arXiv.2403.18591"},{"key":"14_CR12","unstructured":"Horn, F., Sangnier, A.: Deciding the existence of cut-off in parameterized rendez-vous networks. In: CONCUR\u201920. LIPIcs, vol.\u00a0171, pp. 46:1\u201346:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Lower bounds for natural proof systems. In: FOCS 1977, pp. 254\u2013266. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.16"},{"issue":"1","key":"14_CR14","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/990518.990519","volume":"7","author":"RE Ladner","year":"1975","unstructured":"Ladner, R.E.: The circuit value problem is log space complete for P. SIGACT News 7(1), 18\u201320 (1975)","journal-title":"SIGACT News"},{"key":"14_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-642-40184-8_2","volume-title":"CONCUR 2013","author":"S Schmitz","year":"2013","unstructured":"Schmitz, S., Schnoebelen, P.: The power of well-structured systems. In: D\u2019Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 5\u201324. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40184-8_2"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61433-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T18:03:14Z","timestamp":1732212194000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61433-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031614323","9783031614330"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61433-0_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"13 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PETRI NETS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applications and Theory of Petri Nets and Concurrency","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Geneva","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Switzerland","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":"26 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"45","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"apn2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.unige.ch\/petrinets2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}