Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userVerification of Initial-State Opacity for Switched Systems: A Compositional Approach
119
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
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 plausible deniability of a systems secret in the presence of a malicious outside intruder. We propose a methodology of checking a notion of opacity, called approximate initial-state opacity, for networks of discrete-time switched systems. Our framework relies on compositional constructions of finite abstractions for networks of switched systems and their so-called approximate initial-state opacity-preserving simulation functions (InitSOPSFs). Those functions 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, assuming certain stability property of switched systems, we also provide a technique on constructing their finite abstractions together with the corresponding local InitSOPSFs. Finally, we illustrate the effectiveness of our results through an example.
rate research
Read More
In this paper, we propose a compositional approach to construct opacity-preserving finite abstractions (a.k.a symbolic models) for networks of discrete-time nonlinear control systems. Particularly, we introduce new notions of simulation functions that characterize the distance between control systems while preserving opacity properties across them. Instead of treating large-scale systems in a monolithic manner, we develop a compositional scheme to construct the interconnected finite abstractions together with the overall opacity-preserving simulation functions. For a network of incrementally input-to-state stable control systems and under some small-gain type condition, an algorithm for designing local quantization parameters is presented to orderly build the local symbolic models of subsystems such that the network of symbolic models simulates the original network for an a-priori defined accuracy while preserving its opacity properties.
This paper presents a compositional framework for the construction of symbolic models for a network composed of a countably infinite number of finite-dimensional discrete-time control subsystems. We refer to such a network as infinite network. The proposed approach is based on the notion of alternating simulation functions. This notion relates a concrete network to its symbolic model with guaranteed mismatch bounds between their output behaviors. We propose a compositional approach to construct a symbolic model for an infinite network, together with an alternating simulation function, by composing symbolic models and alternating simulation functions constructed for subsystems. Assuming that each subsystem is incrementally input-to-state stable and under some small-gain type conditions, we present an algorithm for orderly constructing local symbolic models with properly designed quantization parameters. In this way, the proposed compositional approach can provide us a guideline for constructing an overall symbolic model with any desired approximation accuracy. A compositional controller synthesis scheme is also provided to enforce safety properties on the infinite network in a decentralized fashion. The effectiveness of our result is illustrated through a road traffic network consisting of infinitely many road cells.
In this paper, we study the problem of designing a simultaneous mode, input, and state set-valued observer for a class of hidden mode switched nonlinear systems with bounded-norm noise and unknown input signals, where the hidden mode and unknown inputs can represent fault or attack models and exogenous fault/disturbance or adversarial signals, respectively. The proposed multiple-model design has three constituents: (i) a bank of mode-matched set-valued observers, (ii) a mode observer, and (iii) a global fusion observer. The mode-matched observers recursively find the sets of compatible states and unknown inputs conditioned on the mode being the true mode, while the mode observer eliminates incompatible modes by leveraging a residual-based criterion. Then, the global fusion observer outputs the estimated sets of states and unknown inputs by taking the union of the mode-matched set-valued estimates over all compatible modes. Moreover, sufficient conditions to guarantee the elimination of all false modes (i.e., mode-detectability) are provided and the effectiveness of our approach is demonstrated and compared with existing approaches using an illustrative example.
The problem of integrating multiple overlapping models and data is pervasive in engineering, though often implicit. We consider this issue of model management in the context of the electrical power grid as it transitions towards a modern Smart Grid. We present a methodology for specifying, managing, and reasoning within multiple models of distributed energy resources (DERs), entities which produce, consume, or store power, using categorical databases and symmetric monoidal categories. Considering the problem of distributing power on the grid in the presence of DERs, we show how to connect a generic problem specification with implementation-specific numerical solvers using the paradigm of categorical databases.
We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal abstraction of the switched system in terms of an uncertain Markov model, namely an Interval Markov Decision Process (IMDP), by accounting for both the stochastic behavior of the system and the uncertainty in the learning step. Then, we synthesize a strategy on the resulting IMDP that maximizes the satisfaction probability of the LTLf specification and is robust against all the uncertainties in the abstraction. This strategy is then refined into a switching strategy for the original stochastic system. We show that this strategy is near-optimal and provide a bound on its distance (error) to the optimal strategy. We experimentally validate our framework on various case studies, including both linear and non-linear switched stochastic systems.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
