eliminate_non_markovian_chains

eliminate_non_markovian_chains(
model,
properties: Property | Iterable[Property],
label_behavior: EliminationLabelBehavior,
) → tuple

Eliminate chains of non-Markovian states in a Markov automaton if possible.

Formulas which are not preserved by the elimination are dropped (with a warning).

Parameters:

  • model – Sparse Markov automaton.

  • properties – Property or properties which are transformed accordingly.

  • label_behavior – How labels of eliminated states are handled.

Returns:

Tuple of the resulting model (an MA or a CTMC) and the transformed formulas.