Software

Here, we present the software 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 perturbed, nonlinear, control systems. It is mainly implemented in C++ and it comes with a small MATLAB interface to access the synthesized controller within MATLAB.

SENSE: Symbolic Controllers for Networked Control Systems

SENSE is an open source framework for the abstraction construction and 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 controllers and simulate the closed loop.
It comes with many helper tools to facilitate the analysis of the resulting symbolic models and the synthesized controllers. One particular tool allows for the automatic code generation of the resulting symbolic controllers.

QUEST: A Tool for the Synthesis of Symbolic Controllers without State-Space Discretization

QUEST is an open source software tool for automated controller synthesis of incrementally input-to-state stable nonlinear control systems. The tool does not need discretizing state set for the construction of symbolic abstractions which can be potentially more beneficial for systems with high-dimensional state sets. 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 formal methods in control. pFaces 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 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.

OmegaThreads: Symbolic Controller Design for omega-regular Objectives

OmegaThreads is a kernel on top of the acceleration ecosystem pFaces to efficiently compute correct-by-construction controllers for control systems from omega-regular specifications.It accepts general nonlinear control systems from which discrete abstractions (a.k.a. symbolic models) are constructed.Specifications are provided directly as deterministic parity Automata (DPA) or as linear temporal logic (LTL) formulae.OmegaThreads constructs two-player parity games and searches for a winning strategies playing as a controller against the symbolic models.If found, OmegaThreads extracts the winning strategies as a Mealy machines.