IMDP (class IMDP)

class IMDP : public MDP

Interval MDP class for abstraction, controller synthesis, and data management. Inherits all functionality from MDP.

Defined in src/IMDP.h with implementations in src/IMDP.cpp.

Constructor

Inherits the MDP constructor:

IMDP imdp(dim_x, dim_u, dim_w);

Optimization Algorithm

void setAlgorithm(nlopt::algorithm alg)

Set the nonlinear optimization algorithm used during abstraction.

Parameters:

alg – An NLopt algorithm (default: nlopt::LN_SBPLX).

See NLopt Algorithms for all options.

Abstraction

Transition Matrix

void minTransitionMatrix()

Compute the minimal transition probability matrix for state-to-state transitions.

void maxTransitionMatrix()

Compute the maximal transition probability matrix for state-to-state transitions.

void transitionMatrixBounds()

Compute both min and max transition matrices efficiently. Exploits sparsity: if max is zero, min is skipped. Use this instead of calling minTransitionMatrix() and maxTransitionMatrix() separately.

Target Transition Vector

void minTargetTransitionVector()

Compute the minimal transition probability vector to the target region.

void maxTargetTransitionVector()

Compute the maximal transition probability vector to the target region.

void targetTransitionVectorBounds()

Compute both min and max target vectors efficiently with sparsity exploitation.

Avoid Transition Vector

void minAvoidTransitionVector()

Compute the minimal transition probability vector to outside the state space (including the avoid region).

void maxAvoidTransitionVector()

Compute the maximal transition probability vector to outside the state space.

Note

Avoid vectors are always required, even when no avoid region is defined, as they capture transitions out of the state space.

Controller Synthesis

All synthesis functions take IMDP_lower:

• true — pessimistic (worst-case noise first, then fix for upper bound)

• false — optimistic (best-case noise first, then fix for lower bound)

Standard Synthesis

void infiniteHorizonReachController(bool IMDP_lower)

Synthesize a reachability (or reach-avoid) controller over an infinite horizon using the interval iteration algorithm.

void infiniteHorizonSafeController(bool IMDP_lower)

Synthesize a safety controller over an infinite horizon.

void finiteHorizonReachController(bool IMDP_lower, size_t timeHorizon)

Synthesize a reachability (or reach-avoid) controller for a finite number of steps using value iteration.

void finiteHorizonSafeController(bool IMDP_lower, size_t timeHorizon)

Synthesize a safety controller for a finite number of steps.

Sorted Synthesis (GPU-Compatible)

Sorted variants eliminate the GLPK dependency and support GPU execution (implemented in src/GPU_synthesis.cpp):

void infiniteHorizonReachControllerSorted(bool IMDP_lower)

void infiniteHorizonSafeControllerSorted(bool IMDP_lower)

void finiteHorizonReachControllerSorted(bool IMDP_lower, size_t timeHorizon)

void finiteHorizonSafeControllerSorted(bool IMDP_lower, size_t timeHorizon)

void finiteHorizonReachControllerSortedStoreMDP(bool IMDP_lower, size_t timeHorizon)

Sorted finite-horizon reachability with intermediate MDP data storage.

Save Functions

void saveMinTransitionMatrix()

void saveMaxTransitionMatrix()

void saveMinTargetTransitionVector()

void saveMaxTargetTransitionVector()

void saveMinAvoidTransitionVector()

void saveMaxAvoidTransitionVector()

void saveController()

Save the synthesized controller to controller.h5.

Load Functions

void loadMinTransitionMatrix(string filename)

void loadMaxTransitionMatrix(string filename)

void loadMinTargetTransitionVector(string filename)

void loadMaxTargetTransitionVector(string filename)

void loadMinAvoidTransitionVector(string filename)

void loadMaxAvoidTransitionVector(string filename)

void loadController(string filename)

Load a previously saved controller from HDF5.