Dionysos

Dionysos is a Julia framework for correct-by-construction controller synthesis through symbolic (abstraction-based) control. It is the software of the ERC project Learning to Control (L2C).

What Dionysos does

Designing a controller for a complex system traditionally requires a team of experts hand-crafting an ad hoc controller over months. Dionysos aims to turn that into an automatic pipeline:

describe the system → select the specification → pick a solver → obtain a controller together with a formal certificate.

The underlying technique is symbolic control: the continuous system is abstracted into a finite-state automaton by discretizing its variables, a controller is synthesized on that finite object with graph algorithms (Dijkstra, A*, fixed-point iterations), and it is then concretized back to the original system with a formal guarantee. To fight the curse of dimensionality, a core research direction of the toolbox is smart / lazy abstractions that co-design the abstraction and the controller, computing only the part of the abstraction that is actually needed.

Dionysos is an ecosystem, not a single algorithm. Its value is a common interface — every solver is a MathOptInterface optimizer, driven through JuMP — so a control task can be re-solved, compared, and benchmarked by swapping the solver rather than rewriting the model.

A control problem in Dionysos

A control problem is a pair (𝒮, Σ):

a system 𝒮 — a MathematicalSystems or HybridSystems object describing the dynamics ẋ = f(x, u) and the state/input constraints;
a specification Σ — a ProblemType such as reach-avoid, safety, reach-and-stay, or co-safe LTL.

It is solved by an optimizer 𝒪 (an AbstractOptimizer), which returns a controller and its certificate.

Current capabilities

Specifications: reach-avoid optimal control, safety, reach-and-stay, and co-safe LTL, plus abstraction-only problems (alternating simulation, bisimulation quotient). See the Problem reference.
Solvers: uniform grid abstraction (SCOTS-style), uniform and lazy ellipsoidal abstractions, hybrid-system abstraction, a PCLF bisimulation quotient, discrete-automaton synthesis, and optimization-based solvers (Bemporad–Morari, branch and bound). See the Optim reference and the Manual.
Interfaces: a canonical JuMP frontend (Model(Dionysos.Optimizer)) and direct MathOptInterface access.

Structure of the documentation

The Manual explains abstraction-based control and how to use Dionysos as a user.
Getting Started walks through the basic building blocks; start there to get familiar with the toolbox.
The Solvers and Utils sections collect runnable examples.
The API Reference documents every public symbol, grouped by module.
The Developer Docs are for contributors.

Need help?

If you need help, open an issue on GitHub.