{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T15:55:59Z","timestamp":1762271759194,"version":"build-2065373602"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,10,26]],"date-time":"2013-10-26T00:00:00Z","timestamp":1382745600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,4]]},"DOI":"10.1007\/s10703-013-0197-1","type":"journal-article","created":{"date-parts":[[2013,10,25]],"date-time":"2013-10-25T13:49:11Z","timestamp":1382708951000},"page":"176-202","source":"Crossref","is-referenced-by-count":8,"title":["Model checking approach to automated planning"],"prefix":"10.1007","volume":"44","author":[{"given":"Yi","family":"Li","sequence":"first","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Jing","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,10,26]]},"reference":[{"key":"197_CR1","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/S0004-3702(99)00071-5","volume":"16","author":"F Bacchus","year":"2000","unstructured":"Bacchus F, Kabanza F, Sherbrooke UD (2000) Using temporal logics to express search control knowledge for planning. Artif Intell 16:123\u2013191","journal-title":"Artif Intell"},{"key":"197_CR2","unstructured":"Berardi D, Giacomo GD (2000) Planning via model checking: some experimental results. Unpublished manuscript"},{"key":"197_CR3","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant RE (1992) Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24:293\u2013318","journal-title":"ACM Comput Surv"},{"key":"197_CR4","unstructured":"Cavada R, Cimatti A, Jochim CA, Keighren G, Olivetti E, Pistore M, Roveri M, Tchaltsev A (2005) NuSMV 2.5 User Manual. CMU and ITC-irst"},{"key":"197_CR5","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/3-540-63912-8_81","volume-title":"Recent advances in AI planning","author":"A Cimatti","year":"1997","unstructured":"Cimatti A, Giunchiglia E, Giunchiglia F, Traverso P (1997) Planning via model checking: a decision procedure for $\\mathcal{AR}$ . In: Recent advances in AI planning, pp 130\u2013142"},{"key":"197_CR6","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1613\/jair.544","volume":"9","author":"M Fox","year":"1998","unstructured":"Fox M, Long D (1998) The automatic inference of state invariants in TIM. J\u00a0Artif Intell Res 9:367\u2013421","journal-title":"J\u00a0Artif Intell Res"},{"key":"197_CR7","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1613\/jair.1129","volume":"20","author":"M Fox","year":"2003","unstructured":"Fox M, Long D (2003) PDDL2.1: an extension to PDDL for expressing temporal planning domains. J\u00a0Artif Intell Res 20:61\u2013124","journal-title":"J\u00a0Artif Intell Res"},{"key":"197_CR8","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/10720246_1","volume-title":"Recent advances in AI planning","author":"F Giunchiglia","year":"2000","unstructured":"Giunchiglia F, Traverso P (2000) Planning as model checking. In: Biundo S, Fox M (eds) Recent advances in AI planning. Lecture notes in computer science, vol 1809. Springer, Berlin, pp 1\u201320"},{"key":"197_CR9","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-73580-9_17","volume-title":"Proceedings of the 7th international conference on abstraction, reformulation, and approximation, SARA\u201907","author":"P Gregory","year":"2007","unstructured":"Gregory P, Long D, Fox M (2007) A meta-CSP model for optimal planning. In: Proceedings of the 7th international conference on abstraction, reformulation, and approximation, SARA\u201907. Springer, Berlin, pp 200\u2013214. http:\/\/portal.acm.org\/citation.cfm?id=1770681.1770700"},{"issue":"8","key":"197_CR10","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare CAR (1978) Communicating sequential processes. Commun ACM 21(8):666\u2013677","journal-title":"Commun ACM"},{"key":"197_CR11","first-page":"571","volume-title":"Proceedings of the 15th European conference on artificial intelligence (ECAI-02)","author":"J Hoffmann","year":"2002","unstructured":"Hoffmann J (2002) Extending FF to numerical state variables. In: Proceedings of the 15th European conference on artificial intelligence (ECAI-02). Wiley, Lyon, pp 571\u2013575"},{"key":"197_CR12","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1613\/jair.855","volume":"14","author":"J Hoffmann","year":"2001","unstructured":"Hoffmann J, Nebel B (2001) The FF planning system: fast plan generation through heuristic search. J\u00a0Artif Intell Res 14:253\u2013302","journal-title":"J\u00a0Artif Intell Res"},{"key":"197_CR13","volume-title":"The SPIN model checker: primer and reference manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann GJ (2003) The SPIN model checker: primer and reference manual. Addison-Wesley, Reading"},{"key":"197_CR14","first-page":"114","volume-title":"Proceedings of the 2008 annual research conference of the South African Institute of Computer Scientists and Information Technologists on IT research in developing countries: riding the wave of technology, SAICSIT \u201908","author":"T H\u00f6rne","year":"2008","unstructured":"H\u00f6rne T, van der Poll JA (2008) Planning as model checking: the performance of ProB vs NuSMV. In: Proceedings of the 2008 annual research conference of the South African Institute of Computer Scientists and Information Technologists on IT research in developing countries: riding the wave of technology, SAICSIT \u201908. ACM, New York, pp 114\u2013123"},{"key":"197_CR15","volume-title":"Abstracts of the 5th international planning competition","author":"HA Kautz","year":"2006","unstructured":"Kautz HA, Selman B, Hoffmann J (2006) SatPlan: planning as satisfiability. In: Abstracts of the 5th international planning competition"},{"key":"197_CR16","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-63912-8_92","volume-title":"Proceedings of the 4th European conference on planning: recent advances in AI planning, ECP \u201997","author":"J Koehler","year":"1997","unstructured":"Koehler J, Nebel B, Hoffmann J, Dimopoulos Y (1997) Extending planning graphs to an ADL subset. In: Proceedings of the 4th European conference on planning: recent advances in AI planning, ECP \u201997. Springer, London, pp 273\u2013285. http:\/\/dl.acm.org\/citation.cfm?id=647867.736939"},{"key":"197_CR17","series-title":"Lecture notes in computer science","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: formal methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel M, Butler M (2003) ProB: a model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: formal methods. Lecture notes in computer science, vol 2805. Springer, Berlin, pp 855\u2013874"},{"key":"197_CR18","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/978-3-642-24372-1_35","volume-title":"Automated technology for verification and analysis","author":"S-W Lin","year":"2011","unstructured":"Lin S-W, Andr\u00e9 \u00c9, Dong J-S, Sun J, Liu Y (2011) An efficient algorithm for learning event-recording automata. In: Bultan T, Hsiung P-A (eds) Automated technology for verification and analysis. LNCS, vol\u00a06996. Springer, Berlin, pp 463\u2013472"},{"key":"197_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/978-3-642-32759-9_24","volume-title":"FM 2012: formal methods","author":"S-W Lin","year":"2012","unstructured":"Lin S-W, Liu Y, Sun J, Dong JS, Andr\u00e9 \u00c9 (2012) Automatic compositional verification of timed systems. In: Giannakopoulou D, M\u00e9ry D (eds) FM 2012: formal methods. LNCS, vol 7436. Springer, Berlin, pp 272\u2013276"},{"key":"197_CR20","doi-asserted-by":"crossref","first-page":"919","DOI":"10.1145\/1370175.1370187","volume-title":"Companion of the 30th international conference on software engineering, ICSE Companion \u201908","author":"Y Liu","year":"2008","unstructured":"Liu Y, Sun J, Dong JS (2008) An analyzer for extended compositional process algebras. In: Companion of the 30th international conference on software engineering, ICSE Companion \u201908. ACM, New York, pp 919\u2013920"},{"key":"197_CR21","first-page":"511","volume-title":"Proceedings of the ACM SIGSOFT international symposium on the foundations of software engineering (FSE 2010)","author":"Y Liu","year":"2010","unstructured":"Liu Y, Sun J, Dong JS (2010) Analyzing hierarchical complex real-time systems. In: Proceedings of the ACM SIGSOFT international symposium on the foundations of software engineering (FSE 2010), pp 511\u2013527"},{"key":"197_CR22","series-title":"ATVA \u201910","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/978-3-642-15643-4_30","volume-title":"Proceedings of the 8th international symposium on automated technology for verification and analysis","author":"Y Liu","year":"2010","unstructured":"Liu Y, Sun J, Dong JS (2010) Developing model checkers using PAT. In: Proceedings of the 8th international symposium on automated technology for verification and analysis, ATVA \u201910, pp 371\u2013377"},{"key":"197_CR23","unstructured":"McDermott DV (1998) PDDL\u2014The Planning Domain Definition Language. Yale Center for Computational Vision and Control"},{"key":"197_CR24","unstructured":"McMillan KL (1992) Symbolic model checking: an approach to the state explosion problem. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA"},{"key":"197_CR25","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/978-3-642-32759-9_28","volume-title":"FM 2012: formal methods","author":"TK Nguyen","year":"2012","unstructured":"Nguyen TK, Sun J, Liu Y, Dong JS, Liu Y (2012) Improved BDD-based discrete analysis of timed systems. In: Giannakopoulou D, M\u00e9ry D (eds) FM 2012: formal methods. LNCS, vol 7436. Springer, Berlin, pp 326\u2013340"},{"key":"197_CR26","volume-title":"Wiley encyclopedia of computer science and engineering","author":"D Peled","year":"2009","unstructured":"Peled D, Pelliccione P, Spoletini P (2009) Wiley encyclopedia of computer science and engineering. Wiley, New York. Chap \u201cModel checking\u201d"},{"key":"197_CR27","first-page":"248","volume-title":"Proceedings of the 13th international joint conference on artificial intelligence","author":"A Reinefeld","year":"1993","unstructured":"Reinefeld A (1993) Complete solution of the eight-puzzle and the benefit of node ordering in IDA*. In: Proceedings of the 13th international joint conference on artificial intelligence, vol 1. Morgan Kaufmann, San Francisco, pp 248\u2013253. http:\/\/portal.acm.org\/citation.cfm?id=1624025.1624060"},{"key":"197_CR28","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Proceedings of the 3rd international symposium on leveraging applications of formal methods, verification and validation (ISoLA 2008)","author":"J Sun","year":"2008","unstructured":"Sun J, Liu Y, Dong JS (2008) Model checking CSP revisited: introducing a process analysis toolkit. In: Proceedings of the 3rd international symposium on leveraging applications of formal methods, verification and validation (ISoLA 2008). Springer, Berlin, pp 307\u2013322"},{"key":"197_CR29","first-page":"23","volume-title":"Proceedings of the 2nd IEEE theoretical aspects of software engineering conference (TASE 2008)","author":"J Sun","year":"2008","unstructured":"Sun J, Liu Y, Dong JS, Sun J (2008) Bounded model checking of compositional processes. In: Proceedings of the 2nd IEEE theoretical aspects of software engineering conference (TASE 2008). IEEE Comput Soc, Los Alamitos, pp 23\u201330"},{"issue":"4","key":"197_CR30","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/s11704-008-0035-6","volume":"2","author":"J Sun","year":"2008","unstructured":"Sun J, Liu Y, Dong JS, Sun J (2008) Compositional encoding for bounded model checking. Frontiers of Computer Science in China 2(4):368\u2013379","journal-title":"Frontiers of Computer Science in China"},{"key":"197_CR31","first-page":"318","volume-title":"Proceedings of the 10th international conference on formal engineering methods (ICFEM 2008)","author":"J Sun","year":"2008","unstructured":"Sun J, Liu Y, Dong JS, Wang HH (2008) Specifying and verifying event-based fairness enhanced systems. In: Proceedings of the 10th international conference on formal engineering methods (ICFEM 2008). Springer, Berlin, pp 318\u2013337"},{"key":"197_CR32","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/TASE.2009.32","volume-title":"Proceedings of the third IEEE international symposium on theoretical aspects of software engineering (TASE\u201909)","author":"J Sun","year":"2009","unstructured":"Sun J, Liu Y, Dong JS, Chen C (2009) Integrating specification and programs for system modeling and verification. In: Chin WN, Qin S (eds) Proceedings of the third IEEE international symposium on theoretical aspects of software engineering (TASE\u201909). IEEE Comput Soc, Los Alamitos, pp 127\u2013135"},{"key":"197_CR33","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Proceedings of the 21th international conference on computer aided verification (CAV 2009)","author":"J Sun","year":"2009","unstructured":"Sun J, Liu Y, Dong JS, Pang J (2009) PAT: towards flexible verification under fairness. In: Proceedings of the 21th international conference on computer aided verification (CAV 2009), Grenoble, France. Springer, Berlin, pp\u00a0709\u2013714"},{"key":"197_CR34","first-page":"581","volume-title":"Proceedings of the 11th international conference on formal engineering methods (ICFEM 2009)","author":"J Sun","year":"2009","unstructured":"Sun J, Liu Y, Dong JS, Zhang X (2009) Verifying stateful timed CSP using implicit clocks and zone abstraction. In: Proceedings of the 11th international conference on formal engineering methods (ICFEM 2009), pp 581\u2013600"},{"key":"197_CR35","first-page":"123","volume-title":"Proceedings of the 6th international symposium on formal methods (FM 2009)","author":"J Sun","year":"2009","unstructured":"Sun J, Liu Y, Roychoudhury A, Liu S, Dong JS (2009) Fair model checking of parameterized systems. In: Proceedings of the 6th international symposium on formal methods (FM 2009), pp 123\u2013139"},{"key":"197_CR36","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1007\/978-3-642-16901-4_26","volume-title":"Formal methods and software engineering","author":"J Sun","year":"2010","unstructured":"Sun J, Song SZ, Liu Y (2010) Model checking hierarchical probabilistic systems. In: Dong J, Zhu H (eds) Formal methods and software engineering. LNCS, vol 6447. Springer, Berlin, pp 388\u2013403"},{"key":"197_CR37","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-642-24559-6_12","volume-title":"Formal methods and software engineering","author":"J Sun","year":"2011","unstructured":"Sun J, Liu Y, Song S, Dong JS, Li X (2011) PRTS: an approach for model checking probabilistic real-time hierarchical systems. In: Qin S, Qiu Z (eds) Formal methods and software engineering. LNCS, vol 6991. Springer, Berlin, pp 147\u2013162"},{"key":"197_CR38","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"364","DOI":"10.1007\/978-3-642-34281-3_26","volume-title":"Formal methods and software engineering","author":"T Wang","year":"2012","unstructured":"Wang T, Song S, Sun J, Liu Y, Dong JS, Wang X, Li S (2012) More anti-chain based refinement checking. In: Aoki T, Taguchi K (eds) Formal methods and software engineering. LNCS, vol 7635. Springer, Berlin, pp 364\u2013380"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0197-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0197-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0197-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T18:20:10Z","timestamp":1746037210000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0197-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,10,26]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["197"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0197-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2013,10,26]]}}}