This paper describes the exploitation of a Validation and Verification technique aiming at enriching the support capabilities of the KnowledgE ENgineering (KEEN) software environment. In particular, the work reports on the formal synthesis of a plan controller associated to a flexible temporal plan. The controller synthesis exploits Timed Game Automata (TGA) for formal modeling and UPPAAL-TIGA as a model checker. The paper introduces a detailed experimental analysis on a real-world case study demonstrating the viability of the approach. In particular, it is shown how the controller synthesis overhead is compatible with the performance expected from a short horizon planner.
Using Validation and Verification Techniques for Robust Plan Execution
Contributo in atti di convegno
ESA, Noordwijk, NLD
International Symposium on Artificial Intelligence, Robotics and Automation in Space 2012, pp. 8, Torino, 4-6 September 2012