Search

This paper focuses on distributed controller synthesis for ensuring the safety of large-scale systems with unknown dynamics and known interconnection structures, employing control barrier certificates. Our approach centers on a distributed framework tailored to create control barrier certificates for safety, utilizing the interconnections within large-scale systems. We introduce a novel application of graph neural networks to synthesize these certificates and distributed controllers in a data-driven fashion. The formal correctness of trained networks is subsequently validated through data-driven techniques involving the solution of a sampling-based optimization problem. To illustrate the effectiveness of our methodology, we conduct experiments on a complex interconnected system comprising as many as 1000 components.

Control barrier certificates have proven effective in formally guaranteeing the safety of the control systems. However, designing a control barrier certificate is a time-consuming and computationally expensive endeavor that requires expert input in the form of domain knowledge and mathematical maturity. Additionally, when a system undergoes slight changes, the new controller and its correctness certificate need to be recomputed, incurring similar computational challenges as those faced during the design of the original controller. Prior approaches have utilized transfer learning to transfer safety guarantees in the form of a barrier certificate while maintaining the control invariant. Unfortunately, in practical settings, the source and the target environments often deviate substantially in their control inputs, rendering the aforementioned approach impractical. To address this challenge, we propose integrating inverse dynamics—a neural network that suggests required action given a desired successor state—of the target system with the barrier certificate of the source system to provide formal proof of safety. In addition, we propose a validity condition that, when met, guarantees correctness of the controller. We demonstrate the efficacy of our method with an inverted pendulum case study.

Traditional hierarchical control methodologies refine controllers from an abstract to a concrete system using a simulation relation established over the state sets of both systems. However, such a relation may yield a large error between the abstract and concrete systems, thus constraining the efficacy of hierarchical control architectures. To address this limitation, we introduce a more versatile simulation relation, namely general approximate alternating simulation relation, which also makes use of the input set of the abstract system. We demonstrate that our novel simulation relation effectively captures the similarity between the abstract and concrete system outperforming conventional simulation relations. Furthermore, it strengthens the hierarchical control architecture by reducing the error between the outputs of a concrete and its abstract system. We provide methods for establishing this new relation in linear control systems alongside their continuous abstractions. The practicality and effectiveness of our approach are underscored through its application in an illustrative example.

In this paper, we provide an automata-based framework for verifying diagnosability property of Cyber-Physical Systems leveraging a notion of so-called hybrid barrier certificates. Concretely, we first construct a so-called (δ,K)-deterministic finite automata ((δ,K)-DFA) associated with the desired diagnosability property, which captures the occurrence of the fault to be diagnosed. Having a (δ,K)-DFA, we show that the verification of diagnosability properties is equivalent to a safety verification problem over a product system between this DFA and the dynamical system of interest. We further show that such a verification problem can be solved via computing hybrid barrier certificates for the product system. To compute the hybrid barrier certificates, we provide a systematic technique leveraging a counter-example guided inductive synthesis framework. Finally, we showcase the effectiveness of our results through a case study.

The success of barrier certificates to ensure the safety of control systems has led to their adoption in designing controllers to guarantee more general ω-regular automata specifications. Recent developments in co-Büchi barrier certificates propose the direct construction of the product of the system and the automaton, ensuring that the accepting states of the automaton are visited finitely often. Despite the benefits, challenges arise when finding these certificates for large-scale systems. To overcome such challenges, we introduce a compositional controller synthesis via co-Büchi barrier certificates. We decompose the large-scale system into an interconnection of smaller subsystems, construct local certificates for these subsystems, and utilize a dissipativity-type condition to guarantee the existence of a certificate for the large-scale system. We design controllers for the subsystems that, when concatenated, act as a formally correct controller for the large-scale system. Finally, we illustrate our approach with a numerical example.

In this paper, we propose a secure-by-construction scheme for synthesizing controllers to enforce safety and security properties simultaneously over control systems. As a key insight, we establish a bridge between the desired safety and security properties by leveraging notions of (augmented) control barrier functions. Based on these functions, we show that one can synthesize secure-by-construction controllers for control systems with continuous state and input sets. Additionally, we provide sum-of-square (SOS) conditions under which the desired (augmented) control barrier functions can be constructed. Finally, we demonstrate the applicability of our results on a case study.

This paper is concerned with the formal synthesis of safety controllers for partially-observable continuous-time polynomial-type systems with unknown dynamics. Given a continuous-time polynomial-type estimator with a partially-unknown dynamic and a known upper bound on the estimation accuracy, we propose a data-driven approach to compute a polynomial-type controller ensuring safety of the system. The proposed framework is based on a notion of so-called control barrier functions and only requires a single output trajectory collected from the system and a single state trajectory collected from its estimator. We show the application of our technique by synthesizing a safety controller for a partially-observable jet engine with unknown dynamics.

This paper is concerned with the controller synthesis problem for discrete-time unknown systems against safety specifications via control barrier certificates. Typically, control barrier certificates provide sufficient conditions for the satisfaction of safety specifications by separating the safe and unsafe regions of the system. By synthesizing these certificates in conjunction with control policies, one is able to keep the system safe. In our work, we parameterize the control barrier certificates and corresponding control policies as neural networks and learn them simultaneously by utilizing finitely many data samples obtained from the unknown system. We derive a so-called validity condition to formally verify the obtained certificates and integrate this condition within the training framework to achieve provably correct guarantees at the end of training time. In particular, we exploit Lipschitz continuity properties of the neural networks and utilize robust training techniques to ensure that the trained networks not only satisfy the required control barrier certificate conditions across the finitely many training data samples but over the entire state set. We then demonstrate the effectiveness of our approach with the help of a case study.

Motivated by a paradigm shift towards a hyper-connected world, we develop a computationally tractable small-gain theorem for networks of infinitely many subsystems, termed as infinite networks. The proposed small-gain theorem addresses exponential input-to-state stability with respect to closed sets, which enables us to analyze diverse stability problems in a unified manner. The small-gain condition, expressed in terms of the spectral radius of a gain operator collecting all the information about the internal Lyapunov gains, can be numerically checked efficiently for a large class of systems. To demonstrate broad applicability of our small-gain theorem, we apply it to consensus of infinitely many agents, and to the design of distributed observers for infinite networks.

This paper is concerned with a data-driven approach for the estimation of infinitesimal generators of continuous-time stochastic systems with unknown dynamics. We first approximate the infinitesimal generator of the solution process via a set of data collected from trajectories of the unknown system. The approximation utilizes both time discretization and sampling from the solution process. Assuming proper continuity assumptions on dynamics of the system, we then quantify the closeness between the infinitesimal generator and its approximation while providing a priori guaranteed confidence bound. We demonstrate that both the time discretization and the number of data play significant roles in providing a reasonable closeness precision. Moreover, for a fixed size of data, variance of the estimation converges to infinity when the time discretization parameter goes to zero. The formulated error bound shows how to pick proper data size and time discretization jointly to prevent this counter-intuitive behavior. The proposed results are demonstrated on a case study.

In this paper, we propose a data-driven approach to formally verify the safety of (potentially) unknown discrete-time continuous-space stochastic systems. The proposed framework is based on a notion of barrier certificates together with data collected from trajectories of unknown systems. We first reformulate the barrier-based safety verification as a robust convex problem (RCP). Solving the acquired RCP is hard in general because not only the state of the system lives in a continuous set, but also and more problematic, the unknown model appears in one of the constraints of RCP. Instead, we leverage a finite number of data, and accordingly, the RCP is casted as a scenario convex problem (SCP). We then relate the optimizer of the SCP to that of the RCP, and consequently, we provide a safety guarantee over the unknown stochastic system with a priori guaranteed confidence. We apply our approach to an unknown room temperature system by collecting sampled data from trajectories of the system and verify formally that temperature of the room lies in a comfort zone for a finite time horizon with a desired confidence.

This paper presents a tight small-gain theorem for networks composed of infinitely many finite-dimensional subsystems. Assuming that each subsystem is exponentially input-to-state stable, we show that if the gain operator, collecting all the information about the internal Lyapunov gains, has a spectral radius less than one, the overall infinite network is exponentially input-to-state stable. We illustrate the effectiveness of our result by applying it to traffic networks.

In this paper a distributed Received Signal Strength (RSS) minimization algorithm is proposed that guarantees strong connectivity of the network topology while minimizing the RSS of the network received at a given eavesdropper’s location. The proposed algorithm is composed of multiple rounds of maximum consensus network communications implementing a distributed greedy solution of the problem. The proposed RSS minimization algorithm is distributed in the sense that nodes do not assume, estimate or communicate any network connectivity knowledge such as a routing table, the Laplacian matrix, neighbour lists or the total number of nodes. The proposed algorithm assumes that the initial network topology is strongly connected and that each agent knows its own location and that of the eavesdropper. We provide an extension of the proposed algorithm for dealing with multiple and moving eavesdropper. In this case, we also propose a heuristic for increasing nodal transmit power to effectively reshape the network topology according to the closer eavesdropper. Performance of the proposed algorithm is demonstrated in simulations.

This paper provides a compositional scheme based on dissipativity approaches for constructing finite abstractions of continuous-time continuous-space stochastic control systems. The proposed framework enjoys the structure of the interconnection topology and employs a notion of stochastic storage functions, that describe joint dissipativity-type properties of subsystems and their abstractions. By utilizing those stochastic storage functions, one can establish a relation between continuous-time continuous-space stochastic systems and their finite counterparts while quantifying probabilistic distances between their output trajectories. Consequently, one can employ the finite system as a suitable substitution of the continuous-time one in the controller design process with a guaranteed error bound. In this respect, we first leverage dissipativity-type compositional conditions for the compositional quantification of the distance between the interconnection of continuous-time continuous-space stochastic systems and that of their discrete-time (finite or infinite) abstractions. We then consider a specific class of stochastic affine systems and construct their finite abstractions together with their corresponding stochastic storage functions. We illustrate the effectiveness of the proposed techniques by applying them to a physical case study.

We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal properties by trajectories of such systems. We express these properties as signal temporal logic formulas and check if the probability of satisfying the property is at least a given threshold. Since the dynamics are parameterized and partially unknown, we collect data from the system and employ Bayesian inference techniques to associate a confidence value to the satisfaction of the property. The main novelty of our approach is to combine both data-driven and model-based techniques in order to have a two-layer probabilistic reasoning over the behavior of the system: one layer is related to the stochastic noise inside the system and the next layer is related to the noisy data collected from the system. We provide approximate algorithms for computing the confidence for linear dynamical systems.

We present a new approach to the cooperative localisation problem by applying the theory of minimum energy filtering. We consider the problem of estimating the pose of a group of mobile robots in an environment where robots can perceive fixed landmarks and neighbouring robots as well as share information with others over a communication channel. Whereas the vast majority of the existing literature applies some variant of a Kalman Filter, we derive a set of filter equations for the global state estimate based on the principle of minimum energy filtering. We show how the filter equations can be decoupled and the calculations distributed among the robots in the network without requiring a central processing node. Finally, we provide a demonstration of the filter’s performance in simulation.

In this paper, we propose a compositional framework for the construction of control barrier functions for networks of continuous-time stochastic control systems. The proposed scheme is based on a notion of so-called pseudo-barrier functions computed for subsystems, using which one can synthesize state-feedback controllers for interconnected systems enforcing safety specifications over a finite-time horizon. Particularly, we first leverage sufficient small-gain type conditions to compositionally construct control barrier functions for interconnected systems based on the corresponding pseudo-barrier functions computed for subsystems. Then, using the constructed control barrier functions, we quantify upper bounds on exit probabilities - the probability that an interconnected system reaches certain unsafe regions - in a finite-time horizon. We employ a systematic technique based on the sum-of-squares optimization program to search for pseudo-barrier functions of subsystems while synthesizing safety controllers. We demonstrate our proposed results by applying them to a temperature regulation in a network of 1000 rooms.

In this paper, we provide a compositional method for the construction of symbolic models (a.k.a. finite abstractions) for infinite networks of discrete-time control systems. The concrete infinite network and its symbolic model are related by a so-called alternating simulation function which allows one to quantify the mismatch between the output behavior of the infinite interconnection of concrete subsystems and that of their symbolic models. We show that such an alternating simulation function can be obtained compositionally by assuming some small-gain type conditions and composing so-called local alternating simulation functions constructed for subsystems. Assuming certain stability property of concrete subsystems, we also provide a technique to synthesize their symbolic models together with their corresponding local alternating simulation functions. Finally, we apply our results to a traffic network divided into infinitely many cells.

This paper proposes a compositional approach for constructing control barrier certificates of large-scale interconnected discrete-time stochastic control systems. The proposed compositional methodology is based on a notion of control sub-barrier certificatesenabling one to construct control barrier certificates of interconnected systems by leveraging some small-gain type conditions. The main goal is to synthesize control policies satisfying safety properties for interconnected systems utilizing those control sub-barrier certificates of subsystems while providing upper bounds on the probability that interconnected systems reach unsafe regions in finite-time horizons. A sum-of-squares optimization problem is formulated for searching control sub-barrier certificates and corresponding local control policies satisfying safety specifications. The proposed compositional approaches are illustrated on a temperature regulation in a circular building containing 1000 rooms by compositionally synthesizing safety controllers to maintain the temperature of each room in a comfort zone in a bounded-time horizon.

Synthesis of controllers for stochastic control systems ensuring safety constraints has gained considerable attention in the last few years. In this paper, we consider the problem of synthesizing controllers for partially observed stochastic control systems to ensure finite-time safety. Given an estimator with a probabilistic guarantee on the accuracy of the estimations, we provide an approach to compute a controller providing a lower bound on the probability that the trajectories of the stochastic control system remain safe over a finite time-horizon. To obtain such controllers, we utilize a notion of control barrier functions. We also provide an approach to compute a probability bound on estimator accuracy by using a notion of so-called stochastic simulation function. The proposed result is illustrated on a case study.

In this paper, we provide a compositional technique for constructing finite abstractions (a.k.a. finite Markov decision processes) for networks of discrete-time stochastic switched systems. The proposed framework is based on the notion of stochastic simulation functions,using which one can employ a finite MDP as a substitution of the original one in the controller design process with guaranteed error bounds on their output trajectories. In this respect, we first leverage dissipativity-type compositional conditions for quantifying the error between the interconnection of stochastic switched subsystems and that of their finite abstractions. We then propose an approach to construct finite MDPs together with their corresponding stochastic simulation functions for a particular class of nonlinearstochastic switched systems. To demonstrate the effectiveness of our proposed results, we apply our approaches to two different case studies.

This paper is concerned with a compositional approach for constructing finite abstractions (a.k.a. finite Markov decision processes) of interconnected discrete-time stochastic control systems. The proposed framework is based on a notion of so-called stochastic simulation functionenabling us to use an abstract system as a substitution of the original one in the controller design process with guaranteed error bounds. In the first part of the paper, we derive sufficient small-gain type conditions for the compositional quantification of the distance in probability between the interconnection of stochastic control subsystems and that of their (finite or infinite) abstractions. In the second part of the paper, we construct finite abstractions together with their corresponding stochastic simulation functions for the class of linear stochastic control systems. We apply our results to the temperature regulation in a circular building by constructing compositionally a finite abstraction of a network containing 1000 rooms. We use the constructed finite abstractions as substitutes to synthesize policies compositionally regulating the temperature in each room for a bounded time horizon.

Abstraction-based synthesis techniques are limited to systems with moderate size. Thus to contribute towards scalability of these techniques, in this paper we propose a compositional abstraction-based synthesis for cascade interconnected discrete-time control systems. Given a cascade interconnection of several components, we provide results on the compositional construction of finite abstractions based on the notion of approximate cascade composition. Then, we provide a compositional controller synthesis for cascade interconnection. Finally, we demonstrate the applicability and effectiveness of the results using a numerical example and compare it with different abstraction and controller synthesis schemes.

Nondeterministic finite transition systems (NFTSs) have been widely used in the past decade to (approximately) abstract physical systems described by ordinary differential equations. One can leverage the NFTSs and algorithmic machinery for automated synthesis of finite systems to automatically synthesize controllers for the original physical systems against complex logical specifications. The current state detection/estimation of NFTSs is of fundamental importance, as the current state is often used inside the synthesized controllers to compute the current input value for the concrete physical systems. In this paper, the problem of detectability is formulated as whether one can determine the current and all subsequent states of the NFTSs considered by using any sufficiently long input sequence and the corresponding output sequence. We design a polynomial time algorithm to verify the detectability, and based on the algorithm, we design a detector, i.e., a partial function that maps the set of (input, output) sequences of a specific length to the set of states, to determine the current and all subsequent states of detectable NFTSs.

In this paper, we revisit maximum likelihood methods for identification of errors-in-variables systems. We assume that the system admits a parametric description, and that the input is a stochastic ARMA process. The cost function associated with the maximum likelihood criterion is minimized by introducing a new iterative solution scheme based on the expectation-maximization method, which proves fast and easily implementable. Numerical simulations show the effectiveness of the proposed method.

In this work, we derive conditions under which compositional abstractions of networks of stochastic hybrid systems can be constructed using the interconnection topology and joint dissipativity-type properties of subsystems and their abstractions. In the proposed framework, the abstraction, itself a stochastic hybrid system (possibly with a lower dimension), can be used as a substitute of the original system in the controller design process. Moreover, we derive conditions for the construction of abstractions for a specific class of stochastic hybrid systems by using the sector property of the system nonlinearity. We provide an example with numerical simulations to illustrate the effectiveness of the proposed dissipativity-type compositional reasoning for interconnected stochastic hybrid systems.

This paper studies the problem of identification for networked systems. We consider both heterogeneous and homogeneous networks. It is assumed that the interconnection topology is time-invariant and known. We demonstrate how the parameter matrices of each individual subsystem can be identified from the input-output information obtained from the whole network. To this end, the well-known technique of Maximum-likelihood (ML) is exploited for obtaining estimations of system matrices.

This paper investigates an approach for the stabilization of continuous-time type III (Takagi-Sugeno-Kang) fuzzy system based on impulsive parallel distributed compensation (PDC). Based on the Lyapunov criterion, some conditions are derived to stabilize type III fuzzy systems. These conditions are given in term of some matrix inequalities.