Model Components

The building blocks of explicit environments (see Environments). Transition and reward functions are stored as nested dicts over integer state and action indices, with interval variants for IMDPs, and the initial state distribution is stored sparsely. State labels assign names to states that satisfy a predicate, e.g., "goal" or "unsafe", so that model checking properties can refer to them. Formatters convert models from external frameworks into this representation, see Extending VeriGym in the import and export guide.

Transition functions

class verigym.TransitionFunction(n_states: int, n_actions: int, T_dict=None)

Base class for transition functions in Verigym environments. It is based on dicts in dicts. All states and actions are flattened to integers indices. ✅ Indexing ❌ Slicing

Example:

T_array  # numpy array of shape (n_states, n_actions, n_states)
T = TransitionFunction.from_array(T_array)
s, a, s_next = 0, 0, 0
T[s, a, s_next] == T[s][a][
    s_next
]  # probability of transitioning from state s to s_next given action a
T[s][a]

classmethod from_array(array: NDArray) → TransitionFunction

Create a TransitionFunction from a 3D numpy array.

Parameters:

array (NDArray) – A 3D numpy array where array[s, a, s’] represents the probability of transitioning from state s to state s’ given action a. Hence, s and a need to already be flattened into integer indices.

Returns:

An instance of TransitionFunction with the transition probabilities set.

Return type:

TransitionFunction

sanity_check() → bool

Check if the transition function is valid, i.e., if the probabilities sum to 1 for each (s,a) pair.

get_sparsity() → float

Returns the sparsity of the transition function.

It is a fraction of all state-action-state transitions that have non-zero probability over all possible state-action-state transitions.

Returns:

Sparsity value of transition function.

Return type:

float

class verigym.environments.transition_func.IntervalTransitionFunction(n_states: int, n_actions: int, T_dict=None)

Bases: TransitionFunction

Extends the TransitionFunction class with intervals over transition probabilities.

classmethod from_array(array: NDArray) → IntervalTransitionFunction

Create a TransitionFunction from a 4D numpy array.

Parameters:

array (NDArray) – A 4D numpy array where array[s, a, s’] represents the interval over all possible probabilities of transitioning from state s to state s’ given action a. Hence, s and a need to already be flattened into integer indices.

Returns:

An instance of IntervalTransitionFunction with the transition probability intervals set.

Return type:

IntervalTransitionFunction

classmethod from_transition_function(transition_function: TransitionFunction) → IntervalTransitionFunction

Create an IntervalTransitionFunction with point intervals [p, p] from a TransitionFunction. Keeps the state-action pairs of transition_function and its successors with a probability > 0.

Parameters:

transition_function (TransitionFunction) – The transition function with point probabilities.

Returns:

An instance of IntervalTransitionFunction where lower bound == upper bound for all transitions.

Return type:

IntervalTransitionFunction

point_estimate() → TransitionFunction

Returns a point estimate within the intervals, used wherever a point estimate is required (e.g., to sample transitions). For each (s,a) pair, it takes the lower bounds and distributes the remaining probability mass over the successors proportionally to the widths of their intervals:

p(s') = lower(s') + (1 - sum(lower)) * (upper(s') - lower(s')) / sum(upper - lower).

If all intervals of (s,a) are points, p(s’) = lower(s’). If the intervals are valid (see sanity_check), every p(s’) lies in its interval and they sum to 1.

Keeps exactly the state-action pairs and successors of the intervals, and does not change the intervals.

Returns:

The point estimate.

Return type:

TransitionFunction

sanity_check() → bool

Check if the transition function is valid, i.e., there exists a valid probability distribution in the intervals for each (s,a) pair. The sums of the lower and upper bounds are compared to 1 up to floating point precision (np.isclose), like the probabilities in TransitionFunction.sanity_check.

get_sparsity() → float

Returns the sparsity of the transition function. It is a fraction of all state-action-state transitions that have non-zero upper probability bounds.

Returns:

Sparsity value of transition function

Return type:

float

Reward functions

class verigym.RewardFunction(n_states: int, n_actions: int, R_dict=None)

Class for reward functions in Verigym environments. It is based on dicts in dicts. All states and actions are flattened to integers indices. ✅ Indexing ❌ Slicing

Example:

R_array  # numpy array of shape (n_states, n_actions)
R = RewardFunction.from_array(R_array)
s, a = 0, 0
R[s, a] == R[s][a]  # reward for taking action a in state s
R[s]

classmethod from_array(array: NDArray) → RewardFunction

Create a RewardFunction from a 2D numpy array.

Parameters:

array (NDArray) – A 2D numpy array of shape (n_states, n_actions) representing the reward function.

Returns:

An instance of RewardFunction initialized with the values from the array.

Return type:

RewardFunction

class verigym.environments.reward_func.IntervalRewardFunction(n_states, n_actions, R_dict=None)

Bases: RewardFunction

Class for reward functions with interval bounds.

classmethod from_array(array: NDArray) → IntervalRewardFunction

Create an IntervalRewardFunction from a 3D numpy array.

Parameters:

array (NDArray) – A 3D numpy array of shape (n_states, n_actions) representing the reward function.

Returns:

An instance of RewardFunction initialized with the values from the array.

Return type:

RewardFunction

classmethod from_reward_function(reward_function: RewardFunction) → IntervalRewardFunction

Create an IntervalRewardFunction with point intervals [r, r] from a RewardFunction. Keeps the state-action pairs of reward_function; all other pairs read as (0.0, 0.0) (see from_dict).

Parameters:

reward_function (RewardFunction) – The reward function with point rewards.

Returns:

An instance of IntervalRewardFunction where lower bound == upper bound for all rewards.

Return type:

IntervalRewardFunction

point_estimate() → RewardFunction

Returns the midpoints (lower + upper) / 2 of the reward intervals, used wherever a point estimate is required. Keeps the state-action pairs of the intervals, and does not change the intervals. Like the interval of a state-action pair without a stored interval (see from_dict), its point estimate reads as 0.0.

Returns:

The point estimate.

Return type:

RewardFunction

classmethod from_dict(R_dict: dict, n_states: int, n_actions: int, fillval=0.0) → IntervalRewardFunction

Create an IntervalRewardFunction from a dict mapping s -> a -> (lower, upper). Only the given state-action pairs are stored; all other pairs read as (fillval, fillval).

Initial state distribution

class verigym.environments.state_distributions.StateDistribution(n_states: int, distr_dict: dict[int, float] | None = None)

Sparse probability distribution over states. Only states with an explicitly written probability are stored; all other states have probability 0.0.

sample(rng: Random) → int

Sample a state according to the distribution, using the random generator rng.

classmethod from_array(array: NDArray) → StateDistribution

Create a StateDistribution from a 1D array, where array[s] is the probability of state s. Only states with non-zero probability are stored.

State labels

TODO: add text

Introduction to this section.

class verigym.environments.labeling.StateLabel(name: str, predicate: Callable)

class verigym.environments.labeling.StateLabeler(labels: set[StateLabel])

class verigym.environments.labeling.AbstractStateLabeler(original_labeler: StateLabeler, abstraction_mapper: AbstractionMapper)

TODO Add docstring @julemarie

Parameters:

• original_labeler (StateLabeler) – The state label manager of the original environment

• abstraction_mapper (AbstractionMapper) – Provides a mapping between original and abstract spaces. For abstractions from discrete state spaces, expects the abstraction_mapper’s backward map to return a set of states. For abstractions from continuous state spaces, expects original states characterized as a 2d list/array where list[0] = lower bound state valuations per dimension, and list[1] = upper bound state valuations per dimension.

Example

abstract_state_idx = 0
abstraction_mapper.abstract_to_original_state(abstract_state_idx)
# discrete:
[0, 1, 2]
# continuous:
[[-1, 1], [-2, 2]]

parse_property(propertystr: str)

Change occurrences of "label" in a property string to "not_label" for correct abstract label over- and underapproximation.

get_labels_of_abstract_state_exist(abstract_state)

Returns state labels for an abstract state, based on the state labels of the contained original states. This function applies the exist operator, i.e., it overapproximates: If any of the original states contained in the abstract state has the label, the abstract state gets the label.

Parameters:

abstract_state (int) – ID/enum representation of the abstract state to find labels for.

Returns:

labels – set of overapproximated state labels for the given abstract state.

Return type:

set

get_labels_of_abstract_state_forall(abstract_state)

Returns state labels for an abstract state, based on the state labels of the contained original states. This function applies the forall operator, i.e., it underapproximates: Only if all original states in the abstract state have the label, the abstract state gets the label.

Parameters:

abstract_state (int) – index of the abstract state to find labels for.

Returns:

labels – set of underapproximated state labels for the given abstract state.

Return type:

set

Formatters

TODO: add text

Introduction to this section.

class verigym.environments.formatter.ExplicitFormatter(model)

Convert an explicit model to a unified format for any ExplicitEnv.

get_full_state_from_idx(state_idx: int) → tuple

The factored state (the values of the variables in var_order) of the state with index state_idx.

class verigym.frameworks.stormpy.formatter.StormpyFormatter(mdp: SparseMdp | SparseIntervalMdp)

Bases: ExplicitFormatter

Convert a stormpy.storage.SparseMdp into a uniform format to support ExplicitEnvs/StormpyEnvs.

Also converts interval MDPs (stormpy.storage.SparseIntervalMdp): their transition probabilities and rewards are (lower, upper) tuples, in an IntervalTransitionFunction and an IntervalRewardFunction. Everything else (actions, labels, valuations, initial states) is the same for both.

get_full_state_from_idx(state_idx)

The factored state (the values of the variables in var_order) of the state with index state_idx.