Planning meets verification and validation in a knowledge engineering environment

The attention for the area of formal methods has significantly increased in AI over last years. The spreading of applications in many real life sectors raised the need for features like robustness, structural guarantee, and safety criticality. Application areas where planning techniques have been successfully deployed are among those that require such formal properties, this motivates our interest in integrating planning and formal methods for verification and validation. In this perspective, this paper describes the integration of Verification and Validation formal techniques within an environment for Knowledge Engineering of Planning with Timelines called KeeN. The system integrates "classical" knowledge engineering features, like those that support users when defining a planning domain, with services that enable domain model validation, planner validation, plan verification, etc. The particular verification and validation capabilities are obtained by exploiting a state-of-the-art verification tool, i.e., UPPAAL-TIGA, to support the design and development of timeline-based planning systems. Distinctive of the framework are the features that assist the plan execution phase, like, for example, those for the automated synthesis of controllers.