在雾中确保逻辑：基于LTL目标的可靠POMDP合成

合成能够在不确定环境中导航且遵循复杂时序约束的自主智能体，仍是一项基本挑战。虽然线性时序逻辑（LTL）为指定此类任务提供了严密的语言，但线性时序逻辑满足性在部分可观测马尔可夫决策过程中的定性验证固具有不可判定性，这使得定量合成尤其在设计可靠奖励信号以支持近似求解器时变得困难。本文通过一种新颖的、具有可靠性的奖励调制机制来弥合这一差距，该机制动态生成基于认证LTL满足性的信念相关奖励。通过将该机制集成到增强型蒙特卡洛规划框架中，我们使智能体能够在部分可观测性的“雾”中进行导航，专注于最大化可验证成功的搜索过程。我们的实验表明，这种方法不仅在现有求解器失败的场景中表现出色，还在多样化的基准领域中保持有效性和可扩展性。