{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T04:12:49Z","timestamp":1770437569855,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642327582","type":"print"},{"value":"9783642327599","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32759-9_22","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T10:12:30Z","timestamp":1345543950000},"page":"252-266","source":"Crossref","is-referenced-by-count":10,"title":["Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Taylor T.","family":"Johnson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Green","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rachel","family":"Dudley","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard Scott","family":"Erwin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Allgeier, S.E., Fitz-Coy, N.G., Erwin, R.S., Lovell, T.A.: Metrics for mission planning of formation flight. In: Proc. AAS\/AIAA Astrodynamics Specialist Conference, Girdwood, AK (July 2011)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Althoff, M., Stursberg, O., Buss, M.: Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: 47th IEEE Conference on Decision and Control (CDC), pp. 4042\u20134048 (December 2008)","DOI":"10.1109\/CDC.2008.4738704"},{"key":"22_CR3","first-page":"93","volume-title":"Hybrid Systems: Computation and Control (HSCC)","author":"M. Althoff","year":"2011","unstructured":"Althoff, M., Le Guernic, C., Krogh, B.H.: Reachable set computation for uncertain time-varying linear systems. In: Hybrid Systems: Computation and Control (HSCC), pp. 93\u2013102. ACM, New York (2011)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Althoff, M., Rajhans, A., Krogh, B., Yaldiz, S., Li, X., Pileggi, L.: Formal verification of phase-locked loops using reachability analysis and continuization. In: IEEE\/ACM International Conference on Computer-Aided Design, ICCAD (2011)","DOI":"10.1109\/ICCAD.2011.6105400"},{"issue":"1","key":"22_CR5","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. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"22_CR6","doi-asserted-by":"publisher","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 Informatica\u00a043, 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"key":"22_CR7","unstructured":"Bate, R.R., Mueller, D.D., White, J.E.: Fundamentals of Astrodynamics. Dover (1971)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Battin, R.H.: An introduction to the mathematics and methods of astrodynamics. AIAA education series. American Institute of Aeronautics and Astronautics (1999)","DOI":"10.2514\/4.861543"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Bosse, A.B., Barnds, W.J., Brown, M.A., Creamer, N.G., Feerst, A., Henshaw, C.G., Hope, A.S., Kelm, B.E., Klein, P.A., Pipitone, F., Plourde, B.E., Whalen, B.P.: Sumo: Spacecraft for the Universal Modification of Orbits. In: Proc. of SPIE, vol.\u00a05419, pp. 36\u201346 (2004)","DOI":"10.1117\/12.547714"},{"key":"22_CR10","first-page":"11","volume-title":"Hybrid Systems: Computation and Control (HSCC)","author":"T. Dang","year":"2010","unstructured":"Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: Hybrid Systems: Computation and Control (HSCC), pp. 11\u201320. ACM, New York (2010)"},{"issue":"2","key":"22_CR11","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1016\/j.na.2005.06.054","volume":"64","author":"D. Flieller","year":"2006","unstructured":"Flieller, D., Riedinger, P., Louis, J.P.: Computation and stability of limit cycles in hybrid systems. Nonlinear Analysis: Theory, Methods, & Applications\u00a064(2), 352\u2013367 (2006)","journal-title":"Nonlinear Analysis: Theory, Methods, & Applications"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G. Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., 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 2011. LNCS, vol.\u00a06806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"issue":"4","key":"22_CR14","doi-asserted-by":"publisher","first-page":"1004","DOI":"10.2514\/1.15531","volume":"29","author":"P. Gurfil","year":"2006","unstructured":"Gurfil, P., Kholshevnikov, K.V.: Manifolds and metrics in the relative spacecraft motion problem. Journal of Guidance Control and Dynamics\u00a029(4), 1004\u20131010 (2006)","journal-title":"Journal of Guidance Control and Dynamics"},{"key":"22_CR15","doi-asserted-by":"publisher","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. Journal on Software Tools for Technology Transfer\u00a01, 110\u2013122 (1997)","journal-title":"Journal on Software Tools for Technology Transfer"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Kaynar, D.K., Lynch, N., Segala, R., Vaandrager, F.: The Theory of Timed I\/O Automata. Synthesis Lectures in Computer Science. Morgan & Claypool (2006)","DOI":"10.2200\/S00006ED1V01Y200508CSL001"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Kurzhanskiy, A.A., Varaiya, P.: Ellipsoidal toolbox. In: 45th IEEE Conference on Decision and Control (CDC), pp. 1498\u20131503 (December 2006)","DOI":"10.1109\/CDC.2006.377036"},{"issue":"1","key":"22_CR18","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/S0890-5401(03)00067-1","volume":"185","author":"N. Lynch","year":"2003","unstructured":"Lynch, N., Segala, R., Vaandrager, F.: Hybrid i\/o automata. Inf. Comput.\u00a0185(1), 105\u2013157 (2003)","journal-title":"Inf. Comput."},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Masur, H., Tabachnikov, S.: Rational billiards and flat structures. In: Hasselblatt, B., Katok, A. (eds.) Handbook of Dynamical Systems, Handbook of Dynamical Systems, vol.\u00a01 Part A, ch. 13, pp. 1015\u20131089. Elsevier Science (2002)","DOI":"10.1016\/S1874-575X(02)80015-7"},{"issue":"1","key":"22_CR20","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1196\/annals.1311.013","volume":"1017","author":"C. Ocampo","year":"2004","unstructured":"Ocampo, C.: Finite burn maneuver modeling for a generalized spacecraft trajectory design and optimization system. Annals of the New York Academy of Sciences\u00a01017(1), 210\u2013233 (2004)","journal-title":"Annals of the New York Academy of Sciences"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"R\u00f6mgens, B.A., Mooij, E., Naeije, M.C.: Verified interval orbit propagation in satellite collision avoidance. In: Proc. AIAA Guidance, Navigation, and Control, Portland, OR (2011)","DOI":"10.2514\/6.2011-6653"},{"key":"22_CR22","unstructured":"Vallado, D.A., McClain, W.D.: Fundamentals of astrodynamics and applications. Space technology library. Microcosm Press (2001)"}],"container-title":["Lecture Notes in Computer Science","FM 2012: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32759-9_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:14:53Z","timestamp":1620130493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32759-9_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642327582","9783642327599"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32759-9_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}