{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T05:48:36Z","timestamp":1762321716288},"publisher-location":"Cham","reference-count":182,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105741"},{"type":"electronic","value":"9783319105758"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_30","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"1047-1110","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":39,"title":["Verification of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Laurent","family":"Doyen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Goran","family":"Frehse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George J.","family":"Pappas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"30_CR1","unstructured":"Proceedings of the 27th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25\u201328, 2012. IEEE (2012)"},{"key":"30_CR2","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1109\/TAC.2013.2285751","volume":"59","author":"M. Althoff","year":"2014","unstructured":"Althoff, M., Krogh, B.: Reachability analysis of nonlinear differential-algebraic systems. IEEE Trans. Autom. Control 59, 371\u2013383 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"key":"30_CR3","volume-title":"Modeling, Design, and Simulation of Systems with Uncertainties","author":"M. Althoff","year":"2011","unstructured":"Althoff, M., Krogh, B.H., Stursberg, O.: Analyzing reachability of linear dynamic systems with parametric uncertainties. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties. Springer, Heidelberg (2011)"},{"key":"30_CR4","first-page":"173","volume-title":"Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control","author":"M. Althoff","year":"2013","unstructured":"Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp.\u00a0173\u2013182. ACM, New York (2013)"},{"key":"30_CR5","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1145\/2185632.2185643","volume-title":"Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control","author":"M. Althoff","year":"2012","unstructured":"Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, pp.\u00a045\u201354. ACM, New York (2012)"},{"key":"30_CR6","doi-asserted-by":"crossref","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. 138, 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Chakraborty et al. [8, 34, 35, 91, 132], pp.\u00a0273\u2013278","DOI":"10.1145\/2038642.2038685"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman et al. [31, 100, 113, 129, 149, 174\u2013177], pp.\u00a0209\u2013229","DOI":"10.1007\/3-540-57318-6_30"},{"issue":"2","key":"30_CR9","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/j.tcs.2005.11.026","volume":"354","author":"R. Alur","year":"2006","unstructured":"Alur, R., Dang, T., Ivancic, F.: Counterexample-guided predicate abstraction of hybrid systems. Theor. Comput. Sci. 354(2), 250\u2013271 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"30_CR10","doi-asserted-by":"crossref","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. Embed. Comput. Syst. 5(1), 152\u2013199 (2006)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"2","key":"30_CR11","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"7","key":"30_CR12","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R. Alur","year":"2000","unstructured":"Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"issue":"3","key":"30_CR13","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1109\/32.489079","volume":"22","author":"R. Alur","year":"1996","unstructured":"Alur, R., Henzinger, T.A., Ho, P.-H.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181\u2013201 (1996)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"30_CR14","first-page":"592","volume-title":"ACM Symposium on Theory of Computing","author":"R. Alur","year":"1993","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: ACM Symposium on Theory of Computing, pp.\u00a0592\u2013601 (1993)"},{"key":"30_CR15","series-title":"LNCS","first-page":"49","volume-title":"HSCC","author":"R. Alur","year":"2001","unstructured":"Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Domenica Di Benedetto, M., Sangiovanni-Vincentelli, A.L. (eds.) HSCC. LNCS, vol.\u00a02034, pp.\u00a049\u201362. Springer, Heidelberg (2001)"},{"key":"30_CR16","series-title":"LNCS","volume-title":"Hybrid Systems: Computation and Control, Proceedings of the 7th International Workshop, HSCC 2004","year":"2004","unstructured":"Alur, R., Pappas, G.J. (eds.): Hybrid Systems: Computation and Control, Proceedings of the 7th International Workshop, HSCC 2004, Philadelphia, PA, USA, March 25\u201327, 2004. LNCS, vol.\u00a02993. Springer, Heidelberg (2004)"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Asarin, E., Dang, T.: Abstraction by projection and application to multi-affine systems. In: Alur and Pappas [24, 46, 53, 62, 101, 114, 164, 168], pp.\u00a032\u201347","DOI":"10.1007\/978-3-540-24743-2_3"},{"issue":"7","key":"30_CR18","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","volume":"43","author":"E. Asarin","year":"2007","unstructured":"Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Inform. 43(7), 451\u2013476 (2007)","journal-title":"Acta Inform."},{"key":"30_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/3-540-46430-1_6","volume-title":"Proc. HSCC 00: Hybrid Systems\u2014Computation and Control","author":"E. Asarin","year":"2000","unstructured":"Asarin, E., Dang, T., Maler, O., Bournez, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Proc. HSCC 00: Hybrid Systems\u2014Computation and Control. LNCS, vol.\u00a01790, pp.\u00a020\u201331. Springer, Heidelberg (2000)"},{"key":"30_CR20","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-642-15643-4_5","volume-title":"Automated Technology for Verification and Analysis","author":"E. Asarin","year":"2010","unstructured":"Asarin, E., Dang, T., Maler, O., Testylier, R.: Using redundant constraints for refinement. In: Automated Technology for Verification and Analysis, pp.\u00a037\u201351. Springer, Heidelberg (2010)"},{"issue":"1","key":"30_CR21","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(94)00228-B","volume":"138","author":"E. Asarin","year":"1995","unstructured":"Asarin, E., Maler, O., Pnueli, A.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theor. Comput. Sci. 138(1), 35\u201365 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"1\u20132","key":"30_CR22","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R. Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"key":"30_CR23","first-page":"217","volume-title":"Proc. of LICS","author":"C. Baier","year":"2008","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Gr\u00f6\u00dfer, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: Proc. of LICS, pp.\u00a0217\u2013226. IEEE, Piscataway (2008)"},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"Balluchi, A., Di Natale, F., Sangiovanni-Vincentelli, A.L., van Schuppen, J.H.: Synthesis for idle speed control of an automotive engine. In: Alur and Pappas [130, 182], pp.\u00a080\u201394","DOI":"10.1007\/978-3-540-24743-2_6"},{"key":"30_CR25","series-title":"LNCS","first-page":"147","volume-title":"Proc. of HSCC","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Proc. of HSCC. LNCS, vol.\u00a02034, pp.\u00a0147\u2013161. Springer, Heidelberg (2001)"},{"key":"30_CR26","series-title":"LNCS","volume-title":"Hybrid Systems: Computation and Control, Proceedings of the 10th International Conference, HSCC 2007","year":"2007","unstructured":"Bemporad, A., Bicchi, A., Buttazzo, G. (eds.): Hybrid Systems: Computation and Control, Proceedings of the 10th International Conference, HSCC 2007, Pisa, Italy. LNCS, vol.\u00a04416. Springer, Heidelberg (2007)"},{"key":"30_CR27","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/3-540-48983-5_7","volume-title":"Hybrid Systems: Computation and Control","author":"Alberto Bemporad","year":"1999","unstructured":"Bemporad, A., Morari, M.: Verification of hybrid systems via mathematical programming. In: Vaandrager and van Schuppen [104], pp.\u00a031\u201345"},{"key":"30_CR28","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1016\/j.tcs.2012.10.042","volume":"493","author":"M. Benerecetti","year":"2013","unstructured":"Benerecetti, M., Faella, M., Minopoli, S.: Automatic synthesis of switching controllers for linear hybrid systems: safety control. Theor. Comput. Sci. 493, 116\u2013138 (2013)","journal-title":"Theor. Comput. Sci."},{"issue":"2\u20133","key":"30_CR29","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1016\/j.tcs.2004.04.019","volume":"335","author":"J.A. Bergstra","year":"2005","unstructured":"Bergstra, J.A., Middelburg, C.A.: Process algebra for hybrid systems. Theor. Comput. Sci. 335(2\u20133), 215\u2013280 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"30_CR30","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1023\/A:1024467732637","volume":"4","author":"M. Berz","year":"1998","unstructured":"Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliab. Comput. 4(4), 361\u2013369 (1998)","journal-title":"Reliab. Comput."},{"issue":"4","key":"30_CR31","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1109\/6979.898228","volume":"1","author":"A. Bicchi","year":"2000","unstructured":"Bicchi, A., Pallottino, L.: On optimal cooperative conflict resolution for air traffic management systems. IEEE Trans. Intell. Transp. Syst. 1(4), 221\u2013231 (2000)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"30_CR32","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0701-6","volume-title":"Complexity and Real Computation","author":"L. Blum","year":"1998","unstructured":"Blum, L., Cucker, F., Shub, M., Smale, S.: Complexity and Real Computation. Springer, New York (1998)"},{"issue":"2\u20133","key":"30_CR33","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/j.tcs.2004.04.003","volume":"321","author":"P. Bouyer","year":"2004","unstructured":"Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Updatable timed automata. Theor. Comput. Sci. 321(2\u20133), 291\u2013345 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR34","first-page":"186","volume-title":"Hybrid Systems","author":"M.S. Branicky","year":"1995","unstructured":"Branicky, M.S.: General hybrid dynamical systems: modeling, analysis, and control. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) Hybrid Systems, vol.\u00a01066, pp.\u00a0186\u2013200. Springer, Heidelberg (1995)"},{"issue":"1","key":"30_CR35","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1109\/9.654885","volume":"43","author":"M.S. Branicky","year":"1998","unstructured":"Branicky, M.S., Borkar, V.S., Mitter, S.K.: A unified framework for hybrid control: model and optimal control theory. IEEE Trans. Autom. Control 43(1), 31\u201345 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"30_CR36","series-title":"LNCS","first-page":"416","volume-title":"Proceedings of ICALP 2011: International Colloquium on Automata, Languages and Programming (Part II)","author":"T. Brihaye","year":"2011","unstructured":"Brihaye, T., Doyen, L., Geeraerts, G., Ouaknine, J., Raskin, J.-F., Worrell, J.: On reachability for hybrid automata over bounded time. In: Proceedings of ICALP 2011: International Colloquium on Automata, Languages and Programming (Part II). LNCS, vol.\u00a06756, pp.\u00a0416\u2013427. Springer, Heidelberg (2011)"},{"key":"30_CR37","first-page":"1","volume-title":"Formal Methods in Computer-Aided Design, 2008. FMCAD\u201908","author":"L. Bu","year":"2008","unstructured":"Bu, L., Li, Y., Wang, L., Li, X.: BACH: bounded reachability checker for linear hybrid automata. In: Formal Methods in Computer-Aided Design, 2008. FMCAD\u201908, pp.\u00a01\u20134. IEEE, Piscataway (2008)"},{"key":"30_CR38","unstructured":"Buchberger, B.: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. PhD thesis, University of Innsbruck (1965)"},{"issue":"1\/2","key":"30_CR39","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1561\/1000000001","volume":"1","author":"L.P. Carloni","year":"2006","unstructured":"Carloni, L.P., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.L.: Languages and tools for hybrid systems design. Found. Trends Electron. Des. Autom. 1(1\/2), 1\u2013193 (2006)","journal-title":"Found. Trends Electron. Des. Autom."},{"key":"30_CR40","first-page":"138","volume-title":"CONCUR","author":"F. Cassez","year":"2000","unstructured":"Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: CONCUR, pp.\u00a0138\u2013152 (2000)"},{"volume-title":"Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, Part of the Seventh Embedded Systems Week, ESWeek 2011","year":"2011","key":"30_CR41","unstructured":"Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.): Proceedings of the 11th International Conference on Embedded Software, EMSOFT 2011, Part of the Seventh Embedded Systems Week, ESWeek 2011, Taipei, Taiwan, October 9\u201314, 2011. ACM, New York (2011)"},{"issue":"1","key":"30_CR42","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1109\/9.186313","volume":"38","author":"C. Chase","year":"1993","unstructured":"Chase, C., Serrano, J., Ramadge, P.J.: Periodicity and chaos from switched flow systems: contrasting examples of discretely controlled continuous systems. IEEE Trans. Autom. Control 38(1), 70\u201383 (1993)","journal-title":"IEEE Trans. Autom. Control"},{"key":"30_CR43","first-page":"183","volume-title":"RTSS","author":"X. Chen","year":"2012","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: RTSS, pp.\u00a0183\u2013192. IEEE, Piscataway (2012)"},{"issue":"6","key":"30_CR44","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1016\/0041-5553(68)90115-8","volume":"8","author":"N.V. Chernikova","year":"1968","unstructured":"Chernikova, N.V.: Algorithm for discovering the set of all solutions of a linear programming problem. USSR Comput. Math. Math. Phys. 8(6), 282\u2013293 (1968)","journal-title":"USSR Comput. Math. Math. Phys."},{"key":"30_CR45","doi-asserted-by":"crossref","unstructured":"Chutinan, A., Krogh, B.H.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager and van Schuppen [8, 27, 29, 35, 52, 91, 118, 120, 131, 132, 134, 135, 143, 167, 179, 180], pp.\u00a076\u201390","DOI":"10.1007\/3-540-48983-5_10"},{"issue":"4","key":"30_CR46","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Fehnker, A., Han, Z., Krogh, B.H., Ouaknine, J., Stursberg, O., Theobald, M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583\u2013604 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"30_CR47","series-title":"LNCS","first-page":"154","volume-title":"Proc. of CAV 2000: Computer Aided Verification","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proc. of CAV 2000: Computer Aided Verification. LNCS, vol.\u00a01855, pp.\u00a0154\u2013169. Springer, Heidelberg (2000)"},{"key":"30_CR48","volume-title":"Iterated Maps on the Interval as Dynamical Systems","author":"P. Collet","year":"1980","unstructured":"Collet, P., Eckmann, J.P.: Iterated Maps on the Interval as Dynamical Systems, vol.\u00a01. Springer, Heidelberg (1980)"},{"key":"30_CR49","series-title":"LNCS","first-page":"134","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Barkhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol.\u00a033, pp.\u00a0134\u2013183. Springer, Heidelberg (1975)"},{"issue":"3","key":"30_CR50","doi-asserted-by":"crossref","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. 12(3), 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"30_CR51","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s00224-006-1338-3","volume":"41","author":"P. Collins","year":"2007","unstructured":"Collins, P.: Optimal semicomputable approximations to reachable and invariant sets. Theory Comput. Syst. 41(1), 33\u201348 (2007)","journal-title":"Theory Comput. Syst."},{"issue":"2","key":"30_CR52","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.jlap.2004.02.001","volume":"62","author":"P.J.L. Cuijpers","year":"2005","unstructured":"Cuijpers, P.J.L., Reniers, M.A.: Hybrid process algebra. J. Log. Algebraic Program. 62(2), 191\u2013245 (2005)","journal-title":"J. Log. Algebraic Program."},{"issue":"5","key":"30_CR53","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1080\/00207170600587531","volume":"79","author":"W. Damm","year":"2006","unstructured":"Damm, W., Hungar, H., Olderog, E.-R.: Verification of cooperating traffic agents. Int. J. Control 79(5), 395\u2013421 (2006)","journal-title":"Int. J. Control"},{"issue":"2","key":"30_CR54","first-page":"128","volume":"17","author":"T. Dang","year":"2012","unstructured":"Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliab. Comput. 17(2), 128\u2013152 (2012)","journal-title":"Reliab. Comput."},{"key":"30_CR55","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"G.B. Dantzig","year":"1973","unstructured":"Dantzig, G.B., Eaves, B.C.: Fourier-Motzkin elimination and its dual. J. Comb. Theory 14, 288\u2013297 (1973)","journal-title":"J. Comb. Theory"},{"issue":"1","key":"30_CR56","first-page":"151","volume":"2","author":"J.-G. Darboux","year":"1878","unstructured":"Darboux, J.-G.: M\u00e9moire sur les \u00e9quations diff\u00e9rentielles alg\u00e9briques du premier ordre et du premier degr\u00e9. Bull. Sci. Math. Astron. 2(1), 151\u2013200 (1878)","journal-title":"Bull. Sci. Math. Astron."},{"issue":"1\u20133","key":"30_CR57","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s10703-008-0056-7","volume":"33","author":"M. Wulf De","year":"2008","unstructured":"De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robust safety of timed automata. Form. Methods Syst. Des. 33(1\u20133), 45\u201384 (2008)","journal-title":"Form. Methods Syst. Des."},{"issue":"3","key":"30_CR58","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/s00165-005-0067-8","volume":"17","author":"M. Wulf De","year":"2005","unstructured":"De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: from timed models to timed implementations. Form. Asp. Comput. 17(3), 319\u2013341 (2005)","journal-title":"Form. Asp. Comput."},{"issue":"5","key":"30_CR59","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1016\/j.ipl.2006.11.018","volume":"102","author":"L. Doyen","year":"2007","unstructured":"Doyen, L.: Robust parametric reachability for timed automata. Inf. Process. Lett. 102(5), 208\u2013213 (2007)","journal-title":"Inf. Process. Lett."},{"key":"30_CR60","series-title":"LNCS","first-page":"144","volume-title":"Proc. of FORMATS 2005: Formal Modelling and Analysis of Timed Systems","author":"L. Doyen","year":"2005","unstructured":"Doyen, L., Henzinger, T.A., Raskin, J.-F.: Automatic rectangular refinement of affine hybrid systems. In: Proc. of FORMATS 2005: Formal Modelling and Analysis of Timed Systems. LNCS, vol.\u00a03829, pp.\u00a0144\u2013161. Springer, Heidelberg (2005)"},{"key":"30_CR61","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/11867340_13","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G.E. Fainekos","year":"2006","unstructured":"Fainekos, G.E., Girard, A., Pappas, G.J.: Temporal logic verification using simulation. In: Formal Modeling and Analysis of Timed Systems, pp.\u00a0171\u2013186. Springer, Heidelberg (2006)"},{"issue":"4","key":"30_CR62","doi-asserted-by":"crossref","first-page":"885","DOI":"10.1142\/S0129054106004169","volume":"17","author":"A. Fehnker","year":"2006","unstructured":"Fehnker, A., Krogh, B.H.: Hybrid system verification is not a sinecure\u2014the electronic throttle control case study. Int. J. Found. Comput. Sci. 17(4), 885\u2013902 (2006)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"1","key":"30_CR63","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1137\/0204006","volume":"4","author":"J. Ferrante","year":"1975","unstructured":"Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69\u201376 (1975)","journal-title":"SIAM J. Comput."},{"key":"30_CR64","series-title":"LNCS","first-page":"126","volume-title":"CSL","author":"M. Fr\u00e4nzle","year":"1999","unstructured":"Fr\u00e4nzle, M.: Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: CSL. LNCS, vol.\u00a01683, pp.\u00a0126\u2013140. Springer, Heidelberg (1999)"},{"volume-title":"Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011","year":"2011","key":"30_CR65","unstructured":"Frazzoli, E., Grosu, R. (eds.): Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12\u201314, 2011. ACM, New York (2011)"},{"key":"30_CR66","unstructured":"Frehse, G.: Compositional verification of hybrid systems using simulation relations. PhD thesis, Radboud Universiteit Nijmegen (October 2005)"},{"issue":"3","key":"30_CR67","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G. Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. Softw. Tools Technol. Transf. 10(3), 263\u2013279 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"30_CR68","series-title":"LNCS","volume-title":"CAV","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV. LNCS, vol.\u00a06806. Springer, Heidelberg (2011)"},{"key":"30_CR69","first-page":"203","volume-title":"Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2013","unstructured":"Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp.\u00a0203\u2013212. ACM, New York (2013)"},{"key":"30_CR70","first-page":"257","volume-title":"DATE","author":"G. Frehse","year":"2006","unstructured":"Frehse, G., Krogh, B.H., Rutenbar, R.A.: Verifying analog oscillator circuits using forward\/backward abstraction refinement. In: Gielen, G.G.E. (ed.) DATE, pp.\u00a0257\u2013262. European Design and Automation Association, Leuven (2006)"},{"issue":"2","key":"30_CR71","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BF01582241","volume":"33","author":"R.M. Freund","year":"1985","unstructured":"Freund, R.M., Orlin, J.B.: On the complexity of four polyhedral set containment problems. Math. Program. 33(2), 139\u2013145 (1985)","journal-title":"Math. Program."},{"key":"30_CR72","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction, CADE-25","author":"N. Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction, CADE-25. LNCS, vol.\u00a09195, pp.\u00a0527\u2013538. Springer, Heidelberg (2015)"},{"key":"30_CR73","series-title":"LNCS","first-page":"279","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.\u00a08413, pp.\u00a0279\u2013294. Springer, Heidelberg (2014)"},{"issue":"3","key":"30_CR74","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1006\/cviu.1998.0674","volume":"72","author":"P.K. Ghosh","year":"1998","unstructured":"Ghosh, P.K., Kumar, K.V.: Support function representation of convex bodies, its application in geometric computing, and some related representations. Comput. Vis. Image Underst. 72(3), 379\u2013403 (1998)","journal-title":"Comput. Vis. Image Underst."},{"key":"30_CR75","series-title":"LNCS","first-page":"291","volume-title":"HSCC","author":"A. Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC. LNCS, vol.\u00a03414, pp.\u00a0291\u2013305. Springer, Heidelberg (2005)"},{"issue":"5","key":"30_CR76","doi-asserted-by":"crossref","first-page":"947","DOI":"10.1016\/j.automatica.2012.02.037","volume":"48","author":"A. Girard","year":"2012","unstructured":"Girard, A.: Controller synthesis for safety and reachability via approximate bisimulation. Automatica 48(5), 947\u2013953 (2012)","journal-title":"Automatica"},{"key":"30_CR77","series-title":"LNCS","first-page":"257","volume-title":"HSCC","author":"A. Girard","year":"2006","unstructured":"Girard, A., Le Guernic, C., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC. LNCS, vol.\u00a03927, pp.\u00a0257\u2013271. Springer, Heidelberg (2006)"},{"issue":"5","key":"30_CR78","doi-asserted-by":"crossref","first-page":"782","DOI":"10.1109\/TAC.2007.895849","volume":"52","author":"A. Girard","year":"2007","unstructured":"Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52(5), 782\u2013798 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"S2","key":"30_CR79","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/2331147.2331164","volume":"11","author":"A. Girard","year":"2012","unstructured":"Girard, A., Zheng, G.: Verification of safety and liveness properties of metric transition systems. ACM Trans. Embed. Comput. Syst. 11(S2), 54 (2012)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"2","key":"30_CR80","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/MCS.2008.931718","volume":"29","author":"R. Goebel","year":"2009","unstructured":"Goebel, R., Sanfelice, R.G., Teel, A.R.: Hybrid dynamical systems. IEEE Control Syst. Mag. 29(2), 28\u201393 (2009)","journal-title":"IEEE Control Syst. Mag."},{"key":"30_CR81","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/3-540-61474-5_76","volume-title":"Computer Aided Verification","author":"M.R. Greenstreet","year":"1996","unstructured":"Greenstreet, M.R.: Verifying safety properties of differential equations. In: Computer Aided Verification. LNCS, vol.\u00a01102, pp.\u00a0277\u2013287. Springer, Heidelberg (1996)"},{"key":"30_CR82","series-title":"LNCS","volume-title":"Hybrid Systems","year":"1993","unstructured":"Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.): Hybrid Systems. LNCS, vol.\u00a0736. Springer, Heidelberg (1993)"},{"key":"30_CR83","series-title":"LNCS","first-page":"540","volume-title":"CAV","author":"C. Guernic Le","year":"2009","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV. LNCS, vol.\u00a05643, pp.\u00a0540\u2013554. Springer, Heidelberg (2009)"},{"key":"30_CR84","series-title":"LNCS","first-page":"190","volume-title":"CAV","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV. LNCS, vol.\u00a05123, pp.\u00a0190\u2013203. Springer, Heidelberg (2008)"},{"issue":"2","key":"30_CR85","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/j.tcs.2005.03.045","volume":"342","author":"E. Haghverdi","year":"2005","unstructured":"Haghverdi, E., Tabuada, P., Pappas, G.J.: Bisimulation relations for dynamical, control, and hybrid systems. Theor. Comput. Sci. 342(2), 229\u2013261 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR86","volume-title":"International Static Analysis Symposium, SAS\u201994","author":"N. Halbwachs","year":"1994","unstructured":"Halbwachs, N., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: International Static Analysis Symposium, SAS\u201994, Namur (1994)"},{"key":"30_CR87","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/REAL.1995.495196","volume-title":"Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS \u201995)","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: the next generation. In: Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS \u201995), p.\u00a056. IEEE, Piscataway (1995)"},{"key":"30_CR88","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-60084-1_85","volume-title":"ICALP: Automata, Languages, and Programming","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A.: Hybrid automata with finite bisimulations. In: ICALP: Automata, Languages, and Programming. LNCS, vol.\u00a0944, pp.\u00a0324\u2013335. Springer, Heidelberg (1995)"},{"key":"30_CR89","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transf. 1, 110\u2013122 (1997)","journal-title":"Softw. Tools Technol. Transf."},{"key":"30_CR90","first-page":"58","volume-title":"Proceedings of the 29th Annual Symposium on Principles of Programming Languages","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proceedings of the 29th Annual Symposium on Principles of Programming Languages, pp.\u00a058\u201370. ACM, New York (2002)"},{"key":"30_CR91","series-title":"NATO ASI Series F: Computer and Systems Sciences","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/978-3-642-59615-5_13","volume-title":"Verification of Digital and Hybrid Systems","author":"T.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Inan, M.K., Kurshan, R.P. (eds.) Verification of Digital and Hybrid Systems. NATO ASI Series F: Computer and Systems Sciences, vol.\u00a0170, pp.\u00a0265\u2013292. Springer, Heidelberg (2000)"},{"key":"30_CR92","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid Systems II","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: A note on abstract interpretation strategies for hybrid automata. In: Hybrid Systems II, pp.\u00a0252\u2013264. Springer, Heidelberg (1995)"},{"key":"30_CR93","doi-asserted-by":"crossref","first-page":"540","DOI":"10.1109\/9.664156","volume":"43","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43, 540\u2013554 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"30_CR94","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"530","DOI":"10.1007\/3-540-61604-7_74","volume-title":"CONCUR: Concurrency Theory","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A., Kopke, P.W.: State equivalences for rectangular hybrid automata. In: CONCUR: Concurrency Theory. LNCS, vol.\u00a01119, pp.\u00a0530\u2013545. Springer, Heidelberg (1996)"},{"key":"30_CR95","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1016\/S0304-3975(99)00038-9","volume":"221","author":"T.A. Henzinger","year":"1999","unstructured":"Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. Theor. Comput. Sci. 221, 369\u2013392 (1999)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR96","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57, 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"30_CR97","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/3-540-46430-1_15","volume-title":"Proc. of HSCC 00: Hybrid Systems\u2014Computation and Control","author":"T.A. Henzinger","year":"2000","unstructured":"Henzinger, T.A., Raskin, J.-F.: Robust undecidability of timed and hybrid systems. In: Proc. of HSCC 00: Hybrid Systems\u2014Computation and Control. LNCS, vol.\u00a01790, pp.\u00a0145\u2013159. Springer, Heidelberg (2000)"},{"key":"30_CR98","series-title":"LNCS","first-page":"265","volume-title":"Formal Methods for Industrial Applications","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Wong-Toi, H.: Using HyTech to synthesize control parameters for a steam boiler. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) Formal Methods for Industrial Applications. LNCS, vol.\u00a01165, pp.\u00a0265\u2013282. Springer, Heidelberg (1995)"},{"key":"30_CR99","series-title":"LNCS","first-page":"381","volume-title":"CAV","author":"P.-H. Ho","year":"1995","unstructured":"Ho, P.-H., Wong-Toi, H.: Automated analysis of an audio control protocol. In: Wolper, P. (ed.) CAV. LNCS, vol.\u00a0939, pp.\u00a0381\u2013394. Springer, Heidelberg (1995)"},{"key":"30_CR100","first-page":"161","volume-title":"ICCPS","author":"T.T. Johnson","year":"2012","unstructured":"Johnson, T.T., Mitra, S.: Parametrized verification of distributed cyber-physical systems: an aircraft landing protocol case study. In: ICCPS, pp.\u00a0161\u2013170. IEEE, Piscataway (2012)"},{"key":"30_CR101","unstructured":"Jula, H., Kosmatopoulos, E.B., Ioannou, P.A.: Collision avoidance analysis for lane changing and merging. PATH Research Report UCB-ITS-PRR-99-13, Institute of Transportation Studies, University of California, Berkeley (1999)"},{"key":"30_CR102","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/978-3-540-71493-4_27","volume-title":"Hybrid Systems: Computation and Control","author":"A. Agung Julius","year":"2007","unstructured":"Agung Julius, A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Hybrid Systems: Computation and Control, pp.\u00a0329\u2013342. Springer, Heidelberg (2007)"},{"key":"30_CR103","doi-asserted-by":"crossref","first-page":"1287","DOI":"10.1109\/JPROC.2012.2189792","volume":"100","author":"K.-D. Kim","year":"2012","unstructured":"Kim, K.-D., Kumar, P.R.: Cyber-physical systems: a perspective at the centennial. Proc. IEEE 100, 1287\u20131308 (2012). Centennial-Issue","journal-title":"Proc. IEEE"},{"key":"30_CR104","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1145\/2461328.2461369","volume-title":"HSCC","author":"Y. Kouskoulas","year":"2013","unstructured":"Kouskoulas, Y., Renshaw, D.W., Platzer, A., Kazanzides, P.: Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Belta, C., Ivancic, F. (eds.) HSCC, pp.\u00a0263\u2013272. ACM, New York (2013)"},{"issue":"1","key":"30_CR105","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BF02684450","volume":"61","author":"W. K\u00fchn","year":"1998","unstructured":"K\u00fchn, W.: Rigorously computed orbits of dynamical systems without the wrapping effect. Computing 61(1), 47\u201367 (1998)","journal-title":"Computing"},{"key":"30_CR106","doi-asserted-by":"crossref","first-page":"1498","DOI":"10.1109\/CDC.2006.377036","volume-title":"45th IEEE Conference on Decision and Control","author":"A.A. Kurzhanskiy","year":"2006","unstructured":"Kurzhanskiy, A.A., Varaiya, P.: Ellipsoidal toolbox (ET). In: 45th IEEE Conference on Decision and Control, pp.\u00a01498\u20131503. IEEE, Piscataway (2006)"},{"issue":"1","key":"30_CR107","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1109\/TAC.2006.887900","volume":"52","author":"A.A. Kurzhanskiy","year":"2007","unstructured":"Kurzhanskiy, A.A., Varaiya, P.: Ellipsoidal techniques for reachability analysis of discrete-time linear systems. IEEE Trans. Autom. Control 52(1), 26\u201338 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"30_CR108","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/PL00009858","volume":"13","author":"G. Lafferriere","year":"2000","unstructured":"Lafferriere, G., Pappas, G.J., Sastry, S.: O-minimal hybrid systems. Math. Control Signals Syst. 13(1), 1\u201321 (2000)","journal-title":"Math. Control Signals Syst."},{"issue":"3","key":"30_CR109","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1006\/jsco.2001.0472","volume":"32","author":"G. Lafferriere","year":"2001","unstructured":"Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231\u2013253 (2001)","journal-title":"J. Symb. Comput."},{"key":"30_CR110","unstructured":"Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. PhD thesis, Universit\u00e9 Grenoble 1, Joseph Fourier (2009)"},{"key":"30_CR111","volume-title":"Introduction to Embedded Systems\u2014A Cyber-Physical Systems Approach","author":"E.A. Lee","year":"2013","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems\u2014A Cyber-Physical Systems Approach (2013). Lulu.com"},{"key":"30_CR112","doi-asserted-by":"crossref","first-page":"344","DOI":"10.1007\/978-3-540-78929-1_25","volume-title":"Hybrid Systems: Computation and Control","author":"F. Lerda","year":"2008","unstructured":"Lerda, F., Kapinski, J., Clarke, E.M., Krogh, B.H.: Verification of supervisory control software using state proximity and merging. In: Hybrid Systems: Computation and Control, pp.\u00a0344\u2013357. Springer, Heidelberg (2008)"},{"issue":"7","key":"30_CR113","doi-asserted-by":"crossref","first-page":"926","DOI":"10.1109\/5.871302","volume":"88","author":"C. Livadas","year":"2000","unstructured":"Livadas, C., Lygeros, J., Lynch, N.A.: High-level modeling and analysis of TCAS. Proc. IEEE 88(7), 926\u2013947 (2000)","journal-title":"Proc. IEEE"},{"key":"30_CR114","series-title":"LNCS","first-page":"42","volume-title":"FM","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. LNCS, vol.\u00a06664, pp.\u00a042\u201356. Springer, Heidelberg (2011)"},{"key":"30_CR115","volume-title":"ITSC","author":"S.M. Loos","year":"2013","unstructured":"Loos, S.M., Witmer, D., Steenkiste, P., Platzer, A.: Efficiency analysis of formally verified adaptive cruise controllers. In: Hegyi, A., De Schutter, B. (eds.) ITSC. Springer, Heidelberg (2013)"},{"key":"30_CR116","series-title":"Applied Optimization","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8851-5","volume-title":"Interactive Decision Maps","author":"A.V. Lotov","year":"2004","unstructured":"Lotov, A.V., Bushenkov, V.A., Kamenev, G.K.: Interactive Decision Maps. Applied Optimization, vol.\u00a089. Kluwer Academic, Boston (2004)"},{"key":"30_CR117","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511807930","volume-title":"Handbook of Hybrid Systems Control: Theory, Tools, Applications","author":"J. Lunze","year":"2009","unstructured":"Lunze, J., Lamnabhi-Lagarrigue, F.: Handbook of Hybrid Systems Control: Theory, Tools, Applications. Cambridge University Press, Cambridge (2009)"},{"issue":"1","key":"30_CR118","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N.A. Lynch","year":"2003","unstructured":"Lynch, N.A., Segala, R., Vaandrager, F.W.: Hybrid I\/O automata. Inf. Comput. 185(1), 105\u2013157 (2003)","journal-title":"Inf. Comput."},{"key":"30_CR119","volume-title":"Int. Workshop on Verification of Infinite-State System (Infinity)","author":"O. Maler","year":"2013","unstructured":"Maler, O.: Algorithmic verification of continuous and hybrid systems. In: Int. Workshop on Verification of Infinite-State System (Infinity) (2013)"},{"key":"30_CR120","first-page":"447","volume-title":"REX Workshop","author":"O. Maler","year":"1991","unstructured":"Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX Workshop, vol.\u00a0600, pp.\u00a0447\u2013484. Springer, Heidelberg (1991)"},{"key":"30_CR121","series-title":"LNCS","volume-title":"Hybrid Systems: Computation and Control, Proceedings of the 6th International Workshop, HSCC 2003","year":"2003","unstructured":"Maler, O., Pnueli, A. (eds.): Hybrid Systems: Computation and Control, Proceedings of the 6th International Workshop, HSCC 2003, Prague, Czech Republic, April 3\u20135, 2003. LNCS, vol.\u00a02623. Springer, Heidelberg (2003)"},{"key":"30_CR122","volume-title":"Embedded System Design: Embedded Systems Foundations of Cyber-Physical Systems","author":"P. Marwedel","year":"2010","unstructured":"Marwedel, P.: Embedded System Design: Embedded Systems Foundations of Cyber-Physical Systems. Springer, Heidelberg (2010)"},{"key":"30_CR123","series-title":"LNCS","first-page":"373","volume-title":"SAS","author":"N. Matringe","year":"2010","unstructured":"Matringe, N., Vieira Moura, A., Rebiha, R.: Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Cousot, R., Martel, M. (eds.) SAS. LNCS, vol.\u00a06337, pp.\u00a0373\u2013389. Springer, Heidelberg (2010)"},{"key":"30_CR124","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1007\/3-540-46430-1_26","volume-title":"Proc. of HSCC 00: Hybrid Systems\u2014Computation and Control","author":"J.S. Miller","year":"2000","unstructured":"Miller, J.S.: Decidability and complexity results for timed automata and semi-linear hybrid automata. In: Proc. of HSCC 00: Hybrid Systems\u2014Computation and Control. LNCS, vol.\u00a01790, pp.\u00a0296\u2013309. Springer, Heidelberg (2000)"},{"key":"30_CR125","first-page":"481","volume-title":"Proc. of the 2nd Int. Joint Conference on Artificial Intelligence","author":"R. Milner","year":"1971","unstructured":"Milner, R.: An algebraic definition of simulation between programs. In: Cooper, D.C. (ed.) Proc. of the 2nd Int. Joint Conference on Artificial Intelligence, London, UK, September 1971. pp.\u00a0481\u2013489. William Kaufmann, British Computer Society, London (1971)"},{"key":"30_CR126","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communicating Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communicating Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"issue":"7","key":"30_CR127","doi-asserted-by":"crossref","first-page":"947","DOI":"10.1109\/TAC.2005.851439","volume":"50","author":"I.M. Mitchell","year":"2005","unstructured":"Mitchell, I.M., Bayen, A.M., Tomlin, C.J.: A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games. IEEE Trans. Autom. Control 50(7), 947\u2013957 (2005)","journal-title":"IEEE Trans. Autom. Control"},{"key":"30_CR128","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"480","DOI":"10.1007\/978-3-540-31954-2_31","volume-title":"Hybrid Systems: Computation and Control","author":"I.M. Mitchell","year":"2005","unstructured":"Mitchell, I.M., Templeton, J.A.: A toolbox of Hamilton-Jacobi solvers for analysis of nondeterministic continuous and hybrid systems. In: Morari, M., Thiele, L. (eds.) Hybrid Systems: Computation and Control. LNCS, vol.\u00a03414, pp.\u00a0480\u2013494. Springer, Heidelberg (2005)"},{"key":"30_CR129","doi-asserted-by":"crossref","unstructured":"Mitra, S., Wang, Y., Lynch, N.A., Feron, E.: Safety verification of model helicopter controller using hybrid input\/output automata. In: Maler and Pnueli [8, 91], pp.\u00a0343\u2013358","DOI":"10.1007\/3-540-36580-X_26"},{"key":"30_CR130","volume-title":"Robotics: Science and Systems","author":"S. Mitsch","year":"2013","unstructured":"Mitsch, S., Ghorbal, K., Platzer, A.: On provably safe obstacle avoidance for autonomous robotic ground vehicles. In: Robotics: Science and Systems (2013)"},{"key":"30_CR131","first-page":"2947","volume-title":"Proceedings of the 31st IEEE Conference on Decision and Control","author":"A. Nerode","year":"1992","unstructured":"Nerode, A., Yakhnis, A.: Modelling hybrid systems as games. In: Proceedings of the 31st IEEE Conference on Decision and Control, vol.\u00a03, pp.\u00a02947\u20132952 (1992)"},{"key":"30_CR132","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1007\/3-540-57318-6_35","volume-title":"Hybrid Systems","author":"Anil Nerode","year":"1993","unstructured":"Nerode, A., Kohn, W.: Models for hybrid systems: automata, topologies, controllability, observability. In: Grossman et al. [135, 141], pp.\u00a0317\u2013356"},{"key":"30_CR133","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-3-7091-6918-6_14","volume-title":"Validation Numerics","author":"A. Neumaier","year":"1993","unstructured":"Neumaier, A.: The wrapping effect, ellipsoid arithmetic, stability and confidence regions. In: Validation Numerics, pp.\u00a0175\u2013190. Springer, Heidelberg (1993)"},{"key":"30_CR134","doi-asserted-by":"crossref","unstructured":"Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: An approach to the description and analysis of hybrid systems. In: Grossman et al. [7, 12, 39, 80, 103, 143, 163, 171, 172], pp.\u00a0149\u2013178","DOI":"10.1007\/3-540-57318-6_28"},{"issue":"2","key":"30_CR135","doi-asserted-by":"crossref","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. Reason. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"30_CR136","doi-asserted-by":"crossref","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)","journal-title":"J. Log. Comput."},{"key":"30_CR137","doi-asserted-by":"crossref","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":"30_CR138","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Quantified differential invariants. In: Frazzoli and Grosu [165], pp.\u00a063\u201372","DOI":"10.1145\/1967701.1967713"},{"key":"30_CR139","series-title":"LNCS","first-page":"431","volume-title":"CADE","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. LNCS, vol.\u00a06803, pp.\u00a0431\u2013445. Springer, Heidelberg (2011)"},{"issue":"4","key":"30_CR140","first-page":"1","volume":"8","author":"A. Platzer","year":"2012","unstructured":"Platzer, A.: A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems. Log. Methods Comput. Sci. 8(4), 1\u201344 (2012). Special issue for selected papers from CSL\u201910","journal-title":"Log. Methods Comput. Sci."},{"key":"30_CR141","doi-asserted-by":"crossref","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. In: LICS [137], pp.\u00a0541\u2013550","DOI":"10.1109\/LICS.2012.64"},{"key":"30_CR142","series-title":"LNCS","first-page":"28","volume-title":"ITP","author":"A. Platzer","year":"2012","unstructured":"Platzer, A.: A differential operator approach to equational differential invariants. In: Beringer, L., Felty, A. (eds.) ITP. LNCS, vol.\u00a07406, pp.\u00a028\u201348. Springer, Heidelberg (2012)"},{"key":"30_CR143","doi-asserted-by":"crossref","unstructured":"Platzer, A.: Logics of dynamical systems. In: LICS [111, 122], pp.\u00a013\u201324","DOI":"10.1109\/LICS.2012.13"},{"issue":"4","key":"30_CR144","first-page":"1","volume":"8","author":"A. Platzer","year":"2012","unstructured":"Platzer, A.: The structure of differential invariants and differential cut elimination. Log. Methods Comput. Sci. 8(4), 1\u201338 (2012)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2","key":"30_CR145","doi-asserted-by":"crossref","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. Reason. 59(2), 219\u2013265 (2017)","journal-title":"J. Autom. Reason."},{"key":"30_CR146","doi-asserted-by":"crossref","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, Heidelberg (2018)"},{"key":"30_CR147","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad et al. [8, 27, 29, 35, 52, 91, 118, 120, 131, 132, 134\u2013136, 167, 179, 180], pp.\u00a0473\u2013486","DOI":"10.1007\/978-3-540-71493-4_37"},{"issue":"1","key":"30_CR148","doi-asserted-by":"crossref","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. 35(1), 98\u2013120 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"30_CR149","series-title":"LNCS","first-page":"547","volume-title":"FM","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. (eds.) FM. LNCS, vol.\u00a05850, pp.\u00a0547\u2013562. Springer, Heidelberg (2009)"},{"key":"30_CR150","series-title":"LNCS","first-page":"171","volume-title":"IJCAR","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR. LNCS, vol.\u00a05195, pp.\u00a0171\u2013178. Springer, Heidelberg (2008)"},{"key":"30_CR151","series-title":"LNCS","first-page":"246","volume-title":"ICFEM","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. LNCS, vol.\u00a05885, pp.\u00a0246\u2013265. Springer, Heidelberg (2009)"},{"key":"30_CR152","doi-asserted-by":"crossref","unstructured":"Prabhakar, P., Viswanathan, M.: A dynamic algorithm for approximate flow computations. In: Frazzoli and Grosu [22], pp.\u00a0133\u2013142","DOI":"10.1145\/1967701.1967722"},{"key":"30_CR153","doi-asserted-by":"crossref","unstructured":"Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur and Pappas [55, 63], pp.\u00a0477\u2013492","DOI":"10.1007\/978-3-540-24743-2_32"},{"issue":"8","key":"30_CR154","doi-asserted-by":"crossref","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. Autom. Control 52(8), 1415\u20131429 (2007)","journal-title":"IEEE Trans. Autom. Control"},{"key":"30_CR155","series-title":"LNCS","first-page":"210","volume-title":"FTRTFT \u201998","author":"A. Puri","year":"1998","unstructured":"Puri, A.: Dynamical properties of timed automata. In: FTRTFT \u201998. LNCS, vol.\u00a01486, pp.\u00a0210\u2013227. Springer, Heidelberg (1998)"},{"key":"30_CR156","series-title":"LNCS","first-page":"95","volume-title":"Proc. of CAV","author":"A. Puri","year":"1994","unstructured":"Puri, A., Varaiya, P.: Decidability of hybrid systems with rectangular differential inclusion. In: Proc. of CAV. LNCS, vol.\u00a0818, pp.\u00a095\u2013104. Springer, Heidelberg (1994)"},{"key":"30_CR157","series-title":"LNCS","first-page":"397","volume-title":"TAMC 2010: 7th Annual Conference on Theory and Applications of Models of Computation","author":"S. Ratschan","year":"2010","unstructured":"Ratschan, S.: Safety verification of non-linear hybrid systems is quasi-semidecidable. In: TAMC 2010: 7th Annual Conference on Theory and Applications of Models of Computation. LNCS, vol.\u00a06108, pp.\u00a0397\u2013408. Springer, Heidelberg (2010)"},{"issue":"1","key":"30_CR158","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/1210268.1210276","volume":"6","author":"S. Ratschan","year":"2007","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. Trans. Embed. Comput. Syst. 6(1), 8 (2007)","journal-title":"Trans. Embed. Comput. Syst."},{"key":"30_CR159","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1145\/1755952.1755984","volume-title":"HSCC","author":"S. Sankaranarayanan","year":"2010","unstructured":"Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp.\u00a0221\u2013230. ACM, New York (2010)"},{"key":"30_CR160","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-540-78800-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Dang, T., Ivan\u010di\u0107, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0188\u2013202. Springer, Heidelberg (2008)"},{"issue":"1","key":"30_CR161","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S. Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods Syst. Des. 32(1), 25\u201355 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"30_CR162","series-title":"LNCS","first-page":"433","volume-title":"CAV","author":"M. Segelken","year":"2007","unstructured":"Segelken, M.: Abstraction and counterexample-guided construction of \u03c9$\\omega $-automata for model checking of step-discrete linear hybrid models. In: Damm, W., Hermanns, H. (eds.) CAV. LNCS, vol.\u00a04590, pp.\u00a0433\u2013448. Springer, Heidelberg (2007)"},{"key":"30_CR163","doi-asserted-by":"crossref","unstructured":"Sokolsky, O., Lee, I., Heimdahl, M.P.E.: Challenges in the regulatory approval of medical cyber-physical systems. In: Chakraborty et al. [44], pp.\u00a0227\u2013232","DOI":"10.1145\/2038642.2038677"},{"issue":"10","key":"30_CR164","doi-asserted-by":"crossref","first-page":"1269","DOI":"10.1016\/j.conengprac.2004.04.002","volume":"12","author":"O. Stursberg","year":"2004","unstructured":"Stursberg, O., Fehnker, A., Han, Z., Krogh, B.H.: Verification of a cruise control system using counterexample-guided search. Control Eng. Pract. 12(10), 1269\u20131278 (2004)","journal-title":"Control Eng. Pract."},{"key":"30_CR165","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-0224-5","volume-title":"Verification and Control of Hybrid Systems: A Symbolic Approach","author":"P. Tabuada","year":"2009","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Heidelberg (2009)"},{"key":"30_CR166","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press, Berkeley (1951)","edition":"2"},{"issue":"6","key":"30_CR167","doi-asserted-by":"crossref","first-page":"665","DOI":"10.1016\/0362-546X(87)90034-4","volume":"11","author":"L. Tavernini","year":"1987","unstructured":"Tavernini, L.: Differential automata and their discrete simulators. Nonlinear Anal. 11(6), 665\u2013683 (1987)","journal-title":"Nonlinear Anal."},{"key":"30_CR168","doi-asserted-by":"crossref","first-page":"514","DOI":"10.1007\/3-540-36580-X_37","volume-title":"Hybrid Systems: Computation and Control","author":"Ashish Tiwari","year":"2003","unstructured":"Tiwari, A.: Approximate reachability for linear systems. In: Maler and Pnueli [6, 96], pp.\u00a0514\u2013525"},{"issue":"1","key":"30_CR169","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A. Tiwari","year":"2008","unstructured":"Tiwari, A.: Abstractions for hybrid systems. Form. Methods Syst. Des. 32(1), 57\u201383 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"30_CR170","series-title":"LNCS","first-page":"658","volume-title":"HSCC","author":"A. Tiwari","year":"2008","unstructured":"Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC. LNCS, vol.\u00a04981, pp.\u00a0658\u2013661. Springer, Heidelberg (2008)"},{"key":"30_CR171","first-page":"9","volume-title":"LICS","author":"A. Tiwari","year":"2011","unstructured":"Tiwari, A.: Logic in software, dynamical and biological systems. In: LICS, pp.\u00a09\u201310. IEEE, Piscataway (2011)"},{"issue":"1","key":"30_CR172","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1109\/JPROC.2002.805818","volume":"91","author":"A. Tiwari","year":"2003","unstructured":"Tiwari, A., Shankar, N., Rushby, J.M.: Invisible formal methods for embedded control systems. Proc. IEEE 91(1), 29\u201339 (2003)","journal-title":"Proc. IEEE"},{"issue":"3","key":"30_CR173","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s00454-008-9097-3","volume":"40","author":"H.R. Tiwary","year":"2008","unstructured":"Tiwary, H.R.: On the hardness of computing intersection, union and Minkowski sum of polytopes. Discrete Comput. Geom. 40(3), 469\u2013479 (2008)","journal-title":"Discrete Comput. Geom."},{"key":"30_CR174","series-title":"Lecture Notes in Control and Information Sciences","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BFb0015088","volume-title":"Control Problems in Robotics and Automation","author":"C. Tomlin","year":"1998","unstructured":"Tomlin, C., Pappas, G., Ko\u0161eck\u00e1, J., Lygeros, J., Sastry, S.: Advanced air traffic automation: a\u00a0case study in distributed decentralized control. In: Siciliano, B., Valavanis, K. (eds.) Control Problems in Robotics and Automation. Lecture Notes in Control and Information Sciences, vol.\u00a0230, pp.\u00a0261\u2013295. Springer, Heidelberg (1998)"},{"issue":"4","key":"30_CR175","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/9.664154","volume":"43","author":"C. Tomlin","year":"1998","unstructured":"Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: a study in multi-agent hybrid systems. IEEE Trans. Autom. Control 43(4), 509\u2013521 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"30_CR176","first-page":"64","volume-title":"FM","author":"S. Umeno","year":"2006","unstructured":"Umeno, S., Lynch, N.A.: Proving safety properties of an aircraft landing protocol using I\/O automata and the PVS theorem prover: a case study. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM, vol.\u00a04085, pp.\u00a064\u201380. Springer, Heidelberg (2006)"},{"key":"30_CR177","doi-asserted-by":"crossref","unstructured":"Umeno, S., Lynch, N.A.: Safety verification of an aircraft landing protocol: a refinement approach. In: Bemporad et al. [136], pp.\u00a0557\u2013572","DOI":"10.1007\/978-3-540-71493-4_43"},{"key":"30_CR178","series-title":"LNCS","volume-title":"Hybrid Systems: Computation and Control, Proceedings of the Second International Workshop, HSCC\u201999","year":"1999","unstructured":"Vaandrager, F.W., van Schuppen, J.H. (eds.) Hybrid Systems: Computation and Control, Proceedings of the Second International Workshop, HSCC\u201999, Berg en Dal, The Netherlands, March 29\u201331, 1999. LNCS, vol.\u00a01569, Springer, Heidelberg (1999)"},{"issue":"1\u20132","key":"30_CR179","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/j.jlap.2005.10.005","volume":"68","author":"D.A. Beek van","year":"2006","unstructured":"van Beek, D.A., Man, K.L., Reniers, M.A., Rooda, J.E., Schiffelers, R.R.H.: Syntax and consistent equation semantics of hybrid Chi. J. Log. Algebraic Program. 68(1\u20132), 129\u2013210 (2006)","journal-title":"J. Log. Algebraic Program."},{"key":"30_CR180","volume-title":"17th IFAC World Congress","author":"D.A. Beek van","year":"2008","unstructured":"van Beek, D.A., Reniers, M.A., Schiffelers, R.R.H., Rooda, J.E.: Concrete syntax and semantics of the compositional interchange format for hybrid systems. In: 17th IFAC World Congress (2008)"},{"key":"30_CR181","series-title":"LNCS","first-page":"390","volume-title":"Hybrid Systems","author":"H. Wong-Toi","year":"1997","unstructured":"Wong-Toi, H.: Analysis of slope-parametric rectangular automata. In: Hybrid Systems. LNCS, vol.\u00a01567, pp.\u00a0390\u2013413. Springer, Heidelberg (1997)"},{"key":"30_CR182","series-title":"LNCS","first-page":"396","volume-title":"HSCC","author":"T. Wongpiromsarn","year":"2009","unstructured":"Wongpiromsarn, T., Mitra, S., Murray, R.M., Lamperski, A.G.: Periodically controlled hybrid systems. In: Majumdar, R., Tabuada, P. (eds.) HSCC. LNCS, vol.\u00a05469, pp.\u00a0396\u2013410. Springer, Heidelberg (2009)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,23]],"date-time":"2022-08-23T21:59:53Z","timestamp":1661291993000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":182,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_30","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}