check_feasibility

check_feasibility(
model: SparseModel,
property: Property | Formula,
*,
region: ParameterRegion | None = None,
region_bound: RationalFunctionCoefficient | float | int | None = None,
method: FeasibilityMethod = FeasibilityMethod.PLA,
region_engine: RegionCheckEngine = RegionCheckEngine.PARAMETER_LIFTING,
environment: Environment | None = None,
) → FeasibilitySynthesisResult

Search for a well-defined parameter valuation satisfying a bounded probability or reward property.

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 and satisfy the method’s and engine’s requirements. Standard parameter lifting, GD, and SCP require a well-defined, graph-preserving region. GD supports DTMCs only. 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.

  • method – Feasibility method: parameter lifting (PLA), gradient descent (GD), or sequential convex programming (SCP).

  • region_engine – Region checking engine, used only for PLA and ignored by GD and SCP. See RegionCheckEngine for arithmetic choices and region requirements.

  • environment – (optional) Environment configuring the analysis.

Returns:

Result with status EXISTS_SAT, ALL_VIOLATED, or UNKNOWN. A witness is present only for EXISTS_SAT.