Overview

This page is the map of the toolbox: how the code is organised, which specifications and solvers exist, and the one interface that ties them together. For the idea behind the method, read Abstraction-based control first; to see it used, read Getting started.

Code structure

The library lives in src, split into six modules loaded in dependency order:

On top of them sits Wrapper, the JuMP front-end reached through Model(Dionysos.Optimizer). It compiles a JuMP model into a system plus a ProblemType and hands both to a solver, so it owns no control semantics of its own.

Systems

Dionysos uses the system types of:

• MathematicalSystems — generic, flexible system definitions (discrete-/continuous-time, constrained, noisy). For instance a NoisyConstrainedAffineControlDiscreteSystem of the form

  \[x(k+1) = A x(k) + B u(k) + c + D w(k), \quad x(k)\in\mathcal{X},\ u(k)\in\mathcal{U},\ w(k)\in\mathcal{W},\]

  where $\mathcal{X}$, $\mathcal{U}$ and $\mathcal{W}$ are the state, input and noise constraints.
• HybridSystems — extends the above to hybrid systems: several modes, guarded transitions, reset maps.

Problems

The specifications currently supported. Each is a system $\mathcal{S}$ plus an initial set $\mathcal{I}$, a horizon $T$, and whatever sets the property itself needs: a target $\mathcal{T}$, a safe set $\mathcal{S}_{\text{safe}}$, a state cost $\mathcal{V}$ and a transition cost $\mathcal{C}$. See the Problem reference for the full definitions.

The safe set of a reach-avoid problem is optional (nothing means the whole state space), and it is not the same as carving the unsafe region out of the state set: a region removed from the state space is never abstracted, so the synthesis cannot reason about it, whereas a safe set keeps it representable and lets the controller actively avoid it. The front-end writes the first as ∉ and the second as Always.

Two abstraction-only problems parametrize the construction of a reusable abstraction without a control objective: AlternatingSimulationProblem and BisimulationQuotientProblem.

Discrete solvers

Once a system has been abstracted, the control problem is a graph problem, and these solvers take it from there. They consume an automaton, so they apply equally to an abstraction of a continuous system, a flattened hybrid product, or an automaton written by hand.

Write $n$ for the number of abstract states, $m$ for the number of inputs and $E$ for the number of transitions. Every algorithm below is built from the controllable predecessor

\[\mathrm{Pre}(Y) = \{\, q \mid \exists u,\ \emptyset \neq \mathrm{Post}(q,u) \subseteq Y \,\}\]

— a state is winning if some input keeps every possible successor inside the set already won. The quantifier over successors is what makes a nondeterministic abstraction sound.

$r$ is the number of times the invariant core grows, and $\lvert Q_\varphi\rvert$ the size of the monitor. Only the last two return a controller with memory.

Continuous solvers

All abstraction-based: they discretize the state and input spaces, synthesize on the resulting automaton with a discrete solver, then concretize the controller back.

Hybrid solvers

For systems with several modes, guarded transitions and reset maps. The first two abstract, the last two attack the hybrid problem directly.

The solver interface

This is the architectural keystone. Every solver is a submodule exposing an Optimizer <: MOI.AbstractOptimizer, configured with raw attributes and run through MOI.optimize!:

1. instantiate — optimizer = MOI.instantiate(SomeFamily.Optimizer);
2. configure — MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), problem) and the solver-specific parameters ("state_grid", "input_grid", "time_step", …);
3. run — MOI.optimize!(optimizer);
4. query — MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller")).

For abstraction-based solvers, optimize! follows the same conceptual pipeline:

concrete problem → abstraction (symbolic model) → abstract problem
                 → abstract controller → concrete controller

The abstraction is cached, so switching the specification on the same system (e.g. safety → reachability) does not recompute it. Solvers compose: a high-level optimizer holds an abstraction_solver and a control_solver and forwards attribute set/get to them.

Why it matters: swapping the solver

Because the specification is a solver-independent object, the same control problem can be handed to a different algorithm without rewriting it. Only the optimizer and its parameters change:

# One problem …
concrete_problem = PR.OptimalControlProblem(system, initial_set, target_set, nothing, nothing)

# … solved by a grid abstraction …
grid = MOI.instantiate(AB.UniformGridAbstraction.Optimizer)
MOI.set(grid, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
MOI.set(grid, MOI.RawOptimizerAttribute("state_grid"), MP.GridFree(x0, hx))
MOI.optimize!(grid)

# … or by an ellipsoidal one, on the very same object.
ellips = MOI.instantiate(AB.UniformEllipsoidAbstraction.Optimizer)
MOI.set(ellips, MOI.RawOptimizerAttribute("concrete_problem"), concrete_problem)
MOI.set(ellips, MOI.RawOptimizerAttribute("sdp_solver"), sdp_solver)
MOI.optimize!(ellips)

Both then answer MOI.TerminationStatus and hand back a concrete_controller, so results are directly comparable. This is what makes benchmarking algorithms — rather than re-implementing problems — the normal way to work in Dionysos. The Solver families examples each drive one optimizer this way.

The two entry styles

The JuMP front-end is the canonical one: it writes the system and the specification as constraints and picks the solver for you. It reaches the uniform grid abstraction and the hybrid abstraction. Start from Getting started; the full vocabulary is in the Wrapper reference.

Direct MathOptInterface builds the ProblemType by hand and configures one family optimizer. It is the way to reach the solvers whose inputs the front-end cannot express — PWA systems, ellipsoid templates, observation regions — and the way new solvers are exercised first.

Both report solution status identically, because the status is answered by the solvers themselves.

Plotting

Every structure worth looking at — trajectories, discretizations, specifications, obstacles, abstractions — carries a @recipe, so results are displayed with the single plot function of Plots.jl. Closed-loop runs can additionally be animated as a multi-panel dashboard with animate_trajectory_dashboard; every example ends with one.