Optim

This folder contains all the different (abstraction-based or not) solvers that can be used. Note that all the solvers are defined using the MathOptInterface framework as a subtype of AbstractOptimizer by implementig the optimize! function.

Abstraction-based solvers

Uniform grid abstraction solver

Dionysos.Optim.Abstraction.UniformGridAbstraction.OptimizerType
Optimizer{T} <: MOI.AbstractOptimizer

A high-level abstraction-based solver that automatically orchestrates system abstraction and control synthesis. This wrapper follows the classical abstraction pipeline (e.g., as in SCOTS), where the state and input spaces are discretized into hyper-rectangular cells, independent of the specific control task.

It delegates responsibility to modular sub-solvers: one for abstraction and one for control, depending on the type of problem to be solved.


Structure and Sub-solvers

The optimizer internally manages two sub-solvers:


Behavior

  • The user sets the control task via: MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem) where my_problem is a subtype of ProblemType.

  • The optimizer automatically dispatches to the appropriate control solver based on the problem type.

  • If the abstraction has not yet been computed, it is automatically built before solving the control problem.

  • Once computed, the abstraction is cached — switching the control problem (e.g., from safety to reachability) does not recompute it.

  • The field solve_time_sec tracks the runtime of the last call to MOI.optimize!.

  • The resulting controller and value function are stored and can be queried from the wrapper.


User-settable and access to subsolver fields

Via MOI.set(...), the user may configure abstraction_solver and control_solver parameters. Any field accessible in the sub-solvers (abstraction or control) can be transparently accessed via:

MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), grid)
MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_value_function"))

Example

using Dionysos, JuMP
optimizer = MOI.instantiate(Dionysos.Optim.UniformGridAbstraction.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("time_step"), 0.1)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("solve_time_sec"))
value_fun = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_value_function"))
controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller"))
source
Dionysos.Optim.Abstraction.UniformGridAbstraction.OptimizerEmptyProblemType
OptimizerEmptyProblem{T} <: MOI.AbstractOptimizer

A solver responsible for constructing a symbolic abstraction of the system dynamics, independently of any control specification.

This optimizer wraps everything needed to solve an EmptyProblem, which is used to generate a symbolic model (abstraction) of either a continuous- or discrete-time system.

The optimizer supports several abstraction modes, optional implicit mappings/state sets, periodic mappings, multithreaded computation, and distributed partition-based abstraction.


Purpose

This optimizer builds a symbolic abstraction by discretizing the state and input spaces, constructing a state/input mapping, defining a source-state domain, and computing the abstract transition relation from a system approximation.

The abstraction method is selected via the approx_mode field. Depending on the chosen mode, the optimizer constructs either an over-approximation, an under-approximation, or a simulation-based abstraction.

The resulting abstract model can then be reused by higher-level control solvers (safety, reachability, co-safe LTL, etc.).


Abstraction semantics

The constructed symbolic model distinguishes between:

  • XMapping: global mapping from concrete states to abstract states.
  • Xset: set of source states that are enumerated when building transitions.
  • Rset: set of retained / allowed states that may appear as transition targets.
  • UMapping: mapping from concrete inputs to abstract inputs.
  • Uset: admissible abstract-input set.

In the standard non-distributed setting, Xset usually coincides with Rset. In distributed mode, the abstraction may be computed on local partitions of Xset, while retaining a common global Rset.


Parameters

Mandatory fields set by the user

  • empty_problem (required): An instance of EmptyProblem containing the system to abstract and the target abstraction region.

  • State discretization (required):

    • either state_grid
    • or h, from which the state grid is built internally.
  • input_grid (required, unless UMapping is set directly): The discretization grid for the input space.

Optional mapping / set fields

  • abstraction_region (optional): Concrete region used to define the abstraction domain. If not provided, the optimizer uses:

    1. empty_problem.region, if available,
    2. otherwise empty_problem.system.X.
  • incl_mode (optional, default = MP.INNER): Inclusion mode used when constructing mappings or state sets.

  • XMapping (optional): Pre-built abstract-state mapping. If not provided, it is constructed from the state grid.

  • Xset (optional): Source abstract-state set. If not provided, it is built from abstraction_region.

  • Rset (optional): Retained / allowed target-state set. If not provided, it defaults to copy(Xset).

  • UMapping (optional): Pre-built abstract-input mapping.

  • Uset (optional): Abstract-input set. If not provided, a default admissible set is built.

Grid / implicit representation settings

  • state_grid (optional): Explicit state grid used for discretization.

  • h (optional): Grid spacing vector used to construct the state grid if state_grid is not provided.

  • use_implicit_mapping (optional, default = false): If true, constructs an implicit state mapping instead of an explicit one.

  • mapping_region (required if use_implicit_mapping = true): Hyper-rectangle used as ambient region for the implicit mapping. It must enclose abstraction_region.

  • use_implicit_stateset (optional, default = false): If true, builds Xset as an implicit state set rather than an explicit set of indices.

Periodic mapping settings

  • use_periodic_mapping (optional, default = false): If true, wraps the state mapping as a periodic mapping.

When enabled, the following fields are required:

  • periodic_dims: indices of periodic dimensions.
  • periodic_periods: period length for each periodic dimension.
  • periodic_start (optional): start point for each periodic dimension. Defaults to zero if not provided.

System approximation settings

  • approx_mode (optional, default = GROWTH): Abstraction technique used to build the system approximation. Supported modes:

    • USER_DEFINED: Use a custom over-approximation map. Set overapproximation_map.

    • GROWTH: Use growth-bound based approximation. Set jacobian_bound, or directly growthbound_map. ngrowthbound controls the internal growth-bound discretization parameter.

    • LINEARIZED: Use linearization and derivative bounds. Set DF_sys, bound_DF, and bound_DDF.

    • CENTER_SIMULATION: Simulate the center of each abstract cell only.

    • RANDOM_SIMULATION: Simulate randomly sampled points in each abstract cell. Set n_samples.

  • efficient (optional, default = true): Whether to use the optimized approximation-specific abstraction kernel when available.

Continuous-time settings

  • time_step (required for continuous-time systems): Sampling step used to discretize a continuous-time approximation.

  • nsystem (optional, default = 5): Number of internal substeps used during continuous-time simulation/discretization routines.

Execution settings

  • threaded (optional, default = false): If true, enables multithreaded abstraction on a single Julia process.

  • distributed (optional, default = false): If true, enables partition-based distributed abstraction across Julia worker processes.

  • distributed_procs (optional): Vector of Julia worker IDs used for distributed abstraction. If nothing, all available workers returned by Distributed.workers() are used.

  • distributed_nparts (optional): Number of source-state partitions used in distributed abstraction. If nothing, defaults to the number of selected worker processes.

  • distributed_partition_strategy (optional, default = :roundrobin): Strategy used to partition the source-state set Xset. Typical choices include :roundrobin and :contiguous.

In distributed mode, each partition receives:

  • the same global XMapping,
  • the same global Rset,
  • a local subset of Xset,

and computes transitions for its own source states. The final abstract transition relation is obtained by merging all locally computed transitions.

Logging / progress settings

  • print_level (optional, default = 1): Verbosity level:

    • 0: silent
    • 1: summary information
    • 2: detailed progress output
  • progress_update_interval (optional, default = Int(1e5)): Number of source-state/input pairs processed between progress updates.

  • progress_dt (optional, default = 0.2): Minimum wall-clock time between progress refreshes in threaded mode.


Internally computed fields (after MOI.optimize!)

  • abstract_system: The resulting symbolic abstraction, of type SymbolicModelList.

  • discrete_time_system: Internally constructed discrete-time system used to generate the abstraction.

  • abstraction_construction_time_sec: Total abstraction-construction time in seconds.

Approximation objects derived from approx_mode


Typical workflow

  1. Define the concrete empty problem and discretization parameters.
  2. Build or infer the state/input mappings and state sets.
  3. Construct the system approximation from approx_mode.
  4. Compute the abstract transition relation, either:
    • sequentially,
    • multithreaded,
    • or distributed across source-state partitions.
  5. Store the resulting symbolic abstraction in abstract_system.

Example

using Dionysos, JuMP
optimizer = MOI.instantiate(Dionysos.Optim.OptimizerEmptyProblem.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("empty_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("state_grid"), state_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("input_grid"), input_grid)
MOI.set(optimizer, MOI.RawOptimizerAttribute("time_step"), 0.1)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)
MOI.set(optimizer, MOI.RawOptimizerAttribute("approx_mode"), GROWTH)
MOI.set(optimizer, MOI.RawOptimizerAttribute("jacobian_bound"), my_jacobian_bound)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstraction_construction_time_sec"))
abstract_system = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_system"))
discrete_time_system = MOI.get(optimizer, MOI.RawOptimizerAttribute("discrete_time_system"))
source
Dionysos.Optim.Abstraction.UniformGridAbstraction.OptimizerOptimalControlProblemType
OptimizerOptimalControlProblem{T} <: MOI.AbstractOptimizer

An optimizer that solves reachability or reach-avoid optimal control problems using symbolic abstractions of the system.

This solver takes as input a concrete problem (typically an instance of OptimalControlProblem) and a symbolic abstraction of the system (i.e., an abstract_system). It then solves the abstract version of the control problem.

Key Behavior

  • Lifts the concrete problem to the symbolic abstraction space (abstract_system) and constructs the corresponding abstract_problem.
  • Computes the controllable_set — the largest set of abstract states from which reachability can be guaranteed.
  • Synthesizes an abstract_controller that brings the system to the target set under worst-case dynamics.
  • Computes the abstract_value_function that maps each state (cell) to the worst-case number of steps needed to reach the target.
  • The solver is successful if the field success is true after MOI.optimize!.

Parameters

Mandatory fields set by the user

  • concrete_problem (required): An instance of OptimalControlProblem that defines the reach-avoid task (system, initial set, target, costs, horizon).

  • abstract_system (required): The symbolic abstraction of the system, usually obtained from an abstraction optimizer such as OptimizerEmptyProblem.

Optional user-tunable parameters

  • early_stop (optional, default = false): If true, the fixpoint algorithm stops early when the initial set is fully contained in the controllable set. If false, it computes the entire maximal controllable set.

  • sparse_input (optional, default = false): If true, uses a sparse representation of the transition table, reducing memory usage when the number of inputs is large but only few are admissible per state (e.g., in determinized abstractions, with new_input = (input, target)).

  • print_level (optional, default = 1): Controls verbosity:

    • 0: silent
    • 1: default
    • 2: detailed logging

Internally computed fields

These fields are generated automatically during MOI.optimize!.

  • abstract_problem: The lifted version of the concrete problem over the abstract system.
  • abstract_problem_time_sec: Time taken to solve the abstract problem.
  • abstract_controller: A controller mapping abstract states to control inputs.
  • controllable_set: Set of abstract states from which the target is reachable.
  • uncontrollable_set: Complementary states with no admissible reachability strategy.
  • value_fun_tab: Tabular value function over abstract states (e.g., cost-to-go or step count).
  • abstract_value_function: Functional form of the abstract value function.
  • concrete_value_function: Functional form of the value function mapped back to the original system.
  • success: Boolean flag indicating whether the solver completed successfully.

Example

using Dionysos, JuMP
optimizer = MOI.instantiate(Dionysos.Optim.OptimizerOptimalControlProblem.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("abstract_system"), abstract_system)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_problem_time_sec"))
controllable_set = MOI.get(optimizer, MOI.RawOptimizerAttribute("controllable_set"))
abstract_value_function = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_value_function"))
concrete_value_function = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_value_function"))
concrete_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller"))
source
Dionysos.Optim.Abstraction.UniformGridAbstraction.OptimizerSafetyProblemType
OptimizerSafetyProblem{T} <: MOI.AbstractOptimizer

An optimizer for solving safety control problems over symbolic system abstractions.

This solver takes as input a SafetyProblem and a symbolic abstraction of the system (e.g., a SymbolicModelList), and computes a controller that ensures the system remains within a safe set over a time horizon or indefinitely.


Key Behavior

  • Lifts the concrete safety problem to the abstract domain and builds an abstract_problem.
  • Computes the invariant set, i.e., the largest set of abstract states from which all trajectories can be safely controlled.
  • Synthesizes an abstract_controller that guarantees safety under worst-case transitions.
  • The optimization is successful if success == true after calling MOI.optimize!.

Parameters

Mandatory fields set by the user

  • concrete_problem (required): An instance of SafetyProblem that specifies the system, initial set, safe set, and horizon.

  • abstract_system (required): A symbolic abstraction of the system, e.g., obtained from OptimizerEmptyProblem.

Optional user-tunable parameters

  • print_level (optional, default = 1): Controls verbosity:
    • 0: silent
    • 1: default (info)
    • 2: verbose debug output

Internally computed fields

These fields are automatically filled in by MOI.optimize!.

  • abstract_problem: The lifted version of the safety problem in the symbolic domain.
  • abstract_problem_time_sec: Time taken to solve the safety problem over the abstract system.
  • abstract_controller: A controller mapping abstract states to admissible inputs that keep the system safe.
  • invariant_set: The largest subset of abstract states from which safety can be maintained.
  • invariant_set_complement: States from which safety cannot be guaranteed.
  • success: Boolean flag indicating whether a valid invariant set and controller were found.

Example

using Dionysos,
optimizer = MOI.instantiate(Dionysos.Optim.OptimizerSafetyProblem.Optimizer)

MOI.set(optimizer, MOI.RawOptimizerAttribute("concrete_problem"), my_problem)
MOI.set(optimizer, MOI.RawOptimizerAttribute("abstract_system"), abstract_system)
MOI.set(optimizer, MOI.RawOptimizerAttribute("print_level"), 2)

MOI.optimize!(optimizer)

time = MOI.get(optimizer, MOI.RawOptimizerAttribute("abstract_problem_time_sec"))
invariant_set = MOI.get(optimizer, MOI.RawOptimizerAttribute("invariant_set"))
abstract_controller = MOI.get(optimizer, MOI.RawOptimizerAttribute("concrete_controller"))
source

Uniform ellipsoid abstraction solver

Hybrid system abstraction solver

PCLF Bisimulation Quotient solver

Other abstraction-based solvers

Other solvers

Dionysos.Optim.BemporadMorari.OptimizerType
Optimizer{T} <: MOI.AbstractOptimizer

Bemporad Morari solver: Optimal control of hybrid systems via a predictive control scheme using mixed integer quadratic programming (MIQP) online optimization procedures.

source
Dionysos.Optim.BranchAndBound.OptimizerType
Optimizer{T} <: MOI.AbstractOptimizer

Branch and bound solver: Optimal control of hybrid systems via a predictive control scheme combining a branch and bound algorithm that can refine Q-functions using Lagrangian duality.

source