: Peter Baumgartner, Sylvie Thiébaux, and Felipe Trevizan.
Heuristic Search Planning With Multi-Objective Probabilistic LTL Constraints.
In Frank Wolter Michael Thielscher, Francesca Toni, editor, KR-2018 -- 16th International Conference on Principles of Knowledge Representation and Reasoning, pages 415--424. AAAI Press, 2018.
AAAI Press.
Correction: The complexity result in Theorem 4 is incorrect. The incorrectnes is based on an oversight in the use of a Tseitin-style CNF transformation when progressing LTL formulas to the next state. A correct progression-based algorithm, of higher complexity though, employs standard CNF instead. The soundness theorem (Theorem 5), and completeness theorem (Theorem 6) still apply with that correction. Moreover, and importantly, it is such a correct version that we had implemented and used in our experiments. The experimental results, hence, are not affected by the incorrectnes, and neither are the other results. [ bib | .pdf ]
We present an algorithm for computing cost-optimal stochastic policies for Stochastic Shortest Path problems (SSPs) subject to multi-objective PLTL constraints, i.e., conjunctions of probabilistic LTL formulas. Established algorithms capable of solving this problem typically stem from the area of probabilistic verification, and struggle with the large state spaces and constraint types found in automated planning. Our approach differs in two crucial ways. Firstly it operates entirely on-the-fly, bypassing the expensive construction of Rabin automata for the formulas and their prohibitive prior synchronisation with the full state space of the SSP. Secondly, it extends recent heuristic search algorithms and admissible heuristics for cost-constrained SSPs, to enable pruning regions made infeasible by the PLTL constraints. We prove our algorithm correct and optimal, and demonstrate encouraging scalability results.