Model Learning

Functions for learning explicit models from a simulator. create_abstraction is the main entry point: it explores the original environment with an exploration policy (see Policies) and returns the learned MDP or IMDP. abstraction_refinement repeats this with finer and finer abstraction mappers until a stopping criterion is met, see the abstraction refinement workflow. The remaining functions are the building blocks of create_abstraction, e.g., for learning from your own data. Feature selection removes state features before learning, see the feature selection workflow. For an introduction, see the model learning guide.

Learning abstractions

verigym.create_abstraction(original_env: VeriGymEnv, abstraction_mapper: AbstractionMapper, exploration_policy: PolicyClass, num_steps: int, n_iterations: int = 1, multithreading: bool = True, verbose: bool = False, return_info=False, intervals: bool = False, assume_iid: bool = False, dataset: list[list[tuple]] | None = None, seed: int = None) → AbstractedExplicitEnv

Creates an abstraction from a VeriGymEnv by discretizing the state and action spaces. Returns an AbstractedExplicitEnv.

Parameters:

• original_env (VeriGymEnv) – The environment / model to be abstracted.

• abstraction_mapper (AbstractionMapper) – Holds the mapping between the original space (of original_env) and the space which we are abstracting into.

• exploration_policy (PolicyClass) – The policy of interacting with the original_env (e.g. a random policy).

• num_steps (int) – Number of steps to simulate within the environment per iteration (also, see n_iterations and dataset). Set to 0 to only use a given dataset without any simulation.

• n_iterations (int) – Number of (interleaving) iterations. For each iteration the exploration_policy.update_for_abstraction_refinement(...) will be called, allowing the policy to update based on the gathered interactions (e.g. for state-based exploration policies). Note, that the total number of simulated steps equals n_iterations * num_steps, or (n_iterations - 1) * num_steps if a dataset is given. For policies that are not interleaving, set n_iterations to 1 (default).

• multithreading (bool, optional) – Whether to multithread or use single thread.

• verbose (bool, optional) – Whether to be verbose, by default False.

• intervals (bool, optional) – Whether to learn transition functions with (confidence) intervals or point-based estimates. Default is False, i.e., point-based estimate learning.

• assume_iid (bool, optional.) – Whether to assume that the data distribution is iid or not. This is only relevant for interval learning. Defaults to False.

• dataset (list[list[tuple]] | None, optional) – Pre-collected trajectories (as returned by VeriGymEnv.simulate()) in the original space. If given, the dataset is used in the first of n_iterations and only the following iterations collect the num_steps samples. To only use the dataset without any simulation, set n_iterations == 1 and num_steps == 0. Defaults to None.

• seed (int | None, optional) – Seeds the simulation of original_env (a different seed per iteration, derived from seed) and the exploration_policy (with exploration_policy.seed(seed), which overrides the policy’s own seed). If None (default), both continue with their current random generators.

Returns:

The abstracted model.

Return type:

AbstractedExplicitEnv

Notes

• If intervals == True, the return type is IntervalAbstractedExplicitEnv, which is a sub-type of AbstractedExplicitEnv. It only stores the intervals, and its point estimates (e.g., to sample transitions) are derived from them, see IntervalTransitionFunction.point_estimate.

• The returned model has an extra terminal sink state with index abstraction_mapper.abstract_n_states (the last enumerated state). Hence it has abstract_n_states + 1 states and its observation_space is Discrete(abstract_n_states + 1).

  • Every step on which original_env terminated (not truncated) transitions into the terminal state. The abstraction mapper never maps an observation to it (meaning no original state maps to the terminal state in the abstract state space).

  • Every action of the terminal state loops back to itself with reward 0 (see add_terminal_sink_state()). Without them, the terminal state would have no actions, i.e., it would be a deadlock.

  • In interval models, these self-loops are given the exact interval (1.0, 1.0).

verigym.abstraction.abstraction_refinement.abstraction_refinement(original_env: GenerativeEnv, mapper_schedule: list, num_steps: int, earlystopping_callback: Callable, make_exploration_policy: Callable[[AbstractionMapper | None], PolicyClass], n_iterations: int = 1, reuse_dataset: bool = True, seed: int | None = None, multithreading: bool = True) → list[tuple[tuple[tuple[float, float]], AbstractedExplicitEnv, StormpyPolicy]]

Learn an abstraction for each mapper in mapper_schedule until earlystopping_callback says stop.

Parameters:

• original_env (verigym.GenerativeEnv) – Environment to abstract.

• mapper_schedule (list) – Abstraction mappers to learn the abstraction for, in order.

• num_steps (int) – Exploration step budget per mapper, split evenly over n_iterations.

• earlystopping_callback (Callable.) – (original_env, abstracted_model) -> (stop: bool, metric: Any). User may copmute metrics as well as return a bool flag stop indicating if abstraction refinement should stop. May also return arbitrary information such as metrics that are returned by this function as a list.

• make_exploration_policy (Callable[[verigym.AbstractionMapper | None], verigym.PolicyClass]) – Constructor for exploration policy. mapper -> policy. Called with None if reuse_dataset is set.

• n_iterations (int, optional) – Number of interleaved exploration/learning rounds per mapper, by default 1

• reuse_dataset (bool, optional) – Collect one dataset up front and share it across all mappers, by default True. Requires n_iterations == 1 and a mapper-independent exploration policy. Not every exploration strategy is compatible with this setting.

• seed (int | None, optional) – Seeds the exploration: the collection of the reused dataset (env and policy, as create_abstraction does) and create_abstraction for every mapper, so all mappers are learned with the same random numbers. If None (default), the env and policies continue with their current random generators.

• multithreading (bool, optional) – Whether create_abstraction learns the abstraction with multiple processes, by default True

Returns:

A list of (metric, abstracted_model), one per mapper tried.

Return type:

list[tuple[tuple[tuple[float, float]], verigym.AbstractedExplicitEnv, verigym.StormpyPolicy]]

verigym.abstraction.learn_abstraction.learn_abstraction(dataset: list[list[tuple[int, int, float, int, bool]]], n_states: int, n_actions: int, abstraction_mapper: AbstractionMapper = None, multithreading: bool = True, terminal_state: int | None = None, verbose=True) → tuple[dict, dict, dict, dict]

Abstraction learning for a given dataset. Single- or multithreaded. Computes the total counts (!) for transition and reward function and initial state distribution. Do not forget to normalize (see normalize_aggregated_counts()) for obtaining probability distributions.

Parameters:

• dataset (list[list[tuple[int, int, float, int, bool]]]) – The dataset of which we are learning the abstraction, with steps (state, action, reward, next_state, terminated).

• n_states (int) – Number of states in the state space. (corresponds to the abstract state space if abstraction_mapper is not None) Includes terminal_state, if given.

• n_actions (int) – Number of actions in the action space. (corresponds to the abstract action space if abstraction_mapper is not None)

• abstraction_mapper (AbstractionMapper, optional) – Mapping from an original space (samples in dataset) to the abstract space. If no mapping is required, set to None, by default None

• multithreading (bool, optional) – Flag for using single- or multithreading, by default True

• terminal_state (int | None, optional) – State (number) that terminated steps transition to (see collect_data_from_trajectories()). The terminal’s self-loops are not added here, see add_terminal_sink_state(). By default None

Returns:

T_counts, R_cumsum, P_tot_counts, state_distr_counts

Return type:

tuple[dict, dict, dict, dict]

verigym.abstraction.learn_abstraction.collect_data_from_trajectories(trajectories: list[list[tuple[int, int, float, int, bool]]], n_states: int, mapper: AbstractionMapper | None = None, terminal_state: int | None = None) → tuple[dict, dict, dict, dict]

Taking a dataset of trajectories populates dicts counting the total occurences in the trajectories and add them to the objects that can then be used for computing the transition and reward function as well as the initial state distribution.

Parameters:

• trajectories (list[list[tuple[int, int, float, int, bool]]]) – Dataset of trajectories (state, action, reward, next_state, terminated), as returned by VeriGymEnv.simulate(). Steps without the terminated flag, i.e. (state, action, reward, next_state), are treated as not terminated.

• n_states (int) – Number of states of the corresponding state space (including terminal_state, if given).

• mapper (AbstractionMapper | None) – Maps from the state and action spaces of an original environment to an abstract environment. If None, an identity map (no mapping) will be perormed. Defaults to None.

• terminal_state (int | None) – State that terminated steps transition into, instead of the (mapped) next_state. If None, terminated steps are counted like any other step. Defaults to None.

Returns:

T_counts, R_cumsum, P_tot_counts, state_distr_counts. The count databases created by _create_count_databases, populated from trajectories.

Return type:

tuple[dict, dict, dict, dict]

verigym.abstraction.learn_abstraction.normalize_aggregated_counts(T_dict, R_dict, P_tot, state_distr, n_states, n_actions)

Normalizes the aggregated counts (see learn_abstraction()) into point estimates. The inputs are not modified in place.

Parameters:

• T_dict (dict) – Mapping s -> a -> s’ -> number of observed transitions (s, a, s’).

• R_dict (dict) – Mapping s -> a -> cumulative reward for each state-action pair (not over time).

• P_tot (dict) – Mapping of (s, a) to total counts. State-action pairs with a total count of 0 are skipped.

• state_distr (dict) – Mapping s -> number of occurences of s as initial state.

• n_states (int) – Number of states.

• n_actions (int) – Number of actions.

Returns:

T, R, S_init

Return type:

tuple[TransitionFunction, RewardFunction, StateDistribution]

verigym.abstraction.learn_abstraction.get_interval_transition_reward(T_counts, R_cumsum, P_tot_counts, n_states, n_actions, confidence=0.9, iid=False)

Construct (confidence) intervals from the observed data.

If iid, computes Clopper-Pearson Binomial intervals. Else, computes Azuma-Hoeffding Martingale intervals.

Expects the raw counts (see learn_abstraction()), not the normalized probabilities. Intervals are only constructed for observed successors; unobserved successors keep the interval (0.0, 0.0), i.e., the same support as the point estimates of normalize_aggregated_counts().

Parameters:

• T_counts (dict) – Mapping s -> a -> s’ -> number of observed transitions (s, a, s’)

• R_cumsum (dict) – Mapping s -> a -> cumulative observed reward (the mean is R_cumsum[s][a] / P_tot_counts[(s, a)])

• P_tot_counts (dict) – Mapping of (s,a) to total counts (e.g., the sum of successor counts in T_counts for each s,a). State-action pairs with a total count of 0 are skipped.

• n_states (int) – |S|

• n_actions (int) – |A|

• confidence (float, optional) – The statistical (high) confidence of the iMDP construction, by default 0.9

• iid (boolean, optional) – Whether the data is independently and identically distributed (i.i.d.), by default False

Feature selection

verigym.abstraction.feature_selection.state_feature_selection(original_env: VeriGymEnv, method: str, reduce_indices: list) → tuple[VeriGymEnv, AbstractionMapper]

Applies feature selection to the observation space of a VeriGymEnv. The returned environment is of the same type as the input. Feature selection does not include model learning.

Parameters:

• original_env (VeriGymEnv) – The environment / model to apply feature selection to. The environment’s observation space should be gym.spaces.MultiDiscrete or gym.spaces.Box.

• method (str) – The method of feature selection. “binning” maintains the shape of the observation space. The selected features will be represented by a single valuation. “masking” adapts the shape of the observation space by removing selected features.

• reduce_indices (list) – The features selected for reduction. If the list is empty, the original model is retained.

class verigym.abstraction.feature_selection.ReduceFeaturesWrapper(env, reduce_indices)

Wrapper that can be applied to observation spaces of types gym.spaces.MultiDiscrete and gym.spaces.Box for feature selection.

The wrapper modifies the dimensionality of the original observation space by “removing” features specified in reduce_indices upon initialization. I.e., the output observation space will have less features than the original. The type of observation space and limits/number of possible values remain as in the original.

Constructor for the observation wrapper.

Args:

env: Environment to be wrapped.

observation(observation)

Returns a modified observation.

Args:

observation: The env observation

Returns:

The modified observation

class verigym.abstraction.feature_selection.BinFeaturesWrapper(env, reduce_indices)

Wrapper that can be applied to observation spaces of types gym.spaces.MultiDiscrete and gym.spaces.Box for feature selection.

The wrapped observation space has the same shape, limits, and type as the original observation. reduce_indices specify the features to be reduced. In case of gym.spaces.Box, for an observation obs, obs[reduce_indices] will take the center of the feature’s interval as value. In case of gym.spaces.MultiDiscrete, for an observation obs, obs[reduce_indices] == 0.

Constructor for the observation wrapper.

Args:

env: Environment to be wrapped.

observation(obs)

Returns a modified observation.

Args:

observation: The env observation

Returns:

The modified observation