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，提出了一种模型检验算法。HyperTWTL扩展了时间窗口时态逻辑（TWTL）——一种用于机器人领域的特定领域形式化规范语言，允许对多个执行迹进行显式且同时的量词化。我们根据迹中时间戳的对齐方式，提出了具有同步语义和异步语义的HyperTWTL。继而，我们展示了HyperTWTL在机器人应用中形式化重要信息流安全策略及并发性的应用。最后，我们通过将问题归约为TWTL模型检验问题，提出了一种用于验证HyperTWTL片段的模型检验算法。