| Documentation & Paper | Build Status | Quality |
|---|---|---|
   |
  |
 |
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).
Controlling a complex system traditionally means a team of experts hand-crafting an ad hoc controller over months. Dionysos turns this into an automatic pipeline:
describe the system → select the specification → pick a solver → obtain a controller together with a formal certificate.
The system is abstracted into a finite-state automaton by discretizing its variables; a controller is synthesized on that finite object with graph algorithms and then concretized back to the original system with a formal guarantee. Dionysos is an ecosystem, not a single algorithm: 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.
It solves reach-avoid, safety, reach-and-stay, and co-safe LTL specifications with a catalog of 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).
Describe a system and a specification in a JuMP model, pick the solver by choosing the optimizer, and read back the controller:
using Dionysos, JuMP, StaticArrays
model = Model(Dionysos.Optimizer)
# State and input variables, with the initial state as `start`.
@variable(model, x_low[i] <= x[i = 1:3] <= x_upp[i], start = x0[i])
@variable(model, -1 <= u[1:2] <= 1)
# Dynamics, written with the `∂` (derivative) operator ...
@constraint(model, ∂(x[1]) == u[1] * cos(α + x[3]) * sec(α))
@constraint(model, ∂(x[2]) == u[1] * sin(α + x[3]) * sec(α))
@constraint(model, ∂(x[3]) == u[1] * tan(u[2]))
# ... and the target set, written with `final`.
@constraint(model, final(x[1]) in MOI.Interval(3.0, 3.6))
@constraint(model, final(x[2]) in MOI.Interval(0.3, 0.9))
# Solver parameters: discretization grids and time step.
set_attribute(model, "time_step", 0.3)
set_attribute(model, "state_grid", Dionysos.Mapping.GridFree(x0, hx))
set_attribute(model, "input_grid", Dionysos.Mapping.GridFree(u0, hu))
optimize!(model)
concrete_controller = get_attribute(model, "concrete_controller")See the Path planning example for the complete, runnable version, and Getting Started for the building blocks.
| Path | Description |
|---|---|
src/ |
The Dionysos library (Utils, System, Problem, Mapping, Symbolic, Optim). |
ext/ |
Package extensions behind optional dependencies (Plots, Symbolics, Spot, CSV, …). |
problems/ |
Reusable benchmark problem library (path planning, DC-DC, pendulum, …). |
scripts/ |
Runnable case-study scripts, one folder per example. |
docs/ |
Documentation site and examples. |
test/ |
Test suite, mirroring the src/ layout. |
Install Julia (≥ 1.10), then add Dionysos from the Julia REPL:
import Pkg
Pkg.add("Dionysos")The full documentation, including the manual, examples, and API reference, is available for the released version and the development version. If Dionysos is useful in your research, please cite the JuliaCon paper.
Contributions are welcome. Please open an issue to report a bug or discuss a feature, and see the Developer Docs in the documentation for the setup, conventions, and Git workflow.
This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme under grant agreement No 864017 - L2C.