Abstraction Mapping

A simulator often has a continuous state space: infinitely many states, so there is no explicit MDP to reason about or it may not provide access to an underlying explicit MDP for proprietary reasons. An abstraction maps that space onto an abstract space. The abstract space may be continuous or discrete. If the abstract space is discrete and the abstraction map maps every original state to exactly one abstract state, VeriGym can sample the simulator and build an explicit MDP from it.

The short version

import gymnasium as gym
from verigym.abstraction.abstractionmapper import linspace_mapper
from verigym.abstraction.gym_utils.transform_observation import ReplaceInfObservation

env = gym.make("CartPole-v1")
env = ReplaceInfObservation(env, neg_inf=-10, pos_inf=10)   # see the note below

# Uniformly discretize the state and actions space
abstraction_mapper = linspace_mapper(env, n_bins_states=5, n_bins_actions=2)

observation, _ = env.reset(seed=42)
abstraction_mapper.original_to_abstract_state(observation)

That abstraction_mapper is the single object create_abstraction needs:

abstracted_env = verigym.create_abstraction(
    original_env=env,
    abstraction_mapper=abstraction_mapper,
    exploration_policy=RandomizedPolicy(...),
    num_steps=1000,
)

Unbounded spaces

You cannot cut an infinite interval into bins. CartPole-v1 has ±inf observation dimensions, so wrap it first: env = ReplaceInfObservation(env, neg_inf=-10, pos_inf=10).

The three objects

object	what it is
BinEdges	where a space is cut — one array of bin edges per dimension
AbstractionMap	the mapping for one space (states or actions)
AbstractionMapper	maps a whole environment (holds an AbstractionMap for each: states and actions)

A mapping does not have to be based on BinEdges. An AbstractionMap is just a forward callable, an (optional) backward callable, and the abstract space they connect. Binning is one way to produce such a mapping as is clustering, tile coding or some irregular partition.

Building an AbstractionMap

For a mapping between an original space and an abstract space: To build an abstraction map, you need to define the abstract space as well as the mapping from the original to abstract space (and, optionally, back again). Either use some of our convenience functions that are based on discretizing the space using BinEdges (more details below) or write your own mapping for a non-binning abstraction (clustering, tile coding, …).

Some convenience functions:

from verigym.abstraction.abstractionmapper import linspace_map, pow_map

abstraction_map = linspace_map(env.action_space, n_bins=5)
abstraction_map = pow_map(env.action_space, n_bins=5, power=2)

The resulting AbstractionMap exposes:

• spaces: original_space / abstract_space

• mapping: original_to_abstract / abstract_to_original

• in case the abstract space is enumerable: original_to_enum / enum_to_original

Building an AbstractionMapper

An AbstractionMapper fulfills this task by holding two AbstractionMaps and exposes access to both. When dealing with gym.Envs we might want to have an abstraction mapping for the whole environment, meaning both, the state and action space.

We can conveniently create an AbstractionMapper via

from verigym.abstraction.abstractionmapper import linspace_mapper

abstraction_mapper = linspace_mapper(env, n_bins_states=5, n_bins_actions=2)

Combining individual abstraction types to state and actions space separately:

from verigym.abstraction.abstractionmapper import AbstractionMapper

state_map = linspace_map(env.observation_space, n_bins=5)
action_map = pow_map(env.action_space, n_bins=5, power=2)
abstraction_mapper = AbstractionMapper(state_map, action_map)

Learning abstractions

Before attempting to learn an abstraction of an original environment, check that all requirements of the abstraction mapper are fulfilled with the function validate_for_abstraction(abstraction_mapper).

Not requiring an abstraction

See Identity mapping section for when you only need an abstraction for the action/state space but not the other. Or no abstraction at all.

Going backwards (abstract → original)

An abstraction may throw information away, and so the backward map may not be able to return your exact original sample, but instead an approximation thereof, or a range in which it lies, depending on what represents an abstract state. What it returns is declared by BackwardKind (stored as attribute AbstractionMap.backward_kind):

BackwardKind	returns	use it for
"point"	one representative sample	deploying a policy
"interval"	lower and upper bound, shape (2, *space.shape)	model checking and labeling — “does x > 2 hold in abstract state 17?”
"set"	an iterable of samples	a finite, explicit set of originals
"unknown"	—	no backward map was given; we raise rather than guess

This has to be declared because it cannot be inferred: for a 2-D Box original space, a point, an interval and a 2-element set are all (2, 2) float arrays.

A backward map is optional. verigym.abstraction.create_abstraction does not need one to compute an abstraction but certain features like transferring state labels from an original to an abstract model, as well as deployment of abstract policies on the original model indeed require specification of a backward map.

Discretizing via BinEdges

BinEdges are a useful tool when an original continuous space is discretized using binning. Through defining the BinEdge we obtain the positions of the bins. We achieve this via helper functions such as generate_box_bins mentioned further below.

The four representations in BinEdges
When creating abstractions through the use of BinEdges, it is important to distinguish the four representations (all corresponding to BackwardKind being "point"):

symbol	name	domain	example	belongs to
O	orig	anything (for example \(\mathbb{R}^d\))	[0.31, 7.42]	the original space
V	value	countable (discretized \(\mathbb{R}^d\))	[0.25, 7.50]	the sample snapped onto its bin edges (of 0.25 increments)
I	idx	\(\mathbb{N}^d\)	[1, 3]	one bin index per dimension
E	enum	\(\mathbb{N}^1\)	8	a single flat integer

The example assumes a 2-dimensional continuous space (\(\mathbb{R}^2\)) as the original space. The example and its abstract space representations are visualized below indicating the conversion functions from one representation to another.

Not all conversion functions are displayed in the visualization. BinEdges provides a conversion between any two of the representations, named BinEdges.<from>_to_<to>:

# one direction
BinEdges.orig_to_idx(sample)     # O -> I
BinEdges.orig_to_enum(sample)    # O -> E
BinEdges.orig_to_value(sample)   # O -> V
BinEdges.value_to_idx(value)     # V -> I
BinEdges.value_to_enum(value)    # V -> E
BinEdges.idx_to_enum(index)      # I -> E
# backward direction
BinEdges.enum_to_idx(8)          # E -> I
BinEdges.enum_to_value(8)        # E -> V
BinEdges.enum_to_orig(8)         # E -> O
BinEdges.idx_to_value(index)     # I -> V
BinEdges.idx_to_orig(index)      # I -> O
BinEdges.value_to_orig(index)    # V -> O
BinEdges.idx_to_interval(index)  # I -> (O, O)

The last function, BinEdges.idx_to_interval, returns an interval given an index input. This means it returns tuple with lower and upper bound in the original space. This corresponds to BackwardKind being "interval".

Choosing where to cut the space

BinEdges places a set of cut points along a dimension; every sample is assigned the index of the bin it falls into. The two outer bins are open-ended, meaning that they catch everything below the first edge, or above the last edge:

generate_box_bins(space, bin_func, n_bins) accepts any callable where bin_func matches (low, high, n_bins) -> array, so adding a new discretization type is a one-line change. We provide some defaults:

• np.linspace — equidistant

• centered_pow_bin — narrow bins in the middle, wide at the borders (e.g. a pole angle near 0)

• your own function — must return n_bins ascending edges from low to high

• data-driven — a closure returning quantiles of observed samples, so visited regions get finer bins

n_bins may be an array, giving each dimension its own resolution.

adjust/explanation to newest BinEdge update

There was a new PR, we need to update the explanation for that.

data-driven

Data-driven will soon be added.

Identity mapping: when no abstraction is needed

Sometimes we do not need an abstraction of the original space. Yet, a function may require an abstraction map nonetheless. In those cases we may use an identity map, which returns every input unchanged:

mapper = AbstractionMapper.initialize_identity_mapper(
    state_space=gym.spaces.Discrete(500),
    action_space=gym.spaces.Discrete(6),
)

AbstractionMap.initialize_identity_map(space) does the same for a single space — useful when states are continuous but actions are already discrete.