{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:02Z","timestamp":1760202662162},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642410352"},{"type":"electronic","value":"9783642410369"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41036-9_11","type":"book-chapter","created":{"date-parts":[[2013,9,3]],"date-time":"2013-09-03T09:49:49Z","timestamp":1378201789000},"page":"109-121","source":"Crossref","is-referenced-by-count":15,"title":["Parameterized Verification of Broadcast Networks of Register Automata"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnaud","family":"Sangnier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Riccardo","family":"Traverso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.-K.: General decidability theorems for infinite-state systems. In: LICS 1996, pp. 313\u2013321. IEEE Computer Society (1996)","key":"11_CR1"},{"issue":"3","key":"11_CR2","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1016\/j.ic.2010.11.003","volume":"209","author":"P.A. Abdulla","year":"2011","unstructured":"Abdulla, P.A., Delzanno, G., Van Begin, L.: A classification of the expressive power of well-structured transition systems. Inf. Comput.\u00a0209(3), 248\u2013279 (2011)","journal-title":"Inf. Comput."},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1006\/inco.1996.0083","volume":"130","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Inf. Comput.\u00a0130(1), 71\u201390 (1996)","journal-title":"Inf. Comput."},{"issue":"1-2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1016\/S0304-3975(00)00105-5","volume":"256","author":"P.A. Abdulla","year":"2001","unstructured":"Abdulla, P.A., Jonsson, B.: Ensuring completeness of symbolic verification methods for infinite-state systems. Theor. Comput. Sci.\u00a0256(1-2), 145\u2013167 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"issue":"1&2","key":"11_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(94)00231-7","volume":"147","author":"A. Cheng","year":"1995","unstructured":"Cheng, A., Esparza, J., Palsberg, J.: Complexity results for 1-safe nets. TCS\u00a0147(1&2), 117\u2013136 (1995)","journal-title":"TCS"},{"issue":"3","key":"11_CR7","first-page":"257","volume":"23","author":"G. Delzanno","year":"2003","unstructured":"Delzanno, G.: Constraint-based verification of parameterized cache coherence protocols. FMSD\u00a023(3), 257\u2013301 (2003)","journal-title":"FMSD"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1016\/j.tcs.2012.09.021","volume":"467","author":"G. Delzanno","year":"2013","unstructured":"Delzanno, G., Rosa-Velardo, F.: On the coverability and reachability languages of monotonic extensions of petri nets. Theor. Comput. Sci.\u00a0467, 12\u201329 (2013)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Delzanno, G., Sangnier, A., Traverso, R.: Parameterized verification of broadcat networks of register automata (technical report) (2013), \n                  \n                    http:\/\/verify.disi.unige.it\/publications\/","key":"11_CR9","DOI":"10.1007\/978-3-642-41036-9_11"},{"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 fuer Informatik (2012)","key":"11_CR10"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-642-15375-4_22","volume-title":"CONCUR 2010 - Concurrency Theory","author":"G. Delzanno","year":"2010","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: Parameterized verification of ad hoc networks. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 313\u2013327. Springer, Heidelberg (2010)"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-19805-2_30","volume-title":"Foundations of Software Science and Computational Structures","author":"G. Delzanno","year":"2011","unstructured":"Delzanno, G., Sangnier, A., Zavattaro, G.: On the power of cliques in the parameterized verification of ad hoc networks. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol.\u00a06604, pp. 441\u2013455. Springer, Heidelberg (2011)"},{"unstructured":"Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: LICS 1998, pp. 70\u201380. IEEE Computer Society (1998)","key":"11_CR13"},{"unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS 1999, pp. 352\u2013359. IEEE Computer Society (1999)","key":"11_CR14"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-28756-5_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Fehnker","year":"2012","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 173\u2013187. Springer, Heidelberg (2012)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-73210-5_14","volume-title":"Integrated Formal Methods","author":"A. Fehnker","year":"2007","unstructured":"Fehnker, A., van Hoesel, L., Mader, A.: Modelling and verification of the LMAC protocol for wireless sensor networks. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 253\u2013272. Springer, Heidelberg (2007)"},{"issue":"1-2","key":"11_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci.\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"11_CR18","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. ACM\u00a039(3), 675\u2013735 (1992)","journal-title":"J. ACM"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-70545-1_21","volume-title":"Computer Aided Verification","author":"S. Joshi","year":"2008","unstructured":"Joshi, S., K\u00f6nig, B.: Applying the graph minor theorem to the verification of graph transformation systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 214\u2013226. Springer, Heidelberg (2008)"},{"issue":"2","key":"11_CR20","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1016\/0304-3975(94)90242-9","volume":"134","author":"M. Kaminski","year":"1994","unstructured":"Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci.\u00a0134(2), 329\u2013363 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"11_CR21","first-page":"251","volume":"88","author":"R. Lazic","year":"2008","unstructured":"Lazic, R., Newcomb, T., Ouaknine, J., Roscoe, A.W., Worrell, J.: Nets with tokens which carry data. Fundam. Inform.\u00a088(3), 251\u2013274 (2008)","journal-title":"Fundam. Inform."},{"issue":"2-3","key":"11_CR22","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0167-6423(95)00017-8","volume":"25","author":"K.V.S. Prasad","year":"1995","unstructured":"Prasad, K.V.S.: A calculus of broadcasting systems. Sci. Comput. Program.\u00a025(2-3), 285\u2013327 (1995)","journal-title":"Sci. Comput. Program."},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-78800-3_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Saksena","year":"2008","unstructured":"Saksena, M., Wibling, O., Jonsson, B.: Graph grammar modeling and verification of ad hoc routing protocols. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 18\u201332. Springer, Heidelberg (2008)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-642-15155-2_54","volume-title":"Mathematical Foundations of Computer Science 2010","author":"P. Schnoebelen","year":"2010","unstructured":"Schnoebelen, P.: Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol.\u00a06281, pp. 616\u2013628. Springer, Heidelberg (2010)"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/978-3-642-04081-8_40","volume-title":"CONCUR 2009 - Concurrency Theory","author":"A. Singh","year":"2009","unstructured":"Singh, A., Ramakrishnan, C.R., Smolka, S.A.: Query-based model checking of ad\u00a0hoc\u00a0network\u00a0protocols. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol.\u00a05710, pp. 603\u2013619. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Reachability Problems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41036-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T02:06:47Z","timestamp":1558318007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41036-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642410352","9783642410369"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41036-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}