Hyperproperties extend trace properties to express properties of sets of traces, and they are increasingly popular in specifying various security and performance-related properties in domains such as cyber-physical systems, smart grids, and automotive. This paper introduces a model checking algorithm for a new formalism, HyperTWTL, which extends Time Window Temporal Logic (TWTL) -- a domain-specific formal specification language for robotics, by allowing explicit and simultaneous quantification over multiple execution traces. We present HyperTWTL with both \emph{synchronous} and \emph{asynchronous} semantics, based on the alignment of the timestamps in the traces. Consequently, we demonstrate the application of HyperTWTL in formalizing important information-flow security policies and concurrency for robotics applications. Finally, we propose a model checking algorithm for verifying fragments of HyperTWTL by reducing the problem to a TWTL model checking problem.

翻译：超属性将迹属性扩展为表达迹集合的性质，在信息物理系统、智能电网、汽车等领域的安全与性能相关属性规范中日益流行。本文提出一种针对新形式化语言HyperTWTL的模型检测算法，该语言通过允许对多条执行迹进行显式且同步的量化，扩展了机器人领域专用形式化规范语言——时间窗口时态逻辑（TWTL）。我们基于迹中时间戳对齐方式，给出了同时具有同步语义和异步语义的HyperTWTL。进而，我们展示了HyperTWTL在形式化重要信息流安全策略与机器人应用并发性方面的应用。最后，我们提出一种模型检测算法，通过将问题规约为TWTL模型检测问题，来验证HyperTWTL的部分子集。