{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T04:52:57Z","timestamp":1726030377832},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030206512"},{"type":"electronic","value":"9783030206529"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-20652-9_5","type":"book-chapter","created":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:03:25Z","timestamp":1558983805000},"page":"71-87","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Traffic Management for Urban Air Mobility"],"prefix":"10.1007","author":[{"given":"Suda","family":"Bharadwaj","sequence":"first","affiliation":[]},{"given":"Steven","family":"Carr","sequence":"additional","affiliation":[]},{"given":"Natasha","family":"Neogi","sequence":"additional","affiliation":[]},{"given":"Hasan","family":"Poonawala","sequence":"additional","affiliation":[]},{"given":"Alejandro Barberia","family":"Chueca","sequence":"additional","affiliation":[]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,5,28]]},"reference":[{"key":"5_CR1","unstructured":"Bluesky - the open air traffic simulator. https:\/\/github.com\/ProfHoekstra\/bluesky"},{"key":"5_CR2","unstructured":"Skygrid Technology. https:\/\/skygrid.com\/technology\/ . Accessed 11 Dec 2018"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5","volume-title":"Lectures on Runtime Verification","year":"2018","unstructured":"Bartocci, E., Falcone, Y. (eds.): Lectures on Runtime Verification. LNCS, vol. 10457. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75632-5"},{"issue":"1\u20132","key":"5_CR4","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/s10703-016-0253-8","volume":"48","author":"A Bauer","year":"2016","unstructured":"Bauer, A., Falcone, Y.: Decentralised LTL monitoring. Formal Methods Syst. Des. 48(1\u20132), 46\u201393 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0253-8","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"5_CR5","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/2000799.2000800","volume":"20","author":"A Bauer","year":"2011","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1\u201314:64 (2011). https:\/\/doi.org\/10.1145\/2000799.2000800","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Bharadwaj, S., Bloem, R., Dimitrova, R., K\u00f6nighofer, B., Topcu, U.: Synthesis of minimum-cost shields for distributed systems. In: 2019 Annual American Control Conference, ACC 2019. IEEE, Philadelphia, 10\u201312 July (2019)","DOI":"10.23919\/ACC.2019.8815233"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1007\/978-3-662-46681-0_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Bloem","year":"2015","unstructured":"Bloem, R., K\u00f6nighofer, B., K\u00f6nighofer, R., Wang, C.: Shield synthesis: In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 533\u2013548. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_51"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-33693-0_12","volume-title":"Integrated Formal Methods","author":"I Cassar","year":"2016","unstructured":"Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 176\u2013192. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33693-0_12"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6","volume-title":"Computer Aided Verification","year":"2016","unstructured":"Chaudhuri, S., Farzan, A. (eds.): CAV 2016. LNCS, vol. 9780. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6"},{"key":"5_CR10","unstructured":"FAA: Order JO 7400.9Y Air Traffic Organization Policy (2014). https:\/\/www.faa.gov\/documentLibrary\/media\/Order\/JO_7400.9Y.pdf"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-16612-9_9","volume-title":"Runtime Verification","author":"Y Falcone","year":"2010","unstructured":"Falcone, Y.: You should better enforce than verify. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 89\u2013105. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_9"},{"issue":"1","key":"5_CR12","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10270-013-0323-y","volume":"14","author":"Y Falcone","year":"2015","unstructured":"Falcone, Y., Jaber, M., Nguyen, T., Bozga, M., Bensalem, S.: Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation. Softw. Syst. Model. 14(1), 173\u2013199 (2015). https:\/\/doi.org\/10.1007\/s10270-013-0323-y","journal-title":"Softw. Syst. Model."},{"issue":"3","key":"5_CR13","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/s10703-014-0217-9","volume":"46","author":"A Francalanza","year":"2015","unstructured":"Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Methods Syst. Des. 46(3), 226\u2013261 (2015). https:\/\/doi.org\/10.1007\/s10703-014-0217-9","journal-title":"Formal Methods Syst. Des."},{"key":"5_CR14","unstructured":"Guestrin, C., Koller, D., Parr, R.: Multiagent planning with factored MDPS. In: Advances in Neural Information Processing Systems, pp. 1523\u20131530 (2002)"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1177\/027836498400300405","volume":"3","author":"JE Hopcroft","year":"1984","unstructured":"Hopcroft, J.E., Schwartz, J.T., Sharir, M.: On the complexity of motion planning for multiple independent objects; pspace- hardness of the \u201cwarehouseman\u2019s problem\u201d. Int. J. Robotic Res. IJRR 3, 76\u201388 (1984). https:\/\/doi.org\/10.1177\/027836498400300405","journal-title":"Int. J. Robotic Res. IJRR"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Jing, G., Ehlers, R., Kress-Gazit, H.: Shortcut through an evil door: optimality of correct-by-construction controllers in adversarial environments. In: 2013 IEEE\/RSJ International Conference on Intelligent Robots and Systems, Tokyo, Japan, pp. 4796\u20134802, 3\u20137 November 2013. https:\/\/doi.org\/10.1109\/IROS.2013.6697048","DOI":"10.1109\/IROS.2013.6697048"},{"issue":"2","key":"5_CR17","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10703-017-0276-9","volume":"51","author":"Bettina K\u00f6nighofer","year":"2017","unstructured":"K\u00f6nighofer, B., et al.: Shield synthesis. Formal Methods Syst. Des. 51(2), 332\u2013361 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0276-9","journal-title":"Formal Methods in System Design"},{"key":"5_CR18","unstructured":"Kottasov\u00e1, I.: Uber invests millions to build flying taxis in France. CNN Business, May 2018. https:\/\/www.cnn.com\/2018\/10\/01\/tech\/uber-flying-taxi-france\/index.html"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-36387-4_2","volume-title":"Automata Logics, and Infinite Games","author":"R Mazala","year":"2002","unstructured":"Mazala, R.: Infinite games. In: Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.) Automata Logics, and Infinite Games. LNCS, vol. 2500, pp. 23\u201338. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4_2"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Moore, A., et al.: Testing enabling technologies for safe UAS urban operations. In: Proceedings of the 2018 Aviation, Technology, Integration, and Operations Conference. No. AIAA-2018-3200, Atlanta, Georgia, June 2018","DOI":"10.2514\/6.2018-3200"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Narkawicz, A., Mu\u00f1oz, C., Dutle, A.: Sensor uncertainty mitigation and dynamic well clear volumes in DAIDALUS. In: Proceedings of the 37th Digital Avionics Systems Conference (DASC). London, England, UK, September 2018","DOI":"10.1109\/DASC.2018.8569468"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Neogi, N., Cuong, C., Dill, E.: A risk based assessment of a small UAS cargo delivery operation in proximity to urban areas. In: Proceedings of the 37th Digital Avionics Systems Conference (DASC). London, England, UK, September 2018","DOI":"10.1109\/DASC.2018.8569494"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Prevot, T., Rios, J., Kopardekar, P., Robinson, J.E., Johnson, M., Jung, J.: UAS Traffic Management (UTM) concept of operations to safely enable low altitude flight operations. In: Proceedings of the 2018 Aviation, Technology, Integration, and Operations Conference. No. AIAA-2016-3292, Washington, DC, June 2016","DOI":"10.2514\/6.2016-3292"},{"key":"5_CR24","unstructured":"Schewe, S.: Synthesis of distributed systems. Ph.D. thesis, Saarland University, Saarbr\u00fccken, Germany (2008)"},{"issue":"4","key":"5_CR25","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/j.ipl.2013.11.012","volume":"114","author":"S Schewe","year":"2014","unstructured":"Schewe, S.: Distributed synthesis is simply undecidable. Inf. Process. Lett. 114(4), 203\u2013207 (2014). https:\/\/doi.org\/10.1016\/j.ipl.2013.11.012 . http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0020019013002925","journal-title":"Inf. Process. Lett."},{"issue":"1","key":"5_CR26","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000). https:\/\/doi.org\/10.1145\/353323.353382","journal-title":"ACM Trans. Inf. Syst. Secur."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20652-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,26]],"date-time":"2019-11-26T09:46:54Z","timestamp":1574761614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20652-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030206512","9783030206529"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20652-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/robonaut.jsc.nasa.gov\/R2\/pages\/nfm2019.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}