Hyperproperties for Time Window Temporal Logic (HyperTWTL) is a domain-specific formal specification language known for its effectiveness in compactly representing security, opacity, and concurrency properties for robotics applications. This paper focuses on HyperTWTL-constrained secure reinforcement learning (SecRL). Although temporal logic-constrained safe reinforcement learning (SRL) is an evolving research problem with several existing literature, there is a significant research gap in exploring security-aware reinforcement learning (RL) using hyperproperties. Given the dynamics of an agent as a Markov Decision Process (MDP) and opacity/security constraints formalized as HyperTWTL, we propose an approach for learning security-aware optimal policies using dynamic Boltzmann softmax RL while satisfying the HyperTWTL constraints. The effectiveness and scalability of our proposed approach are demonstrated using a pick-up and delivery robotic mission case study. We also compare our results with two other baseline RL algorithms, showing that our proposed method outperforms them.

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.