Mascot-SDS is a (open-source) tool for synthesizing controllers—with formal correctness guarantees—for discrete-time dynamical systems in the presence of stochastic perurbation. It is the first tool that can support infinite-horizon control specifications for stochastic dynamical systems. Currently Mascot-SDS can only produce controllers which satisfy a given Büchi specification (repeated reachability) with probability 1.
Mascot-SDS is written in C++, and is an extension of Mascot[1]. The suffix SDS stands for Stochastic Dynamical Systems.
To cite Mascot-SDS, please cite our paper[2] which presents the underlying theory.
Please report any bug/comment to Kaushik Mallik (email: kmallik (at) mpi-sws.org).
[1] K. Hsu, R. Majumdar, K. Mallik, and A.-K. Schmuck. Multi-layered abstraction-based controller synthesis for continuous-time systems. HSCC 2018. [1] R. Majumdar, K. Mallik, and S. Soudjani. Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems. HSCC 2020 (to appear).
