In this paper, we propose a compositional framework for the construction of control barrier certificates for large-scale stochastic switched systems accepting multiple control barrier certificates with some dwell-time conditions. The proposed scheme is based on a notion of so-called augmented pseudo-barrier certificates computed for each switched subsystem, using which one can compositionally synthesize state-feedback controllers for interconnected systems enforcing safety specifications over a finite-time horizon. In particular, we first leverage sufficient max-type small-gain conditions to compositionally construct augmented control barrier certificates for interconnected systems based on the corresponding augmented pseudo-barrier certificates of subsystems. Then we quantify upper bounds on exit probabilities - the probability that an interconnected system reaches certain unsafe regions - in a finite-time horizon using the constructed augmented barrier certificates. We employ a technique based on a counter-example guided inductive synthesis (CEGIS) approach to search for control barrier certificates of each mode while synthesizing safety controllers providing switching signals. We demonstrate our proposed results by applying them first to a room temperature network containing 1000 rooms. Finally, we apply our techniques to a network of 500 switched subsystems (totally 1000 dimensions) accepting multiple barrier certificates with a dwell-time condition, and provide upper bounds on the probability that the interconnected system reaches some unsafe region in a finite-time horizon.
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 as a relation between each switched subsystem and its finite abstraction. Based on some small-gain type conditions, we use those alternating simulation functions to construct compositionally an overall alternating simulation function as a relation between an interconnection of finite abstractions and that of switched subsystems. This overall alternating simulation function allo…
This paper is concerned with a compositional scheme for the construction of control barrier certificates for interconnected discrete-time stochastic systems. The main objective is to synthesize switching control policies against $ω$-regular properties that can be described by accepting languages of deterministic Streett automata (DSA) along with providing probabilistic guarantees for the satisfaction of such specifications. The proposed framework leverages the interconnection topology and a notion of so-called \emph{control sub-barrier certificates} of subsystems, which are used to composition…
The paper presents a methodology for temporal logic verification of continuous-time switched stochastic systems. Our goal is to find the lower bound on the probability that a complex temporal property is satisfied over a finite time horizon. The required temporal properties of the system are expressed using a fragment of linear temporal logic, called safe-LTL with respect to finite traces. Our approach combines automata-based verification and the use of barrier certificates. It relies on decomposing the automaton associated with the negation of specification into a sequence of simpler reachabi…
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 su…
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 system's 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 in…
In this work, we propose a compositional scheme for the safety controller synthesis of interconnected discrete-time stochastic systems with Markovian switching signals. Our proposed approach is based on a notion of so-called control storage certificates computed for individual subsystems, by leveraging which, one can synthesize state-feedback controllers for interconnected systems to enforce safety specifications over finite time horizons. To do so, we employ a sum-of-squares (SOS) optimization approach to search for multiple storage certificates of each switching subsystem while synthesizing …
In this paper, we provide a compositional approach for constructing finite abstractions (a.k.a. finite Markov decision processes (MDPs)) of interconnected discrete-time stochastic switched systems. The proposed framework is based on a notion of stochastic simulation functions, using which one can employ an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds on their output trajectories. To this end, we first provide probabilistic closeness guarantees between the interconnection of stochastic switched subsystems and that of their f…
This paper is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic properties. Our proposed methodology involves decomposition of interconnected systems into smaller subsystems and leverages the notion of control sub-barrier certificates of subsystems, enabling one to construct control barrier certificates of interconnected systems by employing some max-type small-gain conditions. The main goal is to synthesize hybrid controllers enforcing com…
We construct compositional continuous approximations for an interconnection of infinitely many discrete-time switched systems. An approximation (known as abstraction) is itself a continuous-space system, which can be used as a replacement of the original (known as concrete) system in a controller design process. Having synthesized a controller for the abstract system, the controller is refined to a more detailed controller for the concrete system. To quantify the mismatch between the output trajectory of the approximation and of that the original system, we use the notion of so-called simulati…
In this paper, we develop a compositional scheme for the construction of continuous approximations for interconnections of infinitely many discrete-time switched systems. An approximation (also known as abstraction) is itself a continuous-space system, which can be used as a replacement of the original (also known as concrete) system in a controller design process. Having designed a controller for the abstract system, it is refined to a more detailed one for the concrete system. We use the notion of so-called simulation functions to quantify the mismatch between the original system and its app…
This paper addresses the stability problem for discrete-time switched systems under autonomous switching. Each mode of the switched system is modeled as a Linear Parameter Varying (LPV) system, the time-varying parameters can vary arbitrarily fast and are represented in a polytopic form. The Lyapunov theory is employed to get new conditions in the form of parameter-dependent LMIs. The constructed Lyapunov function takes advantage of using an augmented state vector with shifted states in its construction. In this sense, the Lyapunov function employed in this paper can be viewed as a discrete-ti…
We consider discrete-time switching systems composed of a finite family of affine sub-dynamics. First, we recall existing results and present further analysis on the stability problem, the existence and characterization of compact attractors, and the relations these problems have with the joint spectral radius of the set of matrices composing the linear part of the subsystems. Second, we tackle the problem of providing probabilistic certificates of stability along with the existence of forward invariant sets, assuming no knowledge on the system data but only observing a finite number of sample…
Practical Stabilization of Switched Affine Systems under Dwell Time: From Polytopic to p-Norm Lyapunov Functions
Centro Internacional Franco-Argentino de Cs. de la Información y de Sistemas (CIFASIS), UNR–CONICET（中法阿根廷信息与系统国际中心（CIFASIS），罗萨里奥国立大学-国家科学研究委员会）；Military Institute of Engineering（军事工程学院）
Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees
Institute of Science and Technology Austria (ISTA)（奥地利科学技术研究所（ISTA））；Massachusetts Institute of Technology（麻省理工学院）；The Pennsylvania State University（宾夕法尼亚州立大学）
