Compositional Verification of Initial-State Opacity for Switched Systems
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Verification of Initial-State Opacity for Switched Systems: A Compositional Approach
The security in information-flow has become a major concern for cyber-physical systems (CPSs). In this work, we focus on the analysis of an information-flow security property, called opacity. Opacity characterizes the pl…
Comparing the Notions of Opacity for Discrete-Event Systems
Opacity is an information flow property characterizing whether a system reveals its secret to a passive observer. Several notions of opacity have been introduced in the literature. We study the notions of language-based …
Local Opacity Verification for Distributed Discrete Event Systems
This paper studies current-state opacity and initial-state opacity verification of distributed discrete event systems. The distributed system's global model is the parallel composition of multiple local systems: each of …
Decentralized State Estimation and Opacity Verification Based on Partially Ordered Observation Sequences
In this paper, we investigate state estimation and opacity verification problems within a decentralized observation architecture. Specifically, we consider a discrete event system whose behavior is recorded by a set of o…
State EstimationCompositional Abstractions of Interconnected Discrete-Time Switched Systems
In this paper, we introduce a compositional method for the construction of finite abstractions of interconnected discrete-time switched systems. Particularly, we use a notion of so-called alternating simulation function …
Relation