Verification of Hyperproperties for Uncertain Dynamical Systems via Barrier Certificates

TL;DR

This paper introduces a novel discretization-free method for verifying hyperproperties of uncertain dynamical systems using augmented barrier certificates, enabling safety guarantees for complex specifications like opacity and robustness.

Contribution

It presents the first discretization-free verification approach for hyperproperties in uncertain dynamical systems, utilizing automata-based decomposition and barrier certificate synthesis.

Findings

Effective verification on physical case studies

Successful synthesis of polynomial barrier certificates

Verification of opacity and robustness hyperproperties

Abstract

Hyperproperties are system properties that require quantification over multiple execution traces of a system. Hyperproperties can express several specifications of interest for cyber-physical systems--such as opacity, robustness, and noninterference--which cannot be expressed using linear-time properties. This paper presents for the first time a discretization-free approach for the formal verification of discrete-time uncertain dynamical systems against hyperproperties. The proposed approach involves decomposition of complex hyperproperties into several verification conditions by exploiting the automata-based structures corresponding to the complements of the original specifications. These verification conditions are then discharged by synthesizing so-called augmented barrier certificates, which provide certain safety guarantees for the underlying system. For systems with polynomial-type dynamics, we present a sound procedure to synthesize polynomial-type augmented barrier certificates by reducing the problem to sum-of-squares optimizations. We demonstrate the effectiveness of our proposed approaches on two physical case studies against two important hyperproperties: initial-state opacity and initial-state robustness.