{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T11:04:25Z","timestamp":1753182265498,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031404351"},{"type":"electronic","value":"9783031404368"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"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":[[2023]]},"DOI":"10.1007\/978-3-031-40436-8_11","type":"book-chapter","created":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T23:04:03Z","timestamp":1694127843000},"page":"297-322","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Assume-Guarantee Reasoning for\u00a0Additive Hybrid Behaviour"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5487-4972","authenticated-orcid":false,"given":"Pieter J. L.","family":"Cuijpers","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3612-4139","authenticated-orcid":false,"given":"Jonas","family":"Hansen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5953-3384","authenticated-orcid":false,"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,8]]},"reference":[{"key":"11_CR1","doi-asserted-by":"publisher","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Tjoa, A.M., Gruhn, V. (eds.) Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, Vienna, Austria, 10\u201314 September 2001, pp. 109\u2013120. ACM (2001). https:\/\/doi.org\/10.1145\/503209.503226","DOI":"10.1145\/503209.503226"},{"issue":"2","key":"11_CR2","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). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theoret. Comput. Sci."},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-319-95582-7_12","volume-title":"Formal Methods","author":"G Bacci","year":"2018","unstructured":"Bacci, G., Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Reynier, P.-A.: Optimal and robust controller synthesis. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 203\u2013221. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_12"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-28872-2_3","volume-title":"Fundamental Approaches to Software Engineering","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., et al.: Moving from specifications to contracts in component-based design. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43\u201358. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_3"},{"issue":"2\u20133","key":"11_CR5","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2\u20133), 124\u2013400 (2018). https:\/\/doi.org\/10.1561\/1000000053","journal-title":"Found. Trends Electron. Des. Autom."},{"key":"11_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(85)90088-X","volume":"37","author":"JA Bergstra","year":"1985","unstructured":"Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77\u2013121 (1985). https:\/\/doi.org\/10.1016\/0304-3975(85)90088-X","journal-title":"Theor. Comput. Sci."},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-52590-4_40","volume-title":"CAAP \u201990","author":"G Boudol","year":"1990","unstructured":"Boudol, G., Larsen, K.G.: Graphical versus logical specifications. In: Arnold, A. (ed.) CAAP 1990. LNCS, vol. 431, pp. 57\u201371. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52590-4_40"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-319-41528-4_28","volume-title":"Computer Aided Verification","author":"P Bouyer","year":"2016","unstructured":"Bouyer, P., Colange, M., Markey, N.: Symbolic optimal reachability in weighted timed automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 513\u2013530. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_28"},{"issue":"34","key":"11_CR9","doi-asserted-by":"publisher","first-page":"4373","DOI":"10.1016\/j.tcs.2011.05.010","volume":"412","author":"B Caillaud","year":"2011","unstructured":"Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Constraint Markov chains. Theor. Comput. Sci. 412(34), 4373\u20134404 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.05.010","journal-title":"Theor. Comput. Sci."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-56922-7_21","volume-title":"Computer Aided Verification","author":"K \u010cer\u0101ns","year":"1993","unstructured":"\u010cer\u0101ns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification\u2014theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253\u2013267. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56922-7_21"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-78929-1_9","volume-title":"Hybrid Systems: Computation and Control","author":"PJL Cuijpers","year":"2008","unstructured":"Cuijpers, P.J.L., Reniers, M.A.: Lost in translation: hybrid-time flows vs. real-time transitions. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 116\u2013129. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_9"},{"issue":"6","key":"11_CR12","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/s10009-012-0237-y","volume":"14","author":"A David","year":"2012","unstructured":"David, A., et al.: Compositional verification of real-time systems using Ecdar. Int. J. Softw. Tools Technol. Transf. 14(6), 703\u2013720 (2012). https:\/\/doi.org\/10.1007\/s10009-012-0237-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"11_CR13","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u0103ionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015). https:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR14","doi-asserted-by":"publisher","unstructured":"David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: Timed I\/O automata: a complete specification theory for real-time systems. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, 12\u201315 April 2010, pp. 91\u2013100. ACM (2010). https:\/\/doi.org\/10.1145\/1755952.1755967","DOI":"10.1145\/1755952.1755967"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"van Glabbeek, R.J.: The linear time - branching time spectrum I: the semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, chap. 1, pp. 3\u201399. Elsevier Science, Amsterdam (2001). https:\/\/doi.org\/10.1016\/B978-044482830-9\/50019-9","DOI":"10.1016\/B978-044482830-9\/50019-9"},{"key":"11_CR16","doi-asserted-by":"publisher","unstructured":"Hansen, J., Larsen, K.G., Cuijpers, P.J.L.: Balancing flexible production and consumption of energy using resource timed automata. In: 2022 11th Mediterranean Conference on Embedded Computing (MECO), pp. 1\u20136 (2022). https:\/\/doi.org\/10.1109\/MECO55406.2022.9797191","DOI":"10.1109\/MECO55406.2022.9797191"},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/BF01887207","volume":"1","author":"J He","year":"1989","unstructured":"He, J.: Process simulation and refinement. Formal Aspects Comput. 1(3), 229\u2013241 (1989). https:\/\/doi.org\/10.1007\/BF01887207","journal-title":"Formal Aspects Comput."},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-52559-9_70","volume-title":"Stepwise Refinement of Distributed Systems Models, Formalisms, Correctness","author":"H Jifeng","year":"1990","unstructured":"Jifeng, H.: Various simulations and refinements. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 340\u2013360. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52559-9_70"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"He, J.: Service refinement. In: 15th Asia-Pacific Software Engineering Conference (APSEC 2008), 3\u20135 December 2008, Beijing, China, p. 5. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/APSEC.2008.78","DOI":"10.1109\/APSEC.2008.78"},{"key":"11_CR20","unstructured":"He, J., Hoare, C.A.R.: Unifying theories of programming. In: Orlowska, E., Szalas, A. (eds.) Participants Copies for Relational Methods in Logic, Algebra and Computer Science, 4th International Seminar RelMiCS, Warsaw, Poland, 14\u201320 September 1998, pp. 97\u201399 (1998)"},{"key":"11_CR21","doi-asserted-by":"publisher","unstructured":"He, J., Liu, Z., Li, X.: Towards a refinement calculus for object systems. In: Proceedings of the 1st IEEE International Conference on Cognitive Informatics (ICCI 2002), 19\u201320 August 2002, Calgary, Canada, pp. 69\u201376. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/COGINF.2002.1039284","DOI":"10.1109\/COGINF.2002.1039284"},{"key":"11_CR22","series-title":"NATO ASI Series","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"TA Henzinger","year":"2000","unstructured":"Henzinger, T.A., Kurshan, R.P.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series, vol. 170, pp. 265\u2013292. Springer, Heidelberg (2000)"},{"key":"11_CR23","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall (1985)"},{"issue":"2","key":"11_CR24","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/0020-0190(87)90106-2","volume":"24","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127\u2013132 (1987). https:\/\/doi.org\/10.1016\/0020-0190(87)90106-2","journal-title":"Inf. Process. Lett."},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/BFb0002714","volume-title":"Euro-Par\u201997 Parallel Processing","author":"T Hoare","year":"1997","unstructured":"Hoare, T., He, J.: Unifying theories for parallel programming. In: Lengauer, C., Griebl, M., Gorlatch, S. (eds.) Euro-Par 1997. LNCS, vol. 1300, pp. 15\u201330. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0002714"},{"issue":"2","key":"11_CR26","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","volume":"25","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., He, J., Sanders, J.W.: Prespecification in data refinement. Inf. Process. Lett. 25(2), 71\u201376 (1987). https:\/\/doi.org\/10.1016\/0020-0190(87)90224-9","journal-title":"Inf. Process. Lett."},{"key":"11_CR27","unstructured":"Jones, C.B.: Developing methods for computer programs including a notion of interference. Ph.D. thesis, University of Oxford, UK (1981). https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.259064"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-57318-6_25","volume-title":"Hybrid Systems","author":"L Lamport","year":"1993","unstructured":"Lamport, L.: Hybrid systems in TLA$$^{+}$$. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 77\u2013102. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_25"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Computer Aided Verification","author":"K Larsen","year":"2001","unstructured":"Larsen, K., et al.: As cheap as possible: efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493\u2013505. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_47"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232\u2013246. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_19"},{"key":"11_CR31","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Rasmussen, J.I.: Optimal reachability for multi-priced timed automata. Theor. Comput. Sci. 390(2), 197\u2013213 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2007.09.021. Foundations Software Science and Computational Structures","DOI":"10.1016\/j.tcs.2007.09.021"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BFb0024437","volume-title":"Formal Systems Specification","author":"KG Larsen","year":"1996","unstructured":"Larsen, K.G., Steffen, B., Weise, C.: The methodology of modal constraints. In: Broy, M., Merz, S., Spies, K. (eds.) Formal Systems Specification. LNCS, vol. 1169, pp. 405\u2013435. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0024437"},{"key":"11_CR33","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Thomsen, B.: A modal process logic. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS 1988), Edinburgh, Scotland, UK, 5\u20138 July 1988, pp. 203\u2013210. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/LICS.1988.5119","DOI":"10.1109\/LICS.1988.5119"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer, Cham (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3","DOI":"10.1007\/3-540-10235-3"},{"key":"11_CR35","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inform. 6, 319\u2013340 (1976). https:\/\/doi.org\/10.1007\/BF00268134","journal-title":"Acta Inform."},{"key":"11_CR36","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/3-540-57182-5_60","volume-title":"Mathematical Foundations of Computer Science 1993","author":"D Scholefield","year":"1993","unstructured":"Scholefield, D., Zedan, H., Jifeng, H.: Real-time refinement: semantics and application. In: Borzyszkowski, A.M., Soko\u0142owski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 693\u2013702. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57182-5_60"},{"issue":"2","key":"11_CR38","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects Comput. 9(2), 149\u2013174 (1997). https:\/\/doi.org\/10.1007\/BF01211617","journal-title":"Formal Aspects Comput."}],"container-title":["Lecture Notes in Computer Science","Theories of Programming and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-40436-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T23:05:42Z","timestamp":1694127942000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-40436-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031404351","9783031404368"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-40436-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"8 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}