LTLf Adaptive Synthesis for Multi-Tier Goals in Nondeterministic Domains
Giuseppe De Giacomo, Gianmarco Parretti, Shufang Zhu
TL;DR
This work addresses synthesizing adaptive strategies for multi-tier LTL_f goals in fully observable nondeterministic domains. It formalizes maximally winning and maximally pending objectives to drive a game-theoretic synthesis that enforces enforceable goals while exploiting environmental cooperation to achieve additional objectives, with a quadratic overhead in the number of objectives. The proposed approach remains as hard as standard $\texttt{LTL}_f$ synthesis in the domain size (2EXPTIME) but scales polynomially (quadratically) with the count of objectives, enabling practical handling of multi-tier preferences. By combining best-effort single-objective techniques with on-the-fly DFA-game analyses, the method yields sound, complete adaptive strategies and supports parallel computation for scalability. The illustrated robot-navigation example demonstrates how adaptivity enables pursuing temporal preferences without sacrificing the satisfaction of harder, early objectives. Overall, the framework promises scalable, preference-aware planning in nondeterministic environments and provides a foundation for extending to multiple environment models and symbolic implementations.
Abstract
We study a variant of LTLf synthesis that synthesizes adaptive strategies for achieving a multi-tier goal, consisting of multiple increasingly challenging LTLf objectives in nondeterministic planning domains. Adaptive strategies are strategies that at any point of their execution (i) enforce the satisfaction of as many objectives as possible in the multi-tier goal, and (ii) exploit possible cooperation from the environment to satisfy as many as possible of the remaining ones. This happens dynamically: if the environment cooperates (ii) and an objective becomes enforceable (i), then our strategies will enforce it. We provide a game-theoretic technique to compute adaptive strategies that is sound and complete. Notably, our technique is polynomial, in fact quadratic, in the number of objectives. In other words, it handles multi-tier goals with only a minor overhead compared to standard LTLf synthesis.