{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:22:01Z","timestamp":1778498521615,"version":"3.51.4"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031198489","type":"print"},{"value":"9783031198496","type":"electronic"}],"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.springer.com\/tdm"},{"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.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-19849-6_18","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T15:03:32Z","timestamp":1666191812000},"page":"299-319","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Towards Safe and\u00a0Resilient Hybrid Systems in\u00a0the\u00a0Presence of\u00a0Learning and\u00a0Uncertainty"],"prefix":"10.1007","author":[{"given":"Julius","family":"Adelt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paula","family":"Herber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathis","family":"Niehage","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anne","family":"Remke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"issue":"6","key":"18_CR1","doi-asserted-by":"publisher","first-page":"624","DOI":"10.3166\/ejc.16.624-641","volume":"16","author":"A Abate","year":"2010","unstructured":"Abate, A., Katoen, J.P., Lygeros, J., Prandini, M.: Approximate model checking of stochastic hybrid systems. Eur. J. Control. 16(6), 624\u2013641 (2010)","journal-title":"Eur. J. Control."},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-030-90870-6_19","volume-title":"Formal Methods","author":"J Adelt","year":"2021","unstructured":"Adelt, J., Liebrenz, T., Herber, P.: Formal verification of intelligent hybrid systems that are modeled with simulink and the reinforcement learning toolbox. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 349\u2013366. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_19"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Alshiekh, M., Bloem, R., Ehlers, R., K\u00f6nighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)","DOI":"10.1609\/aaai.v32i1.11797"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: ACM International Conference on Embedded Software (EMSOFT), pp. 273\u2013278 (2011)","DOI":"10.1145\/2038642.2038685"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Araiza-Illan, D., Eder, K., Richards, A.: Formal verification of control systems\u2019 properties with theorem proving. In: UKACC International Conference on Control (CONTROL), pp. 244\u2013249. IEEE (2014)","DOI":"10.1109\/CONTROL.2014.6915147"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bertrand, N., et al.: Stochastic timed automata. Log. Methods Comput. Sci. 10(4) (2014)","DOI":"10.2168\/LMCS-10(4:6)2014"},{"issue":"5","key":"18_CR7","doi-asserted-by":"publisher","first-page":"2386","DOI":"10.1109\/TAC.2020.3006967","volume":"66","author":"M Cai","year":"2021","unstructured":"Cai, M., Peng, H., Li, Z., Kan, Z.: Learning-based probabilistic LTL motion planning with environment and motion uncertainties. IEEE Trans. Autom. Control 66(5), 2386\u20132392 (2021)","journal-title":"IEEE Trans. Autom. Control"},{"key":"18_CR8","series-title":"NASA Monographs in Systems and Software Engineering","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-319-48628-4_3","volume-title":"Provably Correct Systems","author":"M Chen","year":"2017","unstructured":"Chen, M., et al.: MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE, pp. 39\u201358. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-48628-4_3"},{"issue":"1","key":"18_CR9","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1109\/TAC.2002.806655","volume":"48","author":"A Chutinan","year":"2003","unstructured":"Chutinan, A., Krogh, B.H.: Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48(1), 64\u201375 (2003)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"4","key":"18_CR10","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10009-014-0329-y","volume":"17","author":"C Ellen","year":"2015","unstructured":"Ellen, C., Gerwinn, S., Fr\u00e4nzle, M.: Statistical model checking for stochastic hybrid systems involving nondeterminism over continuous domains. Int. J. Softw. Tools Technol. Transf. 17(4), 485\u2013504 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"18_CR11","unstructured":"Fulton, N., Hunt, N., Hoang, N., Das, S.: Formal Verification of End-to-End Learning in Cyber-Physical Systems: Progress and Challenges. arXiv:2006.09181 (2020)"},{"key":"18_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\u00a0X: 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). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Fulton, N., Platzer, A.: Safe reinforcement learning via formal methods: toward safe control through proof and learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 32 (2018)","DOI":"10.1609\/aaai.v32i1.12107"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1016\/j.peva.2016.09.002","volume":"105","author":"M Gribaudo","year":"2016","unstructured":"Gribaudo, M., Remke, A.: Hybrid Petri nets with general one-shot transitions. Perform. Eval. 105, 22\u201350 (2016)","journal-title":"Perform. Eval."},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Gudemann, M., Ortmeier, F.: A framework for qualitative and quantitative formal model-based safety analysis. In: IEEE International Symposium on High Assurance Systems Engineering, pp. 132\u2013141. IEEE (2010)","DOI":"10.1109\/HASE.2010.24"},{"issue":"2","key":"18_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10703-012-0167-z","volume":"43","author":"EM Hahn","year":"2013","unstructured":"Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.P.: A compositional modelling and analysis framework for stochastic hybrid systems. Form. Methods Syst. Des. 43(2), 191\u2013232 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-030-59152-6_6","volume-title":"Automated Technology for Verification and Analysis","author":"EM Hahn","year":"2020","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Faithful and effective reward schemes for model-free reinforcement learning of omega-regular objectives. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 108\u2013124. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_6"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Hasanbeig, M., Kantaros, Y., Abate, A., Kroening, D., Pappas, G.J., Lee, I.: Reinforcement learning for temporal logic control synthesis with probabilistic satisfaction guarantees. In: IEEE Conference on Decision and Control (CDC), Nice, France, pp. 5338\u20135343. IEEE (2019)","DOI":"10.1109\/CDC40024.2019.9028919"},{"key":"18_CR19","unstructured":"Hasanbeig, M., Abate, A., Kroening, D.: Cautious reinforcement learning with logical constraints. In: International Foundation for Autonomous Agents and Multiagent Systems, AAMAS 2020, pp. 483\u2013491 (2020)"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Herber, P., Reicherdt, R., Bittner, P.: Bit-precise formal verification of discrete-time MATLAB\/Simulink models using SMT solving. In: International Conference on Embedded Software (EMSOFT), pp. 1\u201310. IEEE (2013)","DOI":"10.1109\/EMSOFT.2013.6658586"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-99154-2_13","volume-title":"Quantitative Evaluation of Systems","author":"S Junges","year":"2018","unstructured":"Junges, S., Jansen, N., Katoen, J.-P., Topcu, U., Zhang, R., Hayhoe, M.: Model checking for safe navigation among humans. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 207\u2013222. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_13"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Kn\u00fcppel, A., Th\u00fcm, T., Schaefer, I.: GUIDO: automated guidance for the configuration of deductive program verifiers. In: IEEE\/ACM International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 124\u2013129. IEEE (2021)","DOI":"10.1109\/FormaliSE52586.2021.00018"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-030-61362-4_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"B K\u00f6nighofer","year":"2020","unstructured":"K\u00f6nighofer, B., Lorber, F., Jansen, N., Bloem, R.: Shield synthesis for reinforcement learning. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 290\u2013306. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_16"},{"key":"18_CR24","unstructured":"Laprie, J.C.: From dependability to resilience. In: IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. G8\u2013G9 (2008)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-030-02450-5_6","volume-title":"Formal Methods and Software Engineering","author":"T Liebrenz","year":"2018","unstructured":"Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89\u2013105. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02450-5_6"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-030-40914-2_7","volume-title":"Formal Aspects of Component Software","author":"T Liebrenz","year":"2020","unstructured":"Liebrenz, T., Herber, P., Glesner, S.: A service-oriented approach for decomposing and verifying hybrid system models. In: Arbab, F., Jongmans, S.-S. (eds.) FACS 2019. LNCS, vol. 12018, pp. 127\u2013146. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-40914-2_7"},{"key":"18_CR27","doi-asserted-by":"publisher","first-page":"102694","DOI":"10.1016\/j.scico.2021.102694","volume":"211","author":"T Liebrenz","year":"2021","unstructured":"Liebrenz, T., Herber, P., Glesner, S.: Service-oriented decomposition and verification of hybrid system models using feature models and contracts. Sci. Comput. Program. 211, 102694 (2021)","journal-title":"Sci. Comput. Program."},{"issue":"6","key":"18_CR28","doi-asserted-by":"publisher","first-page":"583","DOI":"10.3166\/ejc.16.583-594","volume":"16","author":"J Lygeros","year":"2010","unstructured":"Lygeros, J., Prandini, M.: Stochastic hybrid systems: a powerful framework for complex, large scale applications. Eur. J. Control. 16(6), 583\u2013594 (2010)","journal-title":"Eur. J. Control."},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30206-3_12"},{"key":"18_CR30","doi-asserted-by":"crossref","unstructured":"Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: International Conference on Hybrid Systems: Computation and Control, pp. 93\u201398. ACM (2016)","DOI":"10.1145\/2883817.2883826"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Niehage, M., Hartmanns, A., Remke, A.: Learning optimal decisions for stochastic hybrid systems. In: ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 44\u201355. ACM (2021)","DOI":"10.1145\/3487212.3487339"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Pilch, C., Edenfeld, F., Remke, A.: HYPEG: statistical model checking for hybrid petri nets: tool paper. In: EAI International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS), pp. 186\u2013191. ACM Press (2017)","DOI":"10.1145\/3150928.3150956"},{"key":"18_CR33","doi-asserted-by":"crossref","unstructured":"Pilch, C., Niehage, M., Remke, A.: HPnGs go non-linear: statistical dependability evaluation of battery-powered systems. In: IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS), pp. 157\u2013169. IEEE (2018)","DOI":"10.1109\/MASCOTS.2018.00024"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Pilch, C., Remke, A.: Statistical model checking for hybrid petri nets with multiple general transitions. In: Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 475\u2013486. IEEE (2017)","DOI":"10.1109\/DSN.2017.41"},{"issue":"2","key":"18_CR35","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. Reason. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reason."},{"key":"18_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-10431-7_14","volume-title":"Software Engineering and Formal Methods","author":"R Reicherdt","year":"2014","unstructured":"Reicherdt, R., Glesner, S.: Formal verification of discrete-time MATLAB\/Simulink models using boogie. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 190\u2013204. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_14"},{"key":"18_CR37","doi-asserted-by":"crossref","unstructured":"Sadigh, D., Kim, E.S., Coogan, S., Sastry, S.S., Seshia, S.A.: A learning based approach to control synthesis of Markov decision processes for linear temporal logic specifications. In: IEEE Conference on Decision and Control, pp. 1091\u20131096. IEEE (2014)","DOI":"10.21236\/ADA623517"},{"key":"18_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-319-49052-6_10","volume-title":"Hardware and Software: Verification and Testing","author":"F Shmarov","year":"2016","unstructured":"Shmarov, F., Zuliani, P.: Probabilistic hybrid systems verification via SMT and Monte Carlo techniques. In: Bloem, R., Arbel, E. (eds.) HVC 2016. LNCS, vol. 10028, pp. 152\u2013168. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49052-6_10"},{"key":"18_CR39","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"2018","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction, 2nd edn. The MIT Press, Cambridge; London (2018)","edition":"2"},{"key":"18_CR40","unstructured":"The MathWorks: Simulink. https:\/\/de.mathworks.com\/products\/simulink.html"},{"key":"18_CR41","unstructured":"The MathWorks: Reinforcement Learning Toolbox. https:\/\/www.mathworks.com\/products\/reinforcement-learning.html"},{"key":"18_CR42","unstructured":"The MathWorks: Simulink Design Verifier. https:\/\/de.mathworks.com\/products\/simulink-design-verifier.html"},{"key":"18_CR43","unstructured":"The MathWorks: Simulink Example: Water Distribution System Scheduling Using Reinforcement Learning. https:\/\/de.mathworks.com\/help\/reinforcement-learning\/ug\/water-distribution-scheduling-system.html"},{"key":"18_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/978-3-319-24953-7_33","volume-title":"Automated Technology for Verification and Analysis","author":"L Zou","year":"2015","unstructured":"Zou, L., Zhan, N., Wang, S., Fr\u00e4nzle, M.: Formal verification of simulink\/stateflow diagrams. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015. LNCS, vol. 9364, pp. 464\u2013481. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24953-7_33"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19849-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:09:26Z","timestamp":1666224566000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19849-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031198489","9783031198496"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19849-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}