Compositional Verification of Initial-State Opacity for Switched Systems

TL;DR

This paper introduces a compositional method for verifying approximate initial-state opacity in networks of discrete-time switched systems, utilizing simulation functions and small-gain conditions to ensure privacy-preserving properties.

Contribution

It presents a novel compositional framework using InitSOPSFs for verifying initial-state opacity in switched systems, including methods for constructing finite abstractions under stability assumptions.

Findings

Framework effectively verifies initial-state opacity.

Constructs finite abstractions with local InitSOPSFs.

Validated through a practical example.

Abstract

In this work, we propose a compositional framework for the verification of approximate initial-state opacity for networks of discrete-time switched systems. The proposed approach is based on a notion of approximate initial-state opacity-preserving simulation functions (InitSOPSFs), which characterize how close concrete networks and their finite abstractions are in terms of the satisfaction of approximate initial state opacity. We show that such InitSOPSFs can be obtained compositionally by assuming some small-gain type conditions and composing so-called local InitSOPSFs constructed for each subsystem separately. Additionally, for switched systems satisfying certain stability properties, we provide an approach to construct their finite abstractions together with the corresponding local InitSOPSFs. Finally, the effectiveness of our results is illustrated through an example.