{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:40:10Z","timestamp":1745988010543,"version":"3.40.4"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2013,4,11]],"date-time":"2013-04-11T00:00:00Z","timestamp":1365638400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,11]]},"DOI":"10.1007\/s10009-013-0273-2","type":"journal-article","created":{"date-parts":[[2013,4,10]],"date-time":"2013-04-10T14:47:39Z","timestamp":1365605259000},"page":"753-773","source":"Crossref","is-referenced-by-count":1,"title":["Model checking evaluation of airplane landing trajectories"],"prefix":"10.1007","volume":"16","author":[{"given":"Stefano","family":"Quer","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,4,11]]},"reference":[{"key":"273_CR1","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1080\/03081069708717585","volume":"20","author":"J Milan","year":"1997","unstructured":"Milan, J.: The flow management problem is air traffic control: a model of assigning priorities for landings at a congested airport. Transp. Plan. Technol. 20, 131\u2013162 (1997)","journal-title":"Transp. Plan. Technol."},{"issue":"3\/4","key":"273_CR2","first-page":"206","volume":"4","author":"V Ciesielski","year":"1997","unstructured":"Ciesielski, V., Scerri, P.: An anytime algorithm for scheduling of aircraft landing times using genetic algorithms. Aust. J. Intell. Inf. Process. Syst. 4(3\/4), 206\u2013213 (1997)","journal-title":"Aust. J. Intell. Inf. Process. Syst."},{"key":"273_CR3","doi-asserted-by":"crossref","unstructured":"Ciesielski, V., Scerri, P.: Real time genetic scheduling of aircraft landing times. In: Fogel, D. (ed.) IEEE International Conference on Evolutionary Computation (ICEC98), pp. 360\u2013364, NY, USA (1998)","DOI":"10.1109\/ICEC.1998.699759"},{"key":"273_CR4","unstructured":"Wong, G.L.: The dynamic planner: The Sequencer, Scheduler, and Runway Allocator for Air Traffic Control Automation. Technical report, NASA\/TM-2000-209586, NASA Ames Research Center, Moffett Field (2000)"},{"issue":"2","key":"273_CR5","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1287\/trsc.34.2.180.12302","volume":"34","author":"JE Beasley","year":"2000","unstructured":"Beasley, J.E., Krishnamoorthy, M., Sharaiha, Y.M., Abramson, D.: Scheduling aircraft landings\u2014the static case. Transp. Sci. 34(2), 180\u2013197 (2000)","journal-title":"Transp. Sci."},{"key":"273_CR6","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1057\/palgrave.jors.2601650","volume":"55","author":"JE Beasley","year":"2004","unstructured":"Beasley, J.E., Krishnamoorthy, M., Sharaiha, Y.M., Abramson, D.: Displacement problem and dynamically scheduling aircraft landings. J. Oper. Res. Soc. 55, 54\u201364 (2004)","journal-title":"J. Oper. Res. Soc."},{"key":"273_CR7","doi-asserted-by":"crossref","first-page":"1254","DOI":"10.1016\/j.ejor.2006.06.076","volume":"189","author":"K Artiouchine","year":"2008","unstructured":"Artiouchine, K., Baptiste, P., Durr, C.: Runway sequencing with holding patterns. Eur. J. Oper. Res. 189, 1254\u20131266 (2008)","journal-title":"Eur. J. Oper. Res."},{"issue":"2","key":"273_CR8","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1287\/ijoc.1070.0234","volume":"20","author":"K Artiouchine","year":"2008","unstructured":"Artiouchine, K., Baptiste, P., Mattioli, J.: The K king problem, an abstract model for computing aircraft landing trajectories: on modeling a dynamic hybrid system with constraints. INFORMS J. Comput. 20(2), 222\u2013233 (2008)","journal-title":"INFORMS J. Comput."},{"key":"273_CR9","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: Formal verification of curved flight collision avoidance maneuvers: a case study. In: FM: Formal Methods, Second World Congress, Eindhoven, The Netherlands. LNCS, vol. 5850, pp. 547\u2013562. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-05089-3_35"},{"key":"273_CR10","doi-asserted-by":"crossref","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Proc. Computer Aided Verification. LNCS, vol. 5123, pp. 176\u2013189. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_17"},{"issue":"6","key":"273_CR11","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1109\/87.960341","volume":"9","author":"RW Beard","year":"2001","unstructured":"Beard, R.W., Lawton, J., Hadaegh, F.Y.: A coordination architecture for spacecraft formation control. IEEE Trans. Control Syst. Technol. 9(6), 777\u2013790 (2001)","journal-title":"IEEE Trans. Control Syst. Technol."},{"key":"273_CR12","doi-asserted-by":"crossref","unstructured":"Scharf, D.P., Hadaegh, F.Y., Ploen, S.R.: A Survey of Spacecraft Formation Flying Guidance (2004)","DOI":"10.23919\/ACC.2004.1384365"},{"key":"273_CR13","doi-asserted-by":"crossref","first-page":"926","DOI":"10.1109\/70.736776","volume":"14","author":"T Balch","year":"1997","unstructured":"Balch, T., Arkin, R.C.: Behavior-based formation control for multi-robot teams. IEEE Trans. Robot. Autom. 14, 926\u2013939 (1997)","journal-title":"IEEE Trans. Robot. Autom."},{"key":"273_CR14","doi-asserted-by":"crossref","unstructured":"Chiesa, S., Quer, S., Corpino, S., Viola, N.: Heuristic and exact techniques for aircraft maintenance scheduling Proceedings of the Institution of Mechanical Engineers (IMechE), Part G. J. Aerosp. Eng. 223(G7), 989\u2013999 (2009)","DOI":"10.1243\/09544100JAERO463"},{"issue":"12","key":"273_CR15","doi-asserted-by":"crossref","first-page":"1465","DOI":"10.1109\/43.552080","volume":"15","author":"H Cho","year":"1996","unstructured":"Cho, H., Hatchel, G.D., Macii, E., Plessier, B., Somenzi, F.: Algorithms for approximate FSM traversal based on state space decomposition. IEEE Trans. Computer-Aided Design 15(12), 1465\u20131478 (1996)","journal-title":"IEEE Trans. Computer-Aided Design"},{"key":"273_CR16","volume-title":"Synthesis and Optimization of Digital Circuits","author":"GD Micheli","year":"1994","unstructured":"Micheli, G.D.: Synthesis and Optimization of Digital Circuits. McGraw Hill, Hightstown (1994)"},{"key":"273_CR17","unstructured":"Walsh, T.: SAT v CSP. In: Dechter, R. (ed.) CP. Lecture Notes in Computer Science, vol. 1894, pp. 441\u2013456. Springer, Berlin (2000)."},{"key":"273_CR18","unstructured":"Guyot, B., Janik, J.M.: Simplified method of binary\/thermometric encoding with an improved resolution, U. S. Patent No. 649676 (2002)"},{"key":"273_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking. PhD thesis, Boston, Massachussetts (1992)","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"273_CR20","first-page":"28","volume":"2056","author":"J Mullin","year":"1996","unstructured":"Mullin, J.: Trails of destruction. New Scientist 2056, 28\u201331 (1996)","journal-title":"New Scientist"},{"key":"273_CR21","doi-asserted-by":"crossref","unstructured":"Bayen, A.M., Tomlin, C.J.: Real-time discrete control law synthesis for hybrid systems using MILP: Application to congested airspace. In: American Control Conference (2003)","DOI":"10.1109\/ACC.2003.1242452"},{"key":"273_CR22","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Aziz, A., Kuehlmann, A.: Enhancing simulation with BDDs and ATPG. In: Proc. 36th Design Automation Conf., New Orleans, LA, IEEE Computer Society, pp. 385\u2013390 (1999)","DOI":"10.1145\/309847.309965"},{"key":"273_CR23","doi-asserted-by":"crossref","unstructured":"Yang, C.H., Dill, D.L.: Validation with guided search of state space. In: Proc. 35th Design Automation Conf., San Francisco, California, IEEE Computer Society (1998)","DOI":"10.1145\/277044.277201"},{"issue":"4","key":"273_CR24","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"JR Burch","year":"1994","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.L.: Symbolic model checking for sequential circuit verification. IEEE Trans. Computer-Aided Design 13(4), 401\u2013424 (1994)","journal-title":"IEEE Trans. Computer-Aided Design"},{"key":"273_CR25","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package\u2013Release 2.4.1 (2005). http:\/\/vlsi.colorado.edu\/fabio\/CUDD\/"},{"key":"273_CR26","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: TACAS \u201999: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, pp. 193\u2013207. Springer, London (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"273_CR27","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36th Design Automation Conf., New Orleans, Louisiana, IEEE Computer Society, pp. 317\u2013320 (1999)","DOI":"10.1145\/309847.309942"},{"key":"273_CR28","doi-asserted-by":"crossref","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) Proc. Computer Aided Verification. LNCS, vol. 2102, pp. 435\u2013453. Springer, Paris (2001)","DOI":"10.1007\/3-540-44585-4_43"},{"key":"273_CR29","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based Model Checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) Proc. Computer Aided Verification. LNCS, vol. 2725, pp. 1\u201313. Springer, Boulder (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"273_CR30","unstructured":"Bradley, A.: ic3: SAT-Based Model Checking Without Unrolling (2010). http:\/\/ecee.colorado.edu\/bradleya\/ic3\/"},{"key":"273_CR31","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a reimplementation of SMV. In: Proc. International Workshop on Software Tools for Technology Transfer (STTT\u201998), BRICS Notes Series, NS-98-4. pp. 25\u201331 (1998)"},{"key":"273_CR32","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: A new Symbolic Model Verifier. In: Proc. Computer Aided Verification. LNCS, vol. 1633, pp. 495\u2013499. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"key":"273_CR33","unstructured":"Cabodi, G., Nocco, S., Quer, S.: Formal Method Group\u2019s Home Page. http:\/\/fmgroup.polito.it\/"},{"key":"273_CR34","doi-asserted-by":"crossref","unstructured":"Brayton, R., Mishchenko, A.: Abc: An academic industrial-strength verification tool. In: Proc. Computer Aided Verification. LNCS, vol. 6174, pp. 24\u201340. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_5"},{"key":"273_CR35","unstructured":"Mishchenko, A.: ABC: A System for Sequential Synthesis and Verification (2005). http:\/\/www.eecs.berkeley.edu\/alanmi\/abc\/"},{"key":"273_CR36","volume-title":"Introduction to algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to algorithms, 3rd edn. MIT Press, Cambridge (2009)","edition":"3"}],"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-013-0273-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0273-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0273-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:00:46Z","timestamp":1745985646000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0273-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,4,11]]},"references-count":36,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2014,11]]}},"alternative-id":["273"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0273-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2013,4,11]]}}}