-
Data-driven Safety Verification of Stochastic Systems via Barrier Certificates
Authors:
Ali Salamati,
Abolfazl Lavaei,
Sadegh Soudjani,
Majid Zamani
Abstract:
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 acqui…
▽ More
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.
△ Less
Submitted 23 December, 2021;
originally announced December 2021.
-
Data-driven verification and synthesis of stochastic systems via barrier certificates
Authors:
Ali Salamati,
Abolfazl Lavaei,
Sadegh Soudjani,
Majid Zamani
Abstract:
In this work, we study verification and synthesis problems for safety specifications over unknown discrete-time stochastic systems. When a model of the system is available, barrier certificates have been successfully applied for ensuring the satisfaction of safety specifications. In this work, we formulate the computation of barrier certificates as a robust convex program (RCP). Solving the acquir…
▽ More
In this work, we study verification and synthesis problems for safety specifications over unknown discrete-time stochastic systems. When a model of the system is available, barrier certificates have been successfully applied for ensuring the satisfaction of safety specifications. In this work, we formulate the computation of barrier certificates as a robust convex program (RCP). Solving the acquired RCP is hard in general because the model of the system that appears in one of the constraints of the RCP is unknown. We propose a data-driven approach that replaces the uncountable number of constraints in the RCP with a finite number of constraints by taking finitely many random samples from the trajectories of the system. We thus replace the original RCP with a scenario convex program (SCP) and show how to relate their optimizers. We guarantee that the solution of the SCP is a solution of the RCP with a priori guaranteed confidence when the number of samples is larger than a pre-computed value. This provides a lower bound on the safety probability of the original unknown system together with a controller in the case of synthesis. We also discuss an extension of our verification approach to a case where the associated robust program is non-convex and show how a similar methodology can be applied. Finally, the applicability of our proposed approach is illustrated through three case studies.
△ Less
Submitted 9 September, 2023; v1 submitted 19 November, 2021;
originally announced November 2021.
-
Data-Driven Verification under Signal Temporal Logic Constraints
Authors:
Ali Salamati,
Sadegh Soudjani,
Majid Zamani
Abstract:
We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal logic 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…
▽ More
We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal logic 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.
△ Less
Submitted 8 May, 2020;
originally announced May 2020.
-
Improvement of Identification Procedure Using Hybrid Cuckoo Search Algorithm for TurbineGovernor and Excitation System
Authors:
Teimour Hosseinalizadeh,
S. Mahmoud Salamati,
S. Ali Salamati,
G. B. Gharehpetian
Abstract:
In this paper a new method is introduced in order to modify identification process of a gas power plant using a metaheuristic algorithm named Cuckoo Search (CS). Simulations play a significant role in dynamic analyses of power plants. This paper points out to a practical approach in model selection and parameter estimation of gas power plants. The identification and validation process concentrates…
▽ More
In this paper a new method is introduced in order to modify identification process of a gas power plant using a metaheuristic algorithm named Cuckoo Search (CS). Simulations play a significant role in dynamic analyses of power plants. This paper points out to a practical approach in model selection and parameter estimation of gas power plants. The identification and validation process concentrates on two subsystems: governor-turbine and exciter. Standard models GGOV1 and STB6 are preferred for the dynamical structures of governor-turbine and exciter respectively. Considering definite standard structure, main parameters of dynamical model are pre estimated via system identification methods based on field data. Then obtained parameters are tuned carefully using an iterative Cuckoo algorithm. Models must be validated by results derived via a trial and error series of simulation in comparison to measured test data. The procedure gradually yields in a valid model with precise estimated parameters. Simulation results show accuracy of identified models. Besides, a whiteness analysis has been performed in order to show the authenticity of the proposed method in another way. Despite various detailed models, practical attempts of model selection, identification, and validation in a real gas unit could rarely be found among literature. In this paper, Chabahar power plant in Iran, with total install capacity of 320 MW, is chosen as a benchmark for model validation.
△ Less
Submitted 27 December, 2018;
originally announced January 2019.
-
Leveraging Adaptive Model Predictive Controller for Active Cell Balancing in Li-ion Battery
Authors:
Seyed Mahmoud Salamati,
Seyed Ali Salamati,
Mohsen Mahoor,
Farzad Rajaei Salmasi
Abstract:
Automotive industry is moving toward fully electric and hybrid electric vehicles. Accordingly, energy storage unit is one of the most important blocks in these electric drives. Battery stacks which contain a number of cells are being used for supplying the vehicles' energy. Charge equalization for series connected battery strings has a significant effect on battery life. In this paper, an adaptive…
▽ More
Automotive industry is moving toward fully electric and hybrid electric vehicles. Accordingly, energy storage unit is one of the most important blocks in these electric drives. Battery stacks which contain a number of cells are being used for supplying the vehicles' energy. Charge equalization for series connected battery strings has a significant effect on battery life. In this paper, an adaptive model predictive controller (AMPC) is proposed to manage the cell equalizing process. The series connected cells' voltages and currents are collected, then leveraging Recursive Least Square (RLS) method, the future voltage samples for all of the cells are predicted. MPC controller specifies a sequence which results in the optimum balancing performance of the proposed circuit. Simulation results prove that using the suggested algorithm, the voltage set of the series cells has moved more uniformly.
△ Less
Submitted 17 June, 2017;
originally announced June 2017.
