HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications
This work provides a novel verification method for hyperproperties in dynamical systems, addressing a gap in formal verification for properties like privacy and robustness.
The paper introduces HyperCertificates, a functional inductive framework for verifying discrete-time dynamical systems against HyperLTL specifications, which describe hyperproperties like opacity and robustness. The approach is demonstrated on case studies using SOS optimization and SMT solvers.
We introduce a functional inductive framework to verify discrete-time dynamical systems against hyperproperties specified as Hyperlinear temporal logic formulae via a notion of HyperCertificates. Unlike linear temporal logic (LTL) formulae which are concerned with individual traces of a system, hyperproperties are properties that are concerned with how the traces of a system relate to one another. HyperLTL is an extension of LTL for hyperproperties, and is useful to describe specifications such as opacity, privacy as well as notions of robustness. Our notion of HyperCertificates consists of a pair of functions, where the first models the lookahead, and the second relies on a combination of barrier and ranking functions. We use closure certificates, to act as a model for this lookahead and then rely on barrier and ranking function arguments modulo this lookahead to provide guarantees against HyperLTL formulae. We demonstrate how our approach is automatable via existing techniques such as sum-of-squares optimization (SOS) and satisfiability modulo theories (SMT) solvers. Finally, we demonstrate our approach on some case studies.