SySCoRe: Synthesis via Stochastic Coupling Relations

DOI10.1145/3575870.3587123arXiv2302.12294OpenAlexW4375852219MaRDI QIDQ6202092FDOQ6202092

Authors: Birgit C. van Huijgevoort, Sadegh Soudjani, Sofie Haesaert 

Publication date: 21 February 2024

Published in: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/2302.12294

zbMATH Keywords

dynamic programmingstochastic systemsapproximate simulation relationtemporal logic controlcoupling relations

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)

Cites Work

• Title not available (Why is that?)
• SReachTools
• \textsf{AMYTISS}: parallelized automated controller synthesis for large-scale stochastic systems
• StocHy - automated verification and synthesis of stochastic processes
• Verification and Control of Hybrid Systems
• Title not available (Why is that?)
• Construction of Equivalent Stochastic Differential Equation Models
• Probabilistic Reach-Avoid Computation for Partially Degenerate Stochastic Processes
• Title not available (Why is that?)
• Model checking of safety properties
• Title not available (Why is that?)
• On the numerical solution of the discrete-time algebraic Riccati equation
• Automated verification and synthesis of stochastic hybrid systems: a survey
• Title not available (Why is that?)
• Formal methods for discrete-time dynamical systems
• SCOTS: a tool for the synthesis of symbolic controllers
• Symbolic controller synthesis for Büchi specifications on stochastic systems
• Verification of general Markov decision processes by approximate similarity relations and policy refinement
• Formal Synthesis of Stochastic Systems via Control Barrier Certificates
• ProbReach: verified probabilistic delta-reachability for stochastic hybrid systems
• Robust Dynamic Programming for Temporal Logic Control of Stochastic Systems
• State-based confidence bounds for data-driven stochastic reachability using Hilbert space embeddings
• Similarity quantification for linear stochastic systems: a coupling compensator approach

This page was built for publication: SySCoRe: Synthesis via Stochastic Coupling Relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6202092)