OmegaThreads: Symbolic Controller Design for Omega-regular Objectives

OmegaThreads is a tool for automatic synthesis of 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.

OmegaThreads is implemented in C++ and OpenCL on top of pFaces. Inputs are given as text configuration files. A Python interface and a 2D simulator are provided to access the synthesized Mealy machines and to simulate the closed-loop behavior of the control system.

Download

OmegaThreads is an open-source tool and can be downloaded from its GitHub repository. OmegaThreads requires the acceleration ecosystem, pFaces, which can be downloaded from here.

Tool paper and related works

M. Khaled and M. Zamani. OmegaThreads: Symbolic controller design for omega-regular objectives. The 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), May 2021. (Top two finalist for the best poster/demo award )

Support

Please report any problems/bugs you face while installing and running OmegaThreads to Mahmoud Khaled.