LTLf Adaptive Synthesis for Multi-Tier Goals in Nondeterministic Domains
This work addresses the challenge of dynamic goal satisfaction in planning for AI systems, though it is incremental as it builds on existing LTLf synthesis frameworks.
The paper tackles the problem of synthesizing adaptive strategies for achieving multi-tier goals in nondeterministic domains, using LTLf synthesis, and presents a polynomial-time game-theoretic technique that is sound and complete with only quadratic overhead compared to standard methods.
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.