stormvogel.teaching.pomdp_backup ================================ .. py:module:: stormvogel.teaching.pomdp_backup .. autoapi-nested-parse:: Teaching module: belief-space Bellman operator and alpha-vector iteration for POMDPs. Mirrors the structure of :mod:`stormvogel.teaching.bellman`: - :func:`make_operator_pomdp_maxreachprob` is a factory that returns a :class:`BeliefBackupOperator` (analogous to ``make_operator_maxreachprob``). - :class:`BeliefBackupOperator` has an :meth:`~BeliefBackupOperator.apply` method (analogous to ``BellmanOperator.apply``). - :class:`AlphaVI` drives iteration step by step (analogous to ``VI``). Only reachability objectives and deterministic state observations are supported. All arithmetic uses :class:`~fractions.Fraction`. Classes ------- .. autoapisummary:: stormvogel.teaching.pomdp_backup.AlphaVector stormvogel.teaching.pomdp_backup.BeliefBackupOperator stormvogel.teaching.pomdp_backup.ExactBeliefBackupOperator stormvogel.teaching.pomdp_backup.AlphaVI Functions --------- .. autoapisummary:: stormvogel.teaching.pomdp_backup.dot stormvogel.teaching.pomdp_backup.initial_alpha stormvogel.teaching.pomdp_backup.value_function stormvogel.teaching.pomdp_backup._obs_groups stormvogel.teaching.pomdp_backup._build_trans_table stormvogel.teaching.pomdp_backup._cond_alpha_values stormvogel.teaching.pomdp_backup._dominated stormvogel.teaching.pomdp_backup.make_operator_pomdp_maxreachprob stormvogel.teaching.pomdp_backup.make_operator_pomdp_maxreachprob_exact stormvogel.teaching.pomdp_backup._mdp_values stormvogel.teaching.pomdp_backup.mdp_bound_alpha stormvogel.teaching.pomdp_backup.qmdp_alphas stormvogel.teaching.pomdp_backup.plot_alpha_vectors stormvogel.teaching.pomdp_backup.plot_alpha_vector_iterations stormvogel.teaching.pomdp_backup.plot_value_function_comparison Module Contents --------------- .. py:class:: AlphaVector Alpha vector with policy annotation. Represents a hyperplane over the belief simplex (via :attr:`values`) and the policy fragment that witnesses its value: which :attr:`action` to take and, for each possible next observation, which :class:`AlphaVector` to follow (:attr:`successors`). :param values: Mapping from model state to value. States absent from the dict are treated as having value zero. :param action: The action recommended at the witness belief. ``None`` for the initial leaf vector (horizon 0). :param successors: Mapping from observation alias to the next :class:`AlphaVector` to follow after that observation. .. py:attribute:: values :type: dict[stormvogel.model.state.State, fractions.Fraction] .. py:attribute:: action :type: Action | None :value: None .. py:attribute:: successors :type: dict[str, AlphaVector] .. py:function:: dot(alpha: AlphaVector, belief: stormvogel.teaching.belief.Belief) -> fractions.Fraction Inner product α · b = Σ_s α(s) · b(s). :param alpha: An alpha vector. :param belief: A belief distribution over states. :returns: The inner product as an exact :class:`~fractions.Fraction`. .. py:function:: 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 :attr:`~AlphaVector.action` and no :attr:`~AlphaVector.successors`. :param model: The POMDP model. :param target_label: Label identifying target (goal) states. :returns: A leaf :class:`AlphaVector`. .. py:function:: value_function(alphas: list[AlphaVector], belief: stormvogel.teaching.belief.Belief) -> fractions.Fraction Evaluate the PWLC value function at *belief*. :param alphas: The current set of alpha vectors. :param belief: A belief point. :returns: max_{α ∈ alphas} α · b. .. py:function:: _obs_groups(model: stormvogel.model.model.Model) -> dict[str, set[stormvogel.model.state.State]] Partition model states by observation alias. .. py:function:: _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 :data:`EmptyAction`. .. py:function:: _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'). :param alpha: The alpha vector to condition. :param trans: Pre-computed transition table. :param action_label: Action label *a*. :param group: The observation class G_o. :returns: Mapping from each source state *s* to its conditional value. .. py:function:: _dominated(alpha: AlphaVector, others: list[AlphaVector]) -> bool Return ``True`` if *alpha* is component-wise dominated by some other vector. .. py:class:: 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 :class:`~stormvogel.teaching.bellman.BellmanOperator`: :meth:`apply` maps the current set of alpha vectors to a new one by performing a point-based backup at each belief in :attr:`beliefs`. Construct via :func:`make_operator_pomdp_maxreachprob`. :param pomdp: The POMDP model. :param beliefs: Fixed belief points at which backups are performed. :param backup_fn: Inner per-belief backup callable ``(belief, alphas) → AlphaVector``. .. py:attribute:: _pomdp .. py:attribute:: beliefs .. py:attribute:: _backup_fn .. py:method:: apply(alphas: list[AlphaVector]) -> list[AlphaVector] Apply one full backup pass across all belief points. For each belief in :attr:`beliefs`, calls the inner backup function and collects the resulting alpha vectors. Dominated vectors are pruned before returning. :param alphas: The current alpha-vector set (value function approximation). :returns: Updated set of alpha vectors. .. py:function:: 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 :mod:`~stormvogel.teaching.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 :class:`AlphaVector`, and annotates it with the optimal action and its successors. :param pomdp: A POMDP with deterministic state observations. :param target_label: Label identifying target (goal) states. :param beliefs: Belief points at which backups are performed. :returns: A :class:`BeliefBackupOperator`. :raises ValueError: If *pomdp* is not a POMDP. .. py:class:: 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, :meth:`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 :func:`make_operator_pomdp_maxreachprob_exact`. .. py:attribute:: _pomdp .. py:attribute:: _backup_fn .. py:method:: apply(alphas: list[AlphaVector]) -> list[AlphaVector] Generate all candidate alpha vectors and prune dominated ones. :param alphas: The current alpha-vector set. :returns: Updated set of alpha vectors. .. py:function:: 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 :func:`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. :param pomdp: A POMDP with deterministic state observations. :param target_label: Label identifying target (goal) states. :returns: An :class:`ExactBeliefBackupOperator`. :raises ValueError: If *pomdp* is not a POMDP. .. py:class:: AlphaVI(operator: Union[BeliefBackupOperator, ExactBeliefBackupOperator], initial_alphas: list[AlphaVector]) Alpha-vector value iteration for POMDP max-reachability. Analogous to :class:`~stormvogel.teaching.bellman.VI`: holds an operator and drives iteration one step at a time. :param operator: A :class:`BeliefBackupOperator` or :class:`ExactBeliefBackupOperator`. :param initial_alphas: Starting set of alpha vectors (typically a single :func:`initial_alpha`). .. py:attribute:: _operator .. py:attribute:: _alphas .. py:method:: step() -> list[AlphaVector] Apply one backup pass and update the stored alpha vectors. :returns: The updated alpha-vector set. .. py:property:: current_alphas :type: list[AlphaVector] The current alpha-vector set. .. py:function:: _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. :param pomdp: Source POMDP. :param target_label: Label identifying target states. :returns: Mapping from each state of *pomdp* to its MDP value. .. py:function:: 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 :math:`V_\text{MDP}` to the belief space by expectation: .. math:: 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: :math:`V^*(b) \leq V_\text{MDP}(b)`. Requires stormpy (via :func:`stormvogel.model_checking`). :param pomdp: The POMDP model. :param target_label: Label identifying target states. :returns: An :class:`AlphaVector` whose values equal :math:`V_\text{MDP}(s)`. .. py:function:: 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 :math:`a` to maximise the expected MDP value of the successor: .. math:: 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: .. math:: \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 :math:`V_\text{QMDP}(b) = \max_a \alpha_a \cdot b`, and satisfies :math:`V^*(b) \leq V_\text{QMDP}(b) \leq V_\text{MDP}(b)`. Requires stormpy (via :func:`stormvogel.model_checking`). :param pomdp: The POMDP model. :param target_label: Label identifying target states. :returns: One :class:`AlphaVector` per named action, in sorted label order. :raises ValueError: If *pomdp* is not a POMDP. .. py:function:: 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. :param alphas: Alpha vectors to plot. :param s_left: State at the left extreme (belief = 0). :param s_right: State at the right extreme (belief = 1). :param left_label: Display name for *s_left* (defaults to friendly name or id). :param right_label: Display name for *s_right* (defaults to friendly name or id). :param n_points: Number of sample points along the belief axis. :param ax: Matplotlib axes to draw on. A new figure is created if ``None``. :returns: The axes object. .. py:function:: 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 :meth:`AlphaVI.step` calls:: vi = AlphaVI(op, [initial_alpha(model, "target")]) iters = [vi.step() for _ in range(3)] plot_alpha_vector_iterations(iters, s1, s2) :param iterations: List of alpha-vector sets, one per step. :param s_left: State at the left extreme of the belief axis (belief = 0). :param s_right: State at the right extreme (belief = 1). :param left_label: Override display name for *s_left*. :param right_label: Override display name for *s_right*. :param start_k: Step index label for the first panel (default 1). :param n_points: Sample resolution passed to :func:`plot_alpha_vectors`. :param figsize: Figure size override; defaults to (4·n, 4). :returns: ``(fig, axes)`` tuple. .. py:function:: 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. :param alphas_list: List of ``(alphas, label)`` pairs to compare. :param s_left: State at the left extreme of the belief axis (belief = 0). :param s_right: State at the right extreme (belief = 1). :param left_label: Override display name for *s_left*. :param right_label: Override display name for *s_right*. :param n_points: Sample resolution for each curve. :param ax: Matplotlib axes to draw on. A new figure is created if ``None``. :returns: The axes object.