{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:57:06Z","timestamp":1750309026362,"version":"3.41.0"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,6,1]],"date-time":"2017-06-01T00:00:00Z","timestamp":1496275200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,1]]},"DOI":"10.1007\/s10817-017-9416-6","type":"journal-article","created":{"date-parts":[[2017,6,1]],"date-time":"2017-06-01T04:14:00Z","timestamp":1496290440000},"page":"85-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA)"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7652-559X","authenticated-orcid":false,"given":"Muhammad Usama","family":"Sardar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nida","family":"Afaq","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Khaza Anuarul","family":"Hoque","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,6,1]]},"reference":[{"issue":"1","key":"9416_CR1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Form. Methods Syst. Des."},{"doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, Y., Zuck, L.: Parameterized verification with automatically computed inductive assertions? In: Computer Aided Verification, vol. 2102, pp. 221\u2013234. Springer (2001)","key":"9416_CR2","DOI":"10.1007\/3-540-44585-4_19"},{"doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time markov chains. In: Computer Aided Verification, vol. 1102, pp. 269\u2013276. Springer (1996)","key":"9416_CR3","DOI":"10.1007\/3-540-61474-5_75"},{"doi-asserted-by":"crossref","unstructured":"Bai, C., Zhang, X.: Aircraft landing scheduling in the small aircraft transportation system. In: Computational and Information Sciences, pp. 1019\u20131022. IEEE (2011)","key":"9416_CR4","DOI":"10.1109\/ICCIS.2011.65"},{"unstructured":"Baier, C.: On algorithmic verification methods for probabilistic systems. Technical Report, Universit\u00e4t Mannheim (1998)","key":"9416_CR5"},{"key":"9416_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"doi-asserted-by":"crossref","unstructured":"Baier, C., Katoen, J.P., Hermanns, H.: Approximative symbolic model checking of continuous-time markov chains. In: Concurrency Theory, vol. 1664, pp. 146\u2013161. Springer (1999)","key":"9416_CR7","DOI":"10.1007\/3-540-48320-9_12"},{"doi-asserted-by":"crossref","unstructured":"Balakrishnan, H., Chandran, B.: Scheduling aircraft landings under constrained position shifting. In: Guidance, Navigation, and Control Conference and Exhibit. American Institute of Aeronautics and Astronautics (2006)","key":"9416_CR8","DOI":"10.2514\/6.2006-6320"},{"issue":"4","key":"9416_CR9","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/j.cose.2011.02.001","volume":"30","author":"S Basagiannis","year":"2011","unstructured":"Basagiannis, S., Petridou, S., Alexiou, N., Papadimitriou, G., Katsaros, P.: Quantitative analysis of a certified e-mail protocol in mobile environments: a probabilistic model checking approach. Comput. Secur. 30(4), 257\u2013272 (2011)","journal-title":"Comput. Secur."},{"doi-asserted-by":"crossref","unstructured":"Baxley, B., Williams, D., Consiglio, M., Conway, S., Adams, C., Abbott, T.: The small aircraft transportation system, higher volume operations off-nominal operations. In: Aviation, Technology, Integration, and Operations Conference. American Institute of Aeronautics and Astronautics (2005)","key":"9416_CR10","DOI":"10.2514\/6.2005-7461"},{"issue":"6","key":"9416_CR11","doi-asserted-by":"crossref","first-page":"1825","DOI":"10.2514\/1.20493","volume":"45","author":"B Baxley","year":"2008","unstructured":"Baxley, B., Williams, D., Consiglio, M., Adams, C., Abbott, T.: Small aircraft transportation system, higher volume operations concept and research summary. J Aircr 45(6), 1825\u20131834 (2008)","journal-title":"J Aircr"},{"issue":"1","key":"9416_CR12","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S0304-3975(01)00215-8","volume":"292","author":"D Beauquier","year":"2003","unstructured":"Beauquier, D.: On probabilistic timed automata. Theor. Comput. Sci. 292(1), 65\u201384 (2003)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Carre\u00f1o, V.: Concept for multiple operations at non-tower non-radar airports during instrument meteorological conditions. In: Digital Avionics Systems Conference, pp. 5.B.1\u20131\u20135.B.1\u20139. IEEE (2003)","key":"9416_CR13","DOI":"10.1109\/DASC.2003.1245855"},{"doi-asserted-by":"crossref","unstructured":"Carre\u00f1o, V., Mu\u00f1oz, C.: Safety verification of the small aircraft transportation system concept of operations. In: Aviation, Technology, Integration, and Operations Conference. American Institute of Aeronautics and Astronautics (2005)","key":"9416_CR14","DOI":"10.2514\/6.2005-7423"},{"doi-asserted-by":"crossref","unstructured":"Cheng, A., Niktab, H., Walston, M.: Timing analysis of small aircraft transportation system (SATS). In: Embedded and Real-Time Computing Systems and Applications, pp. 58\u201367. IEEE (2012)","key":"9416_CR15","DOI":"10.1109\/RTCSA.2012.46"},{"key":"9416_CR16","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"doi-asserted-by":"crossref","unstructured":"Consiglio, M., Conway, S., Adams, C., Syed, H.: SATS HVO procedures for priority landings and mixed VFR\/IFR operations. In: Digital Avionics Systems Conference, pp. 13.B.2\u20131\u201313.B.2\u20138. IEEE (2005)","key":"9416_CR17","DOI":"10.1109\/DASC.2005.1563428"},{"issue":"2","key":"9416_CR18","doi-asserted-by":"crossref","first-page":"353","DOI":"10.2514\/1.20586","volume":"45","author":"M Consiglio","year":"2008","unstructured":"Consiglio, M., Carreno, V.A., Williams, D.M., Mu\u00f1oz, C.: Conflict prevention and separation assurance in small aircraft transportation systems. J. Aircr. 45(2), 353\u2013358 (2008)","journal-title":"J. Aircr."},{"unstructured":"Consiglio, M., Sturdy, J.: Monte carlo analysis of airport throughput and traffic delays using self separation procedures. In: International Council of the Aeronautical Sciences (2006)","key":"9416_CR19"},{"key":"9416_CR20","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139236119","volume-title":"Temporal Logics in Computer Science: Finite-State Systems","author":"S Demri","year":"2016","unstructured":"Demri, S., Goranko, V., Lange, M.: Temporal Logics in Computer Science: Finite-State Systems. Cambridge University Press, Cambridge (2016)"},{"unstructured":"Dou, L., David, L., Jesse, J., Peter, K.: A small aircraft transportation system (SATS) demand model. Technical Reports NASA\/CR-2001-210874, NASA Technical Reports Server (2001)","key":"9416_CR21"},{"unstructured":"Dowek, G., Mu\u00f1oz, C., Carre\u00f1o, V.: Abstract model of the SATS concept of operations: initial results and recommendations. Technical Reports NASA\/TM-2004-213006, NASA Technical Reports Server (2004)","key":"9416_CR22"},{"issue":"4","key":"9416_CR23","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1109\/TC.2007.1012","volume":"56","author":"A Fedeli","year":"2007","unstructured":"Fedeli, A., Fummi, F., Pravadelli, G.: Properties incompleteness evaluation by functional verification. IEEE Trans Comput 56(4), 528\u2013544 (2007)","journal-title":"IEEE Trans Comput"},{"unstructured":"Gariel, M., Spieser, K., Frazzoli, E.: On the statistics and predictability of go-arounds. In: Intelligent Data Understanding, pp. 75\u201391 (2011)","key":"9416_CR24"},{"doi-asserted-by":"crossref","unstructured":"Greco, A., Magyarits, S., Doucett, S.: Air traffic control studies of small aircraft transportation system operations. In: Digital Avionics Systems Conference. pp. 13.A.4\u20131\u201313.A.4\u201312. IEEE (2005)","key":"9416_CR25","DOI":"10.1109\/DASC.2005.1563425"},{"unstructured":"Green\u00a0Jr, D.F., Jones, D.R.: Runway safety monitor algorithm for runway incursion detection and alerting. Technical Reports NASA\/CR-2002-211416, NASA Technical Reports Server (2002)","key":"9416_CR26"},{"doi-asserted-by":"crossref","unstructured":"G\u00fcdemann, M., Ortmeier, F.: A framework for qualitative and quantitative formal model-based safety analysis. In: High-Assurance Systems Engineering, pp. 132\u2013141. IEEE (2010)","key":"9416_CR27","DOI":"10.1109\/HASE.2010.24"},{"issue":"5","key":"9416_CR28","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Form. Asp. Comput."},{"issue":"3","key":"9416_CR29","doi-asserted-by":"crossref","first-page":"664","DOI":"10.1109\/25.933303","volume":"50","author":"G Harine","year":"2001","unstructured":"Harine, G., Marie, R., Puigjaner, R., Trivedi, K.: Loss formulas and their application to optimization for cellular networks. IEEE Trans. Veh. Technol. 50(3), 664\u2013673 (2001)","journal-title":"IEEE Trans. Veh. Technol."},{"issue":"1","key":"9416_CR30","doi-asserted-by":"crossref","first-page":"26","DOI":"10.2514\/1.3257","volume":"41","author":"BJ Holmes","year":"2004","unstructured":"Holmes, B.J., Durham, M.H., Tarry, S.E.: Small aircraft transportation system concept and technologies. J. Aircr. 41(1), 26\u201335 (2004)","journal-title":"J. Aircr."},{"unstructured":"Johnson, C.: Final Report: Review of the BFU \u00dcberlingen accident report. Contract C\/1.369\/HQ\/SS\/04. Eurocontrol (2004)","key":"9416_CR31"},{"doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: Parameterized verification of distributed cyber-physical systems: an aircraft landing protocol case study. In: Cyber-Physical Systems, pp. 161\u2013170. IEEE (2012)","key":"9416_CR32","DOI":"10.1109\/ICCPS.2012.24"},{"doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: A small model theorem for rectangular hybrid automata networks. In: Formal Techniques for Distributed Systems, vol. 7273, pp. 18\u201334. Springer (2012)","key":"9416_CR33","DOI":"10.1007\/978-3-642-30793-5_2"},{"doi-asserted-by":"crossref","unstructured":"Johnson, T.T., Mitra, S.: Invariant synthesis for verification of parameterized cyber-physical systems with applications to aerospace systems. In: Infotech at Aerospace Conference. American Institute of Aeronautics and Astronautics (2013)","key":"9416_CR34","DOI":"10.2514\/6.2013-4811"},{"doi-asserted-by":"crossref","unstructured":"Kelly, W.E., Valasek, J., Wilt, D., Deaton, J., Alter, K., Davis, R.: The design and evaluation of a traffic situation display for a SATS self controlled area. In: Digital Avionics Systems Conference, pp. 13.A.3\u20131\u201313.A.3\u201312. IEEE (2005)","key":"9416_CR35","DOI":"10.1109\/DASC.2005.1563424"},{"doi-asserted-by":"crossref","unstructured":"Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Taylor & Francis Group, CRC Press (2016)","key":"9416_CR36","DOI":"10.1201\/9781315367910"},{"issue":"11","key":"9416_CR37","doi-asserted-by":"crossref","first-page":"1427","DOI":"10.1016\/j.conengprac.2006.07.003","volume":"15","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Controller dependability analysis by probabilistic model checking. Control Eng. Pract. 15(11), 1427\u20131434 (2007)","journal-title":"Control Eng. Pract."},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Formal Methods for Performance Evaluation, vol. 4486, pp. 220\u2013270. Springer (2007)","key":"9416_CR38","DOI":"10.1007\/978-3-540-72522-0_6"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Computer Aided Verification, vol. 6806, pp. 585\u2013591. Springer (2011)","key":"9416_CR39","DOI":"10.1007\/978-3-642-22110-1_47"},{"unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic Symbolic Model Checker. http:\/\/www.prismmodelchecker.org (2016)","key":"9416_CR40"},{"issue":"72","key":"9416_CR41","doi-asserted-by":"crossref","first-page":"1470","DOI":"10.1098\/rsif.2011.0800","volume":"9","author":"MR Lakin","year":"2012","unstructured":"Lakin, M.R., Parker, D., Cardelli, L., Kwiatkowska, M., Phillips, A.: Design and analysis of DNA strand displacement devices using probabilistic model checking. J. R. Soc. Interface 9(72), 1470\u20131485 (2012)","journal-title":"J. R. Soc. Interface"},{"key":"9416_CR42","series-title":"Prentice Hall Modern Semiconductor Design Series","volume-title":"Hardware Design Verification: Simulation and Formal Method-Based Approaches","author":"WK Lam","year":"2005","unstructured":"Lam, W.K.: Hardware Design Verification: Simulation and Formal Method-Based Approaches. Prentice Hall Modern Semiconductor Design Series. Prentice Hall, Upper Saddle River (2005)"},{"issue":"9","key":"9416_CR43","first-page":"1569","volume":"230","author":"CE Lin","year":"2016","unstructured":"Lin, C.E., Hung, T.W., Chen, H.Y.: TCAS algorithm for general aviation based on ADS-B. J. Aerosp. Eng. 230(9), 1569\u20131591 (2016)","journal-title":"J. Aerosp. Eng."},{"issue":"4","key":"9416_CR44","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/1013886.1007536","volume":"29","author":"C Mu\u00f1oz","year":"2004","unstructured":"Mu\u00f1oz, C., Dowek, G., Carre\u00f1o, V.: Modeling and verification of an air traffic concept of operations. Softw. Eng. Notes 29(4), 175\u2013182 (2004)","journal-title":"Softw. Eng. Notes"},{"doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C., Carre\u00f1o, V., Dowek, G.: Formal analysis of the operational concept for the small aircraft transportation system. In: Rigorous Development of Complex Fault-Tolerant Systems, vol. 4157, pp. 306\u2013325. Springer (2006)","key":"9416_CR45","DOI":"10.1007\/11916246_16"},{"unstructured":"Mu\u00f1oz, C., Dowek, G.: Hybrid verification of an air traffic operational concept. In: Leveraging Applications of Formal Methods, Verification, and Validation, pp. 1\u201313. IEEE\/NASA (2005)","key":"9416_CR46"},{"doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Automated Deduction, vol. 607, pp. 748\u2013752. Springer (1992)","key":"9416_CR47","DOI":"10.1007\/3-540-55602-8_217"},{"doi-asserted-by":"crossref","unstructured":"Peters, M.: Capacity analysis of the NASA Langley airport management module. In: Digital Avionics Systems Conference, pp. 4.D.6\u20131\u20134.D.6\u201312. IEEE (2005)","key":"9416_CR48","DOI":"10.1109\/DASC.2005.1563367"},{"key":"9416_CR49","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M Puterman","year":"2014","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Hoboken (2014)"},{"doi-asserted-by":"crossref","unstructured":"Sardar, M.U.: Towards probabilistic formal analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA). (2016) http:\/\/save.seecs.nust.edu.pk\/projects\/SATS-SMA","key":"9416_CR50","DOI":"10.1007\/s10817-017-9416-6"},{"doi-asserted-by":"crossref","unstructured":"Sardar, M.U., Afaq, N., Hoque, K.A., Johnson, T.T., Hasan, O.: Probabilistic formal verification of the SATS concept of operation. In: NASA Formal Methods, vol. 9690, pp. 191\u2013205. Springer (2016)","key":"9416_CR51","DOI":"10.1007\/978-3-319-40648-0_15"},{"issue":"2","key":"9416_CR52","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250\u2013273 (1995)","journal-title":"Nord. J. Comput."},{"unstructured":"Shortle, J.F., Xie, R., Chen, C., Donohue, G.L.: Estimating collision probabilities of landing airplanes at non-towered aiports. In: Transportation Research Board (2003)","key":"9416_CR53"},{"issue":"1","key":"9416_CR54","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10009-006-0004-z","volume":"9","author":"RI Siminiceanu","year":"2007","unstructured":"Siminiceanu, R.I., Ciardo, G.: Formal verification of the nasa runway safety monitor. Int. J. Softw. Tools Technol. Transf. 9(1), 63\u201376 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"crossref","unstructured":"Umeno, S., Lynch, N.: Proving safety properties of an aircraft landing protocol using I\/O automata and the PVS theorem prover: a case study. In: Formal Methods, vol. 4085, pp. 64\u201380. Springer (2006)","key":"9416_CR55","DOI":"10.1007\/11813040_5"},{"doi-asserted-by":"crossref","unstructured":"Viken, S.A., Brooks, F.M.: Demonstration of four operating capabilities to enable a small aircraft transportation system. In: Digital Avionics Systems Conference, pp. 13.A.1\u20131\u201313.A.1\u201316. IEEE (2005)","key":"9416_CR56","DOI":"10.1109\/DASC.2005.1563422"},{"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, vol. 8413, pp. 620\u2013635. Springer (2014)","key":"9416_CR57","DOI":"10.1007\/978-3-642-54862-8_54"},{"doi-asserted-by":"crossref","unstructured":"Williams, D.M., Consiglio, M., Murdoch, J., Adams, C.: Flight technical error analysis of the SATS higher volume operations simulation and flight experiments. In: Digital Avionics Systems Conference, pp. 13.B.1\u20131\u201313.B.1\u201312. IEEE (2005)","key":"9416_CR58","DOI":"10.1109\/DASC.2005.1563427"},{"unstructured":"Williams, D.M.: Point-to-Point! validation of the small aircraft transportation system higher volume operations concept. In: International Council of the Aeronautical Sciences (2006)","key":"9416_CR59"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9416-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9416-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9416-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:12:57Z","timestamp":1750284777000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9416-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,1]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["9416"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9416-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,6,1]]}}}