Efficient SMT-Based Model Checking for HyperTWTL

Hyperproperties extend trace properties to express properties of sets of traces, and thus, they are increasingly popular in specifying various security and performance-related properties in domains such as autonomous, cyber-physical, and robotic systems. Specifically, Hyperproperties for time window temporal logic (HyperTWTL) are known for their compactness in specifying robotic systems’ safety and security requirements. However, the existing model checking approach for HyperTWTL verification relies on automata-based model checking, which is computationally expensive and suffers from the state-space explosion problem. This paper introduces a bounded model checking approach for verifying HyperTWTL specifications using SMT solvers. Specifically, our proposed verification method reduces the HyperTWTL model checking problem to a first-order logic satisfiability problem and then uses state-of-the-art SMT solvers, i.e., Z3 and CVC4, for verification. The feasibility of the proposed HyperTWTL verification methods is demonstrated through a Technical Surveillance Squadron (TESS), a Robotic Industrial Inspection case study, and also a scalability analysis. Our results show that the proposed method can offer up to \(19\times \) speed up and \(2\times \) memory efficiency compared to the traditional automata-based model checking approach. We also show that the proposed HyperTWTL verification technique can verify large systems, whereas the traditional HyperTWTL verification method suffers from state-space explosion problem.