Problem

AbstractSpecification

Root of the composable specification hierarchy. A spec constrains the (possibly augmented) state x / (x,t) / (x,t,k) and is built by wrapping a base StateSpec with the optional lifts TimedSpec (time) and HybridSpec (mode), mirroring the abstraction it is evaluated against.

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.

HybridSpec{S} <: AbstractSpecification

Mode lift of a spec: per_mode[k] is the spec that must hold in mode k; modes absent from the mapping are not part of the specification.

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, XS} <: 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.
• XS: The safe set the trajectory must stay in until the target is reached, or nothing for the whole state space.

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

The safe set

safe_set is the ◻ of a reach-avoid specification ◻ safe ∧ ◇ target, and is optional: nothing — the default, and what the five-and six-argument constructors give — means the whole state space, so a problem built without it behaves exactly as before.

It is not the same as carving the unsafe region out of stateset(system). A region removed from the state space is never abstracted, so the synthesis cannot reason about it; a safe set keeps it representable and lets the synthesis actively avoid it.

Semantics: safe U target. Every state up to and including the one that reaches the target must be safe, so the target is effectively intersected with the safe set — a target state outside safe_set does not count as reached.

PR.OptimalControlProblem(system, X0, target, nothing, nothing, PR.Infinity(); safe_set = corridor)

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.

Two readings of "and stay"

stay_on_first_entry picks which one is required.

false (the default) is ◇□ in the literal sense: eventually the run is in the target forever. A run may enter the target, leave it, and come back — any number of times, as long as it is finite. That is the weaker property, so it admits the larger winning set.

true additionally forbids those departures: from the first moment the run is in the target it must stay. This is what you want when a departure would be visible or unacceptable — a balancing task that must not fall back, a device that must not leave its operating band once it is in it. It is a strictly stronger requirement, so the winning set is smaller, and a problem solvable under the default may be infeasible here.

PR.ReachAndStayProblem(system, X0, target, safe; stay_on_first_entry = true)

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.

StateSpec{S} <: AbstractSpecification

Base specification: the state x must lie in set under inclusion mode incl_mode.

TimedSpec{B} <: AbstractSpecification

Clock lift of a spec: the base spec base must hold and the time value must lie in [tmin, tmax].

check_safe_set_supported(problem::OptimalControlProblem, solver_name)

Raise if problem carries a safe_set the caller cannot honour.

Solvers that ignore the avoid part of a reach-avoid specification must call this. Dropping it silently would hand back a controller certified against a weaker specification than the one that was asked for, which is exactly the kind of failure a formal-methods toolbox must not have.

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.

hybrid_reach_spec(state_sets, time_sets, mode_ids; incl_mode = UT.INNER) -> HybridSpec

Build a mode-indexed timed specification from parallel (state_sets, time_sets, mode_ids): mode mode_ids[i] requires x ∈ state_sets[i] within the time window of time_sets[i].

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.

Whether the augmented (x, t, k) satisfies the mode-indexed spec (clock-lifted mode).

Whether the augmented (x, k) satisfies the mode-indexed spec (time-free mode).

Whether the concrete state x satisfies the base spec (time-agnostic).

Whether (x, t) satisfies the timed spec.

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

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