Motion Planning Using Hyperproperties for Time Window Temporal Logic

摘要

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.