{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T17:21:38Z","timestamp":1767374498844},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,7,17]],"date-time":"2015-07-17T00:00:00Z","timestamp":1437091200000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s10009-015-0388-8","type":"journal-article","created":{"date-parts":[[2015,7,16]],"date-time":"2015-07-16T09:19:28Z","timestamp":1437038368000},"page":"227-243","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Probabilistic verification and synthesis of the next generation airborne collision avoidance system"],"prefix":"10.1007","volume":"18","author":[{"given":"Christian","family":"von Essen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dimitra","family":"Giannakopoulou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,17]]},"reference":[{"key":"388_CR1","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: STACS 2006, 23rd Annual Symposium on Theoretical Aspects of Computer Science, Marseille, France, February 23\u201325, 2006, pp. 325\u2013336 (2006)","DOI":"10.1007\/11672142_26"},{"key":"388_CR2","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) Proc. 10th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201912), volume 7561 of LNCS, pp. 317\u2013332. Springer (2012)","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"388_CR3","doi-asserted-by":"crossref","unstructured":"Galdino, A.L., Mu\u00f1oz, C., Ayala-Rinc\u00f3n, M.: Formal verification of an optimal air traffic conflict resolution and recovery algorithm. In: Logic, Language, Information and Computation, 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2\u20135, 2007, pp. 177\u2013188 (2007)","DOI":"10.1007\/978-3-540-73445-1_13"},{"issue":"10","key":"388_CR4","doi-asserted-by":"crossref","first-page":"702","DOI":"10.2514\/1.I010178","volume":"11","author":"K Ghorbal","year":"2014","unstructured":"Ghorbal, K., Jeannin, J., Zawadzki, E., Platzer, A., Gordon, G.J., Capell, P.: Hybrid theorem proving of aerospace systems: Applications and challenges. J. Aerospace Inf. Sys. 11(10), 702\u2013713 (2014)","journal-title":"J. Aerospace Inf. Sys."},{"key":"388_CR5","first-page":"102","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comp. 6, 102\u2013111 (1994)","journal-title":"Formal Aspects Comp."},{"key":"388_CR6","doi-asserted-by":"crossref","unstructured":"Jeannin, J., Ghorbal, K., Kouskoulas, Y., Gardner, R., Schmidt, A., Zawadzki, E., Platzer, A.: A formally verified hybrid system for the next-generation airborne collision avoidance system. In: Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11\u201318, 2015, pp. 21\u201336 (2015)","DOI":"10.1007\/978-3-662-46681-0_2"},{"issue":"3","key":"388_CR7","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/JPROC.2003.823141","volume":"92","author":"SJ Julier","year":"2004","unstructured":"Julier, S.J., Uhlmann, J.K.: Unscented filtering and nonlinear estimation. Proc. IEEE 92(3), 401\u2013422 (2004)","journal-title":"Proc. IEEE"},{"issue":"2","key":"388_CR8","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J Katoen","year":"2011","unstructured":"Katoen, J., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"388_CR9","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/10187.001.0001","volume-title":"Decision making under uncertainty: theory and application","author":"MJ Kochenderfer","year":"2015","unstructured":"Kochenderfer, M.J.: Decision making under uncertainty: theory and application. MIT Press, Cambridge (2015). Please cehck and confirm the publisher location is correct and amend if necessary"},{"key":"388_CR10","unstructured":"Kochenderfer, M.J., Chryssanthacopoulos, J.P.: Robust airborne collision avoidance through dynamic programming. Project Report ATC-371, Massachusetts Institute of Technology, Lincoln Laboratory (2011)"},{"issue":"2","key":"388_CR11","first-page":"277","volume":"16","author":"J Kuchar","year":"2007","unstructured":"Kuchar, J., Drumm, A.C.: The traffic alert and collision avoidance system. Lincoln Lab. J. 16(2), 277 (2007)","journal-title":"Lincoln Lab. J."},{"key":"388_CR12","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker. D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14\u201320, 2011, pp. 585\u2013591 (2011)"},{"key":"388_CR13","doi-asserted-by":"crossref","unstructured":"Loos, S.M., Renshaw, D.W., Platzer, A.: Formal verification of distributed aircraft controllers. In: Proceedings of the 16th international conference on Hybrid systems: computation and control, HSCC 2013, April 8\u201311, 2013, Philadelphia, PA, USA, pp. 125\u2013130 (2013)","DOI":"10.1145\/2461328.2461350"},{"key":"388_CR14","doi-asserted-by":"crossref","unstructured":"Lygeros, J., Lynch, N.: On the formal verification of the TCAS conflict resolution algorithms. In: 36th IEEE Conference on Decision and Control, pp. 1829\u20131834 (1997)","DOI":"10.1109\/CDC.1997.657846"},{"key":"388_CR15","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke E.M.: Formal verification of curved flight collision avoidance maneuvers: A case study. In: FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2\u20136, 2009, pp. 547\u2013562 (2009)","DOI":"10.1007\/978-3-642-05089-3_35"},{"issue":"4","key":"388_CR16","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1287\/ijoc.1100.0419","volume":"23","author":"G Rennen","year":"2011","unstructured":"Rennen, G., van Dam, E.R., den Hertog, D.: Enhancement of sandwich algorithms for approximating higher-dimensional convex Pareto sets. INFORMS J. Comp. 23(4), 493\u2013517 (2011)","journal-title":"INFORMS J. Comp."},{"issue":"4","key":"388_CR17","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 multiagent hybrid systems. IEEE Trans. Auto. Cont. 43(4), 509\u2013521 (1998)","journal-title":"IEEE Trans. Auto. Cont."},{"key":"388_CR18","unstructured":"von Essen C.: Quantitative Verification and Synthesis. PhD Thesis, Universit\u00e9 Joseph Fourier, Grenoble, France (2014)"},{"key":"388_CR19","doi-asserted-by":"crossref","unstructured":"von Essen, C., Giannakopoulou, D.: Analyzing the next generation airborne collision avoidance system. In: Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5\u201313, 2014, pp. 620\u2013635 (2014)","DOI":"10.1007\/978-3-642-54862-8_54"},{"issue":"2","key":"388_CR20","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/s10703-013-0195-3","volume":"43","author":"P Zuliani","year":"2013","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow\/Simulink verification. Formal Methods Syst. Design 43(2), 338\u2013367 (2013)","journal-title":"Formal Methods Syst. Design"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0388-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0388-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0388-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,28]],"date-time":"2019-08-28T08:50:50Z","timestamp":1566982250000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0388-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,7,17]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["388"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0388-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,7,17]]}}}