stormvogel.transformations.imc_to_mdp¶
Transformation from interval Markov chains to MDPs.
Functions¶
|
Enumerate vertices of the interval distribution polytope. |
|
Convert an interval Markov chain to an MDP. |
Module Contents¶
- stormvogel.transformations.imc_to_mdp._vertices(lows: list[fractions.Fraction], highs: list[fractions.Fraction]) list[tuple[fractions.Fraction, Ellipsis]]¶
Enumerate vertices of the interval distribution polytope.
A vertex has at most one index k strictly between its bounds; the remaining n-1 indices are fixed to either their lower or upper bound. For each choice of k and each 2^(n-1) assignment of the remaining indices, compute p_k = 1 − Σ(fixed) and accept if lows[k] ≤ p_k ≤ highs[k].
- Parameters:
lows – Lower bounds for each successor probability.
highs – Upper bounds for each successor probability.
- Returns:
Deduplicated list of feasible vertex tuples.
- stormvogel.transformations.imc_to_mdp.imc_to_mdp(model: stormvogel.model.Model) stormvogel.model.Model¶
Convert an interval Markov chain to an MDP.
Each state’s interval distribution defines a polytope of feasible distributions. The vertices of that polytope become the actions of the corresponding MDP state. Labels, state valuations, friendly names, and state rewards are preserved. Transition rewards are not transferred.
- Parameters:
model – An interval MC (DTMC with Interval-valued transitions).
- Returns:
A new MDP with one action per vertex per state.
- Raises:
ValueError – If model is not an interval model.