Planning in Real-Time Domains with Timed CTL Goals via Symbolic Model Checking

Current methods for planning in real-time environments only consider planning goals with a restricted expressiveness, even those using the temporal logic Timed CTL (TCTL). These approaches support TCTL subsets expressing rather simple reachability goals and safety properties, but do not allow the arbitrary nesting and conjunction of TCTL formulas. However, this is a serious drawback in many practical applications. An example are medical systems that have to repeat an action infinitely often within given time bounds. To close this gap, we provide an algorithm for planning with these goals by adapting concepts from symbolic model checking. Hence, we can automatically generate plans fulfilling more complex tasks within a real-time context, while improving safety and efficiency by using formally founded model checking methods.