verify_with_belief_unfolding

verify_with_belief_unfolding(
model: SparsePomdp,
property: Property | Formula,
*,
max_exploration_size: int | None = None,
max_exploration_time: int | None = None,
use_clipping: bool = False,
clipping_resolutions: Sequence[int] | None = None,
cut_zero_gap: bool = False,
exploration_queue_order: ExplorationQueueOrder = ExplorationQueueOrder.FIFO,
build_choice_labeling: bool = True,
generate_policy: bool = False,
environment: Environment | None = None,
) → BeliefBasedModelCheckerResult

Approximate an unbounded reachability probability or expected reachability reward by unfolding the belief MDP.

The POMDP is prepared automatically (made canonic, target observations refined, failure states made absorbing). The POMDP must have exactly one initial state and the property must be non-nested, without threshold and with an explicit optimization direction. The value is a lower bound for maximization and an upper bound for minimization. Without clipping and with completed exploration, the value is the value of the belief MDP.

Parameters:

  • model – POMDP.

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

  • max_exploration_size – (optional) Maximal number of discovered beliefs. Defaults to no limit.

  • max_exploration_time – (optional) Maximal exploration time in seconds. Defaults to no limit.

  • use_clipping – Whether belief clipping is used.

  • clipping_resolutions – Clipping resolution (positive) for each observation of the POMDP. Required for clipping.

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

  • 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.

  • generate_policy – Whether a finite-state controller is generated, see BeliefBasedModelCheckerResult.policy. The controller refers to the prepared POMDP, i.e., actions are ordered as in the canonic POMDP and observations include the refined target observations.

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

Returns:

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