{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T18:37:01Z","timestamp":1767638221122,"version":"3.48.0"},"reference-count":37,"publisher":"Maximum Academic Press","issue":"3","license":[{"start":{"date-parts":[[2010,9,1]],"date-time":"2010-09-01T00:00:00Z","timestamp":1283299200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Knowledge Engineering Review"],"published-print":{"date-parts":[[2010,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    To foster effective use of artificial intelligence planning and scheduling (\n                    <jats:sc>P<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>S)<\/jats:sc>\n                    systems in the real world, it is of great importance to both (a) broaden direct access to the technology for the end users and (b) significantly increase their trust in such technology. Automated\n                    <jats:sc>P<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>S<\/jats:sc>\n                    systems often bring solutions to the users that are neither \u2018obvious\u2019 nor immediately acceptable to them. This is because these tools directly reason on causal, temporal, and resource constraints; moreover, they employ resolution processes designed to optimize the solution with respect to non-trivial evaluation functions. Knowledge engineering environments aim at simplifying direct access to the technology for people other than the original system designers, while the integration of validation and verification (\n                    <jats:sc>V<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>V<\/jats:sc>\n                    ) capabilities in such environments may potentially enhance the users\u2019 trust in the technology. Somehow,\n                    <jats:sc>V<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>V<\/jats:sc>\n                    techniques may represent a complementary technology, with respect to\n                    <jats:sc>P<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>S<\/jats:sc>\n                    , that contributes to developing richer software environments to synthesize a new generation of robust problem-solving applications. The integration of\n                    <jats:sc>V<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>V<\/jats:sc>\n                    and\n                    <jats:sc>P<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>S<\/jats:sc>\n                    techniques in a knowledge engineering environment is the topic of this paper. In particular, it analyzes the use of state-of-the-art\n                    <jats:sc>V<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>V<\/jats:sc>\n                    technology to support knowledge engineering for a timeline-based planning system called MrSPOCK. The paper presents the application domain for which the automated solver has been developed, introduces the timeline-based planning ideas, and then describes the different possibilities to apply\n                    <jats:sc>V<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>V<\/jats:sc>\n                    to planning. Hence, it continues by describing the step of adding\n                    <jats:sc>V<\/jats:sc>\n                    <jats:sc>&amp;<\/jats:sc>\n                    <jats:sc>V<\/jats:sc>\n                    functionalities around the specialized planner, MrSPOCK. New functionalities have been added to perform both model validation and plan verification. Lastly, a specific section describes the benefits as well as the performance of such functionalities.\n                  <\/jats:p>","DOI":"10.1017\/s0269888910000160","type":"journal-article","created":{"date-parts":[[2010,8,23]],"date-time":"2010-08-23T09:25:48Z","timestamp":1282555548000},"page":"299-318","source":"Crossref","is-referenced-by-count":11,"title":["Validation and verification issues in a timeline-based planning system"],"prefix":"10.48130","volume":"25","author":[{"given":"Amedeo","family":"Cesta","sequence":"first","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Alberto","family":"Finzi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Simone","family":"Fratini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Andrea","family":"Orlandini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"given":"Enrico","family":"Tronci","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]}],"member":"27968","published-online":{"date-parts":[[2010,9,1]]},"reference":[{"key":"S0269888910000160_ref5","unstructured":"Cesta A. , Cortellessa G. , Fratini S. , Oddi A. 2009. Developing an end-to-end planning application from a timeline representation framework. In IAAI-09. Proceedings of the 21st Innovative Application of Artificial Intelligence Conference, Pasadena, CA, USA."},{"key":"S0269888910000160_ref28","first-page":"123","volume-title":"Micro-level Knowledge Management","author":"Preece","year":"2001"},{"key":"S0269888910000160_ref7","unstructured":"Cichy B. , Chien S. , Schaffer S. , Tran D. , Rabideau G. , Sherwood R. 2005. Validating the autonomous eo-1 science agent. In VVPS-05. Proceedings of the ICAPS Workshop on Validation & Verification of Planning and Scheduling Systems, Monterey, CA, USA, 75\u201385."},{"key":"S0269888910000160_ref13","first-page":"231","article-title":"Unifying planning and scheduling as timelines in a component-based perspective","volume":"180","author":"Fratini","year":"2008","journal-title":"Archives of Control Sciences"},{"key":"S0269888910000160_ref37","unstructured":"Vidal T. 2000. A unified dynamic approach for dealing with temporal uncertainty and conditional planning. In AIPS-00. Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling, AAAI Press, Menlo Park, CA, USA, 395\u2013402."},{"volume-title":"Model Checking","year":"1999","author":"Clarke","key":"S0269888910000160_ref9"},{"key":"S0269888910000160_ref34","unstructured":"Smith B. , Feather M. , Muscettola N. 2000a. Challenges and methods in testing the remote agent planner. In AIPS-00. Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling, AAAI Press, Menlo Park, CA, USA, 254\u2013263."},{"key":"S0269888910000160_ref15","doi-asserted-by":"crossref","unstructured":"Goldman R. P. , Musliner D. J. , Pelican M. J 2002. Exploiting implicit representations in timed automaton verification for controller synthesis. In HSCC-02. Proceedings of the Fifth International Workshop on Hybrid Systems: Computation and Control. Lecture Notes in Computer Science. Springer, Heidelberg, Germany.","DOI":"10.1007\/3-540-45873-5_19"},{"key":"S0269888910000160_ref11","unstructured":"Fox M. , Long D. , Baldwin L. , Wilson G. , Woods M. , Jameux D. , Aylett R. 2006. On-board timeline validation and repair: a feasibility study. In IWPSS-06. Proceedings of 5th International Workshop on Planning and Scheduling for Space, Monterey, CA, USA."},{"key":"S0269888910000160_ref12","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025842019552"},{"key":"S0269888910000160_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45484-5_8"},{"key":"S0269888910000160_ref36","first-page":"1","volume-title":"Proceedings of IEEE Aerospace Conference","author":"Smith","year":"2005"},{"key":"S0269888910000160_ref20","doi-asserted-by":"crossref","unstructured":"Khatib L. , Muscettola N. , Havelund K. 2001. Mapping temporal planning constraints into timed automata. In TIME-01. The Eigth Int. Symposium on Temporal Representation and Reasoning, IEEE Computer Society, Los Alamitos, CA, USA, 21\u201327.","DOI":"10.1109\/TIME.2001.930693"},{"key":"S0269888910000160_ref19","unstructured":"Jonsson A. , Morris P. , Muscettola N. , Rajan K. , Smith B. 2000. Planning in interplanetary space: theory and practice. In AIPS-00. Proceedings of the Fifth International Conference on Artificial Intelligence Planning and Scheduling, AAAI Press, Menlo Park, CA, USA, 177\u2013186."},{"key":"S0269888910000160_ref16","doi-asserted-by":"crossref","unstructured":"Havelund K. , Groce A. , Holzmann G. , Joshi R. , Smith M. 2008. Automated testing of planning models. In Proceedings of the Fifth International Workshop on Model Checking and Artificial Intelligence, Lecture Notes in Artificial Intelligence. 5\u201317, Springer, Heidelberg, Germany.","DOI":"10.1007\/978-3-642-00431-5_6"},{"key":"S0269888910000160_ref25","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. 1999. Validating the DS1 remote agent experiment. In iSAIRAS-99. Proceeedings Fifth Int. Symposium on Artificial Intelligence, Robotics and Automation in Space, ESA\/ESTEC, Noordwijk, The Netherland."},{"key":"S0269888910000160_ref4","unstructured":"Cesta A. , Cortellessa G. , Fratini S. , Oddi A 2008. Looking for MrSPOCK: issues in deploying a space application. In SPARK-08. ICAPS Workshop on Scheduling and Planning Applications, Sydney, Australia."},{"key":"S0269888910000160_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"key":"S0269888910000160_ref27","unstructured":"Penix J. , Pecheur C. , Havelund K. 1998. Using model checking to validate AI planner domain models. In Proceedings of the 23rd Annual Software Engineering Workshop, Greenbelt, MD, USA."},{"key":"S0269888910000160_ref23","first-page":"5","article-title":"Verification and validation and artificial intelligence","volume":"65","author":"Menzies","year":"2005","journal-title":"Advances in Computers"},{"key":"S0269888910000160_ref31","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888907001063"},{"key":"S0269888910000160_ref30","unstructured":"Siminiceanu R. I. , Butler R. W. , Munoz C. A. 2008. Experimental evaluation of a planning language suitable for formal verification. In Proceedings of the Fifth International Workshop on Model Checking and Artificial Intelligence, Lecture Notes in Computer Science. Springer, Heidelberg, Germany, 18\u201334."},{"key":"S0269888910000160_ref32","doi-asserted-by":"crossref","unstructured":"Smith B. , Rajan K. , Muscettola N. 1997. Knowledge acquisition for the onboard planner of an autonomous spacecraft. In EKAW-97. 10th European Workshop on Knowledge Acquisition, Modeling and Management, volume 1319 of Lecture Notes in Computer Science, Lecture Notes in Computer Science. Springer, Heidelberg, Germany, 253\u2013268.","DOI":"10.1007\/BFb0026790"},{"key":"S0269888910000160_ref18","unstructured":"Howey R. , Long D. 2003. 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, 28\u201337, Trento, Italy, June."},{"key":"S0269888910000160_ref33","doi-asserted-by":"crossref","unstructured":"Smith B. , Millar W. , Dunphy J. , Tung Y.-W. , Nayak P. , Gamble E. , Clark M. 1999. Validation and verification of the remote agent for spacecraft autonomy. In Proceedings of IEEE Aerospace Conference, Morgan Kaufmann, San Francisco, CA, USA.","DOI":"10.1109\/AERO.1999.794352"},{"key":"S0269888910000160_ref6","first-page":"1086","volume-title":"AAAI-94. Proceedings of the Twelfth National Conference on Artificial Intelligence","author":"Cheng","year":"1994"},{"volume-title":"Intelligent Scheduling","year":"1994","author":"Muscettola","key":"S0269888910000160_ref24"},{"key":"S0269888910000160_ref22","doi-asserted-by":"crossref","unstructured":"McMillan K. L. 1993. Symbolic Model Checking. Massachusetts: Kluwer Academic Publishers, ISBN 0792393805.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"S0269888910000160_ref35","doi-asserted-by":"publisher","DOI":"10.1017\/S0269888900001089"},{"key":"S0269888910000160_ref10","unstructured":"Fox M. , Howey R. , Long D. 2005. Exploration of the robustness of plans. In VVPS-05. Proceedings of the ICAPS Workshop on Validation & Verification of Planning and Scheduling Systems, Monterey, CA, USA, 67\u201374."},{"key":"S0269888910000160_ref3","unstructured":"Cesta A. , Fratini S. 2008. The timeline representation framework as a planning and scheduling software development environment. In PlanSIG-08. Proceedings of the 27th Workshop of the UK Planning and Scheduling Special Interest Group, December 11\u201312, Edinburgh, UK."},{"volume-title":"The SPIN Model Checker: Primer and Reference Manual","year":"2004","author":"Holzmann","key":"S0269888910000160_ref17"},{"key":"S0269888910000160_ref29","unstructured":"R-Moreno M. D. , Brat G. , Muscettola N. , Rijsman D. 2007. Validation of a multi-agent architecture for planning and execution. In DX-07. Proceedings of 18th International Workshop on Principles of Diagnosis, Nashville, TN, USA, 368\u2013371."},{"key":"S0269888910000160_ref1","unstructured":"Abdedaim Y. , Asarin E. , Gallien M. , Ingrand F. , Lesire C. , Sighireanu M. 2007. Planning robust temporal plans: a comparison between CBTP and TGA approaches. In ICAPS-07. Proceedings of the Seventeenth International Conference on Automated Planning and Scheduling, The AAAI Press, Menlo Park, CA, USA, 2\u201310."},{"key":"S0269888910000160_ref2","unstructured":"Bensalem S. , Bozga M. , Krichen M. , Tripakis S. 2005. Testing Conformance of real-time applications: case of planetary rover controller. In VVPS-05. Proceedings of the ICAPS Workshop on Validation & Verification of Planning and Scheduling Systems, Monterey, CA, USA, 23\u201332."},{"key":"S0269888910000160_ref8","doi-asserted-by":"crossref","unstructured":"Cimatti A. , Clarke E. , Giunchiglia E. , Giunchiglia F. , Pistore M. , Roveri M. , Sebastiani R. , Tacchella A. 2002. NuSMV 2: an opensource tool for symbolic model checking. In CAV-02. 14th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science. Springer, Heidelberg, Germany.","DOI":"10.1007\/3-540-45657-0_29"},{"key":"S0269888910000160_ref14","unstructured":"Giannakopoulou D. , Pasareanu C. S. , Lowry M. , Washington R. 2005. Lifecycle verification of the NASA Ames K9 rover executive. In VVPS-05. Proceedings of the ICAPS Workshop on Validation & Verification of Planning and Scheduling Systems, Monterey, CA, USA, 75\u201385."}],"container-title":["The Knowledge Engineering Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0269888910000160","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T14:43:57Z","timestamp":1767624237000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0269888910000160\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["S0269888910000160"],"URL":"https:\/\/doi.org\/10.1017\/s0269888910000160","relation":{},"ISSN":["0269-8889","1469-8005"],"issn-type":[{"type":"print","value":"0269-8889"},{"type":"electronic","value":"1469-8005"}],"subject":[],"published":{"date-parts":[[2010,9]]}}}