{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T02:46:16Z","timestamp":1770432376833,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705437","type":"print"},{"value":"9783540705451","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70545-1_17","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"176-189","source":"Crossref","is-referenced-by-count":43,"title":["Computing Differential Invariants of Hybrid Systems as Fixedpoints"],"prefix":"10.1007","author":[{"given":"Andr\u00e9","family":"Platzer","sequence":"first","affiliation":[]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","first-page":"278","volume-title":"LICS","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278\u2013292. IEEE, Los Alamitos (1996)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Davoren, J.M., Nerode, A.: Logics for hybrid systems. Proc. IEEE\u00a088(7) (2000)","DOI":"10.1109\/5.871305"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-48168-0_10","volume-title":"Computer Science Logic","author":"M. Fr\u00e4nzle","year":"1999","unstructured":"Fr\u00e4nzle, M.: Analysis of hybrid systems. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 126\u2013140. Springer, Heidelberg (1999)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems: Computation and Control","year":"2004","unstructured":"Alur, R., Pappas, G.J. (eds.): HSCC 2004. LNCS, vol.\u00a02993. Springer, Heidelberg (2004)"},{"issue":"3","key":"17_CR5","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G.E. Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput.\u00a012(3), 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/11513988_3","volume-title":"Computer Aided Verification","author":"C. Piazza","year":"2005","unstructured":"Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B.: Algorithmic algebraic model checking I: Challenges from systems biology. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 5\u201319. Springer, Heidelberg (2005)"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/3-540-45351-2_9","volume-title":"Hybrid Systems: Computation and Control","author":"H. Anai","year":"2001","unstructured":"Anai, H., Weispfenning, V.: Reach set computations using real quantifier elimination. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 63\u201376. Springer, Heidelberg (2001)"},{"key":"17_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-73099-6_17","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Platzer","year":"2007","unstructured":"Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol.\u00a04548, pp. 216\u2013232. Springer, Heidelberg (2007)"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning (2008)","DOI":"10.1007\/s10817-008-9103-8"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/3-540-36580-X_5","volume-title":"Hybrid Systems: Computation and Control","author":"E. Asarin","year":"2003","unstructured":"Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 20\u201335. Springer, Heidelberg (2003)"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: [27], pp. 473\u2013486","DOI":"10.1007\/978-3-540-71493-4_37"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Donz\u00e9, A., Maler, O.: Systematic simulation using sensitivity analysis. In: [27], pp. 174\u2013189","DOI":"10.1007\/978-3-540-71493-4_16"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Differential algebraic dynamic logic for differential algebraic programs (submitted, 2007)","DOI":"10.1093\/logcom\/exn070"},{"issue":"4","key":"17_CR14","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/BF02248730","volume":"21","author":"E.M. Clarke","year":"1979","unstructured":"Clarke, E.M.: Program invariants as fixedpoints. Computing\u00a021(4), 273\u2013294 (1979)","journal-title":"Computing"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Technical Report CMU-CS-08-103, Carnegie Mellon University (2008)","DOI":"10.21236\/ADA476791"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: a study in multi-agent hybrid systems. IEEE T. Automat. Contr.\u00a043(4) (1998)","DOI":"10.1109\/9.664154"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"646","DOI":"10.1007\/978-3-540-78929-1_55","volume-title":"HSCC","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.D.: Logical verification and systematic parametric analysis in train control. In: Egerstedt, M., Mishra, B. (eds.) HSCC. LNCS, vol.\u00a04981, pp. 646\u2013649. Springer, Heidelberg (2008)"},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. In: [4], pp. 539\u2013554","DOI":"10.1007\/978-3-540-24743-2_36"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"590","DOI":"10.1007\/978-3-540-31954-2_38","volume-title":"Hybrid Systems: Computation and Control","author":"E. Rodr\u00edguez-Carbonell","year":"2005","unstructured":"Rodr\u00edguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 590\u2013605. Springer, Heidelberg (2005)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE T. Automat. Contr.\u00a052(8) (2007)","DOI":"10.1109\/TAC.2007.902736"},{"key":"17_CR21","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. MIT Press, Cambridge (2000)"},{"key":"17_CR22","first-page":"270","volume-title":"ICECCS","author":"M. Massink","year":"2001","unstructured":"Massink, M., Francesco, N.D.: Modelling free flight with collision avoidance. In: ICECCS, pp. 270\u2013280. IEEE Computer Society, Los Alamitos (2001)"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Dowek, G., Mu\u00f1oz, C., Carre\u00f1o, V.A.: Provably safe coordinated strategy for distributed conflict resolution. In: AIAA Conference Proc. AIAA-2005-6047 (2005)","DOI":"10.2514\/6.2005-6047"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/11562948_10","volume-title":"Automated Technology for Verification and Analysis","author":"W. Damm","year":"2005","unstructured":"Damm, W., Pinto, G., Ratschan, S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 99\u2013113. Springer, Heidelberg (2005)"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Hwang, I., Kim, J., Tomlin, C.: Protocol-based conflict resolution for air traffic control. Air Traffic Control Quarterly\u00a015(1) (2007)","DOI":"10.2514\/atcq.15.1.1"},{"key":"17_CR26","unstructured":"Mansfield, E.L.: Differential Gr\u00f6bner Bases. PhD thesis, University Sydney (1991)"},{"key":"17_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"HSCC","year":"2007","unstructured":"Bemporad, A., Bicchi, A., Buttazzo, G. (eds.): HSCC 2007. LNCS, vol.\u00a04416. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:07:36Z","timestamp":1605762456000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705437","9783540705451"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}