Abstract
We are concerned with the synthesis of strategies for sequential decision-making in nondeterministic 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