stormvogel.teaching.qualitative_mdp¶

Qualitative fixpoint algorithms for MDPs.

Implements the operators and provides a generic FixpointIterator and visualise_iterations()

Four operators are defined, each mirroring one qualitative reachability property:

psi_spos() — LFP for \(S_{\text{pos}}\) (possible max reach)
psi_sposmin() — LFP for \(S_{\text{pos}}^{\min}\) (possible min reach)
psi_smaxas() — GFP for \(S_{\text{as}}^{\max}\) (almost-sure max reach)
psi_sminas() — GFP for \(S_{\text{as}}^{\min}\) (almost-sure min reach)

Attributes¶

_Operator

Classes¶

FixpointIterator

Iterate a set-valued operator to its fixpoint.

Functions¶

`psi_spos`(→ frozenset[stormvogel.model.State])	Operator for \(S_{\text{pos}}\) (possible max reachability).
`psi_sposmin`(→ frozenset[stormvogel.model.State])	Operator for \(S_{\text{pos}}^{\min}\) (possible min reachability).
`psi_sminas`(→ frozenset[stormvogel.model.State])	Operator for \(S_{\text{as}}^{\min}\) (almost-sure min reachability).
`psi_smaxas`(→ frozenset[stormvogel.model.State])	Operator for \(S_{\text{as}}^{\max}\) (almost-sure max reachability).
`spos`(→ FixpointIterator)	Return a `FixpointIterator` for \(S_{\text{pos}}\) (LFP).
`sposmin`(→ FixpointIterator)	Return a `FixpointIterator` for \(S_{\text{pos}}^{\min}\) (LFP).
`smaxas`(→ FixpointIterator)	Return a `FixpointIterator` for \(S_{\text{as}}^{\max}\) (GFP).
`sminas`(→ FixpointIterator)	Return a `FixpointIterator` for \(S_{\text{as}}^{\min}\) (GFP).
`_run`(→ frozenset[stormvogel.model.State])
`compute_spos`(→ frozenset[stormvogel.model.State])	Return \(S_{\text{pos}}\) directly (runs LFP to convergence).
`compute_sposmin`(→ frozenset[stormvogel.model.State])	Return \(S_{\text{pos}}^{\min}\) directly (runs LFP to convergence).
`compute_smaxas`(→ frozenset[stormvogel.model.State])	Return \(S_{\text{as}}^{\max}\) directly (runs GFP to convergence).
`compute_sminas`(→ frozenset[stormvogel.model.State])	Return \(S_{\text{as}}^{\min}\) directly (runs GFP to convergence).
`run_and_collect`(→ list[frozenset[stormvogel.model.State]])	Run it to fixpoint and return all intermediate sets as a list.
`visualise_iterations`(snapshots, mdp[, highlight])	Return a pandas DataFrame showing set membership at each iteration.

Module Contents¶

stormvogel.teaching.qualitative_mdp._Operator¶

stormvogel.teaching.qualitative_mdp.psi_spos(X: frozenset[stormvogel.model.State], mdp: stormvogel.model.Model, target: frozenset[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶

Operator for \(S_{\text{pos}}\) (possible max reachability).

A state is added when it has some action with some successor in X. LFP starting from target equals \(S_{\text{pos}}\).

\[\Psi_{\max>0}(X) = T \cup \{s \mid \exists a \in \mathrm{En}(s).\; \exists s' \in X.\; \delta(s,a)(s') > 0\}\]

stormvogel.teaching.qualitative_mdp.psi_sposmin(X: frozenset[stormvogel.model.State], mdp: stormvogel.model.Model, target: frozenset[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶

Operator for \(S_{\text{pos}}^{\min}\) (possible min reachability).

A state is added when every action has some successor in X. LFP starting from target equals \(S_{\text{pos}}^{\min}\).

\[\Psi_{\min>0}(X) = T \cup \{s \mid \forall a \in \mathrm{En}(s).\; \exists s' \in X.\; \delta(s,a)(s') > 0\}\]

stormvogel.teaching.qualitative_mdp.psi_sminas(X: frozenset[stormvogel.model.State], mdp: stormvogel.model.Model, target: frozenset[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶

Operator for \(S_{\text{as}}^{\min}\) (almost-sure min reachability).

A non-target state is kept when every action keeps all its successors inside X. If any action can leave X with positive probability the adversarial scheduler will pick it, so the state is removed.

\[\Psi_{\min=1}(X) = T \cup \{s \in X \mid \forall a \in \mathrm{En}(s).\; \forall s' \in \mathrm{supp}(\delta(s,a)).\; s' \in X\}\]

Note

Must be initialised from \(S_{\text{pos}}^{\min}\) (see sminas()), not from \(S\), because \(S\) is a trivial fixed point of this operator.

stormvogel.teaching.qualitative_mdp.psi_smaxas(X: frozenset[stormvogel.model.State], mdp: stormvogel.model.Model, target: frozenset[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶

Operator for \(S_{\text{as}}^{\max}\) (almost-sure max reachability).

A non-target state is kept when it has some action all of whose successors are in X. GFP starting from \(S_{\text{pos}}\) equals \(S_{\text{as}}^{\max}\).

\[\Psi_{\max=1}(X) = T \cup \{s \mid \exists a \in \mathrm{En}(s).\; \forall s' \in \mathrm{supp}(\delta(s,a)).\; s' \in X\}\]

class stormvogel.teaching.qualitative_mdp.FixpointIterator(operator: _Operator, initial: frozenset[stormvogel.model.State], mdp: stormvogel.model.Model, target: frozenset[stormvogel.model.State])¶

Iterate a set-valued operator to its fixpoint.

Parameters:

operator – One of psi_spos(), psi_sposmin(), psi_smaxas(), or any compatible callable.
initial – Starting set (use target for LFP, all states for GFP).
mdp – The MDP.
target – The fixed target set passed to the operator each step.

_op¶

_current¶

_mdp¶

_target¶

_converged = False¶

property current: frozenset[stormvogel.model.State]¶: The current set.

has_converged() → bool¶: True after a step where the set did not change.

step() → frozenset[stormvogel.model.State]¶: Apply the operator once and return the new set.

stormvogel.teaching.qualitative_mdp.spos(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → FixpointIterator¶: Return a FixpointIterator for \(S_{\text{pos}}\) (LFP).

stormvogel.teaching.qualitative_mdp.sposmin(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → FixpointIterator¶: Return a FixpointIterator for \(S_{\text{pos}}^{\min}\) (LFP).

stormvogel.teaching.qualitative_mdp.smaxas(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → FixpointIterator¶

Return a FixpointIterator for \(S_{\text{as}}^{\max}\) (GFP).

Initialises from \(S_{\text{pos}}\) rather than the full state space. Starting from all states is a trivial fixed point whenever a non-target absorbing state (e.g. a self-looping sink) is present.

stormvogel.teaching.qualitative_mdp.sminas(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → FixpointIterator¶

Return a FixpointIterator for \(S_{\text{as}}^{\min}\) (GFP).

Initialises from \(S_{\text{pos}}^{\min}\) — the result of running sposmin() to convergence — so that states the minimiser can trap forever are excluded before the GFP begins. Starting from the full state space \(S\) would give a trivial fixed point.

stormvogel.teaching.qualitative_mdp._run(it: FixpointIterator) → frozenset[stormvogel.model.State]¶

stormvogel.teaching.qualitative_mdp.compute_spos(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶: Return \(S_{\text{pos}}\) directly (runs LFP to convergence).

stormvogel.teaching.qualitative_mdp.compute_sposmin(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶: Return \(S_{\text{pos}}^{\min}\) directly (runs LFP to convergence).

stormvogel.teaching.qualitative_mdp.compute_smaxas(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶: Return \(S_{\text{as}}^{\max}\) directly (runs GFP to convergence).

stormvogel.teaching.qualitative_mdp.compute_sminas(mdp: stormvogel.model.Model, target_states: list[stormvogel.model.State] | set[stormvogel.model.State]) → frozenset[stormvogel.model.State]¶: Return \(S_{\text{as}}^{\min}\) directly (runs GFP to convergence).

stormvogel.teaching.qualitative_mdp.run_and_collect(it: FixpointIterator, include_initial: bool = True) → list[frozenset[stormvogel.model.State]]¶

Run it to fixpoint and return all intermediate sets as a list.

Parameters:

it – The iterator to run.
include_initial – If True, prepend the initial set before the first step.

Returns:

Ordered list of snapshots; pass the result to visualise_iterations().

stormvogel.teaching.qualitative_mdp.visualise_iterations(snapshots: list[frozenset[stormvogel.model.State]], mdp: stormvogel.model.Model, highlight: bool = True)¶

Return a pandas DataFrame showing set membership at each iteration.

Rows are states; column i shows whether that state was in the set after step i. Pass the list of sets returned by successive FixpointIterator.step() calls (including the initial set if desired).

Parameters:

snapshots – Ordered list of state sets, one per iteration.
mdp – The MDP (used to fix row order via sorted_states).
highlight – If True, colour True cells green and False cells red via a pandas Styler.

Returns:

A styled or plain pandas.DataFrame.