{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T23:28:47Z","timestamp":1759879727462,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030309411"},{"type":"electronic","value":"9783030309428"}],"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-30942-8_23","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"371-388","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["An Axiomatic Approach to Liveness for Differential Equations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7033-2463","authenticated-orcid":false,"given":"Yong Kiam","family":"Tan","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"issue":"2","key":"23_CR1","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1016\/j.nahs.2008.12.005","volume":"3","author":"A Abate","year":"2009","unstructured":"Abate, A., D\u2019Innocenzo, A., Benedetto, M.D.D., Sastry, S.: Understanding deadlock and livelock behaviors in hybrid control systems. Nonlinear Anal. Hybrid Syst. 3(2), 150\u2013162 (2009). \nhttps:\/\/doi.org\/10.1016\/j.nahs.2008.12.005","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"23_CR2","volume-title":"Principles of Cyber-Physical Systems","author":"R Alur","year":"2015","unstructured":"Alur, R.: Principles of Cyber-Physical Systems. MIT Press, Cambridge (2015)"},{"key":"23_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03718-8","volume-title":"Real Algebraic Geometry","author":"J Bochnak","year":"1998","unstructured":"Bochnak, J., Coste, M., Roy, M.F.: Real Algebraic Geometry. Springer, Heidelberg (1998). \nhttps:\/\/doi.org\/10.1007\/978-3-662-03718-8"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-39799-8_18"},{"key":"23_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-35794-7","volume-title":"Ordinary Differential Equations with Applications","author":"C Chicone","year":"2006","unstructured":"Chicone, C.: Ordinary Differential Equations with Applications, 2nd edn. Springer, New York (2006). \nhttps:\/\/doi.org\/10.1007\/0-387-35794-7","edition":"2"},{"key":"23_CR6","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. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1047\u20131110. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10575-8_30"},{"key":"23_CR7","doi-asserted-by":"publisher","unstructured":"Duggirala, P.S., Mitra, S.: Lyapunov abstractions for inevitability of hybrid systems. In: Dang, T., Mitchell, I.M. (eds.) HSCC, pp. 115\u2013124. ACM, New York (2012). \nhttps:\/\/doi.org\/10.1145\/2185632.2185652","DOI":"10.1145\/2185632.2185652"},{"key":"23_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"CAV","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"key":"23_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-54862-8_19","volume-title":"TACAS","author":"K Ghorbal","year":"2014","unstructured":"Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS. LNCS, vol. 8413, pp. 279\u2013294. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-642-54862-8_19"},{"key":"23_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3049797.3049811","volume-title":"HSCC","author":"E Goubault","year":"2017","unstructured":"Goubault, E., Putot, S.: Forward inner-approximated reachability of non-linear continuous systems. In: Frehse, G., Mitra, S. (eds.) HSCC, pp. 1\u201310. ACM, New York (2017). \nhttps:\/\/doi.org\/10.1145\/3049797.3049811"},{"key":"23_CR11","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/2038642.2038659","volume-title":"EMSOFT","author":"J Liu","year":"2011","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 97\u2013106. ACM, New York (2011). \nhttps:\/\/doi.org\/10.1145\/2038642.2038659"},{"key":"23_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems - Specification","author":"Z Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, New York (1992). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-0931-7"},{"issue":"3","key":"23_CR13","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1145\/357172.357178","volume":"4","author":"SS Owicki","year":"1982","unstructured":"Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. Program. Lang. Syst. 4(3), 455\u2013495 (1982). \nhttps:\/\/doi.org\/10.1145\/357172.357178","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"Papachristodoulou, A., Prajna, S.: On the construction of Lyapunov functions using the sum of squares decomposition. In: CDC, vol. 3, pp. 3482\u20133487. IEEE (2002). \nhttps:\/\/doi.org\/10.1109\/CDC.2002.1184414","DOI":"10.1109\/CDC.2002.1184414"},{"issue":"1","key":"23_CR15","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1093\/logcom\/exn070","volume":"20","author":"A Platzer","year":"2010","unstructured":"Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309\u2013352 (2010). \nhttps:\/\/doi.org\/10.1093\/logcom\/exn070","journal-title":"J. Log. Comput."},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS, pp. 13\u201324. IEEE (2012). \nhttps:\/\/doi.org\/10.1109\/LICS.2012.13","DOI":"10.1109\/LICS.2012.13"},{"issue":"2","key":"23_CR17","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 differential dynamic logic. J. Autom. Reas. 59(2), 219\u2013265 (2017). \nhttps:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J. Autom. Reas."},{"issue":"3","key":"23_CR18","doi-asserted-by":"publisher","first-page":"19:1","DOI":"10.1145\/3091123","volume":"18","author":"A Platzer","year":"2017","unstructured":"Platzer, A.: Differential hybrid games. ACM Trans. Comput. Log. 18(3), 19:1\u201319:44 (2017). \nhttps:\/\/doi.org\/10.1145\/3091123","journal-title":"ACM Trans. Comput. Log."},{"key":"23_CR19","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). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63588-0"},{"key":"23_CR20","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1145\/3209108.3209147","volume-title":"LICS","author":"A Platzer","year":"2018","unstructured":"Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Dawar, A., Gr\u00e4del, E. (eds.) LICS, pp. 819\u2013828. ACM, New York (2018). \nhttps:\/\/doi.org\/10.1145\/3209108.3209147"},{"key":"23_CR21","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/11730637_38","volume-title":"HSCC","author":"A Podelski","year":"2006","unstructured":"Podelski, A., Wagner, S.: Model checking of hybrid systems: from reachability towards stability. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC. LNCS, vol. 3927, pp. 507\u2013521. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11730637_38"},{"key":"23_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"542","DOI":"10.1007\/978-3-540-31954-2_35","volume-title":"HSCC","author":"S Prajna","year":"2005","unstructured":"Prajna, S., Rantzer, A.: Primal-dual tests for safety and reachability. In: Morari, M., Thiele, L. (eds.) HSCC. LNCS, vol. 3414, pp. 542\u2013556. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-31954-2_35"},{"issue":"3","key":"23_CR23","doi-asserted-by":"publisher","first-page":"999","DOI":"10.1137\/050645178","volume":"46","author":"S Prajna","year":"2007","unstructured":"Prajna, S., Rantzer, A.: Convex programs for temporal verification of nonlinear dynamical systems. SIAM J. Control Optim. 46(3), 999\u20131021 (2007). \nhttps:\/\/doi.org\/10.1137\/050645178","journal-title":"SIAM J. Control Optim."},{"issue":"7","key":"23_CR24","doi-asserted-by":"publisher","first-page":"4377","DOI":"10.1137\/090749955","volume":"48","author":"S Ratschan","year":"2010","unstructured":"Ratschan, S., She, Z.: Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM J. Control Optim. 48(7), 4377\u20134394 (2010). \nhttps:\/\/doi.org\/10.1137\/090749955","journal-title":"SIAM J. Control Optim."},{"key":"23_CR25","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-319-19249-9_32","volume-title":"FM","author":"A Sogokon","year":"2015","unstructured":"Sogokon, A., Jackson, P.B.: Direct formal verification of liveness properties in continuous and hybrid dynamical systems. In: Bj\u00f8rner, N., de Boer, F.S. (eds.) FM. LNCS, vol. 9109, pp. 514\u2013531. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-19249-9_32"},{"key":"23_CR26","doi-asserted-by":"publisher","unstructured":"Sogokon, A., Jackson, P.B., Johnson, T.T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants. J. Autom. Reas. (2018, to appear). \nhttps:\/\/doi.org\/10.1007\/s10817-018-9497-x","DOI":"10.1007\/s10817-018-9497-x"},{"key":"23_CR27","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1879021.1879025","volume-title":"EMSOFT","author":"A Taly","year":"2010","unstructured":"Taly, A., Tiwari, A.: Switching logic synthesis for reachability. In: Carloni, L.P., Tripakis, S. (eds.) EMSOFT, pp. 19\u201328. ACM, New York (2010). \nhttps:\/\/doi.org\/10.1145\/1879021.1879025"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Platzer, A.: An axiomatic approach to liveness for differential equations. CoRR abs\/1904.07984 (2019)","DOI":"10.1007\/978-3-030-30942-8_23"},{"key":"23_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0601-9","volume-title":"Ordinary Differential Equations","author":"W Walter","year":"1998","unstructured":"Walter, W.: Ordinary Differential Equations. Springer, New York (1998). \nhttps:\/\/doi.org\/10.1007\/978-1-4612-0601-9"}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:08:31Z","timestamp":1588658911000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","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":"129","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":"44","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":"7","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":"34% - 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":"4","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":"5,5","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}