{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T22:49:58Z","timestamp":1768776598113,"version":"3.49.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377051","type":"print"},{"value":"9783031377068","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>There is a pressing need for learning controllers to endow systems with properties of safety and goal-reaching, which are crucial for many safety-critical systems. Reinforcement learning (RL) has been deployed successfully to synthesize controllers from user-defined reward functions encoding desired system requirements. However, it remains a significant challenge in synthesizing provably correct controllers with safety and goal-reaching requirements. To address this issue, we try to design a special hybrid polynomial-DNN controller which is easy to verify without losing its expressiveness and flexibility. This paper proposes a novel method to synthesize such a hybrid controller based on RL, low-degree polynomial fitting and knowledge distillation. It also gives a computational approach, by building and solving a constrained optimization problem coming from verification conditions to produce barrier certificates and Lyapunov-like functions, which can guarantee every trajectory from the initial set of the system with the resulted controller satisfies the given safety and goal-reaching requirements. We evaluate the proposed hybrid controller synthesis method on a set of benchmark examples, including several high-dimensional systems. The results validate the effectiveness and applicability of our approach.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_16","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"304-325","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Hybrid Controller Synthesis for\u00a0Nonlinear Systems Subject to\u00a0Reach-Avoid Constraints"],"prefix":"10.1007","author":[{"given":"Zhengfeng","family":"Yang","sequence":"first","affiliation":[]},{"given":"Li","family":"Zhang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2575-7045","authenticated-orcid":false,"given":"Xia","family":"Zeng","sequence":"additional","affiliation":[]},{"given":"Xiaochao","family":"Tang","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Peng","sequence":"additional","affiliation":[]},{"given":"Zhenbing","family":"Zeng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","unstructured":"Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: theory and applications. In: Proceedings of the 18th European Control Conference (ECC), pp. 3420\u20133431 (2019). https:\/\/doi.org\/10.23919\/ECC.2019.8796030","DOI":"10.23919\/ECC.2019.8796030"},{"key":"16_CR2","unstructured":"Chan, N., Mitra, S.: Verifying safety of an autonomous spacecraft rendezvous mission. arXiv preprint arXiv:1703.06930 (2017)"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Chang, Y.C., Roohi, N., Gao, S.: Neural lyapunov control. In: Advances in Neural Information Processing Systems (NeurIPS), pp. 3245\u20133254 (2019). https:\/\/doi.org\/10.48550\/arXiv.2005.00611","DOI":"10.48550\/arXiv.2005.00611"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Chow, Y., Nachum, O., Duenez-Guzman, E., Ghavamzadeh, M.: A Lyapunov-based approach to safe reinforcement learning. In: Advances in Neural Information Processing Systems (NeurIPS), pp. 8103\u20138112 (2018). https:\/\/doi.org\/10.48550\/arXiv.1805.07708","DOI":"10.48550\/arXiv.1805.07708"},{"key":"16_CR5","doi-asserted-by":"publisher","unstructured":"Delaitre, V., Sivic, J., Laptev, I.: Learning person-object interactions for action recognition in still images. In: Advances in Neural Information Processing Systems (NeurIPS), vol. 24, pp. 234\u2013242 (2011). https:\/\/doi.org\/10.48550\/arXiv.1604.04808","DOI":"10.48550\/arXiv.1604.04808"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Deshmukh, J.V., Kapinski, J.P., Yamaguchi, T., Prokhorov, D.: Learning deep neural network controllers for dynamical systems with safety guarantees. In: 2019 IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 1\u20137. IEEE (2019). https:\/\/doi.org\/10.1109\/ICCAD45719.2019.8942130","DOI":"10.1109\/ICCAD45719.2019.8942130"},{"key":"16_CR7","doi-asserted-by":"publisher","unstructured":"Ding, J., Tomlin, C.J.: Robust reach-avoid controller synthesis for switched nonlinear systems. In: 49th IEEE Conference on Decision and Control (CDC), pp. 6481\u20136486. IEEE (2010). https:\/\/doi.org\/10.1109\/CDC.2010.5717115","DOI":"10.1109\/CDC.2010.5717115"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 157\u2013168 (2019). https:\/\/doi.org\/10.1145\/3302504.3311807","DOI":"10.1145\/3302504.3311807"},{"key":"16_CR9","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.automatica.2016.03.016","volume":"70","author":"PM Esfahani","year":"2016","unstructured":"Esfahani, P.M., Chatterjee, D., Lygeros, J.: The stochastic reach-avoid problem and set characterization for diffusions. Automatica 70, 43\u201356 (2016). https:\/\/doi.org\/10.1016\/j.automatica.2016.03.016","journal-title":"Automatica"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Fan, C., Miller, K., Mitra, S.: Fast and guaranteed safe controller synthesis for nonlinear vehicle models. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 629\u2013652. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_31","DOI":"10.1007\/978-3-030-53288-8_31"},{"key":"16_CR11","doi-asserted-by":"publisher","unstructured":"Fan, J., Huang, C., Li, W., Chen, X., Zhu, Q.: Towards verification-aware knowledge distillation for neural-network controlled systems: invited paper. In: IEEE\/ACM International Conference on Computer-Aided Design (ICCAD), pp. 1\u20138 (2019). https:\/\/doi.org\/10.1109\/ICCAD45719.2019.8942059","DOI":"10.1109\/ICCAD45719.2019.8942059"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Fisac, J.F., Chen, M., Tomlin, C.J., Sastry, S.S.: Reach-avoid problems with time-varying dynamics, targets and constraints. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 11\u201320 (2015). https:\/\/doi.org\/10.1145\/2728606.2728612","DOI":"10.1145\/2728606.2728612"},{"issue":"5s","key":"16_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358228","volume":"18","author":"C Huang","year":"2019","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: reachability analysis of neural-network controlled systems. ACM Trans. Embed. Comput. Syst. 18(5s), 1\u201322 (2019). https:\/\/doi.org\/10.1145\/3358228","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Huang, Z., Wang, Y., Mitra, S., Dullerud, G.E., Chaudhuri, S.: Controller synthesis with inductive proofs for piecewise linear systems: an SMT-based algorithm. In: 54th IEEE Conference on Decision and Control (CDC), pp. 7434\u20137439. IEEE (2015). https:\/\/doi.org\/10.1109\/CDC.2015.7403394","DOI":"10.1109\/CDC.2015.7403394"},{"key":"16_CR15","unstructured":"Huh, S., Yang, I.: Safe reinforcement learning for probabilistic reachability and safety specifications: a Lyapunov-based approach. arXiv preprint arXiv:2002.10126v1 (2020)"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pp. 169\u2013178 (2019). https:\/\/doi.org\/10.1145\/3302504.3311806","DOI":"10.1145\/3302504.3311806"},{"key":"16_CR17","unstructured":"Jin, W., Wang, Z., Yang, Z., Mou, S.: Neural certificates for safe control policies. arXiv preprint arXiv:2006.08465v1 (2020)"},{"key":"16_CR18","unstructured":"Ko\u010dvara, M., Stingl, M.: PENBMI user\u2019s guide (version 2.0) (2005). http:\/\/www.penopt.com"},{"issue":"12","key":"16_CR19","doi-asserted-by":"publisher","first-page":"3521","DOI":"10.1091\/mbc.9.12.3521","volume":"9","author":"MT Laub","year":"1998","unstructured":"Laub, M.T., Loomis, W.F.: A molecular network that produces spontaneous oscillations in excitable cells of dictyostelium. Molecul. Biol. Cell 9(12), 3521\u20133532 (1998). https:\/\/doi.org\/10.1091\/mbc.9.12.3521","journal-title":"Molecul. Biol. Cell"},{"key":"16_CR20","unstructured":"Lillicrap, T.P., et al.: Continuous control with deep reinforcement learning. arXiv preprint arXiv:1509.02971v6 (2015)"},{"issue":"3","key":"16_CR21","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1115\/1.2901415","volume":"55","author":"AM Lyapunov","year":"1992","unstructured":"Lyapunov, A.M.: The general problem of the stability of motion. Int. J. Control 55(3), 531\u2013534 (1992). https:\/\/doi.org\/10.1115\/1.2901415","journal-title":"Int. J. Control"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Mnih, V., et al.: Human-level control through deep reinforcement learning. Nature 518(7540), 529\u2013533 (2015). https:\/\/doi.org\/10.1115\/1.4062310","DOI":"10.1115\/1.4062310"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Oh, J., Chockalingam, V., Lee, H., et al.: Control of memory, active perception, and action in minecraft. In: International Conference on Machine Learning (ICML), pp. 2790\u20132799. PMLR (2016). https:\/\/doi.org\/10.48550\/arXiv.1605.09128","DOI":"10.48550\/arXiv.1605.09128"},{"issue":"8","key":"16_CR24","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1109\/TAC.2007.902736","volume":"52","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Automat. Control 52(8), 1415\u20131428 (2007). https:\/\/doi.org\/10.1109\/TAC.2007.902736","journal-title":"IEEE Trans. Automat. Control"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Richards, S.M., Berkenkamp, F., Krause, A.: The Lyapunov neural network: adaptive stability certification for safe learning of dynamical systems. In: Conference on Robot Learning (CORL), pp. 466\u2013476. PMLR (2018). https:\/\/doi.org\/10.48550\/arXiv.1808.00924","DOI":"10.48550\/arXiv.1808.00924"},{"key":"16_CR26","doi-asserted-by":"publisher","unstructured":"Saveriano, M., Lee, D.: Learning barrier functions for constrained motion planning with dynamical systems. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 112\u2013119. IEEE (2019). https:\/\/doi.org\/10.1109\/IROS40897.2019.8967981","DOI":"10.1109\/IROS40897.2019.8967981"},{"key":"16_CR27","doi-asserted-by":"publisher","unstructured":"Srinivasan, M., Dabholkar, A., Coogan, S., Vela, P.A.: Synthesis of control barrier functions using a supervised machine learning approach. In: IEEE\/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 7139\u20137145. IEEE (2020). https:\/\/doi.org\/10.1109\/IROS45743.2020.9341190","DOI":"10.1109\/IROS45743.2020.9341190"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Taylor, A., Singletary, A., Yue, Y., Ames, A.: Learning for safety-critical control with control barrier functions. In: Learning for Dynamics and Control (L4DC), pp. 708\u2013717. PMLR (2020). https:\/\/doi.org\/10.13140\/RG.2.2.21587.60962","DOI":"10.13140\/RG.2.2.21587.60962"},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Wang, L., Theodorou, E.A., Egerstedt, M.: Safe learning of quadrotor dynamics using barrier certificates. In: IEEE International Conference on Robotics and Automation (ICRA), pp. 2460\u20132465. IEEE (2018). https:\/\/doi.org\/10.1109\/ICRA.2018.8460471","DOI":"10.1109\/ICRA.2018.8460471"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Xiang, W., Tran, H.D., Rosenfeld, J.A., Johnson, T.T.: Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. In: 2018 Annual American Control Conference (ACC), pp. 1574\u20131579. IEEE (2018). https:\/\/doi.org\/10.23919\/ACC.2018.8431048","DOI":"10.23919\/ACC.2018.8431048"},{"issue":"3","key":"16_CR31","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1007\/s00165-021-00544-5","volume":"33","author":"H Zhao","year":"2021","unstructured":"Zhao, H., Zeng, X., Chen, T., Liu, Z., Woodcock, J.: Learning safe neural network controllers with barrier certificates. Formal Aspect. Comput. 33(3), 437\u2013455 (2021). https:\/\/doi.org\/10.1007\/s00165-021-00544-5","journal-title":"Formal Aspect. Comput."},{"key":"16_CR32","doi-asserted-by":"publisher","unstructured":"Zhu, H., Xiong, Z., Magill, S., Jagannathan, S.: An inductive synthesis framework for verifiable reinforcement learning. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 686\u2013701 (2019). https:\/\/doi.org\/10.1145\/3314221.3314638","DOI":"10.1145\/3314221.3314638"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:06:09Z","timestamp":1704452769000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","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":"67","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":"0","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":"26% - 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":"11","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)"}}]}}