Model Checking Time Window Temporal Logic for Hyperproperties

TL;DR

This paper introduces HyperTWTL, a new logic extending Time Window Temporal Logic to specify and verify hyperproperties involving multiple traces, with applications in security and robotics.

Contribution

It presents a novel formalism, HyperTWTL, with synchronous and asynchronous semantics, and a model checking algorithm reducing hyperproperty verification to TWTL model checking.

Findings

HyperTWTL can formalize security policies and concurrency in robotics.

The model checking algorithm effectively verifies HyperTWTL fragments.

HyperTWTL extends TWTL to handle multiple traces with explicit quantification.

Abstract

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.