{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:43:42Z","timestamp":1761648222521},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,10,11]],"date-time":"2014-10-11T00:00:00Z","timestamp":1412985600000},"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":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,1]]},"DOI":"10.1007\/s10817-014-9313-1","type":"journal-article","created":{"date-parts":[[2014,10,10]],"date-time":"2014-10-10T05:17:20Z","timestamp":1412918240000},"page":"31-68","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated Planning as an Early Verification Tool for Distributed Control"],"prefix":"10.1007","volume":"54","author":[{"given":"Kamalesh","family":"Ghosh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Ramesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,10,11]]},"reference":[{"key":"9313_CR1","unstructured":"Albore, A., Palacios, H., Geffner, H.: A translation-based approach to contingent planning. In: Proceedings of the 21st International Joint Conference on AI (IJCAI-09), pp. 1623\u20131628 (2009)"},{"issue":"1","key":"9313_CR2","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1109\/21.47820","volume":"20","author":"C Applegate","year":"1990","unstructured":"Applegate, C., Elsaesser, C., Sanborn, J.: An architecture for adversarial planning. IEEE Trans. Syst. Man Cybern. 20(1), 186\u2013194 (1990)","journal-title":"IEEE Trans. Syst. Man Cybern."},{"key":"9313_CR3","doi-asserted-by":"crossref","unstructured":"Bacchus, F., Kabanza, F.: Using temporal logics to express search control knowledge for planning. Artif. Intell. 116(1\u20132), 123\u2013191 (2000)","DOI":"10.1016\/S0004-3702(99)00071-5"},{"key":"9313_CR4","unstructured":"Baier, J.A., McIlraith, S.A.: Planning with first-order temporally extended goals using heuristic search. In: Proceedings of the National Conference on Artificial Intelligence, Vol. 21, p. 788. AAAI Press; MIT Press, Menlo Park (1999)"},{"key":"9313_CR5","unstructured":"Baier, J.A., McIlraith, S.A.: Planning with temporally extended goals using heuristic search. In: ICAPS, pp. 342\u2013345 (2006)"},{"key":"9313_CR6","unstructured":"Baier, J.A., Fritz, C, McIlraith, S.A.: Exploiting procedural domain control knowledge in state-of-the-art planners. In: Proceedings of the 17th International Conference on Automated Planning and Scheduling (ICAPS\u201907), pp. 26\u201333 (2007)"},{"key":"9313_CR7","unstructured":"Berry, G., Moisan, S., Rigault, J.: Esterel: towards a synchronous and semantically sound high-level language for real-time applications. In: Proceedings of the IEEE Real-Time Systems Symposium, pp. 30\u201340 (1983)"},{"key":"9313_CR8","unstructured":"Bertoli, P., Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Mbp: a model based planner. In: Proceedings of the IJCAI01 Workshop on Planning under Uncertainty and Incomplete Information (2001)"},{"issue":"1-2","key":"9313_CR9","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/S0004-3702(96)00047-1","volume":"90","author":"A Blum","year":"1997","unstructured":"Blum, A., Furst, M.: Fast planning through planning graph analysis. Artif. Intell. 90(1-2), 281\u2013300 (1997)","journal-title":"Artif. Intell."},{"issue":"1","key":"9313_CR10","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1613\/jair.1696","volume":"24","author":"A Botea","year":"2005","unstructured":"Botea, A., Enzenberger, M., M\u00fcller, M., Schaeffer, J.: Macro-ff: improving AI planning with automatically learned macro-operators. J. Artif. Intell. Res. 24(1), 581\u2013621 (2005)","journal-title":"J. Artif. Intell. Res."},{"key":"9313_CR11","doi-asserted-by":"crossref","unstructured":"Broy, M.: Challenges in automotive software engineering. In: Proceedings of the 28th International Conference on Software Engineering, pp. 33\u201342. ACM (2006)","DOI":"10.1145\/1134285.1134292"},{"issue":"1-2","key":"9313_CR12","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/0004-3702(94)90081-7","volume":"69","author":"T Bylander","year":"1994","unstructured":"Bylander, T.: The computational complexity of propositional strips planning. Artif. Intell. 69(1-2), 165\u2013204 (1994)","journal-title":"Artif. Intell."},{"key":"9313_CR13","doi-asserted-by":"crossref","unstructured":"Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: Lustre: a declarative language for real-time programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL \u201987), pp. 178\u2013188. ACM, New York (1987)","DOI":"10.1145\/41625.41641"},{"key":"9313_CR14","unstructured":"Chen, Y., Xing, Z., Zhang, W.: Long-distance mutual exclusion for propositional planning. In: Proceedings of the 20th International Joint Conference on Artifical Intelligence (IJCAI\u201907), pp. 1840\u20131845. Morgan Kaufmann Publishers Inc., San Francisco (2007)"},{"key":"9313_CR15","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model verifier. In: Halbwachs, N., Peled, D. (eds.) Proceedings of the Eleventh Conference on Computer-Aided Verification (CAV\u201999), n0. 1633 in LNCS, pp. 495\u2013499. Springer, Trento (1999)","DOI":"10.1007\/3-540-48683-6_44"},{"issue":"1","key":"9313_CR16","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/S0004-3702(02)00374-0","volume":"147","author":"A Cimatti","year":"2003","unstructured":"Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell. 147(1), 35\u201384 (2003)","journal-title":"Artif. Intell."},{"key":"9313_CR17","doi-asserted-by":"crossref","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Computer Aided Verification, pp. 154\u2013169. Springer (2000)","DOI":"10.1007\/10722167_15"},{"key":"9313_CR18","first-page":"447","volume-title":"Planning with a language for extended goals. In: AAAI\/IAAI","author":"U Dal Lago","year":"2002","unstructured":"Dal Lago, U., Pistore, M., Traverso, P.: Planning with a language for extended goals. In: AAAI\/IAAI, pp. 447\u2013454 (2002)"},{"key":"9313_CR19","unstructured":"Edelkamp, S.: On the compilation of plan constraints and preferences. In: ICAPS, pp. 374\u2013377 (2006)"},{"issue":"3","key":"9313_CR20","first-page":"67","volume":"22","author":"S Edelkamp","year":"2001","unstructured":"Edelkamp, S., Helmert, M.: Mips: the model-checking integrated planning system. AI Mag. 22(3), 67 (2001)","journal-title":"AI Mag."},{"issue":"2","key":"9313_CR21","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2005.07.023","volume":"149","author":"S Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Action planning for directed model checking of petri nets. Electron. Notes Theor. Comput. Sci. 149(2), 3\u201318 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"9313_CR22","unstructured":"Fawcett, C., Helmert, M., Hoos, H., Karpas, E., R\u00f6ger, G., Seipp, J.: Fd-autotune: domain-specific configuration using fast-downward. In: Proceedings of the ICAPS-PAL 2011(8) (2011)"},{"issue":"3\/4","key":"9313_CR23","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0004-3702(71)90010-5","volume":"2","author":"R Fikes","year":"1971","unstructured":"Fikes, R., Nilsson, N.: STRIPS: a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3\/4), 189\u2013208 (1971)","journal-title":"Artif. Intell."},{"key":"9313_CR24","doi-asserted-by":"crossref","unstructured":"Gazen, B., Knoblock, C.: Combining the expressivity of ucpop with the efficiency of graphplan. In: Steel, S., Alami, R. (eds.) Recent Advances in AI Planning, Lecture Notes in Computer Science, Vol. 1348, pp 221\u2013233. Springer, Berlin \/ Heidelberg (1997)","DOI":"10.1007\/3-540-63912-8_88"},{"key":"9313_CR25","volume-title":"Plan Constraints and Preferences in pddl3 - the Language of the Fifth International Planning Competition. Tech. rep., Department of Electronics for Automation","author":"A Gerevini","year":"2005","unstructured":"Gerevini, A., Long, D.: Plan Constraints and Preferences in pddl3 - the Language of the Fifth International Planning Competition. Tech. rep., Department of Electronics for Automation. University of Brescia, Italy (2005)"},{"key":"9313_CR26","unstructured":"Gerevini, A., Serina, I.: LPG: a planner based on local search for planning graphs with action costs. In: Proceedings of the Sixth International Conference on AI Planning and Scheduling, pp. 12\u201322 (2002)"},{"key":"9313_CR27","unstructured":"Gerth, R.: Concise Promela Reference (1997). http:\/\/spinroot.com\/spin\/Man\/Quick.html"},{"key":"9313_CR28","doi-asserted-by":"crossref","unstructured":"Ghosh, K., Dasgupta, P., Ramesh, S.: Planning with action prioritization and new benchmarks for classical planning. In: Thielscher, M., Zhang, D. (eds.) Australasian Conference on Artificial Intelligence. Lecture Notes in Computer Science, Vol. 7691, pp. 779\u2013790. Springer (2012)","DOI":"10.1007\/978-3-642-35101-3_66"},{"key":"9313_CR29","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) Recent Advances in AI Planning, Lecture Notes in Computer Science, Vol. 1809, pp. 1\u201320. Springer, Berlin \/ Heidelberg (2000)","DOI":"10.1007\/10720246_1"},{"key":"9313_CR30","doi-asserted-by":"crossref","unstructured":"Grimm, C.: Languages for System Specification: Selected Contributions on UML, SystemC, System Verilog, Mixed-signal Systems, and Property Specification from FDL\u201903. Springer (2004)","DOI":"10.1007\/b116586"},{"key":"9313_CR31","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10462-007-9049-y","volume":"26","author":"M Helmert","year":"2006","unstructured":"Helmert, M.: The fast downward planning system. J. Artif. Intell. Res. (JAIR) 26, 191\u2013246 (2006)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"9313_CR32","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1613\/jair.855","volume":"14","author":"J Hoffmann","year":"2001","unstructured":"Hoffmann, J., Nebel, B.: The FF planning system: fast plan generation through heuristic search. J. Artif. Intell. Res. (JAIR) 14, 253\u2013302 (2001)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"issue":"5","key":"9313_CR33","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279 \u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9313_CR34","unstructured":"Holzmann, G.: Spin Model Checker, The: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003)"},{"key":"9313_CR35","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of the 2008 23rd IEEE\/ACM International Conference on Automated Software Engineering, pp. 1\u20136. IEEE Computer Society (2008)","DOI":"10.1109\/ASE.2008.9"},{"issue":"11","key":"9313_CR36","doi-asserted-by":"crossref","first-page":"104","DOI":"10.1109\/MC.2003.1244539","volume":"36","author":"S Johnson","year":"2003","unstructured":"Johnson, S.: Formal methods in embedded design. Computer 36(11), 104\u2013106 (2003)","journal-title":"Computer"},{"issue":"1","key":"9313_CR37","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1016\/S0004-3702(01)00109-6","volume":"129","author":"A Junghanns","year":"2001","unstructured":"Junghanns, A., Schaeffer, J.: Sokoban: enhancing general single-agent search methods using domain knowledge. Artif. Intell. 129(1), 219\u2013251 (2001)","journal-title":"Artif. Intell."},{"key":"9313_CR38","unstructured":"Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European Conference on Artificial Intelligence (ECAI \u201992), pp. 359\u2013363. Wiley, New York (1992)"},{"key":"9313_CR39","unstructured":"Kautz, H., Selman, B., Hoffmann, J.: Satplan: planning as satisfiability. In: 5th International Planning Competition (2006)"},{"key":"9313_CR40","unstructured":"Kautz, H.A., Mcallester, D., Selman, B.: Encoding plans in propositional logic. In: Proceedings of the 50th International Conference on the Principle of Knowledge Representation and Reasoning (KR\u201996), pp. 374\u2013384 (1996)"},{"issue":"1","key":"9313_CR41","first-page":"49","volume":"25","author":"P Kissmann","year":"2011","unstructured":"Kissmann, P., Edelkamp, S.: Gamer, a general game playing agent. KI 25(1), 49\u201352 (2011)","journal-title":"KI"},{"issue":"1","key":"9313_CR42","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0004-3702(85)90012-8","volume":"26","author":"RE Korf","year":"1985","unstructured":"Korf, R.E.: Macro-operators: a weak method for learning. Artif. Intell. 26(1), 35\u201377 (1985)","journal-title":"Artif. Intell."},{"key":"9313_CR43","doi-asserted-by":"crossref","unstructured":"Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) Model Checking Software, Lecture Notes in Computer Science, Vol. 3925, pp. 35\u201352. Springer, Berlin \/ Heidelberg (2006)","DOI":"10.1007\/11691617_3"},{"issue":"1-4","key":"9313_CR44","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1023\/A:1016619613658","volume":"30","author":"J Kvarnstr\u00f6m","year":"2000","unstructured":"Kvarnstr\u00f6m, J., Doherty, P.: Talplanner: a temporal logic based forward chaining planner. Ann. Math. Artif. Intell. 30(1-4), 119\u2013169 (2000)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"9313_CR45","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1016\/S0968-090X(00)00022-X","volume":"9","author":"G Marsden","year":"2001","unstructured":"Marsden, G., McDonald, M., Brackstone, M.: Towards an understanding of adaptive cruise control. Transp. Res. Part C Emerg. Technol. 9(1), 33\u201351 (2001)","journal-title":"Transp. Res. Part C Emerg. Technol."},{"key":"9313_CR46","unstructured":"Mcdermott, D., Ghallab, M., Howe, A., Knoblock, C., Ram, A., Veloso, M., Weld, D., Wilkins, D.: Pddl - the Planning Domain Definition Language. Tech. rep., CVC TR-98-003\/DCS TR-1165, Yale Center for Computational Vision and Control (1998)"},{"key":"9313_CR47","first-page":"83","volume":"2173","author":"P McElligott","year":"2008","unstructured":"McElligott, P., Mjeda, A., Thiel, S.: Can formal methods make automotive business sense? A classification of formal methods by usefulness. SAE SP 2173, 83 (2008)","journal-title":"SAE SP"},{"key":"9313_CR48","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357 (1977), 10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"9313_CR49","unstructured":"Prestl, W., Sauer, T., Steinle, J., Tschernoster, O.: The bmw active cruise control acc. In: SAE International Congressional Exposure, 2000, Society of Automotive Engineers, 400 Commonwealth Dr, Warrendale, PA, 15096, USA (2000)"},{"key":"9313_CR50","first-page":"50","volume-title":"Lama 2008 and 2011. The 2011 International Planning Competition","author":"S Richter","year":"2011","unstructured":"Richter, S., Westphal, M., Helmert, M.: Lama 2008 and 2011. The 2011 International Planning Competition, p. 50 (2011)"},{"key":"9313_CR51","first-page":"61","volume-title":"Madagascar: efficient planning with sat. The 2011 International Planning Competition","author":"J Rintanen","year":"2011","unstructured":"Rintanen, J.: Madagascar: efficient planning with sat. The 2011 International Planning Competition, p. 61 (2011)"},{"key":"9313_CR52","unstructured":"Sch\u00e4tz, B., Fleischmann, A., Geisberger, E., Pister, M.: Model-based requirements engineering with autoraid. In: Workshop Modellbasierte Qualit\u00e4tssicherung (QUAM), Lecture Notes in Informatics (LNI), pp. 511\u2013516 (2005)"},{"key":"9313_CR53","unstructured":"Shaparau, D., Pistore, M., Traverso, P.: Fusing procedural and declarative planning goals for nondeterministic domains. In: Proceedings of the 23rd National Conference on Artificial Intelligence (AAAI\u201908), pp. 983\u2013990. AAAI Press (2008)"},{"key":"9313_CR54","unstructured":"Slaney, J.: Randomnet: A Specific-purpose Tool that Generates Random Descriptions of Power Distribution Networks as Part of the PSR (Power Supply Restoration) Benchmark for AI Planning (2005). http:\/\/rsise.anu.edu.au\/jks\/software\/randomnet.tar.gz"},{"key":"9313_CR55","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.4. 1. University of Colorado at Boulder (2005)"},{"key":"9313_CR56","unstructured":"Thi\u00e9baux, S., Cordier, M.: Supply restoration in power distribution systems\u2013a benchmark for planning under uncertainty. In: Pre-Proceedings of the 6th European Conference on Planning (ECP-01), pp. 85\u201396 (2001)"},{"issue":"1\u20132","key":"9313_CR57","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1016\/j.artint.2005.05.004","volume":"168","author":"S Thi\u00e9baux","year":"2005","unstructured":"Thi\u00e9baux, S., Hoffmann, J., Nebel, B.: In defense of pddl axioms. Artif. Intell. 168(1\u20132), 38\u201369 (2005)","journal-title":"Artif. Intell."},{"issue":"2","key":"9313_CR58","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/0004-3702(80)90039-9","volume":"14","author":"D Wilkins","year":"1980","unstructured":"Wilkins, D.: Using patterns and plans in chess. Artif. Intell. 14(2), 165\u2013203 (1980)","journal-title":"Artif. Intell."},{"key":"9313_CR59","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/3-540-48957-6_6","volume":"1558","author":"S Willmott","year":"1999","unstructured":"Willmott, S., Richardson, J., Bundy, A., Levine, J.: An adversarial planning approach to go. Comput. Games 1558, 93\u2013112 (1999)","journal-title":"Comput. Games"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9313-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-014-9313-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-014-9313-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,16]],"date-time":"2019-08-16T02:30:01Z","timestamp":1565922601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-014-9313-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,11]]},"references-count":59,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1]]}},"alternative-id":["9313"],"URL":"https:\/\/doi.org\/10.1007\/s10817-014-9313-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,11]]}}}