{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,3]],"date-time":"2025-10-03T18:12:04Z","timestamp":1759515124238},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540754534"},{"type":"electronic","value":"9783540754541"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75454-1_18","type":"book-chapter","created":{"date-parts":[[2007,9,18]],"date-time":"2007-09-18T01:47:54Z","timestamp":1190080074000},"page":"241-256","source":"Crossref","is-referenced-by-count":9,"title":["Symbolic Reachability Analysis of Lazy Linear Hybrid Automata"],"prefix":"10.1007","author":[{"given":"Susmit","family":"Jha","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bryan A.","family":"Brady","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/11730637_4","volume-title":"Hybrid Systems: Computation and Control","author":"M. Agrawal","year":"2006","unstructured":"Agrawal, M., Stephan, F., Thiagarajan, P.S., Yang, S.: Behavioural approximations for restricted linear differential hybrid automata. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol.\u00a03927, pp. 4\u201318. Springer, Heidelberg (2006)"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Hybrid Systems: Computation and Control","author":"M. Agrawal","year":"2004","unstructured":"Agrawal, M., Thiagarajan, P.S.: Lazy rectangular hybrid automata. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 1\u201315. Springer, Heidelberg (2004)"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/978-3-540-31954-2_4","volume-title":"Hybrid Systems: Computation and Control","author":"M. Agrawal","year":"2005","unstructured":"Agrawal, M., Thiagarajan, P.S.: The discrete time behavior of lazy linear hybrid automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 55\u201369. Springer, Heidelberg (2005)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","first-page":"209","volume-title":"Hybrid Systems","author":"R. Alur","year":"1992","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, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) Hybrid Systems. LNCS, vol.\u00a0736, pp. 209\u2013229. Springer, Heidelberg (1992)"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"358","DOI":"10.1007\/978-3-540-71209-1_28","volume-title":"Proceedings of TACAS 2007","author":"R.E. Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.: Deciding bit-vector arithmetic with abstraction. In: Proceedings of TACAS 2007. LNCS, vol.\u00a04424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-63166-6_32","volume-title":"Computer Aided Verification","author":"W. Chan","year":"1997","unstructured":"Chan, W., Anderson, R., Beame, P., Notkin, D.: Combining constraint solving and symbolic model checking for a class of a systems with non-linear constraints. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 316\u2013327. Springer, Heidelberg (1997)"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"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: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 154\u2013169. Springer, Heidelberg (2000)"},{"key":"18_CR8","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":"18_CR9","doi-asserted-by":"crossref","unstructured":"Deshpande, A., Godbole, D.N.A.G., Varaiya, P.: Design and evaluation tools for automated highway systems. In: Hybrid Systems, pp. 138\u2013148 (1995)","DOI":"10.1007\/BFb0020941"},{"key":"18_CR10","unstructured":"Federal Aviation Administration. Introduction to TCAS II Version 7 (November 2000), http:\/\/www.arinc.com\/downloads\/tcas\/tcas.pdf"},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: HSCC, pp. 258\u2013273 (2005)","DOI":"10.1007\/978-3-540-31954-2_17"},{"issue":"1-2","key":"18_CR12","doi-asserted-by":"publisher","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. TCS\u00a0221(1-2), 369\u2013392 (1999)","journal-title":"TCS"},{"key":"18_CR13","unstructured":"Ho, P.-H.: Automatic analysis of hybrid systems. PhD thesis, Cornell Univ. (1995)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/978-3-540-71493-4_24","volume-title":"HSCC 2007","author":"S.K. Jha","year":"2007","unstructured":"Jha, S.K., Krogh, B.H., Weimer, J., Clarke, E.M.: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 287\u2013300. Springer, Heidelberg (2007)"},{"key":"18_CR15","first-page":"115","volume-title":"RTSS 1999","author":"C. Livadas","year":"1999","unstructured":"Livadas, C., Lygeros, J., Lynch, N.A.: High-level modeling and analysis of tcas. In: RTSS 1999, p. 115. IEEE Computer Society Press, Washington, DC, USA (1999)"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Pappas, G., Tomlin, C., Sastry, S.: Conflict resolution for multi-agent hybrid systems. In: CDC, pp. 1184\u20131189 (1996)","DOI":"10.1109\/CDC.1996.572644"},{"key":"18_CR17","unstructured":"Potocnik, B., Bemporad, A., Torrisi, F., Music, G., Zupancic, B.: Hysdel Modeling and Simulation of Hybrid Dynamical Systems. In: MATHMOD Conference, Vienna, Austria (February 2003)"},{"key":"18_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/11856290_18","volume-title":"Artificial Intelligence and Symbolic Computation","author":"S. Ratschan","year":"2006","unstructured":"Ratschan, S., She, Z.: Constraints for continuous reachability in the verification of hybrid systems. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol.\u00a04120, pp. 196\u2013210. Springer, Heidelberg (2006)"},{"key":"18_CR19","unstructured":"TCAS201 Specification Datasheet. http:\/\/www.aeroflex.com\/products\/avionics\/rf\/datasheets\/tcas201.pdf"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-36580-X_37","volume-title":"Hybrid Systems: Computation and Control","author":"A. Tiwari","year":"2003","unstructured":"Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol.\u00a02623, pp. 514\u2013525. Springer, Heidelberg (2003)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/3-540-45873-5_36","volume-title":"Hybrid Systems: Computation and Control","author":"A. Tiwari","year":"2002","unstructured":"Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol.\u00a02289, pp. 465\u2013478. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75454-1_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:01:58Z","timestamp":1619521318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75454-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540754534","9783540754541"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75454-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}