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.

In this ongoing work, we address data-driven computation of controllers that are correct by design for safety-critical systems and can provably satisfy complex functional requirements. We propose a two-stage approach that decomposes the problem into a data-driven stage and a robust formal controller synthesis stage. The first stage utilizes available Bayesian linear regression methods to compute robust confidence sets for the true parameters of the system. The second stage develops methods for systems subject to both stochastic and parametric uncertainties. We provide simulation relations for enabling control refinement that are founded on coupling uncertainties of stochastic systems via sub-probability measures. Such relations are essential for constructing abstract models that are related to not only one model but to a set of parametric models.