{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:19:36Z","timestamp":1743128376937,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031661488"},{"type":"electronic","value":"9783031661495"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-66149-5_4","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"67-84","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Hypergraph-Based Formalization of\u00a0Hierarchical Reactive Modules and\u00a0a\u00a0Compositional Verification Method"],"prefix":"10.1007","author":[{"given":"Daisuke","family":"Ishii","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"issue":"5","key":"4_CR1","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/s00165-017-0436-0","volume":"30","author":"K Abd Elkader","year":"2018","unstructured":"Abd Elkader, K., Grumberg, O., P\u0103s\u0103reanu, C.S., Shoham, S.: Automated circular assume-guarantee reasoning. Formal Aspects Comput. 30(5), 571\u2013595 (2018). https:\/\/doi.org\/10.1007\/s00165-017-0436-0","journal-title":"Formal Aspects Comput."},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521\u2013525. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028774"},{"unstructured":"Alur, R.: Synchronous Model. In: Principles of Cyber-Physical Systems, pp. 13\u201364. MIT Press (2015)","key":"4_CR3"},{"doi-asserted-by":"publisher","unstructured":"Alur, R., Grosu, R.: Modular refinement of hierarchic reactive machines. In: POPL, pp. 390\u2013402 (2000). https:\/\/doi.org\/10.1145\/325694.325746","key":"4_CR4","DOI":"10.1145\/325694.325746"},{"issue":"1\u20132","key":"4_CR5","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.jlap.2005.10.004","volume":"68","author":"R Alur","year":"2006","unstructured":"Alur, R., Grosu, R., Lee, I., Sokolsky, O.: Compositional modeling and refinement for hierarchical hybrid systems. J. Logic Algebraic Program. 68(1\u20132), 105\u2013128 (2006). https:\/\/doi.org\/10.1016\/j.jlap.2005.10.004","journal-title":"J. Logic Algebraic Program."},{"issue":"1","key":"4_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Methods Syst. Des. 15(1), 7\u201348 (1999). https:\/\/doi.org\/10.1023\/A:1008739929481","journal-title":"Formal Methods Syst. Des."},{"issue":"3","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3461669","volume":"5","author":"G Bakirtzis","year":"2021","unstructured":"Bakirtzis, G., Fleming, C.H., Vasilakopoulou, C.: Categorical semantics of cyber-physical systems theory. ACM Trans. Cyber-Phys. Syst. 5(3), 1\u201332 (2021). https:\/\/doi.org\/10.1145\/3461669","journal-title":"ACM Trans. Cyber-Phys. Syst."},{"issue":"4","key":"4_CR8","doi-asserted-by":"publisher","first-page":"1141","DOI":"10.1007\/s10270-015-0477-x","volume":"15","author":"P Bostr\u00f6m","year":"2016","unstructured":"Bostr\u00f6m, P., Wiik, J.: Contract-based verification of discrete-time multi-rate Simulink models. Softw. Syst. Model. 15(4), 1141\u20131161 (2016). https:\/\/doi.org\/10.1007\/s10270-015-0477-x","journal-title":"Softw. Syst. Model."},{"doi-asserted-by":"publisher","unstructured":"Bretto, A.: Hypergraph Theory: An Introduction. Mathematical Engineering, Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-00080-0","key":"4_CR9","DOI":"10.1007\/978-3-319-00080-0"},{"doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: a declarative language for programming synchronous systems. In: POPL, pp. 178\u2013188 (1987)","key":"4_CR10","DOI":"10.1145\/41625.41641"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"510","DOI":"10.1007\/978-3-319-41540-6_29","volume-title":"Computer Aided Verification","author":"A Champion","year":"2016","unstructured":"Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510\u2013517. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_29"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-41591-8_24","volume-title":"Software Engineering and Formal Methods","author":"A Champion","year":"2016","unstructured":"Champion, A., Gurfinkel, A., Kahsai, T., Tinelli, C.: CoCoSpec: a mode-aware contract language for reactive systems. In: De Nicola, R., K\u00fchn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 347\u2013366. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_24"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-32582-8_3","volume-title":"Model Checking Software","author":"I Dragomir","year":"2016","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: Compositional semantics and analysis of hierarchical block diagrams. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 38\u201356. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-32582-8_3"},{"issue":"6","key":"4_CR14","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/s10009-020-00561-4","volume":"22","author":"I Dragomir","year":"2020","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: The refinement calculus of reactive systems toolset. Int. J. Softw. Tools Technol. Transfer 22(6), 689\u2013708 (2020). https:\/\/doi.org\/10.1007\/s10009-020-00561-4","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"doi-asserted-by":"crossref","unstructured":"Fong, B., Spivak, D.I.: An Invitation to Applied Category Theory: Seven Sketches in Compositionality. Cambridge University Press, Cambridge (2019)","key":"4_CR15","DOI":"10.1017\/9781108668804"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-10575-8_12","volume-title":"Handbook of Model Checking","author":"D Giannakopoulou","year":"2018","unstructured":"Giannakopoulou, D., Namjoshi, K.S., P\u0103s\u0103reanu, C.S.: Compositional reasoning. In: Handbook of Model Checking, pp. 345\u2013383. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_12"},{"doi-asserted-by":"publisher","unstructured":"Murugesan, A., Whalen, M.W., Rayadurgam, S., Heimdahl, M.P.: Compositional verification of a medical device system. In: ACM SIGAda Annual Conference on High Integrity Language Technology, pp. 51\u201364 (2013). https:\/\/doi.org\/10.1145\/2527269.2527272","key":"4_CR17","DOI":"10.1145\/2527269.2527272"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-031-30826-0_3","volume-title":"FASE 2023","author":"T Neele","year":"2023","unstructured":"Neele, T., Sammartino, M.: Compositional automata learning of synchronous systems. In: Lambers, L., Uchitel, S. (eds.) FASE 2023. Lecture Notes in Computer Science, vol. 13991, pp. 47\u201366. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30826-0_3"},{"unstructured":"Ouvrard, X.: Hypergraphs: an introduction and review. CoRR arXiv:2002.05014 (2020)","key":"4_CR19"},{"issue":"3","key":"4_CR20","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-008-0049-6","volume":"32","author":"CS P\u0103s\u0103reanu","year":"2008","unstructured":"P\u0103s\u0103reanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Formal Meth. Syst. Des. 32(3), 175\u2013205 (2008). https:\/\/doi.org\/10.1007\/s10703-008-0049-6","journal-title":"Formal Meth. Syst. Des."},{"key":"4_CR21","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104819","volume":"285","author":"V Preoteasa","year":"2022","unstructured":"Preoteasa, V., Dragomir, I., Tripakis, S.: The refinement calculus of reactive systems. Inf. Comput. 285, 104819 (2022). https:\/\/doi.org\/10.1016\/j.ic.2021.104819","journal-title":"Inf. Comput."},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-319-95246-8_26","volume-title":"Principles of Modeling","author":"S Tripakis","year":"2018","unstructured":"Tripakis, S., Lublinerman, R.: Modular code generation from synchronous block diagrams: interfaces, abstraction, compositionality. In: Lohstroh, M., Derler, P., Sirjani, M. (eds.) Principles of Modeling. LNCS, vol. 10760, pp. 449\u2013477. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95246-8_26"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:06:12Z","timestamp":1728716772000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","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":"10 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":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}