About

Mascot-SDS is a tool for controller synthesis for discrete-time dynamical systems with additive stochastic noise. The control task can be any property expressible in LTL or, more generally, using an omega-automaton. The synthesized controller comes with formal correctness guarantees.

At the moment, the tool computes controllers for almost sure (probability 1) satisfaction of the specification. We will extend support to the quantitative aspect in future.

The references for the tool are listed at the bottom of this page.

Mascot-SDS is written in C++, and is a successor of Mascot^[1]; the suffix SDS stands for Stochastic Dynamical Systems.

HIGHLIGHTS OF THE NEW RELEASE (ver 2.0):

Simplified front-end
Integration with the flexible back-end solver Genie
Lightweight simulator of the synthesized closed-loop

Contact persons for bug reporting:

Mateusz Rychlicki (email: scmkry (at) leeds.ac.uk),
Kaushik Mallik (email: kmallik (at) mpi-sws.org).

Cite our tool as:

R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani. A Flexible Toolchain for Symbolic Rabin Games under Fair and Stochastic Uncertainties.CAV 2023 (to appear).

References for the theory

[1] R. Majumdar, K. Mallik, M. Rychlicki, A.-K. Schmuck, and S. Soudjani. Fast symbolic algorithms for omega-regular games under strong transition fairness. TheoretiCS, 2.
[2] T. Banerjee, R. Majumdar, K. Mallik, A.-K. Schmuck, and S. Soudjani. A direct symbolic algorithm for solving stochastic rabin games.TACAS 2022.
[3] R. Majumdar, K. Mallik, and S. Soudjani. Symbolic Controller Synthesis for Büchi Specifications on Stochastic Systems. HSCC 2020.