Golog is an expressive high-level agent language that includes nondeterministic operators which allow to leave some of the decisions to be made only at execution time. This so-called program realization is typically implemented by means of search, or in an incremental online fashion. In this paper, we consider the more realistic case where parts of the non-determinism are under the control of the environment. Program realization then becomes a synthesis problem, where a successful realization executes the program and satisfies the temporal goal for all possible environment actions. We consider Golog programs in combination with an expressive class of first-order action theories that allow for an unbounded number of objects and non-local effects, together with a temporal goal specified in a first-order extension of LTLf. We solve the synthesis problem by constructing a game arena that captures all possible executions of the program while tracking the satisfaction of the temporal goal and then solving the resulting two-player game. We evaluate the approach in two domains, showing the general feasibility of the approach.

翻译：Golog是一种表达能力较强的高层智能体语言，其包含的非确定性算子允许将部分决策推迟至执行阶段。这类所谓的程序实现通常通过搜索方式实现，或以增量在线方式完成。本文考虑更为现实的情形：部分非确定性由环境控制。此时程序实现转化为一个综合问题，即成功的实现需在程序执行过程中，针对所有可能的环境动作均满足时序目标。我们结合具有无界对象数量和非局部效应表达能力的一阶动作理论来研究Golog程序，其时序目标采用LTLf的一阶扩展进行描述。通过构建能捕获程序所有可能执行路径并追踪时序目标满足状态的博弈竞技场，进而求解所得的双人博弈问题，我们解决了该综合问题。我们在两个领域对该方法进行评估，验证了该方法的总体可行性。