{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,4]],"date-time":"2025-04-04T04:19:10Z","timestamp":1743740350646,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642316227"},{"type":"electronic","value":"9783642316234"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31623-4_3","type":"book-chapter","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T05:03:34Z","timestamp":1341810214000},"page":"43-49","source":"Crossref","is-referenced-by-count":3,"title":["Logical Analysis of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Andr\u00e9","family":"Platzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Proceedings of the 27th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28. IEEE Computer Society (2012)"},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci.\u00a0138(1), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Ar\u00e9chiga, N., Loos, S.M., Platzer, A., Krogh, B.H.: Using theorem provers to guarantee closed-loop system properties. In: Tilbury, D. (ed.) ACC (2012)","DOI":"10.1109\/ACC.2012.6315388"},{"key":"3_CR4","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput.\u00a07(1), 70\u201390 (1978)","journal-title":"SIAM J. Comput."},{"issue":"7","key":"3_CR6","doi-asserted-by":"publisher","first-page":"985","DOI":"10.1109\/5.871305","volume":"88","author":"J.M. Davoren","year":"2000","unstructured":"Davoren, J.M., Nerode, A.: Logics for hybrid systems. IEEE\u00a088(7), 985\u20131010 (2000)","journal-title":"IEEE"},{"issue":"2","key":"3_CR7","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci.\u00a018(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09237-4","volume-title":"First-Order Dynamic Logic","author":"D. Harel","year":"1979","unstructured":"Harel, D.: First-Order Dynamic Logic. Springer, New York (1979)"},{"key":"3_CR9","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":"3_CR10","doi-asserted-by":"crossref","unstructured":"Harel, D., Meyer, A.R., Pratt, V.R.: Computability and completeness in logics of programs (preliminary report). In: STOC, pp. 261\u2013268. ACM (1977)","DOI":"10.1145\/800105.803416"},{"key":"3_CR11","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 Computer Society, Los Alamitos (1996)"},{"issue":"3","key":"3_CR12","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1016\/0890-5401(89)90033-3","volume":"81","author":"S. Istrail","year":"1989","unstructured":"Istrail, S.: An arithmetical hierarchy in propositional dynamic logic. Inf. Comput.\u00a081(3), 280\u2013289 (1989)","journal-title":"Inf. Comput."},{"issue":"3","key":"3_CR13","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst.\u00a019(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0304-3975(81)90019-0","volume":"14","author":"D. Kozen","year":"1981","unstructured":"Kozen, D., Parikh, R.: An elementary proof of the completeness of PDL. Theor. Comp. Sci.\u00a014, 113\u2013118 (1981)","journal-title":"Theor. Comp. Sci."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Leivant, D.: Matching explicit and modal reasoning about programs: A proof theoretic delineation of dynamic logic. In: LICS, pp. 157\u2013168. IEEE Computer Society (2006)","DOI":"10.1109\/LICS.2006.33"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Loos, S.M., Platzer, A.: Safe intersections: At the crossing of hybrid systems and verification. In: Yi, K. (ed.) ITSC, pp. 1181\u20131186. Springer (2011)","DOI":"10.1109\/ITSC.2011.6083138"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-642-21437-0_6","volume-title":"FM 2011: Formal Methods","author":"S.M. Loos","year":"2011","unstructured":"Loos, S.M., Platzer, A., Nistor, L.: Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol.\u00a06664, pp. 42\u201356. Springer, Heidelberg (2011)"},{"issue":"2","key":"3_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0022-0000(81)90016-7","volume":"23","author":"A.R. Meyer","year":"1981","unstructured":"Meyer, A.R., Parikh, R.: Definability in dynamic logic. J. Comput. Syst. Sci.\u00a023(2), 279\u2013298 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"Mitsch, S., Loos, S.M., Platzer, A.: Towards formal verification of freeway traffic control. In: Lu, C. (ed.) ICCPS, pp. 171\u2013180. IEEE (2012)","DOI":"10.1109\/ICCPS.2012.25"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/3-540-08921-7_88","volume-title":"Mathematical Foundations of Computer Science 1978","author":"R. Parikh","year":"1978","unstructured":"Parikh, R.: The Completeness of Propositional Dynamic Logic. In: Winkowski, J. (ed.) MFCS 1978. LNCS, vol.\u00a064, pp. 403\u2013415. Springer, Heidelberg (1978)"},{"issue":"2","key":"3_CR21","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1145\/23005.23008","volume":"34","author":"D. Peleg","year":"1987","unstructured":"Peleg, D.: Concurrent dynamic logic. J. ACM\u00a034(2), 450\u2013479 (1987)","journal-title":"J. ACM"},{"key":"3_CR22","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)"},{"issue":"2","key":"3_CR23","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. Reas.\u00a041(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reas."},{"key":"3_CR24","unstructured":"Platzer, A.: Differential Dynamic Logics: Automated Theorem Proving for Hybrid Systems. Ph.D. thesis, Department of Computing Science, University of Oldenburg (December 2008) (appeared with Springer)"},{"issue":"1","key":"3_CR25","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.\u00a020(1), 309\u2013352 (2010)","journal-title":"J. Log. Comput."},{"key":"3_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4","volume-title":"Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/978-3-642-15205-4_36","volume-title":"Computer Science Logic","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Quantified Differential Dynamic Logic for Distributed Hybrid Systems. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 469\u2013483. Springer, Heidelberg (2010)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1007\/978-3-642-22438-6_34","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Platzer","year":"2011","unstructured":"Platzer, A.: Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 446\u2013460. Springer, Heidelberg (2011)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. In: Logical Methods in Computer Science (2012); special issue for selected papers from CSL 2010","DOI":"10.2168\/LMCS-8(4:17)2012"},{"key":"3_CR30","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. In: LICS [1]"},{"key":"3_CR31","unstructured":"Platzer, A.: Logics of dynamical systems (invited tutorial). In: LICS [1]"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Platzer, A.: The structure of differential invariants and differential cut elimination. In: Logical Methods in Computer Science (to appear, 2012)","DOI":"10.2168\/LMCS-8(4:16)2012"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-540-70545-1_17","volume-title":"Computer Aided Verification","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Clarke, E.M.: Computing Differential Invariants of Hybrid Systems as Fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 176\u2013189. Springer, Heidelberg (2008)"},{"issue":"1","key":"3_CR34","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/s10703-009-0079-8","volume":"35","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Form. Methods Syst. Des.\u00a035(1), 98\u2013120 (2009); special issue for selected papers from CAV 2008","journal-title":"Form. Methods Syst. Des."},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/978-3-642-05089-3_35","volume-title":"FM 2009: Formal Methods","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Clarke, E.M.: Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 547\u2013562. Springer, Heidelberg (2009)"},{"key":"3_CR36","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-10373-5_13","volume-title":"Formal Methods and Software Engineering","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D.: European Train Control System: A Case Study in Formal Verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 246\u2013265. Springer, Heidelberg (2009)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/978-3-642-02959-2_35","volume-title":"Automated Deduction \u2013 CADE-22","author":"A. Platzer","year":"2009","unstructured":"Platzer, A., Quesel, J.-D., R\u00fcmmer, P.: Real World Verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 485\u2013501. Springer, Heidelberg (2009)"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: FOCS, pp. 109\u2013121. IEEE (1976)","DOI":"10.1109\/SFCS.1976.27"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/3-540-63104-6_10","volume-title":"Automated Deduction - CADE-14","author":"W. Reif","year":"1997","unstructured":"Reif, W., Schellhorn, G., Stenzel, K.: Proving System Correctness with KIV 3.0. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 69\u201372. Springer, Heidelberg (1997)"},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/978-3-642-24559-6_25","volume-title":"Formal Methods and Software Engineering","author":"D.W. Renshaw","year":"2011","unstructured":"Renshaw, D.W., Loos, S.M., Platzer, A.: Distributed Theorem Proving for Distributed Hybrid Systems. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 356\u2013371. Springer, Heidelberg (2011)"},{"key":"3_CR42","first-page":"522","volume":"24","author":"K. Segerberg","year":"1977","unstructured":"Segerberg, K.: A completeness theorem in the modal logic of programs. Notices AMS\u00a024, 522 (1977)","journal-title":"Notices AMS"}],"container-title":["Lecture Notes in Computer Science","Descriptional Complexity of Formal Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31623-4_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:25:39Z","timestamp":1743697539000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31623-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642316227","9783642316234"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31623-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}