Strong Fully Observable Non-Deterministic Planning with LTL and LTLf Goals

Strong Fully Observable Non-Deterministic Planning with LTL and LTLf Goals

Alberto Camacho, Sheila A. McIlraith

Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence
Main track. Pages 5523-5531. https://doi.org/10.24963/ijcai.2019/767

We are concerned with the synthesis of strategies for sequential decision-making in non-deterministic dynamical environments where the objective is to satisfy a prescribed temporally extended goal. We frame this task as a Fully Observable Non-Deterministic planning problem with the goal expressed in Linear Temporal Logic (LTL), or LTL interpreted over finite traces (LTLf). While the problem is well-studied theoretically, existing algorithmic solutions typically compute so-called strong-cyclic solutions, which are predicated on an assumption of fairness. In this paper we introduce novel algorithms to compute so-called strong solutions, that guarantee goal satisfaction even in the absence of fairness. Our strategy generation algorithms are complemented with novel mechanisms to obtain proofs of unsolvability. We implemented and evaluated the performance of our approaches in a selection of domains with LTL and LTLf goals.
Keywords:
Planning and Scheduling: Planning Algorithms
Planning and Scheduling: Planning under Uncertainty
Planning and Scheduling: Planning and Scheduling