Title
Automated Synthesis Of Safe Digital Controllers For Sampled-Data Stochastic Nonlinear Systems
Abstract
We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a given threshold. Our technique uses a fast solver and an optimization method to search for candidate controllers, which are then formally evaluated in closed-loop with the system in question by a verified solver. Unstable candidate controllers are discarded by efficiently checking a sufficient condition for Lyapunov stability of sampled-data nonlinear systems. We evaluate our technique on three case studies: an artificial pancreas model, a powertrain control model, and a quadruple-tank process.
Year
DOI
Venue
2019
10.1109/ACCESS.2020.3028476
IEEE ACCESS
Keywords
DocType
Volume
Nonlinear systems, Safety, Stochastic processes, Noise measurement, Closed loop systems, Lyapunov methods, Formal controller synthesis, parameter synthesis, probabilistic guarantees, safety verification, sampled-data nonlinear systems, satisfiability modulo theories, statistical model checking, stochastic systems
Journal
8
ISSN
Citations 
PageRank 
2169-3536
0
0.34
References 
Authors
31
7
Name
Order
Citations
PageRank
Fedor Shmarov112.71
Sadegh Esmaeil Zadeh Soudjani217523.12
Nicola Paoletti39815.69
Ezio Bartocci473357.55
Shan Lin515722.13
Scott A. Smolka62959249.22
Paolo Zuliani702.03