{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T09:53:26Z","timestamp":1768038806740,"version":"3.49.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2022,10,29]],"date-time":"2022-10-29T00:00:00Z","timestamp":1667001600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000181","name":"AFOSR","doi-asserted-by":"crossref","award":["FA9550-16-1-0288"],"award-info":[{"award-number":["FA9550-16-1-0288"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2023,1,31]]},"abstract":"<jats:p>The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivial given the unpredictability of the interplay of the intruder aircraft decisions, the ownship pilot reactions, and the subtlety of the continuous motion dynamics of aircraft. Existing collision avoidance systems, such as TCAS and the Next-Generation Airborne Collision Avoidance System ACAS\u00a0X, have been analyzed assuming severe restrictions on the intruder\u2019s flight maneuvers, limiting their safety guarantees in real-world scenarios where the intruder may change its course.<\/jats:p>\n          <jats:p>This work takes a conceptually significant and practically relevant departure from existing ACAS\u00a0X models by generalizing them to hybrid games with first-class representations of the ownship and intruder decisions coming from two independent players, enabling significantly advanced predictive power. By proving the existence of winning strategies for the resulting Adversarial ACAS\u00a0X in differential game logic, collision-freedom is established for the rich encounters of ownship and intruder aircraft with independent decisions along differential equations for flight paths with evolving vertical\/horizontal velocities. We present three classes of models of increasing complexity: single-advisory infinite-time models, bounded time models, and infinite time, multi-advisory models. Within each class of models, we identify symbolic conditions and prove that there then always is a possible ownship maneuver that will prevent a collision between the two aircraft.<\/jats:p>","DOI":"10.1145\/3544970","type":"journal-article","created":{"date-parts":[[2022,6,25]],"date-time":"2022-06-25T09:35:23Z","timestamp":1656149723000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Formally Verified Next-generation Airborne Collision Avoidance Games in ACAS\u00a0X"],"prefix":"10.1145","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6306-9502","authenticated-orcid":false,"given":"Rachel","family":"Cleaveland","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3194-9759","authenticated-orcid":false,"given":"Stefan","family":"Mitsch","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,29]]},"reference":[{"key":"e_1_3_2_2_2","volume-title":"Evaluation of TCAS II Version 7.1 Using the FAA Fast-time Encounter Generator Model","author":"Chludzinski Barbara J.","year":"2009","unstructured":"Barbara J. Chludzinski. 2009. Evaluation of TCAS II Version 7.1 Using the FAA Fast-time Encounter Generator Model. Technical Report. MIT Lincoln Laboratory."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/1093390.1093393"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.2514\/6.2005-6047"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73445-1_13"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.2514\/1.I010178"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_23"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.2514\/atcq.21.3.275"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/DASC50938.2020.9256616"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_2"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-016-0434-1"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.2514\/1.G005233"},{"key":"e_1_3_2_14_2","first-page":"598","article-title":"Deep neural network compression for aircraft collision avoidance systems","volume":"1810","author":"Julian Kyle D.","year":"2018","unstructured":"Kyle D. Julian, Mykel J. Kochenderfer, and Michael P. Owen. 2018. Deep neural network compression for aircraft collision avoidance systems. CoRR abs\/1810.04240 (2018), 598\u2013608.","journal-title":"CoRR"},{"key":"e_1_3_2_15_2","volume-title":"Robust Airborne Collision Avoidance through Dynamic Programming","author":"Kochenderfer Mykel","year":"2011","unstructured":"Mykel Kochenderfer and James Chryssanthacopoulos. 2011. Robust Airborne Collision Avoidance through Dynamic Programming. Technical Report ATC-371. MIT Lincoln Laboratories."},{"key":"e_1_3_2_16_2","first-page":"17","article-title":"Next generation airborne collision avoidance system","volume":"19","author":"Kochenderfer Mykel","year":"2012","unstructured":"Mykel Kochenderfer, Jessica Holland, and James Chryssanthacopoulos. 2012. Next generation airborne collision avoidance system. Lincoln Lab. J. 19 (01 2012), 17\u201333.","journal-title":"Lincoln Lab. J."},{"key":"e_1_3_2_17_2","unstructured":"Mykel J. Kochenderfer L. P. Espindle James K. Kuchar and John Daniel Griffith. 2008. Correlated encounter model for cooperative aircraft in the national airspace system version 1.0. Technical Report ATC-344. MIT Lincoln Laboratory Cambridge Massachusetts."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_22"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.2514\/6.2018-1923"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461350"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.1997.657846"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14509-4"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.13"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2817824"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9385-1"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3091123"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_35"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0367-0"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31365-3_34"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.664154"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_54"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3544970","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3544970","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3544970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:01Z","timestamp":1750186801000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3544970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,29]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1,31]]}},"alternative-id":["10.1145\/3544970"],"URL":"https:\/\/doi.org\/10.1145\/3544970","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,29]]},"assertion":[{"value":"2021-06-03","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-05-23","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-10-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}