LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments

TL;DR

This paper presents a novel method for synthesizing policies for high-level agent programs in nondeterministic environments, ensuring temporal logic goals are met using a game-theoretic approach.

Contribution

It introduces a framework combining Golog, first-order action theories, and LTLf synthesis to generate robust agent policies under environmental nondeterminism.

Findings

Feasibility demonstrated in domains with unbounded objects

Effective handling of non-local effects in environment

Bridges agent programming with temporal logic synthesis

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.