Generating Controllers for Flexible Plan Execution: a TGA approach

In temporal Planning and Scheduling (P&S) system, the synthesized plans may be temporally flexible and partially specified, therefore they need suitable executive systems for proper on-line execution. In general, instantiating and executing a temporally flexible plan is not an easy task due to constraint propagation and controllability issues. Previous works have tackled these problems by reasoning on the temporal constraints networks underlying the constraint-based plan representation often used by such systems. However, these issues can be addressed from a more abstract and general point of view deploying formal modeling and formal methods. In this work, we pursue such a second direction by presenting a formal method to synthesize a controller associated with a generated flexible temporal plan. Controller synthesis exploits Timed Game Automata (TGA) for formal modeling and UPPAAL-TIGA as a model checker. We present the method discussing both formal and empirical issues. The collected empirical results show the practical feasibility of the approach in a real-world robotic case study.