Problem

AbstractionProblem <: ProblemType

A specification that carries no control objective; it parametrizes the construction of a sound abstraction (symbolic model) that other solvers reuse. trajectory_success is not defined for these problems.

AlternatingSimulationProblem{S, X} <: AbstractionProblem

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

• S: The system to abstract (continuous or discrete-time).
• X: The state-space region of interest to abstract.

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

BisimulationQuotientProblem{S, X, R} <: AbstractionProblem

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

Fields

• system: the switched system to abstract.
• state_set: 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.

CoSafeLTLProblem{S, XI, SPEC, LAB} <: ControlProblem

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, UT.INCL_MODE}: Per-AP semantics used when converting set labels to abstract labels (UT.INNER or UT.OUTER; also reachable as Mapping.INNER/Mapping.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.

ControlProblem <: ProblemType

A specification with a control objective to synthesize: reach-avoid, safety, reach-and-stay, co-safe LTL. Every ControlProblem has an initial_set and a trajectory_success predicate.

Infinity

Sentinel for an infinite time horizon. A problem whose time is Infinity() must be satisfied over an unbounded horizon (e.g. an infinite-horizon safety or reach-and-stay specification). It is never finite, so solvers branch on isfinite(problem.time) to separate the finite from the infinite-horizon case.

OptimalControlProblem{S, XI, XT, XC, TC, T} <: ControlProblem

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: Satisfy the property in at most time T.

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

ProblemType

Root of the control-task specification hierarchy. A problem bundles a system with a specification; a solver consumes it through the MOI interface.

There are two categories:

• ControlProblem: a control objective is synthesized (there is an initial set and a trajectory_success predicate).
• AbstractionProblem: no control objective; the problem only parametrizes the construction of a (reusable) abstraction.

Extending

To add a problem type, subtype ControlProblem or AbstractionProblem and implement:

• discretize_problem — time-discretize the (continuous) system and horizon (unless the generic method already covers it via remake);
• trajectory_success — control problems only — whether a closed-loop trajectory satisfies the specification;
• a plotting @recipe (optional).

ReachAndStayProblem{S, XI, XT, XS, T} <: ControlProblem

Encodes a reach-and-stay control problem (eventually always).

• S: The system to control.
• XI: The initial set of states.
• XT: The target set to be reached and stayed in.
• XS: The safe set in which the system must remain during the approach.
• T: Satisfy the property for at least time T.

This problem aims to synthesize a controller that drives the system from the initial set into the target set and keeps it there indefinitely, while remaining within the safe set during the approach phase.

SafetyProblem{S, XI, XS, T} <: ControlProblem

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: Satisfy the property for at least time T.

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

discretize_problem(problem::ProblemType, Δt::Real; num_substeps = ST.DEFAULT_NUM_SUBSTEPS)

Time-discretize problem: replace its continuous-time system by the Δt-sampled discrete-time system and convert the horizon to a number of steps.

discretize_time(time, Δt::Real; round_up = true)

Convert a continuous-time horizon time into a number of discrete steps of duration Δt. round_up selects the conservative direction: true rounds up (used by "for at least T" specifications such as safety and reach-and-stay), false rounds down (used by "within at most T" specifications such as reach-avoid). An Infinity() horizon stays Infinity().

horizon_round_up(problem::ControlProblem) -> Bool

Rounding direction used when discretizing the problem horizon: true for "for at least T" specifications (safety, reach-and-stay), false for "within at most T" specifications (reach-avoid). Defaults to true.

remake(problem::ProblemType; kwargs...)

Return a copy of problem with the given fields replaced. Used by discretize_problem to swap the system and horizon without a per-type constructor call. Fields not named in kwargs are copied verbatim; the type parameters are re-inferred by the constructor, so replacing a field with a value of a different type (e.g. a discretized system) is fine.

trajectory_success(problem::ControlProblem, traj::ST.Trajectory) -> Bool

Whether the closed-loop trajectory traj satisfies the specification of problem. Defined only for ControlProblems.