compute_extremal_value

compute_extremal_value(
model: SparseModel,
property: Property | Formula,
*,
region: ParameterRegion,
direction: OptimizationDirection,
precision: RationalFunctionCoefficient | float | int,
absolute_precision: bool = False,
engine: RegionCheckEngine = RegionCheckEngine.PARAMETER_LIFTING,
discrete_variables: Iterable[Variable] = (),
environment: Environment | None = None,
) → tuple[RationalFunctionCoefficient | float, dict[Variable, RationalFunctionCoefficient]]

Compute an extremal probability or expected reward over a parameter region.

Requires a sparse parametric DTMC or MDP with exactly one initial state and a quantitative property, e.g. P=? [F "target"]. For MDPs, the property’s min/max determines the scheduler optimization; direction determines the optimization over parameter valuations.

Parameters:

  • model – Parametric sparse DTMC or MDP.

  • property – Quantitative probability or reward property or formula.

  • region – Parameter region satisfying the selected engine’s requirements.

  • direction – Whether to minimize or maximize over parameter valuations.

  • precision – Required precision. Floats must be finite and use their decimal representation, e.g. 1e-6 means exactly 1/1000000.

  • absolute_precision – Whether precision is absolute (True) or relative (False).

  • engine – Region checking engine. See RegionCheckEngine for arithmetic choices and region requirements.

  • discrete_variables – Parameters treated as discrete when splitting regions.

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

Returns:

The value at the returned parameter valuation and that valuation. The value approximates the extremum within the requested precision and can be infinite for rewards.