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.

翻译：本文研究了基于Golog语言的高层智能体程序策略综合问题。Golog是一种基于情境演算并包含非确定性编程结构的语言。与传统程序实现方法（假设智能体具有完全控制权或依赖增量搜索）不同，我们关注环境非确定性显著影响程序执行结果的场景。我们的综合问题旨在推导出一种策略，该策略需成功实现给定的Golog程序，同时确保在有限迹上的线性时序逻辑（LTLf）所表达的时序规约在所有可能的环境行为下均得到满足。通过利用一类表达能力丰富的一阶动作理论，我们构建了一个有限博弈场，该博弈场封装了程序执行过程并追踪时序目标的满足状态。我们采用博弈论方法来推导此类策略。实验结果表明，该方法在具有无界对象和非局部效应的领域中具有可行性。本工作搭建了智能体编程与时序逻辑综合之间的桥梁，为非确定性环境中的鲁棒智能体行为提供了一个理论框架。