{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:42:08Z","timestamp":1777347728422,"version":"3.51.4"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986673","type":"print"},{"value":"9783031986680","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,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"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>Simulation-based compositional abstraction effectively mitigates state space explosion in model checking, particularly for timed systems. However, existing approaches do not support broadcast synchronization, an important mechanism for modeling non-blocking one-to-many communication in multi-component systems. Consequently, they also lack a parallel composition operator that simultaneously supports broadcast synchronization, binary synchronization, shared variables, and committed locations. To address this, we propose a simulation-based compositional abstraction framework for timed systems, which supports these modeling concepts and is compatible with the popular UPPAAL model checker. Our framework is general, with the only additional restriction being that the timed automata are prohibited from updating shared variables when receiving broadcast signals. Through two case studies, our framework demonstrates superior verification efficiency compared to traditional monolithic methods.<\/jats:p>","DOI":"10.1007\/978-3-031-98668-0_8","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T20:45:50Z","timestamp":1753130750000},"page":"162-184","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Compositional Abstraction for\u00a0Timed Systems with\u00a0Broadcast Synchronization"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9434-1695","authenticated-orcid":false,"given":"Hanyue","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Miaomiao","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro, L., da\u00a0Silva, L.D., Faella, M., Legay, A., Roy, P., Sorea, M.: Sociable interfaces. In: Frontiers of Combining Systems, pp. 81\u2013105. Springer, Heidelberg (2005)","DOI":"10.1007\/11559306_5"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R.: Timed automata. In: Proceeding of the 11th International Conference on Computer Aided Verification, pp. 8\u201322. Springer (1999)","DOI":"10.1007\/3-540-48683-6_3"},{"issue":"2","key":"8_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"van Beek, D.A., Reniers, M.A., Schiffelers, R.R.H., Rooda, J.E.: Foundations of a compositional interchange format for hybrid systems. In: Hybrid Systems: Computation and Control, pp. 587\u2013600. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-71493-4_45"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Berendsen, J., Gebremichael, B., Vaandrager, F.W., Zhang, M.: Formal specification and analysis of zeroconf using uppaalS 10(3) (2011)","DOI":"10.1145\/1952522.1952527"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/j.jal.2009.11.001","volume":"8","author":"J Berendsen","year":"2010","unstructured":"Berendsen, J., Jansen, D.N., Schmaltz, J., Vaandrager, F.W.: The axiomatization of override and update. J. Appl. Log. 8(1), 141\u2013150 (2010)","journal-title":"J. Appl. Log."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Berendsen, J., Vaandrager, F.: Compositional abstraction in real-time model checking. In: Formal Modeling and Analysis of Timed Systems, pp. 233\u2013249. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-85778-5_17"},{"key":"8_CR10","unstructured":"Berendsen, J., Vaandrager, F.: Parallel composition in a paper of Jensen, Larsen and Skou is not associative. Technical report, technical note (2007)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Bhat, G., Cleaveland, R., L\u00fcttgen, G.: Dynamic priorities for modeling real-time, pp. 321\u2013336. Springer (1997)","DOI":"10.1007\/978-0-387-35271-8_20"},{"key":"8_CR12","unstructured":"Brockway, M.J.: A Compositional Analysis of Broadcasting Embedded Systems. Ph.D. thesis (2010)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Cao, Y., Duan, Z., Wang, Y.: Uninterrupted automatic broadcasting based on timed automata. In: 2015 3rd International Conference on Applied Computing and Information Technology\/2nd International Conference on Computational Science and Intelligence, pp. 489\u2013494 (2015)","DOI":"10.1109\/ACIT-CSI.2015.93"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Chen, H., Su, Y., Zhang, M., Liu, Z., Mi, J.: Learning assumptions for compositional verification of timed automata. In: Proceeding of the 35th International Conference on Computer Aided Verification, pp. 40\u201361. Springer, Cham (2023)","DOI":"10.1007\/978-3-031-37706-8_3"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Chen, H., Zhang, M., Vaandrager, F.: Compositional abstraction for timed systems with broadcast synchronization (2025). https:\/\/arxiv.org\/abs\/2505.12436","DOI":"10.1007\/978-3-031-98668-0_8"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. Springer, Heidelberg (1997)","DOI":"10.1007\/978-3-642-61455-2_16"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Workshop on Logic of Programs, pp. 52\u201371. Springer (1981)","DOI":"10.1007\/BFb0025774"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: ACM-SIGACT Symposium on Principles of Programming Languages (1992)","DOI":"10.1145\/143165.143235"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Delzanno, G., Podelski, A., Esparza, J.: Constraint-based analysis of broadcast protocols. In: Computer Science Logic, pp. 50\u201366. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48168-0_5"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Dierks, H., Kupferschmid, S., Larsen, K.G.: Automatic abstraction refinement for timed automata. In: Formal Modeling and Analysis of Timed Systems, pp. 114\u2013129. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-75454-1_10"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Ejersbo\u00a0Jensen, H., Guldstrand\u00a0Larsen, K., Skou, A.: Scaling up uppaal. In: Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 19\u201330. Springer, Heidelberg (2000)","DOI":"10.1007\/3-540-45352-0_4"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of the 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp. 352\u2013359 (1999)","DOI":"10.1109\/LICS.1999.782630"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Fehnker, A., van Glabbeek, R., H\u00f6fner, P., McIver, A., Portmann, M., Tan, W.L.: Automated analysis of AODV using UPPAAL. In: Tools and Algorithms for the Construction and Analysis of Systems, pp. 173\u2013187. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28756-5_13"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Fei, Y., Zhu, H., Li, X.: Modeling and verification of NLSR protocol using UPPAAL. In: 2018 International Symposium on Theoretical Aspects of Software Engineering, pp. 108\u2013115 (2018)","DOI":"10.1109\/TASE.2018.00022"},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Fisman, D., Izsak, N., Jacobs, S.: Learning broadcast protocols. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 38, no. 11, pp. 12016\u201312023 (2024)","DOI":"10.1609\/aaai.v38i11.29089"},{"key":"8_CR26","unstructured":"Goorden, M.A., Larsen, K.G., Legay, A., Lorber, F., Nyman, U., Wasowski, A.: Timed I\/O automata: it is never too late to complete your timed specification theory. CoRR abs\/2302.04529 (2023). https:\/\/doi.org\/10.48550\/arXiv.2302.04529"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Hanssen, F., Mader, A., Jansen, P.: Verifying the distributed real-time network protocol RTnet using Uppaal. In: 14th IEEE International Symposium on Modeling, Analysis, and Simulation, pp. 239\u2013246 (2006)","DOI":"10.1109\/MASCOTS.2006.52"},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.tcs.2011.07.018","volume":"413","author":"F Heidarian","year":"2012","unstructured":"Heidarian, F., Schmaltz, J., Vaandrager, F.: Analysis of a clock synchronization protocol for wireless sensor networks. Theoret. Comput. Sci. 413(1), 87\u2013105 (2012)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Henderson, W.D., Tron, S.: Verification of the minimum cost forwarding protocol for wireless sensor networks. In: 2006 IEEE Conference on Emerging Technologies and Factory Automation, pp. 194\u2013201 (2006)","DOI":"10.1109\/ETFA.2006.355457"},{"key":"8_CR30","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Schilling, C., Srba, J.: Simulation Relations and Applications in Formal Methods, pp. 272\u2013291. Springer, Cham (2022)","DOI":"10.1007\/978-3-031-22337-2_13"},{"issue":"1","key":"8_CR32","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Hybrid I\/O automata. Inf. Comput. 185(1), 105\u2013157 (2003)","journal-title":"Inf. Comput."},{"key":"8_CR33","unstructured":"Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)"},{"key":"8_CR34","first-page":"219","volume":"2","author":"NA Lynch","year":"1989","unstructured":"Lynch, N.A., Tuttle, M.R.: An introduction to input\/output automata. CWI Q. 2, 219\u2013246 (1989)","journal-title":"CWI Q."},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Merz, S.: Model checking: a tutorial overview. In: Modeling and Verification of Parallel Processes, vol.\u00a02067, pp. 3\u201338. Springer (2000)","DOI":"10.1007\/3-540-45510-8_1"},{"key":"8_CR36","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Inc (1989)"},{"key":"8_CR37","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence, IJCAI 1971, pp. 481\u2013489. Morgan Kaufmann Publishers Inc. (1971)"},{"issue":"1","key":"8_CR38","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes. I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"I. Inf. Comput."},{"key":"8_CR39","doi-asserted-by":"publisher","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22","DOI":"10.1007\/3-540-11494-7_22"},{"issue":"4","key":"8_CR40","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.ifacol.2021.04.071","volume":"53","author":"R Szpak","year":"2020","unstructured":"Szpak, R., de Queiroz, M.H., Ribeiro Cury, J.E.: Synthesis and implementation of supervisory control for manufacturing systems under processing uncertainties and time constraints. IFAC-PapersOnLine 53(4), 229\u2013234 (2020)","journal-title":"IFAC-PapersOnLine"}],"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-98668-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,27]],"date-time":"2026-04-27T15:07:48Z","timestamp":1777302468000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98668-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986673","9783031986680"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98668-0_8","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":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"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"}}]}}