Motion Planning Using Hyperproperties for Time Window Temporal Logic
Motion Planning Using Hyperproperties for Time Window Temporal Logic
复制标题
DOI：
10.1109/lra.2023.3280830
复制
发表时间：
2023-08
影响因子：
5.2
通讯作者：
Ernest Bonnah;L. Nguyen;Khaza Anuarul Hoque
中科院分区：
文献类型：
--
作者：
Ernest Bonnah;L. Nguyen;Khaza Anuarul Hoque
超性质在动态系统的安全策略验证和控制综合中越来越受欢迎。超属性概括了跟踪属性，以支持对传统跟踪属性无法实现的多个计算跟踪进行推理。最近的工作显示的有效性和前景的Hyperproperties，特别是Hyperproperties的线性时序逻辑（HyperLTL），在最优性，鲁棒性，和隐私意识的机器人运动规划。然而，尽管HyperLTL具有丰富的表达能力，但它无法表达具有时间约束的任务。这封信介绍了HyperTWTL，它扩展了时间窗口时序逻辑（TWTL）的紧凑语义，在多个执行轨迹上进行显式和并发量化。我们证明，HyperTWTL可以用来正式复杂的机器人规划目标。鉴于HyperTWTL规范，我们还提出了一种符号化的方法，通过将规划问题简化为一阶逻辑可满足性问题来合成最优性，鲁棒性和隐私感知策略。然后使用两个工业级SMT求解器解决规划问题。HyperTWTL的可行性和所提出的策略合成方法的效率和可扩展性证明了通过正式的重要的运动规划目标的监视使命的案例研究和合成各自的战略，使用Z3和CVC 4 SMT求解器。
Hyperproperties are increasingly popular in verifying security policies and synthesis of control for dynamic systems. Hyperproperties generalize trace properties to enable reasoning about multiple computation traces that traditional trace properties cannot. Recent works show the effectiveness and prospect of Hyperproperties, specifically Hyperproperties for Linear Temporal Logic (HyperLTL), in optimality-, robustness-, and privacy-aware robotic motion planning. However, despite their rich expressiveness, HyperLTL cannot express tasks with time constraints. This letter presents HyperTWTL, which extends the compact semantics of Time Window Temporal Logic (TWTL) with explicit and concurrent quantification over multiple execution traces. We demonstrate that HyperTWTL can be used to formalize complex robotic planning objectives. Given HyperTWTL specifications, we also propose a symbolic approach for synthesizing optimality-, robustness-, and privacy-aware strategies by reducing the planning problem to a first-order logic satisfiability problem. The planning problem was then solved using two industrial-strength SMT solvers. The feasibility of HyperTWTL and the efficiency and scalability of the proposed strategy synthesis approach are demonstrated by formalizing important motion planning objectives of a surveillance mission case study and synthesizing the respective strategies using Z3 and CVC4 SMT solvers.