Model Checking Time Window Temporal Logic for Hyperproperties

Motivated by the expressiveness of hyperproperties, Hyperproperties extend trace properties to express properties of several hyper-temporal logics, such as HyperLTL [20], sets of traces, and they are increasingly popular in specifying various HyperSTL [38], and HyperMTL [11], were recently proposed by extending security and performance-related properties in domains such the conventional temporal logics such as Linear Temporal as cyber-physical systems, smart grids, and automotive. This paper Logic (LTL) [41], Signal Temporal Logic (STL) [37], and Metric Temporal introduces HyperTWTL, which extends Time Window Temporal Logic (MTL) [33], respectively. Consequently, various model Logic (TWTL)-a domain-specific formal specification language for checking techniques have been proposed for verifying HyperLTL robotics, by allowing explicit and simultaneous quantification over [20, 22, 25, 27], HyperMTL [11, 30], HyperMITL [31], HyperSTL multiple execution traces. We propose two different semantics for [38] specifications employing alternating automata, model checking, HyperTWTL, synchronous and asynchronous, based on the alignment strategy synthesis, and several other methods [32]. of the timestamps in the traces. Consequently, we demonstrate Time bounded specifications are common in many applications, the application of HyperTWTL in formalizing important such as robotics.