verify

verify(
model: SparseModel,
property: Property | Formula,
*,
region: ParameterRegion | None = None,
region_bound: RationalFunctionCoefficient | float | int | None = None,
region_engine: RegionCheckEngine = RegionCheckEngine.PARAMETER_LIFTING,
environment: Environment | None = None,
) → bool

Verify a bounded probability or reward property for all well-defined valuations in a region.

Requires a sparse parametric DTMC or MDP with exactly one initial state. Provide exactly one of region or region_bound. The region must cover all model parameters. Standard parameter lifting requires a well-defined, graph-preserving region. Robust parameter lifting supports DTMCs and can include graph-changing valuations. Unsupported inputs raise an exception.

For MDPs, properties have the following semantics:

Property

Schedulers that must satisfy the bound

P>=0.8 [F "target"]

Every scheduler

Pmin>=0.8 [F "target"]

Every scheduler

Pmax>=0.8 [F "target"]

At least one scheduler (PLA only)

P<=0.8 [F "target"]

Every scheduler

Pmin<=0.8 [F "target"]

At least one scheduler (PLA only)

Pmax<=0.8 [F "target"]

Every scheduler
Parameters:

  • model – Parametric sparse DTMC or MDP.

  • property – Bounded probability or reward property or formula.

  • region – Explicit parameter region.

  • region_bound – Use [region_bound, 1-region_bound] for every parameter; must be in [0, 1/2]. Floats use their decimal representation, e.g. 0.2 means exactly 1/5.

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

  • environment – (optional) Environment configuring the analysis.

Returns:

Whether every well-defined valuation in the region satisfies the property.