Policies

Policies map observations of an environment to actions. All policies inherit from PolicyClass, which uses an AbstractionMapper to translate between the environment and the space the policy was computed for, e.g., to run a policy computed on an abstract model in the original environment. Exploration policies collect data for model learning (see the model learning guide). Policies from other frameworks wrap policies computed by stormpy, PRISM, or Stable-Baselines3 (see importing policies). evaluate_policy estimates the average return of a policy in an environment.

Base class

class verigym.PolicyClass(policy: Any, abstraction_mapper: AbstractionMapper)[source]

An abstract class providing an interface to any kind of model policy. Given an observation in the VeriGym environment, return an action for the VeriGym environment based on the abstract model’s policy.

Initializes a policy.

Parameters:

  • policy (Any) – The object that contains the policy (e.g. computed by an external framework). Can be used in the `self._action_from_policy

  • abstraction_mapper (AbstractionMapper, optional) – An optional mapping that translates actions from e.g. abstracted environment to original environment. By default None, then an identity mapping is used, not changing the outputted action.

get_action(obs, info=None)[source]

Gets an observation from env.observation_space. Queries the model’s policy. Map the action from the model’s policy to env.action_space

Parameters:

obs (object) – An observation in the environment’s observation space

Returns:

action – An action in the environment’s action space

Return type:

object

seed(seed: int | None = None) → None[source]

Seeds the random generator of the policy, e.g. by create_abstraction(seed=...). Deterministic policies ignore it; policies that sample their actions need to redefine it.

Parameters:

seed (int | None, optional) – The seed. If None, the generator is seeded from OS entropy.

update_for_abstraction_refinement(dataset: list[tuple], T_counts: defaultdict[int, defaultdict[int, defaultdict[int, int]]], P_tot: dict, R_cumsum: defaultdict[int, defaultdict[int, float]], S_init_counts: defaultdict[int, int]) → PolicyClass[source]

Updates the policy during the exploration phase of the abstraction learning phase. - If this policy does not change during abstraction learning, it just returns itself, unchanged. - If the policy does update, this function needs to be redefined for that policy class.

Examples for which policies this function may be useful: - state-based sampling (e.g. entropy-based sampling) - RL policy that is updated throughout the abstraction learning process.

Parameters:

  • dataset (list[tuple]) – A dataset with observations, list of tuples (state, action, reward, next_state).

  • T_counts (defaultdict[int, defaultdict[int, defaultdict[int, int]]]) – A nested dict T_count[state][action][next_state] returns the integer count.

  • P_tot (dict[tuple[int, int], int]) – A dict storing the occurrences of state-action pairs. Useful for iterating through T_counts and R_cumsum, see learn_abstraction.py for examples.

  • R_cumsum (defaultdict[int, defaultdict[int, float]]) – A nested dict, where R_cumsum[state][action] returns the cumulative reward encountered for the given state-action pair (not summed up over time). The mean reward is R_cumsum[state][action] / P_tot[(state, action)].

  • S_init_counts (defaultdict[int, int]) – A dict, where S_init_counts[state] returns the number of occurences that state was the intial state.

Returns:

The policy that should be further used for exploring through the abstraction learning.

Return type:

PolicyClass

Exploration policies

class verigym.policy.randomized.RandomizedPolicy(env: VeriGymEnv, seed=None)[source]

Bases: PolicyClass

A policy that returns random actions, as sampled from the provided environment. Works for every class inheriting from VeriGymEnv (and therefore gym.Env).

Initializes a policy.

Parameters:

  • policy (Any) – The object that contains the policy (e.g. computed by an external framework). Can be used in the `self._action_from_policy

  • abstraction_mapper (AbstractionMapper, optional) – An optional mapping that translates actions from e.g. abstracted environment to original environment. By default None, then an identity mapping is used, not changing the outputted action.

seed(seed=None)[source]

Seeds the random generator of the policy, e.g. by create_abstraction(seed=...). Deterministic policies ignore it; policies that sample their actions need to redefine it.

Parameters:

seed (int | None, optional) – The seed. If None, the generator is seeded from OS entropy.

class verigym.policy.qvalue.QValuePolicy(env: VeriGymEnv, abstraction_mapper: AbstractionMapper, Q_init_strategy='zero', discount=0.95, epsilon=0.0, update_iterations=50, seed: int | None = None)[source]

Bases: PolicyClass

A native MDP policy class that selects actions based on (approximate) Q-values.

This policy class allows for static epsilon-greedy (no annealing).

Parameters:

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

  • abstraction_map (AbstractionMapper) – Used in case that env is abstract.

  • Q_init_strategy (str) – How to initialize the Q_table. Default: “zero”. Further options: “uniform”: uniform across actions.

  • discount (float) – Discount factor, used during refinement. Default 0.95.

  • epsilon (float) – Exploration threshold for epsilon-greedy. Default 0.0 (no exploration).

  • update_iterations (int) – The number of iterations to update the Q_table for during abstraction refinement.

  • seed (int) – Initial seed used for rng calls

seed(seed=None)[source]

Seeds the random generator of the policy, e.g. by create_abstraction(seed=...). Deterministic policies ignore it; policies that sample their actions need to redefine it.

Parameters:

seed (int | None, optional) – The seed. If None, the generator is seeded from OS entropy.

update_for_abstraction_refinement(dataset, T_counts, P_tot_counts, R_cumsum, state_distr_counts)[source]

Updates the policy during the exploration phase of the abstraction learning phase. - If this policy does not change during abstraction learning, it just returns itself, unchanged. - If the policy does update, this function needs to be redefined for that policy class.

Examples for which policies this function may be useful: - state-based sampling (e.g. entropy-based sampling) - RL policy that is updated throughout the abstraction learning process.

Parameters:

  • dataset (list[tuple]) – A dataset with observations, list of tuples (state, action, reward, next_state).

  • T_counts (defaultdict[int, defaultdict[int, defaultdict[int, int]]]) – A nested dict T_count[state][action][next_state] returns the integer count.

  • P_tot (dict[tuple[int, int], int]) – A dict storing the occurrences of state-action pairs. Useful for iterating through T_counts and R_cumsum, see learn_abstraction.py for examples.

  • R_cumsum (defaultdict[int, defaultdict[int, float]]) – A nested dict, where R_cumsum[state][action] returns the cumulative reward encountered for the given state-action pair (not summed up over time). The mean reward is R_cumsum[state][action] / P_tot[(state, action)].

  • S_init_counts (defaultdict[int, int]) – A dict, where S_init_counts[state] returns the number of occurences that state was the intial state.

Returns:

The policy that should be further used for exploring through the abstraction learning.

Return type:

PolicyClass

class verigym.policy.qvalue.ActiveLearningPolicy(env: VeriGymEnv, abstraction_mapper: AbstractionMapper, Q_init_strategy='zero', discount=0.95, epsilon=0.0, update_iterations=50, seed=None)[source]

Bases: QValuePolicy

A policy used for active learning of MDPs, based on the state-action count reward method of Araya-Lopéz et. al. (2012).

Parameters:

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

  • abstraction_map (AbstractionMapper) – Used in case that env is abstract.

  • Q_init_strategy (str) – How to initialize the Q_table. Default: “zero”. Further options: “random” -> random values. “uniform”: uniform across actions.

  • discount (float) – Discount factor, used during refinement. Default 0.95.

  • epsilon (float) – Exploration threshold for epsilon-greedy. Default 0.0 (no exploration).

  • update_iterations (int) – The number of iterations to update the Q_table for during abstraction refinement.

update_for_abstraction_refinement(dataset, T_counts, P_tot_counts, R_cumsum, state_distr_counts)[source]

Updates the policy during the exploration phase of the abstraction learning phase. - If this policy does not change during abstraction learning, it just returns itself, unchanged. - If the policy does update, this function needs to be redefined for that policy class.

Examples for which policies this function may be useful: - state-based sampling (e.g. entropy-based sampling) - RL policy that is updated throughout the abstraction learning process.

Parameters:

  • dataset (list[tuple]) – A dataset with observations, list of tuples (state, action, reward, next_state).

  • T_counts (defaultdict[int, defaultdict[int, defaultdict[int, int]]]) – A nested dict T_count[state][action][next_state] returns the integer count.

  • P_tot (dict[tuple[int, int], int]) – A dict storing the occurrences of state-action pairs. Useful for iterating through T_counts and R_cumsum, see learn_abstraction.py for examples.

  • R_cumsum (defaultdict[int, defaultdict[int, float]]) – A nested dict, where R_cumsum[state][action] returns the cumulative reward encountered for the given state-action pair (not summed up over time). The mean reward is R_cumsum[state][action] / P_tot[(state, action)].

  • S_init_counts (defaultdict[int, int]) – A dict, where S_init_counts[state] returns the number of occurences that state was the intial state.

Returns:

The policy that should be further used for exploring through the abstraction learning.

Return type:

PolicyClass

class verigym.policy.qvalue.EntropyLearningPolicy(env: VeriGymEnv, abstraction_mapper: AbstractionMapper, Q_init_strategy='zero', discount=0.95, learning_rate=0.2, update_iterations=50, seed=None)[source]

Bases: QValuePolicy

A policy class for (iteratively) computing max-entropy policies, based on algorithm from Hazan et. al. (2019).

Parameters:

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

  • abstraction_map (AbstractionMapper) – Used in case that env is abstract.

  • Q_init_strategy (str) – How to initialize the Q_table. Default: “zero”. Further options: “random” -> random values. “uniform”: uniform across actions.

  • discount (float) – Discount factor, used during refinement. Default 0.95.

  • learning_rate (float) – The learning rate. Default 0.2

  • update_iterations (int) – The number of iterations to update the Q_table for during abstraction refinement.

update_for_abstraction_refinement(dataset, T_counts, P_tot_counts, R_cumsum, state_distr_counts)[source]

Updates the policy during the exploration phase of the abstraction learning phase. - If this policy does not change during abstraction learning, it just returns itself, unchanged. - If the policy does update, this function needs to be redefined for that policy class.

Examples for which policies this function may be useful: - state-based sampling (e.g. entropy-based sampling) - RL policy that is updated throughout the abstraction learning process.

Parameters:

  • dataset (list[tuple]) – A dataset with observations, list of tuples (state, action, reward, next_state).

  • T_counts (defaultdict[int, defaultdict[int, defaultdict[int, int]]]) – A nested dict T_count[state][action][next_state] returns the integer count.

  • P_tot (dict[tuple[int, int], int]) – A dict storing the occurrences of state-action pairs. Useful for iterating through T_counts and R_cumsum, see learn_abstraction.py for examples.

  • R_cumsum (defaultdict[int, defaultdict[int, float]]) – A nested dict, where R_cumsum[state][action] returns the cumulative reward encountered for the given state-action pair (not summed up over time). The mean reward is R_cumsum[state][action] / P_tot[(state, action)].

  • S_init_counts (defaultdict[int, int]) – A dict, where S_init_counts[state] returns the number of occurences that state was the intial state.

Returns:

The policy that should be further used for exploring through the abstraction learning.

Return type:

PolicyClass

Policies from other frameworks

class verigym.StormpyPolicy(policy, abstraction_mapper: AbstractionMapper, mdp: SparseMdp, label_to_action: dict | None = None)[source]

Bases: PolicyClass

A native MDP policy class that picks actions according to an explicit mapping, such as imported from stormpy.

Initialize using a stormpy policy and mdp.

Parameters:

  • policy (stormpy.storage.Scheduler)

  • abstraction_mapper (AbstractionMapper)

  • mdp (stormpy.storage.SparseMdp)

  • label_to_action (dict | None) – Maps the choice labels of mdp to the actions of the env, e.g., env.formatter.label_to_action for envs loaded from a prism file. If None (default), it is derived from the choice labels, which are the action indices or the action names (see _unwrap_scheduler).

class verigym.frameworks.prism.prismpolicy.PrismPolicy(policy_path: str, abstraction_mapper: AbstractionMapper, action_map: dict = None)[source]

Bases: PolicyClass

For PrismPolicy, the external policy object is a file.

Notes

1. Assumes that the policy file was generated in PRISM with the option states=false. Otherwise, states are represented by valuations instead of indices, which cannot be mapped back using the abstraction mapper. 2. Assumes memoryless deterministic strategies.

Initializes a policy from PRISM-readable output.

Parameters:
policystr

The path to the PRISM policy output file. Should be a tra file. We currently do not support dot files.

abstraction_mapperAbstractionMapper

Maps the state/action spaces of the PRISM model to the gym environment to deploy the policy on.

action_mapdict(str: int)

A mapping from PRISM action label to discrete action index in the gym space.

class verigym.frameworks.stable_baselines3.policy.SB3Policy(policy: PolicyPredictor, env: Env, abstraction_mapper: AbstractionMapper | None = None, deterministic: bool = False)[source]

Bases: PolicyClass

Initializes a verigym compatible policy from a policy by the stable baselines 3 (SB3) framework.

Defaults to an identity AbstractionMapper, meaning the policy’s actions remain unchanged (as there is no abstraction to map from/to).

Parameters:

  • policy (SB3_original_Policy) – The SB3 policy. This can be any object that implements a predict method such as the SB3 framework’s BaseAlgorithm or BasePolicy and child classes.

  • abstraction_mapper (AbstractionMapper, optional) – The abstraction mapper may map the action to another action space (e.g. from abstracted to original environment). Defaults to None, meaning the action remains unchanged.

  • deterministic (bool, optional) – Whether to take the most likely action instead of sampling from the policy’s action distribution. Defaults to False.

Returns:

A verigym compatible policy.

Return type:

SB3Policy

seed(seed=None)[source]

Seeds the generators SB3 samples actions from (random, numpy and torch are global). None leaves them as they are.

Evaluation

verigym.policy.utils.evaluate_policy(model: VeriGymEnv, policy: PolicyClass, n_steps: int) → tuple[float, float][source]

Takes a policy and an environment and does the rollouts on that environment and checks its performance wrt average return.