{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,24]],"date-time":"2026-01-24T15:53:24Z","timestamp":1769270004204,"version":"3.49.0"},"publisher-location":"Cham","reference-count":41,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030302801","type":"print"},{"value":"9783030302818","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30281-8_2","type":"book-chapter","created":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T19:03:54Z","timestamp":1567537434000},"page":"25-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["The Logical Path to Autonomous Cyber-Physical Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,4]]},"reference":[{"key":"2_CR1","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: McIlraith, Weinberger [22]"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 273\u2013278. ACM, New York (2011). \n                      https:\/\/doi.org\/10.1145\/2038642.2038685","DOI":"10.1145\/2038642.2038685"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Bohrer, B., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs - 6th ACM SIGPLAN Conference, CPP 2017, Paris, France, 16\u201317 January 2017, pp. 208\u2013221. ACM, New York (2017). \n                      https:\/\/doi.org\/10.1145\/3018610.3018616","DOI":"10.1145\/3018610.3018616"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Bohrer, B., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: VeriPhy: verified controller executables from verified cyber-physical system models. In: Grossman, D. (ed.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617\u2013630. ACM (2018). \n                      https:\/\/doi.org\/10.1145\/3192366.3192406","DOI":"10.1145\/3192366.3192406"},{"issue":"3","key":"2_CR5","doi-asserted-by":"publisher","first-page":"2910","DOI":"10.1109\/LRA.2019.2923099","volume":"4","author":"B Bohrer","year":"2019","unstructured":"Bohrer, B., Tan, Y.K., Mitsch, S., Sogokon, A., Platzer, A.: A formal safety net for waypoint following in ground robots. IEEE Robot. Autom. Lett. 4(3), 2910\u20132917 (2019). \n                      https:\/\/doi.org\/10.1109\/LRA.2019.2923099","journal-title":"IEEE Robot. Autom. Lett."},{"issue":"1","key":"2_CR6","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s00224-006-1338-3","volume":"41","author":"P Collins","year":"2007","unstructured":"Collins, P.: Optimal semicomputable approximations to reachable and invariant sets. Theory Comput. Syst. 41(1), 33\u201348 (2007). \n                      https:\/\/doi.org\/10.1007\/s00224-006-1338-3","journal-title":"Theory Comput. Syst."},{"key":"2_CR7","unstructured":"Descartes, R.: Meditationes de prima philosophia, in qua Dei existentia et animae immortalitas demonstratur (1641)"},{"key":"2_CR8","doi-asserted-by":"publisher","first-page":"1047","DOI":"10.1007\/978-3-319-10575-8_30","volume-title":"Handbook of Model Checking","author":"L Doyen","year":"2018","unstructured":"Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. Handbook of Model Checking, pp. 1047\u20131110. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-10575-8_30"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-319-57288-8_26","volume-title":"NASA Formal Methods","author":"T Dreossi","year":"2017","unstructured":"Dreossi, T., Donz\u00e9, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 357\u2013372. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-57288-8_26"},{"key":"2_CR10","unstructured":"Dvijotham, K., et al.: Training verified learners with learned verifiers. CoRR abs\/1805.10265 (2018)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Fulton, N., Platzer, A.: Safe AI for CPS. In: IEEE International Test Conference, ITC 2018, Phoenix, AZ, USA, October 29\u2013November 1 2018, pp. 1\u20137. IEEE (2018). \n                      https:\/\/doi.org\/10.1109\/TEST.2018.8624774","DOI":"10.1109\/TEST.2018.8624774"},{"key":"2_CR14","unstructured":"Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: McIlraith, Weinberger [22], pp. 6485\u20136492. \n                      https:\/\/www.aaai.org\/ocs\/index.php\/AAAI\/AAAI18\/paper\/view\/17376"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-030-17462-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Fulton","year":"2019","unstructured":"Fulton, N., Platzer, A.: Verifiably safe off-model reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11427, pp. 413\u2013430. Springer, Cham (2019). \n                      https:\/\/doi.org\/10.1007\/978-3-030-17462-0_28"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Gillula, J.H., Tomlin, C.J.: Guaranteed safe online learning via reachability: tracking a ground target using a quadrotor. In: IEEE International Conference on Robotics and Automation, ICRA 2012, St. Paul, Minnesota, USA, 14\u201318 May 2012, pp. 2723\u20132730. IEEE (2012). \n                      https:\/\/doi.org\/10.1109\/ICRA.2012.6225136","DOI":"10.1109\/ICRA.2012.6225136"},{"issue":"10","key":"2_CR17","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/MC.2007.364","volume":"40","author":"TA Henzinger","year":"2007","unstructured":"Henzinger, T.A., Sifakis, J.: The discipline of embedded systems design. Computer 40(10), 32\u201340 (2007). \n                      https:\/\/doi.org\/10.1109\/MC.2007.364","journal-title":"Computer"},{"issue":"6","key":"2_CR18","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1007\/s10009-016-0434-1","volume":"19","author":"J Jeannin","year":"2017","unstructured":"Jeannin, J., et al.: A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system. STTT 19(6), 717\u2013741 (2017). \n                      https:\/\/doi.org\/10.1007\/s10009-016-0434-1","journal-title":"STTT"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Larsen, K.G.: Verification and performance analysis for embedded systems. In: Chin, W., Qin, S. (eds.) TASE 2009, Third IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, 29\u201331 July 2009, pp. 3\u20134. IEEE Computer Society (2009). \n                      https:\/\/doi.org\/10.1109\/TASE.2009.66","DOI":"10.1109\/TASE.2009.66"},{"key":"2_CR20","unstructured":"2012 27th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE, Los Alamitos (2012)"},{"key":"2_CR21","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-030-29026-9_24","volume-title":"Lecture Notes in Computer Science","author":"Jo\u00e3o G. Martins","year":"2019","unstructured":"Martins, J., Platzer, A., Leite, J.: Dynamic doxastic differential dynamic logic for belief-aware cyber-physical systems. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX. LNCS, vol. 11714. Springer, Cham (2019). \n                      https:\/\/doi.org\/10.1007\/978-3-030-29026-9_24"},{"key":"2_CR22","unstructured":"McIlraith, S.A., Weinberger, K.Q. (eds.): Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, New Orleans, Louisiana, USA, 2\u20137 February 2018. AAAI Press (2018)"},{"issue":"12","key":"2_CR23","doi-asserted-by":"publisher","first-page":"1312","DOI":"10.1177\/0278364917733549","volume":"36","author":"S Mitsch","year":"2017","unstructured":"Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. Int. J. Robot. Res. 36(12), 1312\u20131340 (2017). \n                      https:\/\/doi.org\/10.1177\/0278364917733549","journal-title":"Int. J. Robot. Res."},{"issue":"1\u20132","key":"2_CR24","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10703-016-0241-z","volume":"49","author":"S Mitsch","year":"2016","unstructured":"Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyberphysical system models. Form. Methods Syst. Des. 49(1\u20132), 33\u201374 (2016). \n                      https:\/\/doi.org\/10.1007\/s10703-016-0241-z","journal-title":"Form. Methods Syst. Des."},{"key":"2_CR25","unstructured":"Mitsch, S., Platzer, A.: Verified runtime validation for partially observable hybrid systems. CoRR abs\/1811.06502 (2018). \n                      http:\/\/arxiv.org\/abs\/1811.06502"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-540-73001-9_61","volume-title":"Computation and Logic in the Real World","author":"A Nerode","year":"2007","unstructured":"Nerode, A.: Logic and control. In: Cooper, S.B., L\u00f6we, B., Sorbi, A. (eds.) CiE 2007. LNCS, vol. 4497, pp. 585\u2013597. Springer, Heidelberg (2007). \n                      https:\/\/doi.org\/10.1007\/978-3-540-73001-9_61"},{"issue":"1","key":"2_CR27","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1109\/TIV.2016.2578706","volume":"1","author":"B Paden","year":"2016","unstructured":"Paden, B., C\u00e1p, M., Yong, S.Z., Yershov, D.S., Frazzoli, E.: A survey of motion planning and control techniques for self-driving urban vehicles. IEEE Trans. Intell. Veh. 1(1), 33\u201355 (2016). \n                      https:\/\/doi.org\/10.1109\/TIV.2016.2578706","journal-title":"IEEE Trans. Intell. Veh."},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Pappas, G.J.: Wireless control networks: modeling, synthesis, robustness, security. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) HSCC, pp. 1\u20132. ACM, New York (2011). \n                      https:\/\/doi.org\/10.1145\/1967701.1967703","DOI":"10.1145\/1967701.1967703"},{"key":"2_CR29","unstructured":"Pei, K., Cao, Y., Yang, J., Jana, S.: Towards practical verification of machine learning: the case of computer vision systems. CoRR abs\/1712.01785 (2017)"},{"issue":"2","key":"2_CR30","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143\u2013189 (2008). \n                      https:\/\/doi.org\/10.1007\/s10817-008-9103-8","journal-title":"J. Autom. Reasoning"},{"key":"2_CR31","doi-asserted-by":"publisher","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, vol. 1. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-14509-4"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. In: LICS [20], pp. 541\u2013550. \n                      https:\/\/doi.org\/10.1109\/LICS.2012.64","DOI":"10.1109\/LICS.2012.64"},{"key":"2_CR33","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS [20], pp. 13\u201324. \n                      https:\/\/doi.org\/10.1109\/LICS.2012.13","DOI":"10.1109\/LICS.2012.13"},{"key":"2_CR34","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-40229-1_3","volume-title":"IJCAR","author":"A Platzer","year":"2016","unstructured":"Platzer, A.: Logic & proofs for cyber-physical systems. In: Olivetti, N., Tiwari, A. (eds.) IJCAR. LNCS, vol. 9706, pp. 15\u201321. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-40229-1_3"},{"issue":"2","key":"2_CR35","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: A complete uniform substitution calculus for dierential dynamic logic. J. Autom. Reasoning 59(2), 219\u2013265 (2017). \n                      https:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J. Autom. Reasoning"},{"key":"2_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0","volume-title":"Logical Foundations of Cyber-Physical Systems","author":"A Platzer","year":"2018","unstructured":"Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71493-4_37"},{"issue":"1","key":"2_CR38","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/s10009-015-0367-0","volume":"18","author":"JD Quesel","year":"2016","unstructured":"Quesel, J.D., Mitsch, S., Loos, S., Ar\u00e9chiga, N., Platzer, A.: How to model and prove hybrid systems with KeYmaera: a tutorial on safety. STTT 18(1), 67\u201391 (2016). \n                      https:\/\/doi.org\/10.1007\/s10009-015-0367-0","journal-title":"STTT"},{"key":"2_CR39","volume-title":"Reinforcement Learning","author":"RS Sutton","year":"1998","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning. The MIT Press, Cambridge (1998)"},{"key":"2_CR40","doi-asserted-by":"publisher","unstructured":"Tiwari, A.: Logic in software, dynamical and biological systems. In: LICS, pp. 9\u201310. IEEE Computer Society (2011). \n                      https:\/\/doi.org\/10.1109\/LICS.2011.20","DOI":"10.1109\/LICS.2011.20"},{"issue":"2","key":"2_CR41","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/s10703-013-0195-3","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. Form. Methods Syst. Des. 43(2), 338\u2013367 (2013). \n                      https:\/\/doi.org\/10.1007\/s10703-013-0195-3","journal-title":"Form. Methods Syst. Des."}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30281-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T19:13:55Z","timestamp":1567538035000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30281-8_2"}},"subtitle":["(Invited Paper)"],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030302801","9783030302818"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30281-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"4 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"QEST","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Quantitative Evaluation of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Glasgow","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"qest2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.qest.org\/qest2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}