Frameworks and Model Checking

This module connects to external frameworks, like stormpy for model checking. We include methods for building (I)MDPs from explicit environments, convenience functions for model checking and policy synthesis, as well as wrappers to apply shielding to environments.

Building stormpy models

verigym.frameworks.stormpy.stormpy_utils.build_stormpy_mdp(env: BaseExplicitEnv, overapproximate=True) → SparseMdp

Builds a stormpy.storage.SparseMdp from a BaseExplicitEnv.

Parameters:

env (ExplicitEnv)

Returns:

mdp

Return type:

stormpy.storage.SparseMdp

Notes

• Every state gets one choice per available action, i.e., per action with at least one successor in the transition function.

• Choices are labelled with the env’s action names if it has action labels (e.g., when loaded from a prism file), and with the action indices otherwise. StormpyPolicy maps the choices of a scheduler back to the env’s actions in both cases (see its label_to_action parameter).

• States without available actions are deadlocks. This includes states whose actions have no successors, which used to break the export. A deadlock gets a single unlabelled self-loop with probability 1 and zero reward, and the state label “deadlock”.

verigym.frameworks.stormpy.stormpy_utils.build_stormpy_imdp(env: BaseExplicitEnv, use_reward_uncertainty=False, overapproximate=True)

Builds a stormpy IMDP from any BaseExplicitEnv. If used with an env without intervals instead of an interval env (IntervalEnvMixin, e.g., IntervalExplicitEnv), it will build an IMDP where lower bounds == upper bounds everywhere. Apart from the intervals, the IMDP is the same as the MDP of build_stormpy_mdp (see its notes on choices, choice labels and deadlocks).

Parameters:

• env (BaseExplicitEnv) – The explicit env.

• use_reward_uncertainty (bool = False) – Whether to build uncertainty over rewards. If True and the env is an interval env (IntervalEnvMixin), this will use the interval_reward_function. Else, it will use the reward_function and build interval rewards in stormpy where lower bounds == upper bounds. This is because standard (non-interval) reward functions are technically incompatible with the stormpy IMDP.

• overapproximate (bool = True) – How to handle state labels for abstract state. If True, an abstract state gets assigned a label if any original state in it has the label. Else, an abstract state gets assigned a label only if all original states in it have the label.

Returns:

imdp

Return type:

stormpy.SparseIntervalMdp

verigym.frameworks.stormpy.stormpy_utils.build_stormpy_dtmc(env: BaseExplicitEnv, policy: PolicyClass, overapproximate=True)

Builds a stormpy.storage.SparseDtmc from a BaseExplicitEnv and some policy.

Parameters:

• env (BaseExplicitEnv) – The environment.

• policy (PolicyClass) – A policy for that environment.

• overapproximate (bool) – Whether to overapproximate state labels on abstract environments. Default = True.

Returns:

dtmc

Return type:

stormpy.storage.SparseDtmc

verigym.frameworks.stormpy.stormpy_utils.load_stormpy_model(prismpath: str, property_strs: str | None = None, constants: str | None = None) → SparseMdp

Load a stormpy model from a prism file.

Parameters:

• prismpath (str) – The path to the prism model file

• property_strs (str) – Temporal logic formulas. Optional.

• constants (str) – If the prism model contains unresolved constants, need to provide them here in storm parseable format.

Returns:

mdp – The loaded stormpy mdp.

Return type:

stormpy.storage.SparseMdp

Note

We currently only accept prism, pm or nm files. Will extend to other formats, such as jani in the future.

Model checking

verigym.supplements.modelchecking.get_policy_from_stormpy(env: BaseExplicitEnv, property_str: str) → StormpyPolicy

Given an explicit env and a property, returns a VeriGym compatible policy from stormpy.

Parameters:

• env (BaseExplicitEnv) – The explicit env to model check.

• property_str (str) – The property to check.

Returns:

policy – The policy obtained from stormpy.

Return type:

verigym.StormpyPolicy

verigym.supplements.modelchecking.check_policy_value_in_stormpy(env: BaseExplicitEnv, policy: PolicyClass, property_str: str, only_initial_states=True)

Given an environment, a policy on that environment, and a property, builds a DTMC from the environment’s underlying MDP and the policy, solves it in stormpy, and returns the value vector.

Parameters:

• env (BaseExplicitEnv) – The environment.

• policy (PolicyClass) – The policy on that environment.

• property_str (str) – The property to check.

Returns:

value_vector – Value per state in the DTMC.

Return type:

list

Shielding

class verigym.supplements.shield_wrapper.AbstractPostShieldWrapper(env: VeriGymEnv, shield: ArrayLike, abstraction_mapper: AbstractionMapper, seed=None)

Bases: Wrapper

Implements a simple post-shield over a Gymnasium-environment by overwriting the step function.

Initialises the AbstractPostShieldWrapper.

Parameters:

• env (VeriGymEnv) – The VeriGym environment to apply the shield to.

• shield (np.array) – An array of dimensionality (number abstract states, number actions). For each state-action pair: if shield[state, action] == True, the action is permitted. If False, the action is blocked.

• abstraction_mapper (AbstractionMapper) – An abstraction mapper that maps to a discrete abstract state space on which the shield is defined.

• seed (int, optional) – Seed of the random generator that chooses a safe action when the chosen action is blocked.

Notes

The input environment must have a discrete action space. The abstraction mapper must map to a discrete abstract state space.

reset(**kwargs)

Overwrites Env.reset to store information of the current observation and info. If a seed is passed, the shield’s RNG for choosing a random safe action is reseeded as well.

step(action)

Take a step in the shielded environment, with post-shield semantics. That is, after an action is proposed, the shield checks whether it is permitted. The shield is applied as follows:

If the abstract state corresponding to the current observation allows the chosen action,

returns the result of env.step with the chosen action.

Otherwise, the action is blocked. In that case:

If other actions are available in the state,

randomly chooses an available action, and returns the result of env.step with the random action.

Otherwise, if no permitted action is available, terminates the episode.