Mascot follows the abstraction-based control paradigm. The controller synthesis happens in three stages: (a) abstraction (by means of state space and time discretization) of the continuous system by a finite state abstract system, (b) synthesis of an abstract controller for the abstract system, (c) refinement of the abstract controller to a concrete controller.
The innovation of Mascot is the replacement of a single monolithic abstraction by lazily computed multiple abstractions of varying granularity. The synthesis starts on a very coarse (and cheap to compute) abstraction layer. The finer abstraction layers (expensive to compute), which are initially empty, are explored and used for synthesis only when needed. On an example controlling an unicycle in a maze, the speed-up was 5x as compared to the normal monolithic synthesis on the finest abstraction layer. For details, please refer to the paper[1,2,3].
[1] K. Hsu, R. Majumdar, K. Mallik, and A.-K. Schmuck. Multi-layered abstraction-based controller synthesis for continuous-time systems. HSCC 2018. [2] K. Hsu, R. Majumdar, K. Mallik, and A.-K. Schmuck. Lazy Abstraction-Based Control for Reachability. arXiv preprint arXiv:1804.02722. [3] K. Hsu, R. Majumdar, K. Mallik, and A.-K. Schmuck. Lazy Abstraction-Based Control for Safety Specifications. arXiv preprint arXiv:1804.02666.
