verify_with_belief_discretization

verify_with_belief_discretization(
model: SparsePomdp,
property: Property | Formula,
resolution: int = 2,
*,
use_dynamic: bool = False,
cut_zero_gap: bool = False,
exploration_queue_order: ExplorationQueueOrder = ExplorationQueueOrder.FIFO,
build_choice_labeling: bool = True,
environment: Environment | None = None,
) → BeliefBasedModelCheckerResult

Approximate an unbounded reachability probability or expected reachability reward by discretizing the belief space (Freudenthal triangulation).

The POMDP is prepared as for verify_with_belief_unfolding(). The value is an upper bound for maximization and a lower bound for minimization. Completed exploration refers to the discretized MDP and does not imply that the value is exact.

Parameters:

  • model – POMDP.

  • property – Unbounded reachability probability or expected reachability reward property or formula, e.g., Pmax=? [F "goal"].

  • resolution – Resolution (positive) of the discretization. Higher resolutions give tighter bounds.

  • use_dynamic – Whether the resolution is selected per belief using dynamic triangulation.

  • cut_zero_gap – Whether non-target beliefs are cut whose preprocessing bounds coincide.

  • exploration_queue_order – Order in which discovered beliefs are explored.

  • build_choice_labeling – Whether choice labels are built for the belief MDP. Requires choice labels in the POMDP.

  • environment – (optional) Environment configuring the solvers. Defaults to stormpy.environments.default().

Returns:

The result containing the bound, whether the exploration was completed and statistics.