{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T09:06:03Z","timestamp":1760346363638,"version":"3.40.4"},"reference-count":88,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,12,17]],"date-time":"2013-12-17T00:00:00Z","timestamp":1387238400000},"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,2]]},"DOI":"10.1007\/s10009-013-0294-x","type":"journal-article","created":{"date-parts":[[2013,12,16]],"date-time":"2013-12-16T09:25:32Z","timestamp":1387185932000},"page":"1-12","source":"Crossref","is-referenced-by-count":32,"title":["Verification and validation meet planning and scheduling"],"prefix":"10.1007","volume":"16","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Orlandini","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,17]]},"reference":[{"key":"294_CR1","unstructured":"Mars Science Laboratory (MSL) mission website. http:\/\/mars.jpl.nasa.gov\/msl . Accessed Nov 2013"},{"key":"294_CR2","unstructured":"VVPS 2005 workshop website. http:\/\/icaps05.uni-ulm.de\/workshops.html"},{"key":"294_CR3","unstructured":"VVPS 2009 workshop website. http:\/\/www-vvps09.imag.fr"},{"key":"294_CR4","unstructured":"VVPS 2011 workshop website. http:\/\/icaps11.icaps-conference.org\/workshops\/vvps.html"},{"key":"294_CR5","unstructured":"Abdedaim, Y., Asarin, E., Gallien, M., Ingrand, F., Lesire, C., Sighireanu, M.: Planning robust temporal plans: a comparison between CBTP and TGA approaches. In: Proceedings of the Seventeenth International Conference on Automated Planning and Scheduling (ICAPS\u201907), pp. 2\u201310 (2007)"},{"key":"294_CR6","unstructured":"Albarghouthi, A., Baier, J.A., McIlraith, S.A.: On the use of planning technology for verification. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"issue":"2\u20133","key":"294_CR7","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/j.tcs.2004.11.007","volume":"336","author":"C Artho","year":"2005","unstructured":"Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test-case generation and runtime verification. Theor. Comput. Sci. 336(2\u20133), 209\u2013234 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"294_CR8","unstructured":"Artho, C., Havelund, K., Biere. A.: High-level data races. Softw. Test. Verif. Reliab. 13(4), 207\u2013227 (2004)"},{"key":"294_CR9","doi-asserted-by":"crossref","unstructured":"Bakera, M., Edelkamp, S., Kissmann, P., Renner, C.D.: Solving $$\\mu $$ \u03bc -calculus parity games by symbolic planning. In: Peled. D., Wooldridge, M. (eds.) MoChArt. Lecture Notes in Computer Science, vol. 5348, pp. 15\u201333. Springer, New York (2008)","DOI":"10.1007\/978-3-642-00431-5_2"},{"issue":"11","key":"294_CR10","doi-asserted-by":"crossref","first-page":"365","DOI":"10.2514\/1.49356","volume":"7","author":"H Barringer","year":"2010","unstructured":"Barringer, H., Groce, A., Havelund, K., Smith, M.: Formal analysis of log files. J. Aerosp. Comput. Inf. Commun. 7(11), 365\u2013390 (2010)","journal-title":"J. Aerosp. Comput. Inf. Commun."},{"key":"294_CR11","doi-asserted-by":"crossref","unstructured":"Barringer, H., Havelund, K., Kurklu, E., Morris, R.: Checking flight rules with TraceContract: application of a Scala DSL for trace analysis. In: Scala Days 2011. Stanford University, California (2011)","DOI":"10.1007\/978-3-642-21437-0_7"},{"key":"294_CR12","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K., Lime, D.: UPPAAL-TIGA: time for playing games! In: Proceedings of 19th International Conference on Computer Aided Verification (CAV\u201907), vol. 4590 in LNCS, pp. 121\u2013125. Springer, New York (2007)","DOI":"10.1007\/978-3-540-73368-3_14"},{"key":"294_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45319-9_13","volume-title":"Efficient Guiding Towards Cost-Optimality in UPPAAL","author":"G Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K., Pettersson, P., Romijn, J.: Efficient Guiding Towards Cost-Optimality in UPPAAL. Springer, New York (2001)"},{"key":"294_CR14","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Optimal scheduling using priced timed automata. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS\u201905) (2005)","DOI":"10.1145\/1059816.1059823"},{"key":"294_CR15","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Bozga, M., Krichen, M., Tripakis, S.: Testing conformance of real-time applications: case of planetary rover controller. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS\u201905), pp. 23\u201332 (2005)","DOI":"10.1016\/j.entcs.2004.01.036"},{"key":"294_CR16","doi-asserted-by":"crossref","unstructured":"Bodik, R., Jobstmann, B.: Algorithmic program synthesis: introduction. Int. J. Softw. Tools Technol. Transf. STTT 15(5\u20136), 397\u2013411 (October 2013)","DOI":"10.1007\/s10009-013-0287-9"},{"key":"294_CR17","unstructured":"Bozzano, M., Cimatti, A., Roveri, M., Tchaltsev, A.: A comprehensive approach to on-board autonomy verification and validation. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR18","unstructured":"Brat, G., Drusinsky, D., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M., Pasareanu, C., Visser, W., Washington, R.: Experimental evaluation of verification and validation tools on Martian rover software. Form. Methods Syst. Des. 25(2), 167\u2013198 (2004)"},{"key":"294_CR19","unstructured":"Brat, G., Gannakopoulou, D., Izygon, M., Alex, E., Wang, L., Frank, J., Molin, A.: Model-based verification and validation for procedure authoring. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR20","doi-asserted-by":"crossref","unstructured":"Cerrito, S., Mayer, M.C.: Using linear temporal logic to model and solve planning problems. In: Giunchiglia, F (ed.) Artificial Intelligence: Methodology, Systems, and Applications. Lecture Notes in Computer Science, vol 1480, pp. 141\u2013152. Springer, New York (1998)","DOI":"10.1007\/BFb0057441"},{"key":"294_CR21","doi-asserted-by":"crossref","unstructured":"Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Verifying flexible timeline-based plans. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)","DOI":"10.1007\/978-3-642-04617-9_7"},{"key":"294_CR22","doi-asserted-by":"crossref","first-page":"111","DOI":"10.3233\/FI-2011-397","volume":"107","author":"A Cesta","year":"2011","unstructured":"Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Flexible plan verification: feasibility results. Fundamenta Informaticae 107, 111\u2013137 (2011)","journal-title":"Fundamenta Informaticae"},{"key":"294_CR23","unstructured":"Cichy, B., Chien, S., Schaffer, S., Tran, D., Rabideau, G., Sherwood, R.: Validating the autonomous EO-1 science agent. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS\u201905), pp. 75\u201385 (2005)"},{"key":"294_CR24","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Giunchiglia, F., Giunchiglia, E., Traverso, P.: Planning via model checking: a decision procedure for AR. In: Steel, S., Alami, R. (eds.) ECP. Lecture Notes in Computer Science, vol. 1348, pp. 130\u2013142. Springer, New York (1997)","DOI":"10.1007\/3-540-63912-8_81"},{"key":"294_CR25","unstructured":"Cimatti, A., Roveri, M., Traverso, P.: Strong planning in non-deterministic domains via model checking. In: Simmons, R.G., Veloso, M.M., Smith, S.F. (eds.) AIPS, pp. 36\u201343. AAAI, Pittsburgh (1998)"},{"key":"294_CR26","doi-asserted-by":"crossref","unstructured":"Crampton, J., Huth, M., Kuo, J.H.-P.: Authorized workflow schemas : deciding realizability through LTL(F) model checking. Int. J. Softw. Tools Technol. Transf. STTT (2014)","DOI":"10.1007\/s10009-012-0269-3"},{"key":"294_CR27","unstructured":"Dierks, H.: Finding optimal plans for domains with restricted continuous effects with UPPAAL-CORA. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS\u201905) (2005)"},{"key":"294_CR28","unstructured":"Dixon, L., Smaill, A., Bundy, A.: Verified planning by deductive synthesis in intuitionistic linear logic. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR29","doi-asserted-by":"crossref","unstructured":"Edelkamp, S.: Promela planning. In: Ball, T., Rajamani, S.K. (eds.) SPIN. Lecture Notes in Computer Science, vol. 2648, pp. 197\u2013212. Springer, New York (2003)","DOI":"10.1007\/3-540-44829-2_13"},{"issue":"2","key":"294_CR30","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. Electr. Notes Theor. Comput. Sci. 149(2), 3\u201318 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"294_CR31","first-page":"1362","volume-title":"AAAI","author":"S Edelkamp","year":"2005","unstructured":"Edelkamp, S., Jabbar, S., Lluch-Lafuente, A.: Cost-algebraic heuristic search. In: Veloso, M.M., Kambhampati, S. (eds.) AAAI, pp. 1362\u20131367. AAAI Press\/The MIT Press, Cambridge (2005)"},{"key":"294_CR32","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Kellershoff, M., Sulewski, D.: Program model checking via action planning. In: van der Meyden, R., Smaus, J.-G. (eds.) MoChArt. Lecture Notes in Computer Science, vol. 6572, pp. 32\u201351. Springer, New York (2010)","DOI":"10.1007\/978-3-642-20674-0_3"},{"issue":"1","key":"294_CR33","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1023\/A:1008711707946","volume":"8","author":"M Feather","year":"2001","unstructured":"Feather, M., Smith, B.: Automatic generation of test oracles\u2014from pilot studies to application. Autom. Softw. Eng. 8(1), 31\u201361 (2001)","journal-title":"Autom. Softw. Eng."},{"key":"294_CR34","unstructured":"Fox, M., Howey, R., Long, D.: Exploration of the robustness of plans. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS\u201905), pp. 67\u201374 (2005)"},{"key":"294_CR35","unstructured":"Fox, M., Long, D., Baldwin, L., Wilson, G., Woods, M., Jameux, D., Aylett, R.: On-board timeline validation and repair: a feasibility study. In: Proceedings of 5th International Workshop on Planning and Scheduling for Space (IWPSS\u201906) (2006)"},{"key":"294_CR36","doi-asserted-by":"crossref","unstructured":"Freitag, B., Margaria, T., Steffen, B.: A pragmatic approach to software synthesis. In: Wing, J.M., Wexelblat, R.L. (eds.) Workshop on Interface Definition Languages, Portland, Oregon, USA, pp. 46\u201358. ACM Press, New York (1994)","DOI":"10.1145\/185084.185102"},{"key":"294_CR37","unstructured":"Giannakopoulou, D., Pasareanu, C.S., Lowry, M., Washington, R.: Lifecycle verification of the NASA Ames K9 rover executive. In: Proceedings of the ICAPS Workshop on Verification and Validation of Model-Based Planning and Scheduling Systems (VVPS\u201905), pp. 75\u201385 (2005)"},{"key":"294_CR38","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) ECP. Lecture Notes in Computer Science, vol. 1809, pp. 1\u201320. Springer, New York (1999)","DOI":"10.1007\/10720246_1"},{"key":"294_CR39","doi-asserted-by":"crossref","unstructured":"Goldberg, A., Havelund, K., McGann, C.: Runtime verification for autonomous spacecraft software. In: Proceedings of IEEE Aerospace Conference, IEEE Computer Society, USA (2005)","DOI":"10.1109\/AERO.2005.1559341"},{"key":"294_CR40","unstructured":"Goldman, R.P., Kuter, U., Schneider, A.: Using classical planners for plan verification and counterexample generation. In: Proceedings of AAAI Workshop on Problem Solving Using Classical, Planning (2012)"},{"key":"294_CR41","doi-asserted-by":"crossref","unstructured":"Goldman, R.P., Musliner, D.J., Pelican, M.J.: Exploiting implicit representations in timed automaton verification for controller synthesis. In: Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control (HSCC\u201902) (2002)","DOI":"10.1007\/3-540-45873-5_19"},{"key":"294_CR42","doi-asserted-by":"crossref","unstructured":"Goldman, R.P., Pelican, M.J., Musliner, D.J.: A loop acceleration technique to speed up verification of automatically-generated plans. Int. J. Softw. Tools Technol. Transf. STTT (2014)","DOI":"10.1007\/s10009-013-0284-z"},{"key":"294_CR43","doi-asserted-by":"crossref","unstructured":"Havelund, K., Groce, A., Holzmann, G., Joshi, R., Smith, M.: Automated testing of planning models. In: Proceedings of the Fifth International Workshop on Model Checking and Artificial Intelligence, pp. 90\u2013105 (2008)","DOI":"10.1007\/978-3-642-00431-5_6"},{"key":"294_CR44","unstructured":"Havelund, K., Lowry, M., Park, S., Pecheur, C., Penix, J., Visser, W., White, J.L.: Formal analysis of the Remote Agent\u2014before and after flight. In: The Fifth NASA Langley Formal Methods Workshop, Virginia (2001)"},{"issue":"8","key":"294_CR45","doi-asserted-by":"crossref","first-page":"749","DOI":"10.1109\/32.940728","volume":"27","author":"K Havelund","year":"2001","unstructured":"Havelund, K., Lowry, M., Penix, J.: Formal analysis of a spacecraft controller using SPIN. IEEE Trans. Softw. Eng. 27(8), 749\u2013765 (2001). An earlier version occurred in the proceedings of 4th SPIN, workshop, 1998","journal-title":"IEEE Trans. Softw. Eng."},{"key":"294_CR46","unstructured":"Howey, R., Long, D.: VAL\u2019s progress: the automatic validation tool for PDDL2.1 used in the international planning competition. In: Proceedings of the ICAPS Workshop on The Competition: Impact, Organization, Evaluation, Benchmarks, pp. 28\u201337, Trento (2003)"},{"key":"294_CR47","unstructured":"Johnston, M.D., Tran, D.: Verification and validation of a deep space network scheduling application. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR48","unstructured":"Jonsson, A., Morris, P., Muscettola, N., Rajan, K., Smith, B.: Planning in interplanetary space: theory and practice. In: Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling (AIPS\u201900), pp. 177\u2013186 (2000)"},{"key":"294_CR49","unstructured":"Kautz, H., Selman, B.: BLACKBOX: a new approach to the application of theorem proving to problem solving. In: AIPS\u201998 Workshop on Planning as Combinatorial, Search, pp. 58\u201360 (1998)"},{"key":"294_CR50","unstructured":"Kautz, H., Selman, B.: Unifying sat-based and graph-based planning. In: Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI-99), vol. 99, pp. 318\u2013325 (1999)"},{"key":"294_CR51","unstructured":"Kautz, H.A., Selman, B., et al.: Planning as satisfiability. In: Proceedings of the International European Conference on Artificial Intelligence (ECAI-92), vol. 92, pp. 359\u2013363 (1992)"},{"key":"294_CR52","doi-asserted-by":"crossref","unstructured":"Khatib, L., Muscettola, N., Havelund, K.: Verification of plan models using UPPAAL. In: First International Workshop on Formal Approaches to Agent-Based Systems, NASA\u2019s Goddard Space center, Maryland. Lecture Notes in Artificial Intelligence, vol. 1871. Springer, New York (2000)","DOI":"10.1007\/3-540-45484-5_9"},{"key":"294_CR53","doi-asserted-by":"crossref","unstructured":"Khatib, L., Muscettola, N., Havelund, K.: Mapping temporal planning constraints into timed automata. In: The Eigth International Symposium on Temporal Representation and Reasoning (TIME\u201901), pp. 21\u201327 (2001)","DOI":"10.1109\/TIME.2001.930693"},{"key":"294_CR54","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS\u201905), Pittsburgh, pp. 531\u2013542 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"294_CR55","doi-asserted-by":"crossref","unstructured":"Lindsey, T., Pecheur, C.: Simulation-based verification of autonomous controllers with Livingstone PathFinder. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201904), Barcelona, Spain. Lecture Notes in Computer Science, vol. 2988 (2004)","DOI":"10.1007\/978-3-540-24730-2_28"},{"key":"294_CR56","unstructured":"Long, D., Fox, M., Howey, R.: Planning domains and plans: validation, verification and analysis. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR57","doi-asserted-by":"crossref","unstructured":"Lowry, M.R., Havelund, K., Penix, J.: Verification and validation of AI systems that control deep-space spacecraft. In: Foundations of Intelligent Systems, Proceedings of 10th International Symposium, ISMIS\u201997, Charlotte. Lecture Notes in Computer Science, vol. 1325, pp. 35\u201347. Springer, New York (1997)","DOI":"10.1007\/3-540-63614-5_3"},{"issue":"1","key":"294_CR58","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10849-006-9022-1","volume":"16","author":"MC Mayer","year":"2007","unstructured":"Mayer, M.C., Limongelli, C., Orlandini, A., Poggioni, V.: Linear temporal logic as an executable semantics for planning languages. J. Log. Lang. Inf. 16(1), 63\u201389 (2007)","journal-title":"J. Log. Lang. Inf."},{"key":"294_CR59","volume-title":"Some Philosophical Problems from the Standpoint of Artificial Intelligence","author":"J McCarthy","year":"1968","unstructured":"McCarthy, J., Hayes, P.: Some Philosophical Problems from the Standpoint of Artificial Intelligence. Stanford University, USA (1968)"},{"key":"294_CR60","unstructured":"McDermott, D., Ghallab, M., Howe, A., Knoblock, C., Ram, A., Veloso, M., Weld, D., Wilkins, D.: PDDL-the planning domain definition language. Technical Report CVC TR98003\/DCS TR1165, New Haven, CT. Yale Center for Computational Vision and Control (1998)"},{"key":"294_CR61","first-page":"5","volume":"65","author":"T Menzies","year":"2005","unstructured":"Menzies, T., Pecheur, C.: Verification and validation and artificial intelligence. Adv. Comput. 65, 5\u201345 (2005)","journal-title":"Adv. Comput."},{"key":"294_CR62","unstructured":"Morris, P.H., Muscettola, N.: Temporal dynamic controllability revisited. In: Proceedings of the 20th National Conference on Artificial Intelligence (AAAI-05) (2005)"},{"key":"294_CR63","volume-title":"Intelligent Scheduling","author":"N Muscettola","year":"1994","unstructured":"Muscettola, N.: HSTS: integrating planning and scheduling. In: Zweben, M., Fox, M.S. (eds.) Intelligent Scheduling. Morgan Kauffmann, Burlington (1994)"},{"key":"294_CR64","unstructured":"Musliner, D.J., Pelican, M.J.S., Schlette, P.J.: Verifying equivalence of procedures in different languages: preliminary results. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR65","unstructured":"Nayak, P.P., Bernard, D.E., Dorais, G., Gamble, E.B., Kanefsky, B., Kurien, J., Millar, W., Muscettola, N., Rajan, K., Rouquette, N., Smith, B.D., Taylor, W.: Validating the DS1 Remote Agent experiment. In: Proceeedings of the Fifth International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS\u201999) (1999)"},{"key":"294_CR66","doi-asserted-by":"crossref","unstructured":"Orlandini, A., Finzi, A., Cesta, A., Fratini, S.: TGA-based controllers for flexible plan execution. In: Advances in Artificial Intelligence (KI 2011), 34th Annual German Conference on AI. Lecture Notes in Computer Science, vol. 7006, pp. 233\u2013245. Springer, New York (2011)","DOI":"10.1007\/978-3-642-24455-1_22"},{"key":"294_CR67","unstructured":"Patron, P., Birch, A.: Plan proximity: an enhanced metric for plan stability. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR68","unstructured":"Penix, J., Pecheur, C., Havelund, K.: Using model checking to validate AI planner domain models. In: Proceedings of the 23 $$^{rd}$$ r d Annual Software Engineering, Workshop (1998)"},{"key":"294_CR69","doi-asserted-by":"crossref","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI\u201906). Lecture Notes in Computer Science, vol. 3855, pp. 364\u2013380. Springer, New York (2006)","DOI":"10.1007\/11609773_24"},{"key":"294_CR70","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society, USA (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"294_CR71","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symposium on Principles of Programming Languages (POPL\u201989), pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"294_CR72","first-page":"123","volume-title":"Micro-Level Knowledge Management","author":"A Preece","year":"2001","unstructured":"Preece, A.: Evaluating verification and validation methods in knowledge engineering. In: Roy, R. (ed.) Micro-Level Knowledge Management, pp. 123\u2013145. Morgan-Kaufman, Burlington (2001)"},{"key":"294_CR73","unstructured":"R-Moreno, M.D., Brat, G., Muscettola, N., Rijsman, D.: Validation of a multi-agent architecture for planning and execution. In: Proceedings of 18th International Workshop on Principles of Diagnosis (DX\u201907) (2007)"},{"key":"294_CR74","unstructured":"Raimondi, F., Pecheur, C., Brat, G.: PDVer, a tool to verify PDDL planning domains. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR75","doi-asserted-by":"crossref","unstructured":"Razavi, N., Farzan, A., McIlraith, S.A.: Generating effective tests for concurrent programs via AI automated planning techniques. Int. J. Softw. Tools Technol. Transf. STTT (2014)","DOI":"10.1007\/s10009-013-0277-y"},{"key":"294_CR76","unstructured":"Shah, M., Chrpa, L., Jimoh, F., Kitchin, D., McCluskey, T., Parkinson, S., Vallati, M.: Knowledge engineering tools in planning: state-of-the-art and future challenges. In: Proceedings of the ICAPS Workshop on Knowledge Engineering for Planning and Scheduling (KEPS 2013) (2013)"},{"key":"294_CR77","unstructured":"Siminiceanu, R.I., Butler, R.W., Munoz, C.A.: Experimental evaluation of a planning language suitable for formal verification. In: Proceedings of the Fifth International Workshop on Model Checking and Artificial Intelligence, pp. 18\u201334 (2008)"},{"key":"294_CR78","unstructured":"Smith, B., Feather, M., Muscettola, N.: Challenges and methods in testing the Remote Agent planner. In: Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling (AIPS\u201900), pp. 254\u2013263 (2000)"},{"key":"294_CR79","doi-asserted-by":"crossref","unstructured":"Smith, B., Millar, W., Dunphy, J., Tung, Y.-W., Nayak, P., Gamble, E., Clark, M.: Validation and verification of the Remote Agent for spacecraft autonomy. In: Proceedings of IEEE Aerospace Conference (1999)","DOI":"10.1109\/AERO.1999.794352"},{"key":"294_CR80","doi-asserted-by":"crossref","unstructured":"Smith, B., Rajan, K., Muscettola, N.: Knowledge acquisition for the onboard planner of an autonomous spacecraft. In: 10th European Workshop on Knowledge Acquisition, Modeling and Management (EKAW\u201997). Lecture Notes in Computer Science, vol. 1319, pp. 253\u2013268 (1997)","DOI":"10.1007\/BFb0026790"},{"key":"294_CR81","doi-asserted-by":"crossref","unstructured":"Smith, M.H., Holzmann, G.J., Cucullu, G.C., Smith, B.D.: Model checking autonomous planners: even the best laid plans must be verified. In: Proceedings of IEEE Aerospace Conference, pp. 1\u201311. IEEE Computer Society, USA (2005)","DOI":"10.1109\/AERO.2005.1559607"},{"key":"294_CR82","unstructured":"Srivastava, S., Immerman, N., Zilberstein, S.: Finding plans with branches, loops and preconditions. In: Proceedings of the ICAPS Workshop on Verification and Validation of Planning and Scheduling Systems (VVPS\u201909) (2009)"},{"key":"294_CR83","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation. In: Bartocci, E., Ramakrishnan, C. (eds.) Model Checking Software, vol. 7976, pp. 341\u2013357. Lecture Notes in Computer Science. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39176-7_21"},{"issue":"1\u20132","key":"294_CR84","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/s100090050003","volume":"1","author":"B Steffen","year":"1997","unstructured":"Steffen, B., Margaria, T., Braun, V.: The electronic tool integration platform: concepts and design. Int. J. Softw. Tools Technol. Transf. STTT 1(1\u20132), 9\u201330 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf. STTT"},{"key":"294_CR85","unstructured":"Vaquero, T., Silva, J., Beck, J.: A brief review of tools and methods for knowledge engineering for planning and scheduling. In: Proceedings of the ICAPS Workshop on Knowledge Engineering for Planning and Scheduling (KEPS 2011) (2011)"},{"key":"294_CR86","unstructured":"Vidal, T.: A unified dynamic approach for dealing with temporal uncertainty and conditional planning. In: Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling (AIPS\u201900) (2000)"},{"key":"294_CR87","doi-asserted-by":"crossref","unstructured":"Wehrle, M. Helmert, M.: The causal graph revisited for directed model checking. In: Palsberg, J., Su, Z. (eds.) SAS. Lecture Notes in Computer Science, vol. 5673, pp. 86\u2013101. Springer, New York (2009)","DOI":"10.1007\/978-3-642-03237-0_8"},{"key":"294_CR88","first-page":"971","volume":"2","author":"BC Williams","year":"1996","unstructured":"Williams, B.C., Nayak, P.P.: A model-based approach to reactive self-configuring systems. AAAI\/IAAI 2, 971\u2013978 (1996)","journal-title":"AAAI\/IAAI"}],"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-0294-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0294-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0294-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T05:50:43Z","timestamp":1746078643000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0294-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,17]]},"references-count":88,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["294"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0294-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2013,12,17]]}}}