Solve Interface

solve(problem::AbstractIntervalMDPProblem, alg::RobustValueIteration; callback=nothing)

Solve minimizes/maximizes optimistic/pessimistic specification problems using value iteration for interval Markov processes.

It is possible to provide a callback function that will be called at each iteration with the current value function and iteration count. The callback function should have the signature callback(V::AbstractArray, k::Int).

solve can be called without specifying the algorithm, in which case it defaults to RobustValueIteration.

Examples

using IntervalMDP

prob1 = IntervalAmbiguitySets(;
    lower = [
        0.0 0.5
        0.1 0.3
        0.2 0.1
    ],
    upper = [
        0.5 0.7
        0.6 0.5
        0.7 0.3
    ],
)

prob2 = IntervalAmbiguitySets(;
    lower = [
        0.1 0.2
        0.2 0.3
        0.3 0.4
    ],
    upper = [
        0.6 0.6
        0.5 0.5
        0.4 0.4
    ],
)

prob3 = IntervalAmbiguitySets(;
    lower = [
        0.0 0.0
        0.0 0.0
        1.0 1.0
    ],
    upper = [
        0.0 0.0
        0.0 0.0
        1.0 1.0
    ]
)

transition_probs = [prob1, prob2, prob3]
initial_state = [1]
mdp = IntervalMarkovDecisionProcess(transition_probs, initial_state)

# output

FactoredRobustMarkovDecisionProcess
├─ 1 state variables with cardinality: (3,)
├─ 1 action variables with cardinality: (2,)
├─ Initial states: [1]
├─ Transition marginals:
│  └─ Marginal 1:
│     ├─ Conditional variables: states = (1,), actions = (1,)
│     └─ Ambiguity set type: Interval (dense, Matrix{Float64})
└─Inferred properties
   ├─Model type: Interval MDP
   ├─Number of states: 3
   ├─Number of actions: 2
   ├─Default model checking algorithm: Robust Value Iteration
   └─Default Bellman operator algorithm: O-Maximization

reach_states = [3]
time_horizon = 10
prop = FiniteTimeReachability(reach_states, time_horizon)
spec = Specification(prop, Pessimistic, Maximize)

# output

Specification
├─ Satisfaction mode: Pessimistic
├─ Strategy mode: Maximize
└─ Property: FiniteTimeReachability
   ├─ Time horizon: 10
   └─ Reach states: CartesianIndex{1}[CartesianIndex(3,)]

# Verification
problem = VerificationProblem(mdp, spec)
sol = solve(problem, RobustValueIteration(default_bellman_algorithm(mdp)); callback = (V, k) -> println("Iteration ", k))
V, k, res = sol  # or `value_function(sol), num_iterations(sol), residual(sol)`

# output

Iteration 1
Iteration 2
Iteration 3
Iteration 4
Iteration 5
Iteration 6
Iteration 7
Iteration 8
Iteration 9
Iteration 10
IntervalMDP.VerificationSolution{Float64, Vector{Float64}, Nothing}([0.9597716063999999, 0.9710050144, 1.0], [0.01593864639999998, 0.011487926399999848, -0.0], 10, nothing)

# Control synthesis
problem = ControlSynthesisProblem(mdp, spec)
sol = solve(problem, RobustValueIteration(default_bellman_algorithm(mdp)); callback = (V, k) -> println("Iteration ", k))
σ, V, k, res = sol # or `strategy(sol), value_function(sol), num_iterations(sol), residual(sol)`

# output

Iteration 1
Iteration 2
Iteration 3
Iteration 4
Iteration 5
Iteration 6
Iteration 7
Iteration 8
Iteration 9
Iteration 10
IntervalMDP.ControlSynthesisSolution{TimeVaryingStrategy{1, Vector{Tuple{Int32}}}, Float64, Vector{Float64}, Nothing}(TimeVaryingStrategy{1, Vector{Tuple{Int32}}}(Vector{Tuple{Int32}}[[(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)], [(1,), (2,), (1,)]]), [0.9597716063999999, 0.9710050144, 1.0], [0.01593864639999998, 0.011487926399999848, -0.0], 10, nothing)

solve(problem::AbstractIntervalMDPProblem, alg::IntervalValueIteration; callback=nothing)

Solve reach-avoid specification problems using interval value iteration (IVI) for interval Markov processes.

In contrast to RobustValueIteration, IVI propagates both a lower and an upper bound on the reach-avoid satisfaction probability simultaneously. The lower bound is initialized to zero everywhere except on the reach set, where it is set to one. The upper bound is initialized to one everywhere except on the avoid set, where it is set to zero. At each iteration, the strategy is synthesized with respect to one of the two bounds — the lower bound when the satisfaction mode is Pessimistic and the upper bound when it is Optimistic — and the synthesized strategy is then applied directly to the other bound. For infinite-horizon problems, value iteration terminates when the gap between the upper and lower bound over the set of initial states drops below convergence_eps.

IVI is only defined for reach-avoid properties (see FiniteTimeReachAvoid and InfiniteTimeReachAvoid).

It is possible to provide a callback function that will be called at each iteration with the lower and upper bound value functions and the iteration count. The callback should have the signature callback(V_lower::AbstractArray, V_upper::AbstractArray, k::Int).

The returned VerificationSolution or ControlSynthesisSolution stores the satisfaction-mode bound as its value_function (V_lower for Pessimistic, V_upper for Optimistic), the gap V_upper - V_lower as its residual, and the other bound in additional_data.

VerificationSolution{R, MR <: AbstractArray{R}, D}

The solution of a VerificationProblem, as returned by solve.

Fields

• value_function::MR: the value function, one entry per state of the system (product states for a product process).
• residual::MR: for RobustValueIteration, the difference between the value functions of the last two iterations; for IntervalValueIteration, the gap V_upper - V_lower between the upper and lower bound.
• num_iterations::Int: the number of value iteration steps performed.
• additional_data::D: algorithm-specific data; nothing for RobustValueIteration, and for IntervalValueIteration the bound that is not stored in value_function (V_upper for Pessimistic, V_lower for Optimistic satisfaction mode).

Use the accessors value_function, residual and num_iterations to read the solution. The solution can also be destructured as V, k, res = solution (value function, number of iterations, residual).

ControlSynthesisSolution{C <: AbstractStrategy, R, MR <: AbstractArray{R}, D}

The solution of a ControlSynthesisProblem, as returned by solve.

Fields

• strategy::C: the synthesized strategy, a StationaryStrategy for infinite-horizon properties and a TimeVaryingStrategy for finite-horizon properties.
• value_function::MR: the value function under the synthesized strategy, one entry per state of the system (product states for a product process).
• residual::MR: for RobustValueIteration, the difference between the value functions of the last two iterations; for IntervalValueIteration, the gap V_upper - V_lower between the upper and lower bound.
• num_iterations::Int: the number of value iteration steps performed.
• additional_data::D: algorithm-specific data; nothing for RobustValueIteration, and for IntervalValueIteration the bound that is not stored in value_function (V_upper for Pessimistic, V_lower for Optimistic satisfaction mode).

Use the accessors strategy, value_function, residual and num_iterations to read the solution. The solution can also be destructured as σ, V, k, res = solution (strategy, value function, number of iterations, residual).

residual(s::VerificationSolution)

Return the residual of a verification solution.

residual(s::ControlSynthesisSolution)

Return the residual of a control synthesis solution.

num_iterations(s::VerificationSolution)

Return the number of iterations of a verification solution.

num_iterations(s::ControlSynthesisSolution)

Return the number of iterations of a control synthesis solution.

value_function(s::VerificationSolution)

Return the value function of a verification solution.

value_function(s::ControlSynthesisSolution)

Return the value function of a control synthesis solution.

strategy(s::ControlSynthesisSolution)

Return the strategy of a control synthesis solution.

StationaryStrategy

A stationary strategy is a strategy that is the same for all time steps.

TimeVaryingStrategy

A time-varying strategy is a strategy that may vary over time. Since we need to store the strategy for each time step, the strategy is finite, and thus only applies to finite time specifications, of the same length as the strategy.

RobustValueIteration

A robust value iteration algorithm for solving interval Markov decision processes (IMDPs) with interval ambiguity sets. This algorithm is designed to handle both finite and infinite time specifications, optimizing for either the maximum or minimum expected value based on the given specification.

IntervalValueIteration

An interval value iteration algorithm for solving reach-avoid problems on interval Markov decision processes. IVI propagates both a lower and an upper bound on the satisfaction probability and synthesizes the strategy with respect to one bound (lower for Pessimistic, upper for Optimistic) while applying the synthesized strategy directly to the other bound. For infinite-horizon problems, termination is based on the gap between the two bounds over the initial states.

IVI is only defined for reach-avoid properties; see FiniteTimeReachAvoid and InfiniteTimeReachAvoid.

AbstractUpdateSequence

Abstract supertype for objects that describe which source states a Bellman operator call should update.

There are two flavours:

• FullUpdateSequence and other "flat" sequences: a vector-like collection of CartesianIndex values over the source space of an IntervalMarkovProcess. Flat sequences implement the standard AbstractVector interface (length, linear getindex, iteration, firstindex/lastindex) so they slot directly into for jₛ in states loops, the @threadstid chunking macro, and CUDA kernels.
• ProductUpdateSequence: a structured pair (dfa_states, mp_states) for ProductProcess models, where mp_states may either be a single flat sequence shared by every DFA state or an indexed collection that varies per DFA state.

Subtypes are not required to subtype AbstractVector — the product variant does not, because flattening "(dfa, mp)" to a single vector would lose the structural distinction the product-process Bellman helper relies on.

FullUpdateSequence(shape::Tuple{Vararg{Integer}})
FullUpdateSequence(model)

Lazy flat update sequence covering every source state. Wraps a CartesianIndices over the source shape so iteration and linear indexing are allocation-free. The struct is isbits, so it can be passed to a CUDA kernel without an Adapt.adapt_structure definition.

Implements the AbstractVector{CartesianIndex{N}} interface — length, linear getindex, iteration, firstindex/lastindex, IndexLinear style — directly, without subtyping AbstractVector. This keeps the AbstractUpdateSequence hierarchy free of the AbstractArray contract that does not fit the structured ProductUpdateSequence.

ProductUpdateSequence(dfa_states, mp_states)

Update sequence for a ProductProcess. The product-process Bellman helper sweeps over the DFA dimension explicitly and dispatches to the underlying Markov-process Bellman for each DFA state; this type carries the two pieces separately:

• dfa_states::AbstractUpdateSequence — the DFA states to update. Typically a FullUpdateSequence of source_shape(automaton(model)), but any flat sequence of CartesianIndex{1} works (e.g. for skipping terminal states).
• mp_states::M — the source-state sweep for the underlying Markov process. May be:
  • a single AbstractUpdateSequence (same sweep for every DFA state — the default), or
  • an AbstractVector{<:AbstractUpdateSequence} indexed by DFA-state integer (one sweep per DFA state).

The accessor mp_sequence(p, dfa_state) returns the mp sub-sequence used for the given DFA state, dispatching on the kind of mp_states.