Abstractions
To build an abstraction, in addition to the definition of the system dynamics and the specification, we also need to define select inputs and partition the state space/region of interest. Since there are multiple options for both, we wrap them as input and state abstractions, such that the abstraction method to build the finite-state abstractions can ignore the details of the choice of input and state partitioning.
Input abstractions
IntervalMDPAbstractions.InputAbstraction — TypeInputAbstractionAbstract type for input abstractions.
IntervalMDPAbstractions.InputGridSplit — TypeInputGridSplitInput abstraction for splitting the input space into a grid.
IntervalMDPAbstractions.InputLinRange — TypeInputLinRangeInput abstraction for points on a grid of the input space.
IntervalMDPAbstractions.InputDiscrete — TypeInputDiscreteInput abstraction for a set of discrete points in the input space.
IntervalMDPAbstractions.inputs — Functioninputs(input::InputAbstraction)Return the set of inputs of a given input abstraction.
IntervalMDPAbstractions.numinputs — Functionnuminputs(input::InputAbstraction)Return the number of inputs, i.e. the size of the set of inputs, of a given input abstraction.
To define a new input abstraction, introduce a new struct type that inherits from InputAbstraction and implements inputs and numinputs methods. The inputs method should return the set of inputs (set-based, singletons, or discrete) and the numinputs should return the number of inputs in the set.
State abstractions
IntervalMDPAbstractions.StateAbstraction — TypeStateAbstractionAbstract type for state abstractions.
IntervalMDPAbstractions.StateUniformGridSplit — TypeStateUniformGridSplitState abstraction for splitting the state space into a uniform grid.
IntervalMDPAbstractions.regions — Functionregions(state::StateUniformGridSplit)Return the regions of the state abstraction.
IntervalMDPAbstractions.numregions — Functionnumregions(state::StateUniformGridSplit)Return the number of regions of the state abstraction.
IntervalMDPAbstractions.statespace — Functionstatespace(state::StateUniformGridSplit)Return the state space of the state abstraction. This should must be a hyperrectangle and should be equal to the union of the regions.
Right now, we only support state abstractions that are based on a uniform grid split of the state space. However, one can easily imagine a non-uniform grid or a refinement-based partitioning for heterogenous abstractions. To implement such a state abstraction, define a new struct type that inherits from StateAbstraction and implements regions, numregions, and statespace methods.
Target models
IntervalMDPAbstractions.IMDPTarget — TypeIMDPTargetThe traditional target for IMDP abstractions. This is a standard IMDP where each region in the abstraction corresponds to a state in the IMDP with one additional state for transitions to outside the partitioned region.
IntervalMDPAbstractions.SparseIMDPTarget — TypeSparseIMDPTargetSimilar to IMDPTarget, but uses a sparse matrix to represent the transition probabilities.
IntervalMDPAbstractions.OrthogonalIMDPTarget — TypeOrthogonalIMDPTargetA target for IMDP abstractions where, for each source state, the transition probabilities are orthogonally decomposed [1]. One state is appended along each axis to capture the transitions to outside the partitioned region.
Benefits compared to IMDPTarget include less memory usage, faster computation of the transition probabilities and value iteration, and tighter uncertainty set (see [1] for a proof).
[1] Mathiesen, Frederik Baymler, Sofie Haesaert, and Luca Laurenti. "Scalable control synthesis for stochastic systems via structural IMDP abstractions." arXiv preprint arXiv:2411.11803 (2024).
IntervalMDPAbstractions.SparseOrthogonalIMDPTarget — TypeSparseOrthogonalIMDPTargetSimilar to OrthogonalIMDPTarget, but uses a sparse matrix to represent the transition probabilities.
IntervalMDPAbstractions.MixtureIMDPTarget — TypeMixtureIMDPTargetA target for IMDP abstractions where, for each source state, the transition probabilities are decomposed as a mixture [1]. One state is appended along each axis to capture the transitions to outside the partitioned region.
Benefits compared to IMDPTarget include less memory usage and faster computation of the transition probabilities and value iteration.
[1] Mathiesen, Frederik Baymler, Sofie Haesaert, and Luca Laurenti. "Scalable control synthesis for stochastic systems via structural IMDP abstractions." arXiv preprint arXiv:2411.11803 (2024).
IntervalMDPAbstractions.SparseMixtureIMDPTarget — TypeSparseMixtureIMDPTargetSimilar to MixtureIMDPTarget, but uses a sparse matrix to represent the transition probabilities.
Constructing finite-state abstractions
IntervalMDPAbstractions.abstraction — Functionabstraction(prob, state_abstraction::StateUniformGridSplit, input_abstraction, target_model::AbstractIMDPTarget)Construct an abstraction of a system and a specification under a uniform grid partitioning of the state space with an arbitrary input abstraction and an IMDP as the target model.
The argument prob contains both the system and the specification. The type of the system determines how the transition probability bounds are computed. The resulting IMDP has numregions(state_abstraction) + 1 states, where the last state is an absorbing state, representing transitioning to outside the partitioned region. This absorbing state is implicitly encoded in the ambiguity sets, i.e. not stored and automatically handled by IntervalMDP.jl.
The specification is converted based on the state_abstraction and target_model arguments in addition to whether the specification is pessimistic or optimistic. To encode the specification, at least one avoid state is required, i.e. the last, absorbing state. As a consequence, (concrete) reachability specifications are converted to (abstract) reach-avoid specifications with the last state as the avoid state.
Returns mdp and spec as the abstracted IMDP and the converted specification, respectively.
abstraction(prob, state_abstraction::StateUniformGridSplit, input_abstraction, target_model::AbstractOrthogonalIMDPTarget)Construct an abstraction of a system and a specification under a uniform grid partitioning of the state space with an arbitrary input abstraction and an orthogonal IMDP as the target model.
The argument prob contains both the system and the specification. The type of the system determines how the marginal transition probability bounds are computed. The resulting orthogonal IMDP has IntervalMDPAbstractions.splits(state_abstraction) .+ 1 states along each axis, where the last state along each axis is an absorbing state, representing transitioning to outside the partitioned region. This absorbing state for each axis is implicitly encoded in the ambiguity sets, i.e. not stored and automatically handled by IntervalMDP.jl.
The specification is converted based on the state_abstraction and target_model arguments in addition to whether the specification is pessimistic or optimistic. To encode the specification, at least one avoid state is required, i.e. the last, absorbing state. As a consequence, (concrete) reachability specifications are converted to (abstract) reach-avoid specifications with the last state as the avoid state.
Returns mdp and spec as the abstracted IMDP and the converted specification, respectively.
abstraction(prob, state_abstraction::StateUniformGridSplit, input_abstraction, target_model::AbstractMixtureIMDPTarget)Construct an abstraction of a system and a specification under a uniform grid partitioning of the state space with an arbitrary input abstraction and a mixture of orthogonal IMDPs as the target model.
The argument prob contains both the system and the specification. The type of the system determines how the marginal mixture transition probability bounds are computed. The resulting mixture IMDP has IntervalMDPAbstractions.splits(state_abstraction) .+ 1 states along each axis, where the last state along each axis is an absorbing state, representing transitioning to outside the partitioned region. This absorbing state for each axis is implicitly encoded in the ambiguity sets, i.e. not stored and automatically handled by IntervalMDP.jl.
The specification is converted based on the state_abstraction and target_model arguments in addition to whether the specification is pessimistic or optimistic. To encode the specification, at least one avoid state is required, i.e. the last, absorbing state. As a consequence, (concrete) reachability specifications are converted to (abstract) reach-avoid specifications with the last state as the avoid state.
Returns mdp and spec as the abstracted IMDP and the converted specification, respectively.