LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments
Till Hofmann, Jens Claßen
TL;DR
This work advances the synthesis of policies for high-level agent programs by integrating Golog, a first-order action language, with LTLf specifications in nondeterministic environments. It introduces a decidable fragment based on acyclic Basic Action Theories and a finite game arena that encodes program executions and temporal goals, enabling a policy to realize a given Golog program across all environmental behaviors. The approach hinges on characteristic graphs, world types, and on-the-fly TNF/XNF transformations to track satisfaction of the LTLf specification, solved via game-theoretic strategy synthesis. Experiments in dishwasher and warehouse domains demonstrate feasibility and reveal scalability challenges, particularly due to nondeterministic effects and state-space blow-ups, while pointing to future work on symmetry detection and optimization. Overall, the framework bridges agent programming and temporal-logic synthesis, enabling robust, environment-responsive execution of complex, parameterized tasks.
Abstract
We investigate the synthesis of policies for high-level agent programs expressed in Golog, a language based on situation calculus that incorporates nondeterministic programming constructs. Unlike traditional approaches for program realization that assume full agent control or rely on incremental search, we address scenarios where environmental nondeterminism significantly influences program outcomes. Our synthesis problem involves deriving a policy that successfully realizes a given Golog program while ensuring the satisfaction of a temporal specification, expressed in Linear Temporal Logic on finite traces (LTLf), across all possible environmental behaviors. By leveraging an expressive class of first-order action theories, we construct a finite game arena that encapsulates program executions and tracks the satisfaction of the temporal goal. A game-theoretic approach is employed to derive such a policy. Experimental results demonstrate this approach's feasibility in domains with unbounded objects and non-local effects. This work bridges agent programming and temporal logic synthesis, providing a framework for robust agent behavior in nondeterministic environments.