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.