GitHub

Problem Types

This module defines a set of structures used to represent different control problems.

All problems are subtypes of the abstract type ProblemType, which provides a common interface for control problems.

Supported Problems

  • EmptyProblem: Used to construct an abstraction of a dynamical system without solving a control problem.

  • OptimalControlProblem: A reach-avoid optimal control problem defined over a finite time horizon, supporting state and transition costs.

  • SafetyProblem: A safety specification problem requiring the system to remain within a safe set for the entire time horizon.

  • CoSafeLTLProblem: A co-safe LTL specification problem requiring the system to satisfy a co-safe LTL formula, i.e. to reach an accepting condition in finite time (equivalently: achieve a “good prefix” after which the specification is permanently satisfied).

Each of these problem types is detailed below:

Dionysos.Problem.EmptyProblem — Type
EmptyProblem{S, X} <: ProblemType

A problem type used to construct an abstraction of a dynamical system.

  • S: The system to abstract (continuous or discrete-time).
  • X: The region of interest (e.g., a subset of the state space).

This problem encodes no control objective. It is intended for generating symbolic models that can later be reused by other solvers.

source
Dionysos.Problem.OptimalControlProblem — Type
OptimalControlProblem{S, XI, XT, XC, TC, T} <: ProblemType

Encodes a reach-avoid optimal control problem over a finite horizon.

  • S: The system to control.
  • XI: The initial set of states.
  • XT: The target set to be reached.
  • XC: A state cost function or structure.
  • TC: A transition cost function or structure.
  • T: The time horizon (number of allowed time steps).

This problem aims to find a control strategy that reaches the target set from the initial set, minimizing the accumulated cost over time.

source
Dionysos.Problem.SafetyProblem — Type
SafetyProblem{S, XI, XS, T} <: ProblemType

Encodes a safety control problem over a finite horizon.

  • S: The system to control.
  • XI: The initial set of states.
  • XS: The safe set in which the system must remain.
  • T: The time horizon (number of allowed time steps).

This problem aims to synthesize a controller that ensures the system remains within the safe set for the entire duration of the time horizon.

source
Dionysos.Problem.CoSafeLTLProblem — Type
CoSafeLTLProblem{S, XI, SPEC, LAB} <: ProblemType

Encodes a co-safe LTL control problem.

  • S: The system to control.
  • XI: The initial set of states.
  • SPEC: The co-safe LTL specification object (e.g. a Spot/LTL formula or an automaton/monitor wrapper).
  • LAB: The labeling payload type used in labeling (typically a concrete set type such as a LazySet, or an abstract labeling such as Vector{Int} / bitset / etc.).

Fields

  • system::S: The (concrete or abstract) system to control.

  • initial_set::XI: Initial set of states (or initial abstract states).

  • spec::SPEC: The co-safe LTL specification.

  • labeling::Dict{Symbol, LAB}: Unified container mapping each atomic proposition (AP) :ap to its labeling object. In a concrete problem, values are typically sets (e.g. LazySets / Dionysos sets) over the state space. In an abstract problem, values are typically collections of abstract states (e.g. Vector{Int}).

  • ap_semantics::Dict{Symbol, Any}: Per-AP semantics used when converting set labels to abstract labels. Values: Dionysos.Domain.INNER or Dionysos.Domain.OUTER.

  • strict_spot::Bool: If true, enforce Spot-style strict AP semantics / alphabet handling (useful to catch missing APs). If false, be permissive (e.g. treat missing APs as false / ignore absent labels depending on your pipeline).

This problem aims to synthesize a controller such that the generated trajectory satisfies the co-safe LTL formula, i.e. it reaches an accepting condition in finite time.

source