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)