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

  • AlternatingSimulationProblem: Used to construct a sound abstraction of a dynamical system without solving a control problem.

  • BisimulationQuotientProblem: Used to construct a quotient bisimulation of a switched system based on an observation map.

  • 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.AlternatingSimulationProblem — Type
AlternatingSimulationProblem{S, X} <: ProblemType

A problem type used to construct a sound 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.BisimulationQuotientProblem — Type
BisimulationQuotientProblem{S,X,D,R,P,G} <: ProblemType

A problem type used to construct a finite bisimulation (exact equivalence abstraction) quotient induced.

Fields

  • system: the switched system to abstract.
  • region: the state-space region of interest X.
  • observation_regions: the regions of interest used to define the observation map.

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 (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.

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