stormvogel.teaching.pomdp_backup¶

Teaching module: belief-space Bellman operator and alpha-vector iteration for POMDPs.

Mirrors the structure of stormvogel.teaching.bellman:

make_operator_pomdp_maxreachprob() is a factory that returns a BeliefBackupOperator (analogous to make_operator_maxreachprob).
BeliefBackupOperator has an apply() method (analogous to BellmanOperator.apply).
AlphaVI drives iteration step by step (analogous to VI).

Only reachability objectives and deterministic state observations are supported. All arithmetic uses Fraction.

Classes¶

`AlphaVector`	Alpha vector with policy annotation.
`BeliefBackupOperator`	Belief-space Bellman backup operator for POMDP max-reachability.
`ExactBeliefBackupOperator`	Exact (non-point-based) belief backup operator for POMDP max-reachability.
`AlphaVI`	Alpha-vector value iteration for POMDP max-reachability.

Functions¶

`dot`(→ fractions.Fraction)	Inner product α · b = Σ_s α(s) · b(s).
`initial_alpha`(→ AlphaVector)	Return the horizon-0 leaf alpha vector.
`value_function`(→ fractions.Fraction)	Evaluate the PWLC value function at belief.
`_obs_groups`(→ dict[str, set[stormvogel.model.state.State]])	Partition model states by observation alias.
`_build_trans_table`(...)	Pre-compute P(s' \| s, a) as a nested dict.
`_cond_alpha_values`(...)	Compute the conditional alpha β^{a,o,α} for one observation group.
`_dominated`(→ bool)	Return `True` if alpha is component-wise dominated by some other vector.
`make_operator_pomdp_maxreachprob`(→ BeliefBackupOperator)	Return the Bellman backup operator for POMDP max-reachability.
`make_operator_pomdp_maxreachprob_exact`(...)	Return the exact Bellman backup operator for POMDP max-reachability.
`_mdp_values`(→ dict[stormvogel.model.state.State, ...)	Return the optimal fully-observable MDP value for every POMDP state.
`mdp_bound_alpha`(→ AlphaVector)	Return the fully-observable MDP value function as an alpha vector.
`qmdp_alphas`(→ list[AlphaVector])	Return the QMDP alpha vectors, one per named action.
`plot_alpha_vectors`(alphas, s_left, s_right[, ...])	Plot alpha vectors over the 1-D belief simplex spanned by two states.
`plot_alpha_vector_iterations`(iterations, s_left, s_right)	Plot alpha-vector sets for successive VI steps as side-by-side panels.
`plot_value_function_comparison`(alphas_list, s_left, ...)	Plot the upper envelopes of multiple alpha-vector sets in one panel.

Module Contents¶

class stormvogel.teaching.pomdp_backup.AlphaVector¶

Alpha vector with policy annotation.

Represents a hyperplane over the belief simplex (via values) and the policy fragment that witnesses its value: which action to take and, for each possible next observation, which AlphaVector to follow (successors).

Parameters:

values – Mapping from model state to value. States absent from the dict are treated as having value zero.
action – The action recommended at the witness belief. None for the initial leaf vector (horizon 0).
successors – Mapping from observation alias to the next AlphaVector to follow after that observation.

values: dict[stormvogel.model.state.State, fractions.Fraction]¶

action: Action | None = None¶

successors: dict[str, AlphaVector]¶

stormvogel.teaching.pomdp_backup.dot(alpha: AlphaVector, belief: stormvogel.teaching.belief.Belief) → fractions.Fraction¶

Inner product α · b = Σ_s α(s) · b(s).

Parameters:

alpha – An alpha vector.
belief – A belief distribution over states.

Returns:

The inner product as an exact Fraction.

stormvogel.teaching.pomdp_backup.initial_alpha(model: stormvogel.model.model.Model, target_label: str) → AlphaVector¶

Return the horizon-0 leaf alpha vector.

Assigns value 1 to every state carrying target_label and 0 to all others. Has no action and no successors.

Parameters:

model – The POMDP model.
target_label – Label identifying target (goal) states.

Returns:

A leaf AlphaVector.

stormvogel.teaching.pomdp_backup.value_function(alphas: list[AlphaVector], belief: stormvogel.teaching.belief.Belief) → fractions.Fraction¶

Evaluate the PWLC value function at belief.

Parameters:

alphas – The current set of alpha vectors.
belief – A belief point.

Returns:

max_{α ∈ alphas} α · b.

stormvogel.teaching.pomdp_backup._obs_groups(model: stormvogel.model.model.Model) → dict[str, set[stormvogel.model.state.State]]¶: Partition model states by observation alias.

stormvogel.teaching.pomdp_backup._build_trans_table(model: stormvogel.model.model.Model) → dict[stormvogel.model.state.State, dict[str, list[tuple[fractions.Fraction, stormvogel.model.state.State]]]]¶

Pre-compute P(s’ | s, a) as a nested dict.

Returns:: table[s][action_label] = [(prob, s'), ...]. The empty string is used as the key for the EmptyAction.

stormvogel.teaching.pomdp_backup._cond_alpha_values(alpha: AlphaVector, trans: dict[stormvogel.model.state.State, dict[str, list[tuple[fractions.Fraction, stormvogel.model.state.State]]]], action_label: str, group: set[stormvogel.model.state.State]) → dict[stormvogel.model.state.State, fractions.Fraction]¶

Compute the conditional alpha β^{a,o,α} for one observation group.

β(s) = Σ_{s’ ∈ group} P(s’ | s, a) · α(s’).

Parameters:

alpha – The alpha vector to condition.
trans – Pre-computed transition table.
action_label – Action label a.
group – The observation class G_o.

Returns:

Mapping from each source state s to its conditional value.

stormvogel.teaching.pomdp_backup._dominated(alpha: AlphaVector, others: list[AlphaVector]) → bool¶: Return True if alpha is component-wise dominated by some other vector.

class stormvogel.teaching.pomdp_backup.BeliefBackupOperator(pomdp: stormvogel.model.model.Model, beliefs: list[stormvogel.teaching.belief.Belief], backup_fn: Callable[[stormvogel.teaching.belief.Belief, list[AlphaVector]], AlphaVector])¶

Belief-space Bellman backup operator for POMDP max-reachability.

Analogous to BellmanOperator: apply() maps the current set of alpha vectors to a new one by performing a point-based backup at each belief in beliefs.

Construct via make_operator_pomdp_maxreachprob().

Parameters:

pomdp – The POMDP model.
beliefs – Fixed belief points at which backups are performed.
backup_fn – Inner per-belief backup callable (belief, alphas) → AlphaVector.

_pomdp¶

beliefs¶

_backup_fn¶

apply(alphas: list[AlphaVector]) → list[AlphaVector]¶

Apply one full backup pass across all belief points.

For each belief in beliefs, calls the inner backup function and collects the resulting alpha vectors. Dominated vectors are pruned before returning.

Parameters:: alphas – The current alpha-vector set (value function approximation).
Returns:: Updated set of alpha vectors.

stormvogel.teaching.pomdp_backup.make_operator_pomdp_maxreachprob(pomdp: stormvogel.model.model.Model, target_label: str, beliefs: list[stormvogel.teaching.belief.Belief]) → BeliefBackupOperator¶

Return the Bellman backup operator for POMDP max-reachability.

Pre-computes the observation partition, target indicators, and transition table from pomdp once. The inner backup function mirrors the _bellman(s, values) pattern from bellman: for each action it selects the best alpha vector per observation group (by maximising the conditional dot product with the current belief), combines the resulting conditional alphas into a new AlphaVector, and annotates it with the optimal action and its successors.

Parameters:

pomdp – A POMDP with deterministic state observations.
target_label – Label identifying target (goal) states.
beliefs – Belief points at which backups are performed.

Returns:

A BeliefBackupOperator.

Raises:

ValueError – If pomdp is not a POMDP.

class stormvogel.teaching.pomdp_backup.ExactBeliefBackupOperator(pomdp: stormvogel.model.model.Model, backup_fn: Callable[[list[AlphaVector]], list[AlphaVector]])¶

Exact (non-point-based) belief backup operator for POMDP max-reachability.

Instead of backing up at a fixed set of belief points, apply() generates all alpha vectors that are optimal somewhere on the belief simplex: for each action and each assignment of current alpha vectors to observation groups, one candidate alpha vector is produced. Dominated candidates are then pruned.

This corresponds to the inner backup pass of exact PBVI / full alpha-vector iteration. No belief grid is required.

Construct via make_operator_pomdp_maxreachprob_exact().

_pomdp¶

_backup_fn¶

apply(alphas: list[AlphaVector]) → list[AlphaVector]¶

Generate all candidate alpha vectors and prune dominated ones.

Parameters:: alphas – The current alpha-vector set.
Returns:: Updated set of alpha vectors.

stormvogel.teaching.pomdp_backup.make_operator_pomdp_maxreachprob_exact(pomdp: stormvogel.model.model.Model, target_label: str) → ExactBeliefBackupOperator¶

Return the exact Bellman backup operator for POMDP max-reachability.

Unlike make_operator_pomdp_maxreachprob(), no belief grid is needed. For each action and each assignment of current alpha vectors to observation groups, one candidate alpha vector is produced. Duplicate candidates (arising when two alphas yield identical conditional vectors for an observation group) are removed before enumeration.

Parameters:

pomdp – A POMDP with deterministic state observations.
target_label – Label identifying target (goal) states.

Returns:

An ExactBeliefBackupOperator.

Raises:

ValueError – If pomdp is not a POMDP.

class stormvogel.teaching.pomdp_backup.AlphaVI(operator: BeliefBackupOperator | ExactBeliefBackupOperator, initial_alphas: list[AlphaVector])¶

Alpha-vector value iteration for POMDP max-reachability.

Analogous to VI: holds an operator and drives iteration one step at a time.

Parameters:

operator – A BeliefBackupOperator or ExactBeliefBackupOperator.
initial_alphas – Starting set of alpha vectors (typically a single initial_alpha()).

_operator¶

_alphas¶

step() → list[AlphaVector]¶

Apply one backup pass and update the stored alpha vectors.

Returns:: The updated alpha-vector set.

property current_alphas: list[AlphaVector]¶: The current alpha-vector set.

stormvogel.teaching.pomdp_backup._mdp_values(pomdp: stormvogel.model.model.Model, target_label: str) → dict[stormvogel.model.state.State, fractions.Fraction]¶

Return the optimal fully-observable MDP value for every POMDP state.

Copies pomdp, strips observations, runs max-reachability model checking, and maps results back to the original state objects via their stable UUIDs.

Parameters:

pomdp – Source POMDP.
target_label – Label identifying target states.

Returns:

Mapping from each state of pomdp to its MDP value.

stormvogel.teaching.pomdp_backup.mdp_bound_alpha(pomdp: stormvogel.model.model.Model, target_label: str) → AlphaVector¶

Return the fully-observable MDP value function as an alpha vector.

The MDP upper bound lifts the optimal fully-observable value \(V_\text{MDP}\) to the belief space by expectation:

\[V_\text{MDP}(b) = \sum_s b(s)\, V_\text{MDP}(s) = \alpha_\text{MDP} \cdot b.\]

Because any observation-based policy is also an MDP policy, this is an upper bound: \(V^*(b) \leq V_\text{MDP}(b)\).

Requires stormpy (via stormvogel.model_checking()).

Parameters:

pomdp – The POMDP model.
target_label – Label identifying target states.

Returns:

An AlphaVector whose values equal \(V_\text{MDP}(s)\).

stormvogel.teaching.pomdp_backup.qmdp_alphas(pomdp: stormvogel.model.model.Model, target_label: str) → list[AlphaVector]¶

Return the QMDP alpha vectors, one per named action.

QMDP assumes the state becomes fully observable after the first action, so the agent picks \(a\) to maximise the expected MDP value of the successor:

\[V_\text{QMDP}(b) = \max_{a} \sum_s b(s) \sum_{s'} P(s'\mid s,a)\, V_\text{MDP}(s').\]

Each alpha vector encodes one action’s contribution:

\[\alpha_a(s) = \mathbb{1}[s \in T] + \mathbb{1}[s \notin T] \cdot \sum_{s'} P(s'\mid s,a)\, V_\text{MDP}(s').\]

The value function is \(V_\text{QMDP}(b) = \max_a \alpha_a \cdot b\), and satisfies \(V^*(b) \leq V_\text{QMDP}(b) \leq V_\text{MDP}(b)\).

Requires stormpy (via stormvogel.model_checking()).

Parameters:

pomdp – The POMDP model.
target_label – Label identifying target states.

Returns:

One AlphaVector per named action, in sorted label order.

Raises:

ValueError – If pomdp is not a POMDP.

stormvogel.teaching.pomdp_backup.plot_alpha_vectors(alphas: list[AlphaVector], s_left: stormvogel.model.state.State, s_right: stormvogel.model.state.State, left_label: str | None = None, right_label: str | None = None, n_points: int = 300, ax=None)¶

Plot alpha vectors over the 1-D belief simplex spanned by two states.

Each alpha vector is drawn as a line over the belief axis. The x-axis represents the probability of being in s_right (0 = certainly s_left, 1 = certainly s_right). Lines are colored by action label. The upper envelope (the PWLC value function) is overlaid as a thick black curve.

Parameters:

alphas – Alpha vectors to plot.
s_left – State at the left extreme (belief = 0).
s_right – State at the right extreme (belief = 1).
left_label – Display name for s_left (defaults to friendly name or id).
right_label – Display name for s_right (defaults to friendly name or id).
n_points – Number of sample points along the belief axis.
ax – Matplotlib axes to draw on. A new figure is created if None.

Returns:

The axes object.

stormvogel.teaching.pomdp_backup.plot_alpha_vector_iterations(iterations: list[list[AlphaVector]], s_left: stormvogel.model.state.State, s_right: stormvogel.model.state.State, left_label: str | None = None, right_label: str | None = None, start_k: int = 1, n_points: int = 300, figsize: tuple[float, float] | None = None)¶

Plot alpha-vector sets for successive VI steps as side-by-side panels.

Each panel shows the alpha vectors after one Bellman backup step, with the step number k as the panel title. Pass the results of repeated AlphaVI.step() calls:

vi = AlphaVI(op, [initial_alpha(model, "target")])
iters = [vi.step() for _ in range(3)]
plot_alpha_vector_iterations(iters, s1, s2)

Parameters:

iterations – List of alpha-vector sets, one per step.
s_left – State at the left extreme of the belief axis (belief = 0).
s_right – State at the right extreme (belief = 1).
left_label – Override display name for s_left.
right_label – Override display name for s_right.
start_k – Step index label for the first panel (default 1).
n_points – Sample resolution passed to plot_alpha_vectors().
figsize – Figure size override; defaults to (4·n, 4).

Returns:

(fig, axes) tuple.

stormvogel.teaching.pomdp_backup.plot_value_function_comparison(alphas_list: list[tuple[list[AlphaVector], str]], s_left: stormvogel.model.state.State, s_right: stormvogel.model.state.State, left_label: str | None = None, right_label: str | None = None, n_points: int = 300, ax=None)¶

Plot the upper envelopes of multiple alpha-vector sets in one panel.

Each entry in alphas_list is drawn as a single PWLC curve — the upper envelope of its alpha vectors. This is useful for comparing bounds, e.g. the exact-VI lower bound against QMDP and the plain MDP upper bound.

Parameters:

alphas_list – List of (alphas, label) pairs to compare.
s_left – State at the left extreme of the belief axis (belief = 0).
s_right – State at the right extreme (belief = 1).
left_label – Override display name for s_left.
right_label – Override display name for s_right.
n_points – Sample resolution for each curve.
ax – Matplotlib axes to draw on. A new figure is created if None.

Returns:

The axes object.