Flexible Plan Verification: Feasibility Results

Timeline-based planning techniques have demonstrated wide application possibilities in heterogeneous domains. However, a problem for a wider diffusion of such technology still stems in the reduced community that has been studying formal properties of this planning approach. In this sense, we are currently studying the connection between plan generation and execution from the particular perspective of verifying a flexible plan before its actual execution. Nevertheless, a complexity issue should be considered. In fact, validation and verification processes usually exploit formal methods, such as model-checking, that present hard complexity. In this work, we explore how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. In particular, we show the feasibility of our own approach by reporting some preliminary empirical results gathered in a real-world case study.