Hostname: page-component-586b7cd67f-t8hqh Total loading time: 0 Render date: 2024-11-21T09:29:50.507Z Has data issue: false hasContentIssue false
  • English
  • Français

Validation and verification issues in a timeline-based planning system

Published online by Cambridge University Press:  01 September 2010

Amedeo Cesta ,
Alberto Finzi ,
Simone Fratini ,
Andrea Orlandini  and
Enrico Tronci
Amedeo Cesta*
Affiliation:
Consiglio Nazionale delle Ricerche, Istituto di Scienze e Tecnologie della Cognizione, Via S.Martino della Battaglia 44, I-00185 Rome, Italy; e-mail: name.surname@istc.cnr.it
Alberto Finzi*
Affiliation:
Dipartimento di Scienze Fisiche, Universitá adi Napoli “Federico Secondo”, Via Cinthia, I-80126 Naples, Italy; e-mail: finzi@na.infn.it
Simone Fratini*
Affiliation:
Consiglio Nazionale delle Ricerche, Istituto di Scienze e Tecnologie della Cognizione, Via S.Martino della Battaglia 44, I-00185 Rome, Italy; e-mail: name.surname@istc.cnr.it
Andrea Orlandini*
Affiliation:
Dipartimento di Informatica e Automazione, Universitá adi Roma Tre, Via della Vasca Navale 79, I-00146 Rome, Italy; e-mail: orlandin@dia.uniroma3.it
Enrico Tronci*
Affiliation:
Dipartimento di Informatica, Universitá adi Roma “La Sapienza”, Via Salaria 198, I-00198 Rome, Italy; e-mail: tronci@di.uniroma1.it
Get access Rights & Permissions [Opens in a new window]

Abstract

To foster effective use of artificial intelligence planning and scheduling (P&S) 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 P&S systems often bring solutions to the users that are neither ‘obvious’ 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 (V&V) capabilities in such environments may potentially enhance the users’ trust in the technology. Somehow, V&V techniques may represent a complementary technology, with respect to P&S, that contributes to developing richer software environments to synthesize a new generation of robust problem-solving applications. The integration of V&V and P&S techniques in a knowledge engineering environment is the topic of this paper. In particular, it analyzes the use of state-of-the-art V&V 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 V&V to planning. Hence, it continues by describing the step of adding V&V 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.

Type
Articles
Information
The Knowledge Engineering Review , Volume 25 , Special Issue 3: Planning and scheduling , September 2010 , pp. 299 - 318
Copyright
Copyright © Cambridge University Press 2010

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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–10.Google Scholar
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–32.Google Scholar
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–12, Edinburgh, UK.Google Scholar
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.Google Scholar
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.Google Scholar
Cheng, C.-C., Smith, S. F. 1994. Generating feasible schedules under complex metric constraints. In AAAI-94. Proceedings of the Twelfth National Conference on Artificial Intelligence, AAAI Press/MIT Press, Cambridge, MA, USA, 1086–1091.Google Scholar
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–85.Google Scholar
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.CrossRefGoogle Scholar
Clarke, E. M., Grumberg, O., Peled, D. A. 1999. Model Checking. The MIT Press.Google Scholar
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–74.Google Scholar
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.Google Scholar
Frank, J., Jonsson, A. 2003. Constraint based attribute and interval planning. Journal of Constraints 8(4), 339–364.Google Scholar
Fratini, S., Pecora, F., Cesta, A. 2008. Unifying planning and scheduling as timelines in a component-based perspective. Archives of Control Sciences 180(2), 231–271.Google Scholar
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–85.Google Scholar
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.CrossRefGoogle Scholar
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–17, Springer, Heidelberg, Germany.Google Scholar
Holzmann, G. J. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison Wesley.Google Scholar
Howey, R., Long, D. 2003. VAL’s 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–37, Trento, Italy, June.Google Scholar
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–186.Google Scholar
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–27.Google Scholar
Larsen, K. G., Pettersson, P., Yi, W. 1997. UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 10(1–2), 134–152.CrossRefGoogle Scholar
McMillan, K. L. 1993. Symbolic Model Checking. Massachusetts: Kluwer Academic Publishers, ISBN 0792393805.Google Scholar
Menzies, T., Pecheur, C. 2005. Verification and validation and artificial intelligence. Advances in Computers 65, 5–45.Google Scholar
Muscettola, N. 1994. HSTS: integrating planning and scheduling. In Zweben, M. & Fox, M. S. (eds), Intelligent Scheduling. Morgan Kauffmann.Google Scholar
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.Google Scholar
Pecheur, C., Simmons, R. G. 2001. From livingstone to SMV. In FAABS-00. Proceedings of the First International Workshop on Formal Approaches to Agent-Based Systems—Revised Papers, 103–113, London, UK: Springer-Verlag. ISBN 3-540-42716-3.Google Scholar
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.Google Scholar
Preece, A. 2001. Evaluating verification and validation methods in knowledge engineering. In Micro-level Knowledge Management, Roy, R. (ed.). Morgan-Kaufman, 123–145.Google Scholar
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–371.Google Scholar
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–34.Google Scholar
Simpson, R. M., Kitchin, D. E., McCluskey, T. L. 2007. Planning domain definition using GIPO. The Knowledge Engineering Review 22(2), 117–134.Google Scholar
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–268.Google Scholar
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.Google Scholar
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–263.Google Scholar
Smith, D., Frank, J., Jonsson, A. 2000b. Bridging the gap between planning and scheduling. Knowledge Engineering Review 150(1), 47–83.CrossRefGoogle Scholar
Smith, M. H., Holzmann, G. J., Cucullu, G. C., Smith, B. D. 2005. Model checking autonomous planners: even the best laid plans must be verified. In Proceedings of IEEE Aerospace Conference. IEEE Computer Society, 1–11.Google Scholar
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–402.Google Scholar