|
Software
Here, we present the software tools developed in the HyConSys lab. You can access each tool from the following list:
 SCOTS, a powerful software tool, facilitates the automatic synthesis of controllers for nonlinear control systems based on symbolic models, also referred to as discrete abstractions. This innovative tool takes a differential equation describing a nonlinear control system as input. By employing a Lipschitz-type estimation on the right-hand-side of the differential equation, coupled with various discretization parameters, SCOTS computes a symbolic model that establishes a feedback refinement relation with the original control system.
Notably, SCOTS offers comprehensive support for the computation of minimal and maximal fixed points, enabling the synthesis of controllers that adhere to both invariance and reachability specifications. The flexibility of the tool is further augmented by allowing atomic propositions, which serve as the basis for specifying requirements, to be defined using finite unions and intersections of polytopes as well as ellipsoids.
While the core computations are performed in C++, SCOTS also provides a convenient Matlab interface. This interface facilitates simulation of the closed-loop system and facilitates visualization of the abstract state space, in conjunction with the atomic propositions.
|
 In the realm of networked control systems (NCS), the traditional focus on basic stabilizability has shifted to more advanced objectives, such as expressing requirements through linear temporal logic formulae or automata on infinite strings. To tackle these complex challenges, a promising approach involves symbolic models, which approximate concrete systems using finite abstractions, enabling the automated synthesis of correct-by-construction controllers. SENSE, a cutting-edge tool, has been specifically developed for constructing finite abstractions for NCS and synthesizing controllers to enforce complex specifications over the plant, while accounting for various non-idealities of the communication channels.
By leveraging operations on binary decision diagrams (BDDs), SENSE efficiently constructs a symbolic model of the NCS based on the symbolic model of the plant and network parameters. It further synthesizes symbolic controllers that satisfy a wide range of specifications. The tool offers seamless interfaces for simulating and visualizing the resulting closed-loop systems using OMNET++ and MATLAB. Additionally, SENSE is capable of generating implementation-ready code in VHDL, Verilog, or C/C++ directly from the synthesized controllers.
|
 QUEST is an exceptional open-source software tool designed for the automated synthesis of controllers for incrementally input-to-state stable nonlinear control systems. This tool accepts ordinary differential equations as the descriptions of the nonlinear control systems. By employing a state-space quantization-free approach, QUEST constructs symbolic models that effectively address the challenging issue of the curse of dimensionality, particularly when dealing with high-dimensional state-spaces.
With its advanced capabilities, QUEST facilitates the computation of both minimal and maximal fixed points, enabling the synthesis of controllers that enforce safety and reachability specifications. Leveraging the power of C++, all computations within the tool are executed efficiently, ensuring optimal performance.
|
 pFaces stands out as a remarkable and extensible software ecosystem specifically crafted to expedite the application of symbolic control techniques. Its comprehensive features enable the seamless design of parallel algorithms while efficiently managing available computing resources during their execution.
In the realm of abstraction-based controller synthesis, pFaces truly shines by introducing novel parallel algorithms that harness the full potential of heterogeneous computing platforms. Whether it's CPUs, GPUs, or Hardware Accelerators (HWAs), pFaces seamlessly dispatches these cutting-edge algorithms for parallel execution, capitalizing on the power of multiple processing elements (PEs).
The remarkable results obtained using pFaces are truly astounding, demonstrating a significant reduction in computation time by several orders of magnitude as the number of PEs increases. This unprecedented level of performance easily surpasses the capabilities of existing tools, establishing pFaces as the forefront solution in accelerating symbolic control techniques.
|
 AMYTISS, implemented in C++,OpenCL, is an exceptional tool specifically designed for the development of correct-by-construction controllers for large-scale discrete-time stochastic systems. At its core, AMYTISS leverages the power of finite Markov decision processes (MDPs) to create finite abstractions of the original systems. These abstractions serve as the foundation for synthesizing controllers that fulfill bounded-time high-level properties, including safety, reachability, and reach-avoid specifications.
AMYTISS stands out by offering scalable parallel algorithms that support parallel execution across diverse computing platforms, including CPUs, GPUs, and hardware accelerators (HWAs). This flexibility enables users to harness the full potential of high-performance computing (HPC) platforms and cloud-computing services. By leveraging these advanced resources, AMYTISS effectively mitigates the notorious state-explosion problem that plagues the analysis of large-scale stochastic systems, making it a truly groundbreaking tool in the field.
|
 PIRK, serving as a powerful kernel within the pFaces acceleration ecosystem, empowers researchers and engineers to efficiently compute reachable sets for general nonlinear systems characterized by extraordinarily high dimensions. By leveraging the capabilities of high-performance computing (HPC) platforms, PIRK opens up new horizons for analyzing and visualizing reachable sets in the context of high-dimensional nonlinear systems.
This pioneering tool introduces three innovative parallel algorithms that revolutionize the computation of interval approximations for forward reachable sets. The first algorithm capitalizes on the component-wise contraction properties of the system. The second algorithm leverages mixed monotonicity, further enhancing the accuracy and effectiveness of the interval approximations. Finally, the third algorithm harnesses the power of Monte Carlo-based approaches.
The scalability and versatility of PIRK have been thoroughly tested and proven on various systems, pushing the boundaries of dimensionality to new heights. With state dimensions reaching up to an impressive 4 billion, PIRK enables researchers to delve into the intricate behavior of high-dimensional nonlinear systems and obtain valuable insights into their reachable sets.
|
 OmegaThreads, an innovative kernel built upon the robust pFaces acceleration ecosystem, revolutionizes the automatic synthesis of correct-by-construction controllers for control systems, enabling the realization of complex specifications expressed in omega-regular formalisms. With OmegaThreads, the process begins by accepting general nonlinear control systems, from which symbolic models, also known as discrete abstractions, are constructed. The power lies in the flexibility of specification inputs, which can be provided either as deterministic parity Automata (DPA) or as expressive linear temporal logic (LTL) formulae, allowing for a wide range of specifications to be accommodated.
Using state-of-the-art techniques, OmegaThreads constructs two-player parity games and diligently searches for winning strategies, with the controller playing against the symbolic models. Once a winning strategy is found, OmegaThreads extracts the strategies as Mealy machines, providing a tangible representation of the synthesized controllers.
The implementation of OmegaThreads is meticulously crafted in C++ and OpenCL, leveraging the capabilities of pFaces to deliver optimal performance. The user-friendly nature of OmegaThreads is enhanced through its support for text configuration files as inputs, simplifying the integration of the tool into existing workflows. To further facilitate interaction and analysis, OmegaThreads offers a Python interface and a versatile 2D simulator, empowering users to access and explore the synthesized Mealy machines while simulating the closed-loop behavior of the control system.
|
|