transform_to_discrete_time_model

transform_to_discrete_time_model(

model,

properties: Property | Iterable[Property],

) → tuple

Transform a continuous-time model (CTMC or MA) into a discrete-time model (DTMC or MDP).

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

Parameters:

• model – Sparse continuous-time model.

• properties – Property or properties which are transformed accordingly.

Returns:

Tuple of the discrete-time model and the transformed formulas.