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. The suffix SDS stands for Stochastic Dynamical Systems.
To cite Mascot-SDS, please cite our paper which presents the underlying theory.
Please report any bug/comment to Kaushik Mallik (email: kmallik (at) mpi-sws.org).