perform_bisimulation

perform_bisimulation(
model,
properties: Property | Iterable[Property],
*,
bisimulation_type: BisimulationType = BisimulationType.STRONG,
options: BisimulationOptions | None = None,
quotient_format: QuotientFormat = QuotientFormat.DD,
)

Minimize a model via bisimulation while preserving the given properties.

Parameters:

  • model – The model (sparse or symbolic).

  • properties – Property or properties which are preserved by the minimization.

  • bisimulation_type – Type of bisimulation (strong or weak).

  • options – (optional) Further options for the bisimulation of sparse models. If given, its bisimulation type takes precedence over the bisimulation_type argument.

  • quotient_format – Format of the quotient for symbolic models (DD for a symbolic quotient, SPARSE for a sparse quotient).

Returns:

The minimized model.