SySCoRe: Synthesis via Stochastic Coupling Relations

DOI10.1145/3575870.3587123MaRDI QIDQ6202092zbMATH OpenOpenAlexFDO

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)

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)

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.

Cites work

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

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)