自动机与流的结合：面向基于流的机器人任务与运动规划的时态逻辑编译
When Automata Meet Streams: Temporal Logic Compilation for Stream-Based Robotics Task and Motion Planning
AI总结：
该研究提出SAM-TD方法，将LTL_f约束编译为自动机并嵌入动作模式，实现基于流的TAMP对动态生成对象的时态约束处理，在机器人环境中验证了其可行性与竞争力。
AI中文摘要：
基于流的机器人任务与运动规划（TAMP）将离散符号规划与动态生成的连续几何参数（如位姿、抓取和轨迹）相集成。然而，基于流的规划器通常仅对目标可达性进行推理，而长程任务还需遵守时态规范，如安全关键的顺序、不变性和活性约束。目前尚无方法能为基于流的求解器强制执行此类时态约束，因为流会在规划过程中通过迭代流细化循环生成不断扩展的几何对象集，导致现有时态逻辑编译技术不兼容。因此，我们提出了带令牌销毁的同步动作监控（SAM-TD），这是一种在基于流的TAMP中强制执行任意有限迹线性时态逻辑（LTL_f）规范的编译方法。SAM-TD将任意LTL_f约束转换为自动机，并将回归后的自动机保护条件嵌入规划开始前预先指定的动作模式中。通过这种方式，SAM-TD可处理规划过程中流生成的对象，从而避免了枚举固定对象集或修改底层规划器的需求。在搜索过程中，SAM-TD同步更新自动机状态，并使用所有自动机共享的有效性令牌来剪枝违反约束的分支。我们证明SAM-TD支持规划搜索过程中迭代流细化产生的动态流对象。实验结果首次在三个机器人PDDLStream环境中展示了基于流的TAMP在LTL_f约束下的可行性。此外，在标准离散PDDL基准上，SAM-TD与最先进的时态约束编译方法具有竞争力。
英文摘要：
Stream-based robotics Task and Motion Planning (TAMP) integrates discrete symbolic planning with dynamically generated continuous geometric parameters, such as poses, grasps, and trajectories. However, stream-based planners typically reason only about goal reachability, whereas long-horizon tasks also demand adherence to temporal specifications, such as safety-critical ordering, invariance, and liveness constraints. No methods currently exist to enforce such temporal constraints for stream-based solvers because streams generate an expanding geometric object set via iterative stream refinement loops during planning, rendering existing temporal-logic compilation techniques incompatible. We therefore present Synchronous Action Monitoring with Token Destruction (SAM-TD), a compilation method that enforces arbitrary Linear Temporal Logic over finite traces ($\textrm{LTL}_f$) specifications in stream-based TAMP. SAM-TD translates arbitrary $\textrm{LTL}_f$ constraints into automata and embeds regressed automaton guards into action schemas, which are pre-specified before planning begins. By doing so, SAM-TD can handle objects generated by streams during planning, thus circumventing the need to enumerate a fixed object set or modify the underlying planner. During search, SAM-TD synchronously updates automaton states and uses a validity token shared across all automata to prune constraint-violating branches. We show that SAM-TD supports dynamically generated stream objects from iterative stream refinements during plan search. Experimental results provide the first ever demonstration of stream-based TAMP under $\textrm{LTL}_f$ constraints in three robotics PDDLStream environments. Furthermore, on standard discrete PDDL benchmarks, SAM-TD is competitive with state-of-the-art temporal-constraint compilation methods.
