Here, we present the software and tools developed in the HyConSys lab. You can access each tool from the following list:

SCOTS: A Tool for the Synthesis of Symbolic Controllers

SCOTS is an open source software tool for the synthesis of symbolic controllers for possibly perturbed, nonlinear, control systems. It is mainly implemented in C++ and it comes with a small MATLAB interface to access the synthesized controller from within MATLAB.

SENSE: Abstraction-Based Synthesis of Networked Control Systems

SENSE is an open source framework for the abstraction construction and for synthesizing symbolic controllers for networked control systems. It is mainly implemented in C++ and it comes with MATLAB and OMNET++ interfaces to access the synthesized controller and simulate the closed loop.
It comes with many helper tools to facilitate the analysis of the resulting symbolic models and the synthesized symbolic controllers. One particular tool allows for the automatic code generation of the resulting symbolic controllers.

QUEST: A Tool for State-Space Quantization-Free Synthesis of Symbolic Controllers

QUEST is an open source software tool for automated controller synthesis of incrementally input-to-state stable nonlinear control systems using state-space quantization-free approach for the construction of symbolic abstraction which can be potentially more beneficial for systems with high-dimensional state spaces. The tool is implemented in C++.

pFaces: An Acceleration Ecosystem for Formal Methods in Control

pFaces is a generic Cloud-ready, multi-compute-platform, tool for accelerating parallel algorithms designed for mformal methods in control. Faces is an acceleration engine that works with kernels representing different software sections. Other tools are implemented as parallel algorithms on top of pFaces as kernels.

AMYTISS: Parallel Automated Controller Synthesis for Large-scale Stochastic Systems

AMYTISS is a kernel on top of the acceleration ecosystem pFaces, for designing correct-by-construction controllers of stochastic discrete-time systems. AMYTISS is used to: (1) build finite Markov decision processes (MDPs) as finite abstractions of given original stochastic discrete-time systems; and (2) synthesize controllers for the constructed finite MDPs satisfying bounded-time safety specifications and reach-avoid specifications.

PIRK: Parallel Computation of Reachable Sets for General Nonlinear Systems

PIRK is a kernel on top of the acceleration ecosystem pFaces to efficiently compute reachable sets for general nonlinear systems of extremely high dimensions. It introduces three parallel algorithms for computing interval approximations of forward reachable sets, based on: component-wise contraction properties, mixed monotonicity, and Monte Carlo-based approaches.