# Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems

## TL;DR

This paper introduces an automated method for synthesizing digital controllers that guarantee safety in stochastic nonlinear systems, combining rapid candidate generation with rigorous verification to ensure probabilistic safety thresholds.

## Contribution

The paper presents a novel synthesis approach that integrates Monte Carlo-based candidate generation with SMT-based verification for safety guarantees in nonlinear stochastic systems.

## Key findings

- Successfully applied to artificial pancreas, powertrain, and quadruple-tank systems.
- Achieved high safety probability with rapid candidate synthesis.
- Validated safety guarantees using SMT-based confidence intervals.

## 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. The proposed synthesis method alternates between two steps: generation of a candidate controller pc, and verification of the candidate. pc is found by maximizing a Monte Carlo estimate of the safety probability, and by using a non-validated ODE solver for simulating the system. Such a candidate is therefore sub-optimal but can be generated very rapidly. To rule out unstable candidate controllers, we prove and utilize Lyapunov's indirect method for instability of sampled-data nonlinear systems. In the subsequent verification step, we use a validated solver based on SMT (Satisfiability Modulo Theories) to compute a numerically and statistically valid confidence interval for the safety probability of pc. If the probability so obtained is not above the threshold, we expand the search space for candidates by increasing the controller degree. We evaluate our technique on three case studies: an artificial pancreas model, a powertrain control model, and a quadruple-tank process.