{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T07:59:00Z","timestamp":1743062340408,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_7","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"131-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Asynchronous Correspondences Between Hybrid Trajectory Semantics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0101-9953","authenticated-orcid":false,"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57318-6_30"},{"issue":"2","key":"7_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. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"7_CR3","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30080-9_1","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"R Alur","year":"2004","unstructured":"Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1\u201324. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_1"},{"key":"7_CR5","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.scico.2015.02.003","volume":"105","author":"R Banach","year":"2015","unstructured":"Banach, R., Butler, M.J., Qin, S., Verma, N., Zhu, H.: Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program. 105, 92\u2013123 (2015)","journal-title":"Sci. Comput. Program."},{"key":"7_CR7","unstructured":"Caspi, P., Halbwachs, N.: An approach to real time systems modeling. In: ICDCS. IEEE Computer Society, pp. 710\u2013716 (1982)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_6","volume-title":"NASA Formal Methods","author":"X Chen","year":"2022","unstructured":"Chen, X., Sankaranarayanan, S.: Reachability analysis for cyber-physical systems: are we there yet? In: Deshmukh, J.V., Havelund, K., Perez, I. (eds.) NFM 2022. LNCS, vol. 13260. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_6"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-78428-7_1","volume-title":"Model and Data Engineering","author":"Z Cheng","year":"2021","unstructured":"Cheng, Z., M\u00e9ry, D.: A refinement strategy for hybrid system design with safety constraints. In: Attiogb\u00e9, C., Ben Yahia, S. (eds.) MEDI 2021. LNCS, vol. 12732, pp. 3\u201317. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78428-7_1"},{"issue":"1\u20132","key":"7_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1\u20132), 47\u2013103 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR11","volume-title":"Principles of Abstract Interpretation","author":"P Cousot","year":"2021","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press, Cambridge (2021)"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"D\u2019Innocenzo, A., Julius, A.A., Pappas, G.J., Di Benedetto, M.D., Di Gennaro, S.: Verification of temporal properties on hybrid automata by simulation relations. In: CDC, pp. 4039\u20134044. IEEE (2007)","DOI":"10.1109\/CDC.2007.4434716"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11603009_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"L Doyen","year":"2005","unstructured":"Doyen, L., Henzinger, T.A., Raskin, J.-F.: Automatic rectangular refinement of affine hybrid systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 144\u2013161. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11603009_13"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/11867340_15","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G Frehse","year":"2006","unstructured":"Frehse, G.: On timed simulation relations for hybrid systems and compositionality. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 200\u2013214. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11867340_15"},{"issue":"2","key":"7_CR15","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s10626-007-0029-9","volume":"18","author":"A Girard","year":"2008","unstructured":"Girard, A., Julius, A.A., Pappas, G.J.: Approximate simulation relations for hybrid systems. Discret. Event Dyn. Syst. 18(2), 163\u2013179 (2008). https:\/\/doi.org\/10.1007\/s10626-007-0029-9","journal-title":"Discret. Event Dyn. Syst."},{"issue":"5\u20136","key":"7_CR16","doi-asserted-by":"publisher","first-page":"568","DOI":"10.3166\/ejc.17.568-578","volume":"17","author":"A Girard","year":"2011","unstructured":"Girard, A., Pappas, G.J.: Approximate bisimulation: a bridge between computer science and control theory. Eur. J. Control. 17(5\u20136), 568\u2013578 (2011)","journal-title":"Eur. J. Control."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid Systems II","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: A note on abstract interpretation strategies for hybrid automata. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 252\u2013264. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60472-3_13"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: STOC, pp. 373\u2013382. ACM (1995)","DOI":"10.1145\/225058.225162"},{"key":"7_CR19","volume-title":"Analysis of Numerical Methods","author":"E Isaacson","year":"1994","unstructured":"Isaacson, E., Keller, H.B.: Analysis of Numerical Methods. Dover, Mineola (1994)"},{"key":"7_CR20","volume-title":"Introduction to the Theory of Dynamical Systems","author":"A Katok","year":"1999","unstructured":"Katok, A., Hasselblatt, B.: Introduction to the Theory of Dynamical Systems. Cambridge University Press, Cambridge (1999)"},{"key":"7_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2698-5","volume-title":"Undergraduate Analysis","author":"S Lang","year":"1997","unstructured":"Lang, S.: Undergraduate Analysis, 2nd edn. Springer, Heidelberg (1997)","edition":"2"},{"key":"7_CR22","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0017-8","volume-title":"Switching in Systems and Control","author":"D Liberzon","year":"2003","unstructured":"Liberzon, D.: Switching in Systems and Control. Birkh\u00e4user, Basel (2003)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/3-540-58043-3_24","volume-title":"A Decade of Concurrency Reflections and Perspectives","author":"N Lynch","year":"1994","unstructured":"Lynch, N.: Simulation techniques for proving properties of real-time systems. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 375\u2013424. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58043-3_24"},{"key":"7_CR24","unstructured":"MathWorks. Simulation and model-based design. https:\/\/www.mathworks.com\/products\/simulink.html (2022)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/11783596_19","volume-title":"Mathematics of Program Construction","author":"L Meinicke","year":"2006","unstructured":"Meinicke, L., Hayes, I.J.: Continuous action system refinement. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 316\u2013337. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11783596_19"},{"key":"7_CR26","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Proceedings IJCAI, vol. 1971, pp. 481\u2013489 (1971)"},{"key":"7_CR27","series-title":"PHI Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science, Prentice Hall, Hoboken (1989)"},{"issue":"2","key":"7_CR28","first-page":"617","volume":"47","author":"H Nyquist","year":"1928","unstructured":"Nyquist, H.: Certain topics in telegraph transmission theory. Proc. IEEE 47(2), 617\u2013644 (1928)","journal-title":"Proc. IEEE"},{"key":"7_CR29","unstructured":"Proakis, J.G., Manolakis, D.G.: Digital Signal Processing. Pearson, 4th (edn) (2006)"},{"key":"7_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511801204","volume-title":"An Introduction to Ordinary Differential Equations","author":"JC Robinson","year":"2004","unstructured":"Robinson, J.C.: An Introduction to Ordinary Differential Equations. Cambridge University Press, Cambridge (2004)"},{"issue":"1","key":"7_CR31","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1016\/S0304-3975(02)00547-9","volume":"290","author":"M R\u00f6kk\u00f6","year":"2003","unstructured":"R\u00f6kk\u00f6, M., Ravn, A.P., Sere, K.: Hybrid action systems. Theor. Comput. Sci. 290(1), 937\u2013973 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR32","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"D Sangiorgi","year":"2011","unstructured":"Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Shannon, C.E.: Communication in the presence of noise. In: Proceedings of the I.R.E., pp. 10\u201321 (1949)","DOI":"10.1109\/JRPROC.1949.232969"},{"issue":"2","key":"7_CR34","doi-asserted-by":"publisher","first-page":"209","DOI":"10.2140\/pjm.1974.54.209","volume":"54","author":"Z Shmuely","year":"1974","unstructured":"Shmuely, Z.: The structure of Galois connections. Pac. J. Math. 54(2), 209\u2013225 (1974)","journal-title":"Pac. J. Math."},{"key":"7_CR35","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1016\/j.scico.2014.04.015","volume":"94","author":"S Wen","year":"2014","unstructured":"Wen, S., Abrial, J.-R., Zhu, H.: Formalizing hybrid systems with Event-B and the Rodin platform. Sci. Comput. Program. 94, 164\u2013202 (2014)","journal-title":"Sci. Comput. Program."},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-030-30942-8_23","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"YK Tan","year":"2019","unstructured":"Tan, Y.K., Platzer, A.: An axiomatic approach to liveness for differential equations. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 371\u2013388. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_23"},{"key":"7_CR37","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pacific J. of Math. 5, 285\u2013310 (1955)","journal-title":"Pacific J. of Math."},{"issue":"1","key":"7_CR38","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994)","journal-title":"Inf. Comput."},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/3-540-46430-1_37","volume-title":"Hybrid Systems: Computation and Control","author":"J Zhang","year":"2000","unstructured":"Zhang, J., Johansson, K.H., Lygeros, J., Sastry, S.: Dynamical systems revisited: hybrid systems with Zeno executions. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 451\u2013464. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46430-1_37"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T00:06:37Z","timestamp":1672358797000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}