Generalizing Platform-Aware Mission Planning for Infinite-State Timed Transition Systems

The Platform-Aware Mission Planning (PAMP) problem, formalizes the relationship between an automated temporal planning problem and an execution platform modeled as a Timed Automaton. The PAMP problem consists in finding a valid plan that guarantees the plan executability and the satisfaction of a safety property on the platform, regardless of non-determinism. In this paper, we significantly generalize the PAMP problem along three directions. First, we consider platforms represented as infinite state timed transition systems (TTSs), allowing a more natural and expressive modeling of realistic systems. Second, we introduce a new feature to model relations between the fluents of the planning problem and the platform variables. Finally, we generalize the semantics to cope with unbounded traces. We define a solution method for the resulting generalized PAMP, combining an automated temporal planner and an infinite-state model-checker. Our method is largely more efficient than the existing approach for bounded PAMP problems, despite being strictly more expressive.