HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications
2026-05-01 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors present a new method to check if systems that change over time follow special rules called hyperproperties, which look at relationships between multiple system behaviors rather than just one. They use a technique called HyperCertificates, which combines two functions to predict future behavior and ensure safety. Their method can be automated using existing math tools like SOS optimization and SMT solvers. The authors also show how their approach works through some practical examples.
discrete-time dynamical systemshyperpropertiesHyperlinear temporal logic (HyperLTL)linear temporal logic (LTL)HyperCertificatesclosure certificatesbarrier functionsranking functionssum-of-squares optimization (SOS)satisfiability modulo theories (SMT) solvers
Authors
Vishnu Murali, Amin Falah, Ashutosh Trivedi, Majid Zamani
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.