用时序逻辑规范机器人行为，确保其在真实环境中的可靠运行。
Temporal logics and formal synthesis for robot planning and control
- 采用线性与信号时序逻辑描述机器人随时间变化的行为需求。
- 结合形式化合成方法，生成可验证的规划与控制策略。
- 适合需要高可靠性保障的自动驾驶、服务机器人等场景。
随着机器人从受控环境走向真实世界，确保其按预期运行变得愈发关键。核心在于对期望行为进行严格规范，捕捉复杂的时序、空间与逻辑要求。同时，需借助可证明保证的规划与控制合成方法来实现这些规范。本文介绍时序逻辑（特别是线性时序逻辑和信号时序逻辑）作为表达机器人随时间行为的有力工具。随后讨论形式化合成的基本原理，涵盖基于图与博弈的离散方法，以及采样式运动规划、轨迹优化和基于控制证书的合成方法。最后，指出在真实机器人部署中形式化合成面临的挑战，强调建模精度、计算可行性与可达成的严格保证之间的权衡。
原文摘要 · Abstract (English)
As robots move from controlled environments into real-world settings, it becomes increasingly crucial to ensure that they perform as expected. A key step toward that goal is a rigorous specification of the desired robot behavior, capturing intricate temporal, spatial, and logical requirements. Complementing this, plan and control synthesis methods are needed to fulfill these specifications with provable guarantees. This manuscript presents temporal logics - particularly linear and signal temporal logic - as expressive specification languages for robot behavior over time. We then discuss principles of formal synthesis, from discrete graph- and game-based approaches to sampling-based motion planning, trajectory optimization, and control-certificate-based synthesis. Finally, we outline challenges in deploying formal synthesis in real-world robotics, emphasizing the interplay between modeling fidelity, computational tractability, and the types of rigorous guarantees that can be achieved.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。