{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T14:52:32Z","timestamp":1768315952409,"version":"3.49.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319465197","type":"print"},{"value":"9783319465203","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-46520-3_26","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T06:40:27Z","timestamp":1474440027000},"page":"412-427","source":"Crossref","is-referenced-by-count":35,"title":["STL Model Checking of Continuous and Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Hendrik","family":"Roehm","sequence":"first","affiliation":[]},{"given":"Jens","family":"Oehlerking","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Heinz","sequence":"additional","affiliation":[]},{"given":"Matthias","family":"Althoff","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Ahmadyan, S.N., Kumar, J.A., Vasudevan, S.: Runtime verification of nonlinear analog circuits using incremental time-augmented RRT algorithm. In: Proceedings of Design, Test & Automation in Europe (2013)","DOI":"10.7873\/DATE.2013.019"},{"key":"26_CR2","unstructured":"Althoff, M.: An introduction to CORA . In: Proceedings of the Workshop on Applied Verification for Continuous and Hybrid Systems, pp. 120\u2013151 (2015)"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Althoff, M., Dolan, J.M.: Reachability computation of low-order models for the safety verification of high-order road vehicle models. In: American Control Conference, pp. 3559\u20133566. IEEE (2012)","DOI":"10.1109\/ACC.2012.6314777"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: Proceedings of 5th Symposium on Logic in Computer Science, pp. 414\u2013425 (1990)","DOI":"10.1109\/LICS.1990.113766"},{"issue":"1","key":"26_CR5","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996)","journal-title":"J. ACM"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Asarin, E., et al.: Recent progress in continuous and hybrid reachability analysis. In: Conference on Computer Aided Control Systems Design, pp. 1582\u20131587 (2006)","DOI":"10.1109\/CACSD-CCA-ISIC.2006.4776877"},{"key":"26_CR7","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":"26_CR8","doi-asserted-by":"crossref","unstructured":"Bresolin, D.: HyLTL: a temporal logic for model checking hybrid systems. In: Proceedings Third International Workshop on Hybrid Autonomous Systems, pp. 73\u201384. HAS (2013)","DOI":"10.4204\/EPTCS.124.8"},{"key":"26_CR9","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-662-46681-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68\u201382. Springer, Heidelberg (2015)"},{"issue":"42","key":"26_CR11","doi-asserted-by":"crossref","first-page":"4262","DOI":"10.1016\/j.tcs.2009.06.021","volume":"410","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262\u20134291 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Computer Aided Verification, pp. 379\u2013395 (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"issue":"1","key":"26_CR13","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/j.arcontrol.2009.03.002","volume":"33","author":"H Gu\u00e9guen","year":"2009","unstructured":"Gu\u00e9guen, H., Lefebvre, M., Zaytoon, J., Nasri, O.: Safety verification and reachability analysis for hybrid systems. Ann. Rev. Control 33(1), 25\u201336 (2009)","journal-title":"Ann. Rev. Control"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Lee, E.A.: CPS foundations. In: Design Automation Conference, pp. 737\u2013742 (2010)","DOI":"10.1145\/1837274.1837462"},{"key":"26_CR15","unstructured":"Lee, I., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: Runtime assurance based on formal specifications. In: Proceedings of the IntemationaI Conference on Parallel and Distributed Processing Techniques and Applications (1999)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/978-3-540-78127-1_26","volume-title":"Pillars of Computer Science","author":"O Maler","year":"2008","unstructured":"Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475\u2013505. Springer, Heidelberg (2008)"},{"key":"26_CR17","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring properties of analog and mixed-signal circuits. J. Softw. Tools Technol. Transfer 15, 247\u2013268 (2013)","journal-title":"J. Softw. Tools Technol. Transfer"},{"issue":"4","key":"26_CR18","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/MSP.2013.77","volume":"11","author":"S Mitra","year":"2013","unstructured":"Mitra, S., Wongpiromsarn, T., Murray, R.M.: Verifying cyber-physical interactions in safety-critical systems. IEEE Secur. Priv. 11(4), 28\u201337 (2013)","journal-title":"IEEE Secur. Priv."},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1007\/978-3-540-31954-2_34","volume-title":"Hybrid Systems: Computation and Control","author":"A Pinto","year":"2005","unstructured":"Pinto, A., Sangiovanni-Vincentelli, A.L., Carloni, L.P., Passerone, R.: Interchange formats for hybrid systems: review and proposal. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 526\u2013541. Springer, Heidelberg (2005)"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/978-3-540-71493-4_37","volume-title":"Hybrid Systems: Computation and Control","author":"A Platzer","year":"2007","unstructured":"Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 473\u2013486. Springer, Heidelberg (2007)"},{"issue":"8","key":"26_CR21","doi-asserted-by":"crossref","first-page":"1363","DOI":"10.1109\/JPROC.2010.2050377","volume":"98","author":"R Poovendran","year":"2010","unstructured":"Poovendran, R.: Cyberphysical systems: close encounters between two parallel worlds. Proc. IEEE 98(8), 1363\u20131366 (2010)","journal-title":"Proc. IEEE"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Rajkumar, R., Lee, I., Sha, L., Stankovic, J.: Cyber-physical systems: the next computing revolution. In: Design Automation Conference, pp. 731\u2013736 (2010)","DOI":"10.1145\/1837274.1837461"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"Sanwal, M.U., Hasan, O.: Formal verification of cyber-physical systems: coping with continuous elements. In: Proceedings of the 16th International Conference on Computational Science and its Applications, pp. 358\u2013371 (2013)","DOI":"10.1007\/978-3-642-39637-3_29"},{"key":"26_CR24","unstructured":"Sauter, G., Dierks, H., Fr\u00e4nzle, M., Hansen, M.R.: Lightweight hybrid model checking facilitating online prediction of temporal properties. In: Proceedings of the 21st Nordic Workshop on Programming Theory, NWPT09, pp. 20\u201322 (2009)"},{"key":"26_CR25","volume-title":"Introduction to the Theory of Differential Inclusions","author":"GV Smirnov","year":"2002","unstructured":"Smirnov, G.V.: Introduction to the Theory of Differential Inclusions. American Mathematical Society, Providence (2002)"},{"key":"26_CR26","unstructured":"Tan, L., Kim, J., Sokolsky, O., Lee, I.: Model-based testing and monitoring for hybrid embedded systems. In: Model-Based Testing and Monitoring for Hybrid Embedded Systems, pp. 487\u2013492 (2004)"},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Wang, Z., Zaki, M.H., Tahar, S.: Statistical runtime verification of analog and mixed signal designs. In: Conference on Signals, Circuits and Systems (2009)","DOI":"10.1109\/ICSCS.2009.5412620"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46520-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T19:19:52Z","timestamp":1498331992000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46520-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319465197","9783319465203"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46520-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}