create_monitor_verifier

create_monitor_verifier(
mc: SparseDtmc,
monitor: SparseMdp,
risk: Sequence[object],
*,
expression_manager: ExpressionManager | None = None,
use_restart_semantics: bool = True,
accepting_label: str = 'accepting',
step_prefix: str = 'step',
horizon_label: str = 'horizon',
) → MonitorVerifier

Create the POMDP for verifying a monitor against a Markov chain.

Parameters:

  • mc – Markov chain.

  • monitor – Monitor given as MDP whose actions are labels of the Markov chain.

  • risk – Risk for each state of the Markov chain.

  • expression_manager – (optional) Expression manager for the variables of the product.

  • use_restart_semantics – Whether restart semantics are used instead of a sink state.

  • accepting_label – Label of the accepting states of the monitor.

  • step_prefix – Prefix of the labels of the monitor steps.

  • horizon_label – Label of the monitor states reaching the horizon.

Returns:

The monitor verifier containing the product POMDP.