Flexible TimelineBased Plan Verification

Abstract. Flexible temporal planning is a general technique that has demon-strated wide applications possibilities in heterogeneous domains. A key problem for widening applicability of these techniques is the robust connection between plan generation and execution. This paper describes how a model-checking veri-fication tool, based on UPPAAL-TIGA, is suitable for verifying flexible temporal plans. Moreover, we further investigate a particular perspective, i.e., the one of verifying dynamic controllability before actual plan execution.