{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T02:49:05Z","timestamp":1780627745212,"version":"3.54.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986819","type":"print"},{"value":"9783031986826","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We consider the verification of parameterized networks of replicated processes whose architecture is described by hyperedge-replacement graph grammars in the style of Courcelle. Due to the undecidability of verification problems such as reachability or coverability of a given configuration,\u00a0in which we count the number of replicas in each local state,\u00a0we develop two orthogonal verification techniques. We present\u00a0a counting abstraction able to produce, from a graph grammar describing a parameterized system, a finite set of Petri nets\u00a0that over-approximate the behaviors of the original system. The counting abstraction is implemented in a prototype tool, evaluated on\u00a0a non-trivial set of test cases. Moreover, we identify a decidable fragment, for which the coverability problem is in  and -hard.\n<\/jats:p>","DOI":"10.1007\/978-3-031-98682-6_13","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:15:08Z","timestamp":1753154108000},"page":"238-262","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Counting Abstraction and\u00a0Decidability for\u00a0the\u00a0Verification of\u00a0Structured Parameterized Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4412-5684","authenticated-orcid":false,"given":"Marius","family":"Bozga","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3204-3294","authenticated-orcid":false,"given":"Radu","family":"Iosif","sequence":"additional","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-0003-2726-5036","authenticated-orcid":false,"given":"Neven","family":"Villani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A.,\u00a0Cerans, K.,\u00a0Jonsson, B.,\u00a0Tsay, Y.: General decidability theorems for infinite-state systems. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27\u201330 July 1996, pp. 313\u2013321. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"5","key":"13_CR2","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1142\/S0129054109006887","volume":"20","author":"PA Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno, G., Henda, N.B., Rezine, A.: Monotonic abstraction: on efficient verification of parameterized systems. Int. J. Found. Comput. Sci. 20(5), 779\u2013801 (2009)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"2","key":"13_CR3","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/s10703-008-0062-9","volume":"34","author":"PA Abdulla","year":"2009","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Approximated parameterized verification of infinite-state processes with global conditions. Formal Methods Syst. Des. 34(2), 126\u2013156 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Aminof, B., Jacobs, S., Khalimov, A., Rubin, S.: Parameterized model checking of tokenpassing systems. In: VMCAI 2014. LNCS, vol. 8318, pp. 262\u2013281. Springer (2014)","DOI":"10.1007\/978-3-642-54013-4_15"},{"issue":"3","key":"13_CR5","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s00446-017-0302-6","volume":"31","author":"B Aminof","year":"2018","unstructured":"Aminof, B., Kotek, T., Rubin, S., Spegni, F., Veith, H.: Parameterized model checking of rendezvous systems. Distributed Comput. 31(3), 187\u2013222 (2018)","journal-title":"Distributed Comput."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Aminof, B., Rubin, S.: Model checking parameterised multi-token systems via the composition method. In IJCAR 2016. LNCS, vol. 9706, pp. 499\u2013515. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_34"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Bloem, R.,\u00a0Jacobs, S.,\u00a0Khalimov, A.: Decidability of Parameterized Verification. Morgan & Claypool Publishers (2015)","DOI":"10.1007\/978-3-031-02011-7"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers (2015)","DOI":"10.1007\/978-3-031-02011-7"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Bozga, M.,\u00a0Esparza, J.,\u00a0Iosif, R.,\u00a0Sifakis, J.,\u00a0Welzel, C.: Structural invariants for the verification of systems with parameterized architectures. In:\u00a0Biere, A.,\u00a0Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, 25\u201330 April 2020, Proceedings, Part I. LNCS, vol. 12078, pp. 228\u2013246. Springer (2020)","DOI":"10.1007\/978-3-030-45190-5_13"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Bozga, M.,\u00a0Iosif, R.,\u00a0Sangnier, A.,\u00a0Villani, N.: Counting abstraction for the verification of structured parameterized networks (full version) (2025). arxiv.org\/abs\/2502.15391","DOI":"10.1007\/978-3-031-98682-6_13"},{"key":"13_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2020.100621","volume":"119","author":"M Bozga","year":"2021","unstructured":"Bozga, M., Iosif, R., Sifakis, J.: Checking deadlock-freedom of parametric component-based systems. J. Log. Algebraic Methods Program. 119, 100621 (2021)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Bozga, M.,\u00a0Iosif, R.,\u00a0Sifakis, J.: Verification of component-based systems with recursive architectures. Theor. Comput. Sci. 940(Part), 146\u2013175 (2023)","DOI":"10.1016\/j.tcs.2022.10.022"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Bradbury, J.,\u00a0Cordy, J.,\u00a0Dingel, J.,\u00a0Wermelinger, M.: A survey of self-management in dynamic software architecture specifications. In: Proceedings of the 1st ACM SIGSOFT Workshop on Self-Managed Systems, pp. 28\u201333. ACM (2004)","DOI":"10.1145\/1075405.1075411"},{"issue":"1","key":"13_CR14","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M Browne","year":"1989","unstructured":"Browne, M., Clarke, E., Grumberg, O.: Reasoning about networks with many identical finite state processes. Inf. Comput. 81(1), 13\u201331 (1989)","journal-title":"Inf. Comput."},{"key":"13_CR15","unstructured":"Butting, A.,\u00a0Heim, R.,\u00a0Kautz, O., Ringert, J.O.,\u00a0Rumpe, B.,\u00a0Wortmann, A.: A classification of dynamic reconfiguration in component and connector architecture description. In: Proceedings of MODELS 2017 Satellite Event: Workshops (ModComp). CEUR Workshop Proceedings, vol. 2019, pp. 10\u201316. CEUR-WS.org (2017)"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Chen, Y.,\u00a0Hong, C., Lin, A.W.,\u00a0R\u00fcmmer, P.: Learning to prove safety over parameterised concurrent systems. In:\u00a0Stewart, D.,\u00a0Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, pp. 76\u201383. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102244"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach. Encyclopedia of Mathematics and its Applications. Cambridge University Press (2012)","DOI":"10.1017\/CBO9780511977619"},{"key":"13_CR18","doi-asserted-by":"crossref","unstructured":"Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. In: Fundamentals of Computation Theory, pp. 221\u2013232. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60249-6_54"},{"key":"13_CR19","unstructured":"Esparza, J., Raskin, M.A.,\u00a0Welzel, C.: Regular model checking upside-down: an invariant-based approach. In:\u00a0Klin, B.,\u00a0Lasota, S.,\u00a0Muscholl, A. (eds.) 33rd International Conference on Concurrency Theory, CONCUR 2022, Warsaw, Poland, 12\u201316 September 2022. LIPIcs, vol. 243, pp. 23:1\u201323:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"issue":"2","key":"13_CR20","doi-asserted-by":"publisher","first-page":"719","DOI":"10.1007\/s10270-014-0426-0","volume":"14","author":"A Finkel","year":"2015","unstructured":"Finkel, A., Leroux, J.: Recent and simple algorithms for petri nets. Softw. Syst. Model. 14(2), 719\u2013725 (2015)","journal-title":"Softw. Syst. Model."},{"issue":"1","key":"13_CR21","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00263744","volume":"6","author":"Z Galil","year":"1976","unstructured":"Galil, Z.: Hierarchies of complete problems. Acta Informatica 6(1), 77\u201388 (1976). https:\/\/doi.org\/10.1007\/BF00263744","journal-title":"Acta Informatica"},{"issue":"3","key":"13_CR22","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":"13_CR23","doi-asserted-by":"crossref","unstructured":"Hirsch, D.,\u00a0Inverardi, P.,\u00a0Montanari, U.: Graph grammars and constraint solving for software architecture styles. In: Proceedings of the Third International Workshop on Software Architecture, ISAW 1998, New York, NY, USA, pp. 69\u201372. Association for Computing Machinery (1998)","DOI":"10.1145\/288408.288426"},{"issue":"1","key":"13_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theoret. Comput. Sci. 256(1), 93\u2013112 (2001)","journal-title":"Theoret. Comput. Sci."},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Kesten, Y.,\u00a0Pnueli, A.,\u00a0Shahar, E., Zuck, L.D.: Network invariants in action. In: CONCUR 2002 - Concurrency Theory, 13th International Conference. LNCS, vol. 2421, pp. 101\u2013115. Springer (2002)","DOI":"10.1007\/3-540-45694-5_8"},{"issue":"7","key":"13_CR26","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1109\/32.708567","volume":"24","author":"D Le Metayer","year":"1998","unstructured":"Le Metayer, D.: Describing software architecture styles using graph grammars. IEEE Trans. Software Eng. 24(7), 521\u2013533 (1998)","journal-title":"IEEE Trans. Software Eng."},{"key":"13_CR27","doi-asserted-by":"crossref","unstructured":"Lesens, D.,\u00a0Halbwachs, N.,\u00a0Raymond, P.: Automatic verification of parameterized linear networks of processes. In: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 346\u2013357. ACM Press (1997)","DOI":"10.1145\/263699.263747"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Lin, A.W., R\u00fcmmer, P.: Regular model checking revisited. In: Olderog, E., Steffen, B., Yi, W. (eds.) Model Checking, Synthesis, and Learning - Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday. LNCS, vol. 13030, pp. 97\u2013114. Springer (2021)","DOI":"10.1007\/978-3-030-91384-7_6"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"Shtadler, Z.,\u00a0Grumberg, O.: Network grammars, communication behaviors and automatic verification. In:\u00a0Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems, International Workshop. LNCS, vol. 407, pp. 151\u2013165. Springer (1989)","DOI":"10.1007\/3-540-52148-8_13"},{"key":"13_CR30","unstructured":"Villani, N.,\u00a0Iosif, R.,\u00a0Sangnier, A.,\u00a0Bozga, M.: Parcosys: counting abstraction for the verification of structured parameterized networks (2025). Ongoing development version at https:\/\/gricad-gitlab.univ-grenoble-alpes.fr\/neven\/parcosys"},{"key":"13_CR31","doi-asserted-by":"crossref","unstructured":"Wolf, K.: Petri net model checking with LoLA 2. In:\u00a0Khomenko, V., Roux, O.H. (eds.) Application and Theory of Petri Nets and Concurrency - 39th International Conference, PETRI NETS 2018, Bratislava, Slovakia, 24\u201329 June 2018, Proceedings. LNCS, vol. 10877, pp. 351\u2013362. Springer (2018)","DOI":"10.1007\/978-3-319-91268-4_18"},{"key":"13_CR32","unstructured":"Wolf, K.,\u00a0Lohmann, N.: LoLA: a low level petri net analyzer. https:\/\/theo.informatik.uni-rostock.de\/theo-forschung\/tools\/lola\/"},{"key":"13_CR33","doi-asserted-by":"crossref","unstructured":"Wolper, P.,\u00a0Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: Automatic Verification Methods for Finite State Systems, International Workshop. LNCS, vol. 407, pp. 68\u201380. Springer (1989)","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98682-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:38:40Z","timestamp":1759999120000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98682-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986819","9783031986826"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98682-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}