{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T02:19:13Z","timestamp":1743128353542,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816841"},{"type":"electronic","value":"9783030816858"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we investigate the design of a safe hybrid controller for an aircraft that switches between a classical linear quadratic regulator (LQR) controller and a more intelligent artificial neural network (ANN) controller. Our objective is to switch safely between\n the controllers, such that the aircraft is always recoverable within a fixed amount of time while allowing the maximum time of operation for the ANN controller. There is a <jats:italic>priori<\/jats:italic> known safety zone for the LQR controller operation in which the aircraft never stalls, over accelerates, or exceeds maximum structural loading, and hence, by switching to the LQR controller just before exiting this zone, one can guarantee safety. However, this <jats:italic>priori<\/jats:italic> known safety zone is conservative, and therefore, limits the time of operation for the ANN controller. We apply reachability analysis to expand the known safety zone, such that the LQR controller will always be able to drive the aircraft back to the safe zone from the expanded zone (\u201crecoverable zone\") within a fixed duration. The \u201crecoverable zone\" extends the time of operation of the ANN controller. We perform simulations using the hybrid controller corresponding to the recoverable zone and observe that the design is indeed safe.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_27","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"566-579","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formally Verified Switching Logic for Recoverability of Aircraft Controller"],"prefix":"10.1007","author":[{"given":"Ratan","family":"Lal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aaron","family":"McKinnis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dustin","family":"Hauptman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shawn","family":"Keshmiri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pavithra","family":"Prabhakar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"Abdelhameed, M.M.: Adaptive neural network based controller for robots. Mechatronics 9, 147\u2013162 (1999)","DOI":"10.1016\/S0957-4158(98)00041-5"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Akametalu, A.K., Fisac, J.F., Gillula, J.H., Kaynama, S., Zeilinger, M.N., Tomlin, C.J.: Reachability-based safe learning with gaussian processes. In: Conference on Decision and Control (2014)","DOI":"10.1109\/CDC.2014.7039601"},{"key":"27_CR3","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1145\/1132357.1132363","volume":"5","author":"R Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivancic, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embedded Comput. Syst. (TECS) 5, 152\u2013199 (2006)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1016\/j.neunet.2003.07.001","volume":"17","author":"AA Argiriou","year":"2004","unstructured":"Argiriou, A.A., Bellas-Velidis, I., Kummert, M., Andr\u00e9, P.: A neural network controller for hydronic heating systems of solar buildings. Neural Netw. 17, 472\u2013440 (2004)","journal-title":"Neural Netw."},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. Computation and Control. In: International Workshop on Hybrid Systems (2000)","DOI":"10.1007\/3-540-46430-1_6"},{"key":"27_CR6","unstructured":"Azhar, M.A.H.B., Dimond, K.R.: Design of an FPGA based adaptive neural controller for intelligent robot navigation. In: Proceedings Euromicro Symposium on Digital System Design. Architectures, Methods and Tools (2002)"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Bak, S., Johnson, T.T., Caccamo, M., Sha, L.: Real-time reachability for verified simplex design. In: IEEE Real-Time Systems Symposium (2014)","DOI":"10.1109\/RTSS.2014.21"},{"key":"27_CR8","doi-asserted-by":"publisher","first-page":"143","DOI":"10.12720\/joig.1.3.143-146","volume":"1","author":"NS Bhangal","year":"2013","unstructured":"Bhangal, N.S.: Design and performance of LQR and LQR based fuzzy controller for double inverted pendulum system. J. Image Graph. 1, 143\u2013146 (2013)","journal-title":"J. Image Graph."},{"key":"27_CR9","unstructured":"Brown, J.A.: Stall avoidance system for aircraft, 1986. US Patent 4,590,475 (1986)"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., Sankaranarayanan, S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: International Conference on Hybrid Systems: Computation and Control, (2019)","DOI":"10.1145\/3302504.3311807"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: NASA Formal Methods Symposium (2018)","DOI":"10.1007\/978-3-319-77935-5_9"},{"key":"27_CR12","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. CoRR, abs\/1803.06567 (2018)"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D\u2019Souza, D., Kumar, K.N. (eds.) Automated Technology for Verification and Analysis (2017)","DOI":"10.1007\/978-3-319-68167-2_19"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Frehse, G., et al.: SpaceEX: scalable verification of hybrid systems. In: International Conference on Computer Aided Verification (2011)","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: IEEE Symposium on Security and Privacy (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. Computation and Control. In: International Workshop on Hybrid Systems (2005)","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Julian, K.D., Kochenderfer, M.J., Owen, M.P.: Deep Neural Network Compression for Aircraft Collision Avoidance Systems. arXiv e-prints (2018)","DOI":"10.2514\/1.G003724"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. CoRR (2017)","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"27_CR19","doi-asserted-by":"publisher","first-page":"882","DOI":"10.7763\/IJMLC.2012.V2.258","volume":"2","author":"MR Khosravani","year":"2012","unstructured":"Khosravani, M.R.: Application of neural network on flight control. Int. J. Mach. Learn. Comput. 2, 882\u2013885 (2012)","journal-title":"Int. J. Mach. Learn. Comput."},{"key":"27_CR20","doi-asserted-by":"crossref","unstructured":"Lal, R., Prabhakar, P.: Bounded error flowpipe computation of parameterized linear systems. In: International Conference on Embedded Software (2015)","DOI":"10.1109\/EMSOFT.2015.7318279"},{"key":"27_CR21","doi-asserted-by":"crossref","unstructured":"Lal, R., Prabhakar, P.: Safety analysis using compositional bounded error approximations of communicating hybrid systems. In: IEEE 56th Annual Conference on Decision and Control (CDC) (2017)","DOI":"10.1109\/CDC.2017.8263997"},{"key":"27_CR22","doi-asserted-by":"crossref","unstructured":"Lal, R., Prabhakar, P.: Hierarchical abstractions for reachability analysis of probabilistic hybrid systems. In: 56th Annual Allerton Conference on Communication, Control, and Computing (Allerton) (2018)","DOI":"10.1109\/ALLERTON.2018.8635976"},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"Lal, R., Prabhakar, P.: Compositional construction of bounded error over-approximations of acyclic interconnected continuous dynamical systems. In: ACM-IEEE International Conference on Formal Methods and Models for System Design (2019)","DOI":"10.1145\/3359986.3361210"},{"key":"27_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358217","volume":"18","author":"R Lal","year":"2019","unstructured":"Lal, R., Prabhakar, P.: Counterexample guided abstraction refinement for polyhedral probabilistic hybrid systems. ACM Trans. Embedded Comput. Syst. (TECS) 18, 1\u201323 (2019)","journal-title":"ACM Trans. Embedded Comput. Syst. (TECS)"},{"key":"27_CR25","unstructured":"Lewis, F.W., Jagannathan, S., Yesildirak, A.: Neural Network Control of Robot Manipulators and Non-linear Systems. CRC Press, Boca Raton (1998)"},{"key":"27_CR26","doi-asserted-by":"publisher","first-page":"1138","DOI":"10.3382\/ps.2012-02827","volume":"92","author":"M Mehri","year":"2013","unstructured":"Mehri, M.: A comparison of neural network models, fuzzy logic, and multiple linear regression for prediction of hatchability. Poult. Sci. 92, 1138\u20131142 (2013)","journal-title":"Poult. Sci."},{"key":"27_CR27","doi-asserted-by":"publisher","first-page":"562","DOI":"10.2514\/3.43777","volume":"3","author":"RC Montgomery","year":"1966","unstructured":"Montgomery, R.C., Moul, M.T.: Analysis of deep-stall characteristics of t-tailed aircraft configurations and some recovery procedures. J. Airc. 3, 562\u2013566 (1966)","journal-title":"J. Airc."},{"key":"27_CR28","first-page":"25","volume":"45","author":"VG Nair","year":"2012","unstructured":"Nair, V.G., Dileep, M.V., George, V.: Aircraft yaw control system using LQR and fuzzy logic controller. Int. J. Comput. Appl. 45, 25\u201330 (2012)","journal-title":"Int. J. Comput. Appl."},{"key":"27_CR29","doi-asserted-by":"crossref","unstructured":"Prabhakar, P., Viswanathan, M.: A dynamic algorithm for approximate flow computations. In: International Conference on Hybrid Systems: Computation and Control (2011)","DOI":"10.1145\/1967701.1967722"},{"key":"27_CR30","doi-asserted-by":"crossref","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: International Conference on Computer Aided Verification (2010)","DOI":"10.1007\/978-3-642-14295-6_24"},{"key":"27_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-662-54577-5_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Roohi","year":"2017","unstructured":"Roohi, N., Prabhakar, P., Viswanathan, M.: HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 573\u2013588. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_33"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2016)","DOI":"10.1007\/978-3-662-49674-9_48"},{"key":"27_CR33","doi-asserted-by":"crossref","unstructured":"Ruan, W., Huang, X., Kwiatkowska, M.: Reachability analysis of deep neural networks with provable guarantees. CoRR, abs\/1805.02242 (2018)","DOI":"10.24963\/ijcai.2018\/368"},{"key":"27_CR34","doi-asserted-by":"crossref","unstructured":"Shukla, D., Lal, R., Hauptman, D., Keshmiri, S.S., Prabhakar, P., Beckage, N.: Flight test validation of a safety-critical neural network based longitudinal controller for a fixed-wing UAS. In: AIAA AVIATION (2020)","DOI":"10.2514\/6.2020-3093"},{"key":"27_CR35","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. PACMPL 3(POPL), 41:1\u201341:30 (2019)","DOI":"10.1145\/3290354"},{"key":"27_CR36","doi-asserted-by":"publisher","first-page":"1378","DOI":"10.1016\/j.epsr.2007.12.004","volume":"78","author":"NS Sisworahardjo","year":"2008","unstructured":"Sisworahardjo, N.S., El-Sharkh, M.Y., Alam, M.S.: Neural network controller for microturbine power plants. Electr. Power Syst. Res. 78, 1378\u20131384 (2008)","journal-title":"Electr. Power Syst. Res."},{"key":"27_CR37","unstructured":"Umair, S.M., Usman, R.: Automation of irrigation system using ANN based controller. Int. J. Electr. Comput. Sci. (2010)"},{"key":"27_CR38","doi-asserted-by":"crossref","unstructured":"Veanes, M., Bj\u00f8rner, N., Raschke, A.: An SMT approach to bounded reachability analysis of model programs. In: International Conference on Formal Techniques for Networked and Distributed Systems (2008)","DOI":"10.1007\/978-3-540-68855-6_4"},{"key":"27_CR39","unstructured":"Wang, T.: Aircraft wing stall control device and method, 1987. US Patent 4,702,441 (1987)"},{"key":"27_CR40","unstructured":"Xiang, W., et al.: Verification for machine learning, autonomy, and neural networks survey. CoRR, abs\/1810.01989 (2018)"},{"key":"27_CR41","doi-asserted-by":"crossref","unstructured":"Zeynelgil, H.L., Demiroren, A., Sengor, N.S.: The application of ANN technique to automatic generation control for multi-area power system. Int. J. Electr. Power Energy Systems (2002)","DOI":"10.1016\/S0142-0615(01)00049-7"},{"key":"27_CR42","doi-asserted-by":"publisher","first-page":"1835","DOI":"10.1016\/S0005-1098(00)00116-3","volume":"36","author":"T Zhang","year":"2000","unstructured":"Zhang, T., Ge, S.S., Hang, C.C.: Adaptive neural network control for strict-feedback nonlinear systems using backstepping design. Automatica 36, 1835\u20131846 (2000)","journal-title":"Automatica"}],"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-030-81685-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:08:54Z","timestamp":1626480534000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"15 July 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","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":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"290","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":"63","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":"22% - 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":"12","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)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}