Dionysos.jl: a Modular Platform for Smart Symbolic Control

TL;DR

Dionysos.jl addresses the scalability challenge of abstraction-based, correct-by-design control for complex cyber-physical systems by introducing smart abstractions that use overlapping cells and state-dependent local controllers within a memoryless concretization framework. The package provides modular, Julia-based tooling built on JuMP and MathOptInterface, exposing a System/Problem/Optim trio to define models, problems, and solvers that operate on either partitions or covers with hyperrectangular or ellipsoidal cells. Key contributions include the memoryless concretization relation (MCR), interface-driven concretization, and lazy abstraction concepts that enable deterministic, scalable synthesis with safety guarantees; the framework unifies classical ASR/FRR approaches with modern, data- and problem-driven cell design. Empirical results demonstrate favorable benchmarking against SCOTS and CoSyMA on representative problems, highlighting speedups when problem structure is leveraged and the practicality of smart abstractions for higher-dimensional tasks. The work advances practical, safe control synthesis for CPS by enabling plug-and-play smart abstractions and a modular solver ecosystem, with future directions toward a meta-solver that uses learning to optimize solver meta-parameters.

Abstract

We introduce Dionysos.jl, a modular package for solving optimal control problems for complex dynamical systems using state-of-the-art and experimental techniques from symbolic control, optimization, and learning. More often than not with Cyber-Physical systems, the only sensible way of developing a controller is by discretizing the different variables, thus transforming the control task into a purely combinatorial problem on a finite-state mathematical object, called an abstraction of this system. Although this approach offers a safety-critical framework, the available techniques suffer important scalability issues. In order to render these techniques practical, it is necessary to construct smarter abstractions that differ from classical techniques by partitioning the state-space in a non trivial way.

Figures (8)

• Figure 1: The three steps of abstraction-based control.
• Figure 2: Types of discretization of the concrete state space. Let $\mathcal{S}_{1} = (\mathcal{X}_1,\mathcal{U}_1,F_1)$ with $\mathcal{X}_1 = [0,1]^2$, $\mathcal{S}_{2} = (\mathcal{X}_2,\mathcal{U}_2,F_2)$ with $\mathcal{X}_2 = \{q_1,q_2,q_3,q_4\}$, $R_1 \subseteq \mathcal{X}_1\times \mathcal{X}_2$ and $R_2 \subseteq \mathcal{X}_1\times \mathcal{X}_2$ are explicit from the figure. Left: $R_1$ is a strict single-valued map, i.e., it induces a full partition of $\mathcal{X}_1$. Right: $R_2$ is a non-strict set-valued map, i.e., it induces a partial cover of $\mathcal{X}_1$.
• Figure 3: Comparison of piecewise constant and state-dependent controllers. The red region illustrates $F_1(x_1, u)$ for all $x_1 \in R^{-1}(x_2)$, given $u \in \mathcal{U}_1$ where $u \in \mathcal{U}_2(x_2)$. The blue region shows $G_1(x_1) = F_1(x_1, \kappa(x_1))$ for all $x_1\in R^{-1}(x_2)$, where $\kappa \in \mathcal{U}_2(x_2)$ is a local state-dependent controller $\kappa:\mathcal{X}_1\rightarrow\mathcal{U}_1$. Left: The two-dimensional concrete system with its state space discretization. Right: The corresponding abstract system, highlighting the non-deterministic transition $F_2(x_2,u)$ and the deterministic transition $F_2(x_2,\kappa)$.
• Figure 4: Comparison between classical and smart abstractions for a planar system with state trajectory (blue line) and value function (color map) obtained for the optimal control problem of departing from $\mathcal{X}_I$ and reaching $\mathcal{X}_T$ while avoiding obstacles $\mathcal{X}_O$. Left: Abstraction covering the entire state space with a naive grid-based partition. Non-colored represents a region where no controller could be designed. Right: Abstraction partially covering the state space with ellipsoidal cells and a local feedback controller.
• Figure 5: Summary of Section \ref{['sec:package']}. The System module is an extension of MathematicalSystems.jl and HybridSystems.jl, and implements mathematical definitions of dynamical systems. The Problem module contains mathematical definitions of control problems. All problem structures have a system as a field. The Optim module contains the control strategies to solve the problems. It is built on top of the optimization packages MathOptInterface.jl and JuMP.jl.

Theorems & Definitions (8)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Definition 6
• Definition 7
• Example 1