Solve Interface

solve(problem::AbstractIntervalMDPAlgorithm, 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

prob1 = IntervalProbabilities(;
    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 = IntervalProbabilities(;
    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 = IntervalProbabilities(;
    lower = [0.0; 0.0; 1.0],
    upper = [0.0; 0.0; 1.0]
)

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

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

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

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

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.

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.