具有时序逻辑约束的基于吸引力的滚动时域路径规划

本文的目标是在具有动态变化、局部感知奖励的分区环境中规划机器人的运动。我们假设可以给出关于奖励动态的任意假设。机器人旨在完成高层时序逻辑监视任务，并在访问区域中局部优化奖励收集。这两个目标往往相互冲突，只能达成某种妥协。我们通过考虑用户定义的偏好函数来解决这一问题，该函数捕捉了收集高奖励的重要性与向监视区域推进的重要性之间的权衡。我们的解决方案利用了基于自动机的模型检验方法中的思想。我们在一个说明性示例中展示了所提出框架的用途和优势。