Optimality properties of planning via Petri net unfolding: A formal analysis

We provide a theoretical analysis of planning via Petri net unfolding, a novel technique for synthesising parallel plans. Parallel plans are generally valued for their execution flexi-bility, which manifests as alternative choices for the order-ing of operators and potentially faster plan executions. Being a relatively new approach, the flexibility properties of plans synthesised via unfolding, and even the concurrency seman-tics supported by this technique, are particularly unclear and only understood at an informal level. In this paper, we first formally characterise the concurrency semantics of planning via unfolding as a further restriction on the standard notion of independence. More importantly, we then prove that plans obtained using this approach are optimal deorderings and op-timal reorderings in terms of the number of ordering con-straints on operators and plan execution time, respectively. These results provide objective guarantees on the quality of plans obtained by the unfolding technique