stormvogel.teaching.bellman¶

Classes¶

`Gets`	Sympy function rendering as a LaTeX assignment arrow (`\gets`).
`BellmanOperator`
`VI`	Plain value iteration.
`IVI`	Interval value iteration: two VI runs from below (0) and above (1) simultaneously.

Functions¶

`_latex`(self, printer)
`equations_prob`(model, min, zero_states, one_states[, ...])
`maxreachprob`(model, target_label[, operator])
`minreachprob`(model, target_label[, operator])
`zero_value`(→ dict[zero_value.model, zero_value.model])
`one_value`(→ dict[one_value.model, one_value.model])
`value_to_latex`(values[, name])
`make_operator_minreachprob`(mdp, target_label)
`make_operator_maxreachprob`(mdp, target_label)
`_robust_action_value`(→ Any)	Greedy corner-point expected value for one action on an interval transition.
`make_operator_robust_maxreachprob`(imdp, target_label)	Bellman operator for robust maximum reachability on an interval MDP.
`make_operator_robust_minreachprob`(imdp, target_label)	Bellman operator for robust minimum reachability on an interval MDP.
`make_operator_coop_maxreachprob`(imdp, target_label)	Bellman operator for cooperative maximum reachability on an interval MDP.
`make_operator_coop_minreachprob`(imdp, target_label)	Bellman operator for cooperative minimum reachability on an interval MDP.
`make_operator_max_discounted_reward`(mdp, reward_name, ...)	Bellman operator for maximum discounted expected reward.
`make_operator_min_discounted_reward`(mdp, reward_name, ...)	Bellman operator for minimum discounted expected reward.
`make_operator_max_reachreward`(mdp, reward_name, done_label)	Bellman operator for maximum expected reachability reward.
`make_operator_min_reachreward`(mdp, reward_name, done_label)	Bellman operator for minimum expected reachability reward.
`visualise_iterations`(iterations[, ...])

Module Contents¶

class stormvogel.teaching.bellman.Gets¶

Bases: sympy.Function

Sympy function rendering as a LaTeX assignment arrow (\gets).

nargs = 2¶

stormvogel.teaching.bellman._latex(self, printer)¶

stormvogel.teaching.bellman.equations_prob(model: equations_prob.model[float], min: bool, zero_states: Iterable[equations_prob.model], one_states: Iterable[equations_prob.model], operator=False)¶

stormvogel.teaching.bellman.maxreachprob(model: maxreachprob.model[float], target_label: str, operator=False)¶

stormvogel.teaching.bellman.minreachprob(model: minreachprob.model[float], target_label: str, operator=False)¶

stormvogel.teaching.bellman.zero_value(model: zero_value.model) → dict[zero_value.model, zero_value.model]¶

stormvogel.teaching.bellman.one_value(model: one_value.model) → dict[one_value.model, one_value.model]¶

stormvogel.teaching.bellman.value_to_latex(values: dict[stormvogel.model.State, stormvogel.model.Value], name='V')¶

stormvogel.teaching.bellman.make_operator_minreachprob(mdp, target_label)¶

stormvogel.teaching.bellman.make_operator_maxreachprob(mdp, target_label)¶

stormvogel.teaching.bellman._robust_action_value(branch: Any, values: Any, nature_maximizes: bool) → Any¶

Greedy corner-point expected value for one action on an interval transition.

Assigns probabilities within [lower, upper] to maximise or minimise the expected value by greedily shifting remaining mass towards the most favourable successor states.

Parameters:

branch – List of (Interval, State) pairs for the action.
values – Current value estimate per state.
nature_maximizes – If True, nature pushes mass to high-value states; if False, nature pushes mass to low-value states.

stormvogel.teaching.bellman.make_operator_robust_maxreachprob(imdp, target_label)¶

Bellman operator for robust maximum reachability on an interval MDP.

The agent maximises; nature plays adversarially (minimises expected value). Requires stormpy.

stormvogel.teaching.bellman.make_operator_robust_minreachprob(imdp, target_label)¶

Bellman operator for robust minimum reachability on an interval MDP.

The agent minimises; nature plays adversarially (maximises expected value). Requires stormpy.

stormvogel.teaching.bellman.make_operator_coop_maxreachprob(imdp, target_label)¶

Bellman operator for cooperative maximum reachability on an interval MDP.

The agent maximises; nature plays cooperatively (also maximises expected value). Requires stormpy.

stormvogel.teaching.bellman.make_operator_coop_minreachprob(imdp, target_label)¶

Bellman operator for cooperative minimum reachability on an interval MDP.

The agent minimises; nature plays cooperatively (also minimises expected value). Requires stormpy.

stormvogel.teaching.bellman.make_operator_max_discounted_reward(mdp, reward_name: str, discount: float)¶

Bellman operator for maximum discounted expected reward.

V(s) = r(s) + discount * max_a Σ p(s,a,s’) * V(s’). All states are updated; discount < 1 ensures convergence.

Parameters:

reward_name – Name of the reward model on mdp.
discount – Discount factor γ ∈ (0, 1).

stormvogel.teaching.bellman.make_operator_min_discounted_reward(mdp, reward_name: str, discount: float)¶

Bellman operator for minimum discounted expected reward.

V(s) = r(s) + discount * min_a Σ p(s,a,s’) * V(s’). All states are updated; discount < 1 ensures convergence.

Parameters:

reward_name – Name of the reward model on mdp.
discount – Discount factor γ ∈ (0, 1).

stormvogel.teaching.bellman.make_operator_max_reachreward(mdp, reward_name: str, done_label: str)¶

Bellman operator for maximum expected reachability reward.

V(s) = r(s) + max_a Σ p(s,a,s’) * V(s’), with done states fixed at 0.

Parameters:

reward_name – Name of the reward model on mdp.
done_label – Label identifying absorbing/terminal states (value fixed at 0).

stormvogel.teaching.bellman.make_operator_min_reachreward(mdp, reward_name: str, done_label: str)¶

Bellman operator for minimum expected reachability reward.

V(s) = r(s) + min_a Σ p(s,a,s’) * V(s’), with done states fixed at 0.

Parameters:

reward_name – Name of the reward model on mdp.
done_label – Label identifying absorbing/terminal states (value fixed at 0).

class stormvogel.teaching.bellman.BellmanOperator[ValueType: stormvogel.model.Value](mdp: stormvogel.model.Model[ValueType], zero_states, one_states, bellman_update)¶

_model¶

_zerostates¶

_onestates¶

_bellman_update¶

apply(values: dict[stormvogel.model.State, stormvogel.model.Value]) → dict[stormvogel.model.State, stormvogel.model.Value]¶

stormvogel.teaching.bellman.visualise_iterations(iterations, background_gradient: str | None = None, digits: int = 5)¶

class stormvogel.teaching.bellman.VI(operator: BellmanOperator, initial_values: dict[stormvogel.model.State, stormvogel.model.Value])¶

Plain value iteration.

_operator¶

_values¶

step() → dict[stormvogel.model.State, stormvogel.model.Value]¶

property current_values: dict[stormvogel.model.State, stormvogel.model.Value]¶

class stormvogel.teaching.bellman.IVI(lower_vi: VI, upper_vi: VI)¶

Interval value iteration: two VI runs from below (0) and above (1) simultaneously.

Both use the same operator. The gap between lower and upper bounds shrinks each iteration; convergence is detected when they agree within a tolerance.

_lower_vi¶

_upper_vi¶

step() → dict[stormvogel.model.State, tuple[Any, Any]]¶

property current_values: dict[stormvogel.model.State, tuple[Any, Any]]¶: Return per-state (lower, upper) bound pairs.