{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T06:00:48Z","timestamp":1774332048054,"version":"3.50.1"},"publisher-location":"Cham","reference-count":51,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319486277","type":"print"},{"value":"9783319486284","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-48628-4_5","type":"book-chapter","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T12:45:31Z","timestamp":1488372331000},"page":"95-120","source":"Crossref","is-referenced-by-count":6,"title":["Linking Discrete and Continuous Models, Applied to Traffic Manoeuvrers"],"prefix":"10.1007","author":[{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders P.","family":"Ravn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rafael","family":"Wisniewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,3,2]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Safety assessment of autonomous cars using verification techniques. In: American Control Conference (ACC) 2007, pp. 4154\u20134159. IEEE (2007)","DOI":"10.1109\/ACC.2007.4282809"},{"issue":"1","key":"5_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"5_CR3","doi-asserted-by":"crossref","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. TCS 126(2), 183\u2013235 (1994)","journal-title":"TCS"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Ames, A.D., Cousineau, E.A., Powell, M.J.: Dynamically stable bipedal robotic walking with nao via human-inspired hybrid zero dynamics. In: HSCC 2012, pp. 135\u2013144. ACM (2012)","DOI":"10.1145\/2185632.2185655"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Arechiga, N., Loos, S.M., Platzer, A., Krogh, B.H.: Using theorem provers to guarantee closed-loop system properties. In: American Control Conference (ACC) 2012, pp. 3573\u20133580. IEEE (2012)","DOI":"10.1109\/ACC.2012.6315388"},{"issue":"4","key":"5_CR6","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s11786-011-0098-x","volume":"5","author":"W Damm","year":"2011","unstructured":"Damm, W., Ihlemann, C., Sofroni-Stokkermans, V.: PTIME parametric verification of safety properties for reasonable linear hybrid systems. Math. Comput. Sci. 5(4), 469\u2013497 (2011)","journal-title":"Math. Comput. Sci."},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Damm, W., M\u00f6hlmann, E., Rakow, A.: Component based design of hybrid systems: a case study on concurrency and coupling. In: HSCC 2014, pp. 145\u2013150. ACM (2014)","DOI":"10.1145\/2562059.2562120"},{"key":"5_CR8","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W-P Roever de","year":"1998","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, New York (1998)"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z: Foundations and Advanced Applications. Springer, London (2014)","DOI":"10.1007\/978-1-4471-5355-9"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.D., Choi, J., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171\u2013185. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-88387-6_14"},{"issue":"3","key":"5_CR11","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Form. Methods Syst. Des. 30(3), 179\u2013198 (2007)","journal-title":"Form. Methods Syst. Des."},{"issue":"3","key":"5_CR12","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263\u2013279 (2008)","journal-title":"STTT"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Frehse, G., Guernic, C., Donz\u00e9, A., Cotton, S., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1145\/2461328.2461361","volume":"2014","author":"G Frehse","year":"2013","unstructured":"Frehse, G., Kateja, R., Guernic, C.L.: Flowpipe approximation and clustering in space-time. HSCC 2014, 203\u2013212 (2013)","journal-title":"HSCC"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds).: Hybrid Systems. LNCS, vol. 736, Springer, Heidelberg (1993)","DOI":"10.1007\/3-540-57318-6"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Grumberg, O.: Abstraction and reduction in model checking. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliabilty. Nato Science Series II. Math., Physics and Chemistry, vol. 62, pp. 213\u2013260. Kluwer Academic Publishers, Boston (2002)","DOI":"10.1007\/978-94-010-0413-8_9"},{"issue":"6","key":"5_CR17","doi-asserted-by":"crossref","first-page":"938","DOI":"10.1109\/TAC.2006.876952","volume":"51","author":"L Habets","year":"2006","unstructured":"Habets, L., Collins, P., van Schuppen, J.: Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Trans. Autom. Control 51(6), 938\u2013948 (2006)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS 1996, pp. 278\u2013292. IEEE (1996)","DOI":"10.1109\/LICS.1996.561342"},{"issue":"1\u20132","key":"5_CR19","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. STTT 1(1\u20132), 110\u2013122 (1997)","journal-title":"STTT"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Hereid, A., Kolathaya, S., Jones, M.S., Van Why, J., Hurst, J.W., Ames, A.D.: Dynamic Multi-domain Bipedal Walking with Atrias Through Slip Based Human-Inspired Control. HSCC 2014. pp. 263\u2013272, ACM (2014)","DOI":"10.1145\/2562059.2562143"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R.: Proving safety of traffic manoeuvres on country roads. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 196\u2013212. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39698-4_12"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Hilscher, M., Linker, S., Olderog, E.-R., Ravn, A.P.: An abstract model for proving safety of multi-lane traffic manoeuvres. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 404\u2013419. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24559-6_28"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, London (1998)","DOI":"10.1007\/BFb0002714"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. HSCC 2005, 25\u201353 (2005)","DOI":"10.1007\/978-3-540-31954-2_2"},{"key":"5_CR25","unstructured":"Linker, S.: Proofs for traffic safety: combining diagrams and logic. Ph.D thesis, Dept. of. Comp. Sci, Univ. of Oldenburg (2015)"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Linker, S., Hilscher, M.: Proof theory of a multi-lane spatial logic. Logical Methods Comput. Sci. 11(3), 2015. See: https:\/\/arxiv.org\/abs\/1504.06986","DOI":"10.2168\/LMCS-11(3:4)2015"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive cruise control: hybrid, distributed, and now formally verified. In: Butler, M.J., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 42\u201356. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-21437-0_6"},{"issue":"4","key":"5_CR28","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1109\/9.664155","volume":"43","author":"J Lygeros","year":"1998","unstructured":"Lygeros, J., Godbole, D.N., Sastry, S.S.: Verified hybrid controllers for automated vehicles. IEEE Trans. Autom. Control 43(4), 522\u2013539 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I\/O automata revisited. HSCC 2001, 403\u2013417 (2001)","DOI":"10.1007\/3-540-45351-2_33"},{"key":"5_CR30","unstructured":"MathWorks. Stateflow (1995)"},{"key":"5_CR31","unstructured":"Moor, T., Raisch, J., Davoren, J.: Admissiblity criteria for a hierarchical design of hybrid systems. In: Proceedings IFAD Conference on Analysis and Design of Hybrid Systems, pp. 389\u2013394. St. Malo, France (2003)"},{"key":"5_CR32","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1023\/A:1013339920783","volume":"12","author":"T Moor","year":"2002","unstructured":"Moor, T., Raisch, J., O\u2019Young, S.: Discrete supervisory control of hybrid systems based on l-complete approximations. Discret. Event Dyn. Syst. 12, 83\u2013107 (2002)","journal-title":"Discret. Event Dyn. Syst."},{"issue":"2","key":"5_CR33","doi-asserted-by":"crossref","first-page":"10","DOI":"10.1109\/MC.1985.1662795","volume":"18","author":"B Moszkowski","year":"1985","unstructured":"Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. Computer 18(2), 10\u201319 (1985)","journal-title":"Computer"},{"key":"5_CR34","unstructured":"Nadjm-Tehrani, S., Str\u00f6mberg, J.: From physical modelling to compositional models of hybrid systems. In: Langmaack, H., de\u00a0Roever, W.P., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems \u2013 ProCoS, vol. 863 of LNCS, pp. 583\u2013604. Springer (1994)"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Olderog, E.-R., Ravn, A., Wisniewski, R.: Linking spatial and dynamic models for traffic maneuvers. In: 54th IEEE Conference on Decision and Control (CDC), 8 pp. IEEE (2015)","DOI":"10.1109\/CDC.2015.7403292"},{"key":"5_CR36","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Spinger, Heidelberg (2010)"},{"key":"5_CR37","series-title":"Mechanical engineering series","volume-title":"Vehicle Dynamics and Control","author":"R Rajamani","year":"2006","unstructured":"Rajamani, R.: Vehicle Dynamics and Control. Mechanical engineering series. Springer Science, New York (2006)"},{"key":"5_CR38","doi-asserted-by":"crossref","unstructured":"Rajhans, A., Krogh, B.H.: Compositional heterogeneous abstraction. In: HSCC 2013, pp. 253\u2013262. ACM (2013)","DOI":"10.1145\/2461328.2461368"},{"key":"5_CR39","unstructured":"Randell, D.A., Cui, Z., Cohn, A.G.: A spatial logic based on regions and connection. In: Proceedings 3rd International Conference Knowledge Representation and Reasoning (1992)"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"Sch\u00e4fer, A.: A calculus for shapes in time and space. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 463\u2013478. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-540-31862-0_33"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Shao, Z., Liu, J.: Spatio-temporal hybrid automata for cyber-physical systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 337\u2013354. Springer, Heidelberg (2005)","DOI":"10.1007\/978-3-642-39718-9_20"},{"key":"5_CR42","doi-asserted-by":"crossref","unstructured":"Sreenath, K., Hill Jr., C.R., Kumar, V.: A partially observable hybrid system model for bipedal locomotion for adapting to terrain variations. In: HSCC 2013, pp. 137\u2013142. ACM (2013)","DOI":"10.1145\/2461328.2461352"},{"key":"5_CR43","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-1-4020-5587-4_5","volume-title":"Handbook of Spatial Logics","author":"J Benthem van","year":"2007","unstructured":"van Benthem, J., Bezhanishvili, G.: Modal logics of space. In: Aiello, M., Pratt-Hartmann, I., Benthem, J. (eds.) Handbook of Spatial Logics, pp. 217\u2013298. Springer, Netherlands (2007)"},{"issue":"2","key":"5_CR44","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1109\/9.250509","volume":"38","author":"P Varaija","year":"1993","unstructured":"Varaija, P.: Smart cars on smart roads: problems of control. IEEE Trans. Autom. Control AC 38(2), 195\u2013207 (1993)","journal-title":"IEEE Trans. Autom. Control AC"},{"key":"5_CR45","doi-asserted-by":"crossref","unstructured":"Werling, M., Gindele, T., Jagszent, D., Gr\u00f6ll, L.: A robust algorithm for handling traffic in urban scenarios. In: Proceedings of IEEE Intelligent Vehicles Symposium, pp. 168\u2013173. Eindhoven, NL (2008)","DOI":"10.1109\/IVS.2008.4621260"},{"key":"5_CR46","volume-title":"Using Z \u2013 Specification, Refinement, and Proof","author":"J Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z \u2013 Specification, Refinement, and Proof. Prentice Hall, New Jersey (1996)"},{"key":"5_CR47","unstructured":"Zabat, M., Stabile, N., Farascaroli, S., Browand, F.: The aerodynamic performance of platoons: a final report. UC Berkeley (1995). http:\/\/escholarship.org\/uc\/item\/8ph187fw"},{"key":"5_CR48","doi-asserted-by":"crossref","unstructured":"Zabczyk, J.: Mathematical Control Theory \u2013 An Introduction. Birkh\u00e4user (2008)","DOI":"10.1007\/978-0-8176-4733-9"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Zhan, N., Wang, S., Zhao, H.: Formal modelling, analysis and verification of hybrid systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050, pp. 207\u2013281. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39721-9_5"},{"issue":"5","key":"5_CR50","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C., Ravn, A.: A calculus of durations. IPL 40(5), 269\u2013276 (1991)","journal-title":"IPL"},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"Ziegler, J., Bender, P., Dang, T., Stiller, C.: Trajectory planning for bertha \u2013 A local, continuous method. In: 2014 IEEE Intelligent Vehicles Symposium Proceedings, Dearborn, MI, USA, June 8-11, 2014, pp. 450\u2013457 (2014)","DOI":"10.1109\/IVS.2014.6856581"}],"container-title":["NASA Monographs in Systems and Software Engineering","Provably Correct Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48628-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T22:19:15Z","timestamp":1750025955000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48628-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319486277","9783319486284"],"references-count":51,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48628-4_5","relation":{},"ISSN":["1860-0131","2197-6597"],"issn-type":[{"value":"1860-0131","type":"print"},{"value":"2197-6597","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}