HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications

TL;DR

This paper presents a new framework using HyperCertificates to verify discrete-time dynamical systems against hyperproperties specified in HyperLTL, combining barrier and ranking functions with lookahead modeling.

Contribution

It introduces HyperCertificates, a novel inductive method for verifying hyperproperties in dynamical systems using barrier and ranking functions with lookahead modeling.

Findings

Framework is automatable via SOS and SMT techniques.

Successfully applied to case studies demonstrating effectiveness.

Provides guarantees for hyperproperties like opacity and privacy.

Abstract

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.