Verifying Flexible Timeline-Based Plans

The synthesis of flexible temporal plans has demonstrated wide applications possibilities in heterogeneous domains. We are currently studying the connection between plan genera-tion and execution from the particular perspective of verifying a flexible plan before actual execution. This paper explores how a model-checking verification tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. We first describe the formal model, the formalism, and the verifi-cation method. Furthermore we discuss our own approach and some preliminary empirical results using a real-world case study