在不确定环境中合成满足时序要求的智能体程序
LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments
- 用博弈论方法构建程序执行的有限博弈框架
- 确保在所有环境行为下都能满足LTLf时序规范
- 适用于有无限对象和非局部效应的复杂场景
我们研究了基于情境演算的Golog语言表达的高层智能体程序的策略合成问题，该语言包含非确定性编程构造。与传统假设完全控制或依赖增量搜索的方法不同，本文针对环境不确定性显著影响程序结果的场景。合成目标是推导出一个策略，使给定的Golog程序在所有可能的环境行为下均能成功执行，并满足线性时序逻辑在有限轨迹（LTLf）上的时序规范。通过利用一类一阶动作理论，我们构建了一个封装程序执行过程并追踪时序目标满足情况的有限博弈框架，并采用博弈论方法求解策略。实验表明该方法在具有无界对象和非局部效应的领域中具备可行性。本工作连接了智能体编程与时序逻辑合成，为不确定环境下的鲁棒智能体行为提供了统一框架。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。