Flexible Plan Verification: Feasibility Results

• Autorzy: Cesta A. , Fratini S. , Orlandini A. , Finzi A. , Tronci E.
• Języki publikacji: EN

Abstrakty

EN

Timeline-based planning techniques have demonstrated wide application possibilities in heterogeneous real world domains. For a wider diffusion of this technology, a more thorough investigation of the connections with formal methods is needed. This paper is part of a research program aimed at studying the interconnections between timeline-based planning and standard techniques for formal validation and verification (V&V). In this line, an open issue consists of studying the link between plan generation and plan execution from the particular perspective of verifying temporal plans before their actual execution. The present work addresses the problem of verifying flexible temporal plans, i.e., those plans usually produced by least-commitment temporal planners. Such plans only impose minimal temporal constraints among the planned activities, hence are able to adapt to on-line environmental changes by trading some of the retained flexibility. This work shows how a model-checking verification tool based on Timed Game Automata (TGA) can be used to verify such plans. In particular, flexible plan verification is cast as a model-checking problem on those automata. The effectiveness of the proposed approach is shown by presenting a detailed experimental analysis with a real world domain which is used as a flexible benchmark

Słowa kluczowe

EN

timeline-based planning; validation and verification; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 107, nr 2/3
• Strony: 111--137
• Opis fizyczny: Bibliogr. 30 poz., tab., wykr.

Twórcy

autor

Cesta A.

autor

Fratini S.

autor

Orlandini A.

autor

Finzi A.

autor

Tronci E.

• Consiglio Nazionale delle Ricerche, Istituto di Scienze e Tecnologie della Cognizione Via S.Martino della Battaglia 44, I-00185 Rome, Italy,

Bibliografia

• [1] Abdedaim, Y., Asarin, E., Gallien, M., Ingrand, F., Lesire, C., Sighireanu, M.: Planning Robust Temporal Plans: A Comparison Between CBTP and TGA Approaches, ICAPS-07. Proc. of the Seventeenth International Conference on Automated Planning and Scheduling, 2007.
• [2] Alur, R., Dill, D. L.: A Theory of Timed Automata, Theoretical Computer Science, 126, 1994, 183-235.
• [3] Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K. G., Lime, D.: UPPAAL-TIGA: Time for Playing Games!, in: CAV-07. Proc. of Computer Aided Verification, number 4590 in Lecture Notes in Computer Science, Springer, 2007, 121-125.
• [4] Cassez, F., David, A., Fleury, E., Larsen, K. G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games, CONCUR 2005, Springer-Verlag, 2005.
• [5] Cesta, A., Cortellessa, G., Fratini, S., Oddi, A.: MRSPOCK: Steps in Developing an End-to-End Space Application, Computational Intelligence, 2010, Accepted for publication.
• [6] Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Flexible Timeline-Based Plan Verification, in: KI-09, vol. 5803 of Lecture Notes in Artificial Intelligence, Springer, 2009, 49-56.
• [7] Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Validation and Verification Issues in a Timeline-Based Planning System, Knowledge Engineering Review, 2010, 25, pp 299-318.
• [8] Cesta, A., Finzi, A., Fratini, S., Orlandini, A., Tronci, E.: Analyzing Flexible Timeline-Based Plans, ECAI-10. Procedings of the 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 2010.
• [9] Cesta, A., Fratini, S., Oddi, A., Pecora, F.: APSI Case#1: Pre-planning Science Operations in MARS EXPRESS, i-SAIRAS-08. Proc. of the 9th Int. Symp. on Artificial Intelligence, Robotics and Automation in Space, JPL, Pasadena, CA, 2008.
• [10] Cesta, A., Oddi, A.: DDL.1: A Formal Description of a Constraint Representation Language for Physical Domains,, in: New Directions in AI Planning (M. Ghallab, A. Milani, Eds.), IOS Press: Amsterdam, 1996, 341-452.
• [11] Chien, S., Tran, D., Rabideau, G., Schaffer, S., Mandl, D., Frye, S.: Timeline-Based Space Operations Scheduling with External Constraints, ICAPS-10. Proc. of the Twentieth International Conference on Automated Planning and Scheduling, 2010.
• [12] Clarke, E. M., Grumberg, O., Peled, D. A.: Model Checking, The MIT Press, 1999.
• [13] Frank, J., Jonsson, A.: Constraint Based Attribute and Interval Planning, Journal of Constraints, 8(4), 2003, 339-364.
• [14] Hoare, C. A. R.: Communicating Sequential Processes, Commun. ACM, 26(1), 1983, 100-106.
• [15] Howey, R., Long, D.: VAL's Progress: The Automatic Validation Tool for PDDL2.1 Used in the International Planning Competition, Proc. of the ICAPS Workshop on The Competition: Impact, Organization, Evaluation, Benchmarks, Trento, Italy, June 2003.
• [16] Jonsson, A., Morris, P., Muscettola, N., Rajan, K., Smith, B.: Planning in Interplanetary Space: Theory and Practice, AIPS-00. Proc. of the Fifth Int. Conf. on Artificial Intelligence Planning and Scheduling, 2000.
• [17] Khatib, L., Muscettola, N., Havelund, K.: Mapping Temporal Planning Constraints into Timed Automata, TIME-01. The Eigth Int. Symposium on Temporal Representation and Reasoning, 2001.
• [18] Larsen, K., Pettersson, P., Yi, W.: Compositional and Symbolic Model-Checking of Real-time Systems, Real-Time Systems Symposium, IEEE International, 0, 1995, 76, ISSN 1052-8725.
• [19] Larsen, K. G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell, International Journal on Software Tools for Technology Transfer, 1(1-2), 1997, 134-152.
• [20] Maler, O., Pnueli, A., Sifakis, J.: On the Synthesis of Discrete Controllers for Timed Systems, STACS, LNCS, Springer, 1995.
• [21] Milner, R.: Communication and Concurrency, Prentice-Hall, Inc., 1989, ISBN 0-13-115007-3.
• [22] Morris, P. H., Muscettola, N.: Temporal Dynamic Controllability Revisited, AAAI-05. Proc. of the Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, Pittsburgh, Pennsylvania, USA, 2005.
• [23] Morris, P. H., Muscettola, N., Vidal, T.: Dynamic Control of Plans With Temporal Uncertainty, IJCAI-01. Proc. of the Seventeenth International Joint Conference on Artificial Intelligence, Seattle, Washington, USA, 2001.
• [24] Muscettola, N.: HSTS: Integrating Planning and Scheduling, in: Intelligent Scheduling (Zweben, M. and Fox, M.S., Ed.), Morgan Kauffmann, 1994, 169-212.
• [25] Muscettola, N., Smith, S., Cesta, A., D'Aloisi, D.: Coordinating Space Telescope Operations in an Integrated Planning and Scheduling Architecture, IEEE Control Systems, 12(1), 1992, 28-37.
• [26] Sistla, A. P., Clarke, E. M.: The Complexity of Propositional Linear Temporal Logics, J. ACM, 32(3), 1985, 733-749, ISSN 0004-5411.
• [27] Smith, D., Frank, J., Jonsson, A.: Bridging the Gap Between Planning and Scheduling, Knowledge Engineering Review, 15(1), 2000, 47-83.
• [28] Vidal, T.: Controllability Characterization and Checking in Contingent Temporal Constraint Networks, KR-00. Principles of Knowledge Representation and Reasoning Proc. of the Seventh International Conference, Breckenridge, Colorado, USA, 2000.
• [29] Vidal, T., Fargier, H.: Handling Contingency in Temporal Constraint Networks: From Consistency To Controllabilities, JETAI, 11(1), 1999, 23-45.
• [30] Yovine, S.: Model Checking Timed Automata, in: Lectures on Embedded Systems, vol. 1494 of Lecture Notes in Computer Science, Springer, 1998, 114-152.