# SySCoRe: Synthesis via Stochastic Coupling Relations

## TL;DR

SySCoRe is a MATLAB toolbox that synthesizes controllers for stochastic systems with complex temporal logic specifications, supporting nonlinear dynamics and providing formal robustness guarantees with efficient computation methods.

## Contribution

It introduces a novel approach supporting nonlinear dynamics and infinite-horizon specifications, with probabilistic coupling and tensor-based computations for robust controller synthesis.

## Key findings

- Provides non-trivial lower bounds for infinite-horizon properties
- Supports complex co-safe temporal logic specifications
- Efficiently computes transition probabilities using tensor representation

## Abstract

We present SySCoRe, a MATLAB toolbox that synthesizes controllers for stochastic continuous-state systems to satisfy temporal logic specifications. Starting from a system description and a co-safe temporal logic specification, SySCoRe provides all necessary functions for synthesizing a robust controller and quantifying the associated formal robustness guarantees. It distinguishes itself from other available tools by supporting nonlinear dynamics, complex co-safe temporal logic specifications over infinite horizons and model-order reduction. To achieve this, SySCoRe generates a finite-state abstraction of the provided model and performs probabilistic model checking. Then, it establishes a probabilistic coupling to the original stochastic system encoded in an approximate simulation relation, based on which a lower bound on the satisfaction probability is computed. SySCoRe provides non-trivial lower bounds for infinite-horizon properties and unbounded disturbances since its computed error does not grow linearly in the horizon of the specification. It exploits a tensor representation to facilitate the efficient computation of transition probabilities. We showcase these features on several benchmarks and compare the performance of the tool with existing tools.