Validation and Verification issues in Timeline-based Planning and Scheduling Systems

Planning and Scheduling (P&S) systems have been deployed in several application domains. Most of these results have been achieved by small group of specialists molding their own specialized know-how. A key objective pursued in the P&S Knowledge Engineering sub community is the synthesis of software environments that would allow the development of applications to people that, as a minimum, are not “leading edge” specialist. Example of such environments are ITSIMPLE (Vaquero et al. 2013), GIPO (Simpson, Kitchin, and McCluskey 2007b), and EUROPA (Barreiro et al. 2012).


Over the last year and a half we have been developing our own Knowledge Engineering ENvironment (KEEN) that is built around the state of the art framework for P&S with timelines called APSI-TRF (Cesta et al. 2009). The particular perspective we are pursuing with KEEN is the one of integrating classical knowledge engineering features connected to support for domain definition, domain refinement, etc. with services of automated Validation and Verification (V&V) techniques as those surveyed in (Cesta et al. 2010b). 

This research stream would show the possible role of V&V techniques in domain validation, planner validation, plan verification etc. 

Some further motivation for our work comes from a project in robot autonomy (Ceballos et al. 2011) that pushed us to better investigate problems of robustness of plans at execution time. In particular, working on the representation of flexible temporal plans, that is the key feature of a timeline-based representation, we have obtained results related to checking the dynamic controllability property (Cesta et al. 2010a; 2011) as well as to automatically generate robust plan controllers (Orlandini et al. 2011b). In those works, the problem of verifying flexible plans has been addressed considering an abstract plan view as a set of timelines with formal tools like model checkers. Then, the flexible plan verification problem has been translated in a model checking problem with Timed Game Automata (TGA), exploiting UPPAAL-TIGA (Behrmann et al. 2007) as verification tool. The goal pursued with KEEN synthesis is to obtain an integrated environment where all these results can be situated in a rational tool design and their use facilitated by the software environment.

In a very early paper (Orlandini et al. 2011a) we described the general idea and a sketchy plan to develop KEEN as situated within the GOAC robotic project for ESA (Ceballos et al. 2011). The current paper describes aspects of the current environment. In particular we describe new features of the environment for Domain Definition and Visualization and then some of the V&V tools at work starting from the defined domain. To make the example more concrete we have used as a running example the GOAC domain where we have accumulated quite an amount of basic knowledge.




Barreiro, J.; Boyce, M.; Do, M.; Franky, J.; Iatauro, M.; Kichkaylo, T.; Morris, P.; Ong, J.; Remolina, E.; Smith, T.; and Smith, D. 2012. EUROPA: A Platform for AI Planning, Scheduling, Constraint Programming, and Optimization. In ICKEPS 2012: the 4th Int. Competition on Knowledge Engineering for Planning and Scheduling.

Behrmann, G.; Cougnard, A.; David, A.; Fleury, E.; Larsen, K.; and Lime, D. 2007. UPPAAL-TIGA: Time for playing games! In Proc. of CAV-07, number 4590 in LNCS, 121–125. Springer.

Ceballos, A.; Bensalem, S.; Cesta, A.; de Silva, L.; Fratini, S.; Ingrand, F.; Ocon, J.; Orlandini, A.; Py, F.; Rajan, K.; Rasconi, R.; and vanWinnendael, M. 2011. A Goal-Oriented Autonomous Controller for Space Exploration. In ASTRA-11. 11th Symposium on Advanced Space Technologies in Robotics and Automation.

Cesta, A.; Cortellessa, G.; Fratini, S.; and 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.

Cesta, A.; Finzi, A.; Fratini, S.; Orlandini, A.; and Tronci, E. 2010a. Analyzing Flexible Timeline Plan. In ECAI 2010. Proceedings of the 19th European Conference on Artificial Intelligence, volume 215. IOS Press.

Cesta, A.; Finzi, A.; Fratini, S.; Orlandini, A.; and Tronci, E. 2010b. Validation and Verification Issues in a Timeline-Based Planning System. Knowledge Engineering Review 25(3):299–318.

Cesta, A.; Finzi, A.; Fratini, S.; Orlandini, A.; and Tronci, E. 2011. Flexible plan verification: Feasibility results. Fundamenta Informaticae 107:111–137.

Chien, S.; Tran, D.; Rabideau, G.; Schaffer, S.; Mandl, D.; and Frye, S. 2010. Timeline-Based Space Operations Scheduling with External Constraints. In ICAPS-10. Proc. of the 20th International Conference on Automated Planning and Scheduling.

Chien, S. A.; Johnston, M.; Frank, J.; Giuliano, M.; Kavelaars, A.; Lenzen, C.; and Policella, N. 2012. A Generalized Timeline Representation, Services, and Interface for Automating Space Mission Operations. In SpaceOps.

Orlandini, A.; Finzi, A.; Cesta, A.; Fratini, S.; and Tronci, E. 2011a. Enriching APSI with Validation Capabilities: the KEEN environment and its use in Robotic. In ASTRA 2011. Proc. of 11th Symposium on Advanced Space Technologies in Robotics and Automation. Noordwijk, the Netherlands.

Orlandini, A.; Finzi, A.; Cesta, A.; and Fratini, S. 2011b. Tga-based controllers for flexible plan execution. In KI 2011: Advances in Artificial Intelligence, 34th Annual German Conference on AI., volume 7006 of Lecture Notes in Computer Science, 233– 245. Springer.

Simpson, R. M.; Kitchin, D. E.; and McCluskey, T. L. 2007b. Planning Domain Definition Using GIPO. Knowledge Eng. Review 22(2):117–134.

Vaquero, T. S.; Silva, J. R.; Tonidandel, F.; and Beck, J. C. 2013. itsimple: Towards an integrated design system for real planning applications. The Knowledge Engineering Review.