uppaal-gym 1.0.0

Gymnasium environments for UPPAAL hybrid-system benchmark models

uppaal-gym

Gymnasium environments for classic UPPAAL hybrid-system benchmark models. Designed for research at the intersection of reinforcement learning and formal methods.

Installation

pip install uppaal-gym

Or from source:

git clone https://github.com/andreashhpetersen/uppaal-gym
cd uppaal-gym
pip install -e .

Environments

All environments follow the standard Gymnasium API and are registered automatically on import uppaal_gym.

ID	Observation	Actions	Termination
BouncingBall-v0	position, velocity (2D continuous)	0: do nothing, 1: hit ball	Ball stops (low position and velocity)
CruiseControl-v0	ego velocity, front velocity, distance (3D continuous)	0: decelerate, 1: accelerate, 2: neutral	Collision (distance ≤ 0)
DCDCBoostConverter-v0	inductor current, capacitor voltage, resistance (3D continuous)	0: switch off, 1: switch on	Safety constraint violated
OilPump-v0	cycle time, oil volume, pump status, latency (4D continuous)	0: pump off, 1: pump on	Oil volume outside [4.9, 25.1]
RandomWalk-v0	position, time (2D continuous)	0: slow, 1: fast	Goal reached (x ≥ 1) or timeout (t ≥ 1)
Spiral-v0	agent position, destination position (4D continuous)	0: move outward, 1: move inward, 2: stay course	Rock collision or destination reached

PasswordGuessing-v0 is also registered but requires words and options arguments — instantiate it directly via PasswordEnv(words, options).

Environment details

BouncingBall-v0 — A ball bounces under gravity. The agent can hit the ball to add velocity. The episode ends when the ball loses enough energy to stop. The agent is penalised for hitting (-1) and heavily for termination (-1000).

CruiseControl-v0 — An ego vehicle follows a front vehicle with stochastic acceleration. The agent controls ego acceleration to maintain a safe following distance. Reward is -distance each step; collision gives -10000.

DCDCBoostConverter-v0 — A DC-DC boost converter must keep inductor current x1 ∈ [0, 4] A and capacitor voltage x2 ∈ [14.5, 15.5] V despite a randomly fluctuating load resistance. Reward is negative distance from target values (x1_ref=0.35, x2_ref=15).

OilPump-v0 — An oil pump refills a tank consumed at varying rates over a 20-second cycle. The pump has a 2-second switching latency. The agent must keep oil volume within [4.9, 25.1].

RandomWalk-v0 — A 2D random walk where the agent must reach x = 1 before t = 1. Fast moves cost more (-3) but advance position more; slow moves cost less (-1). Timeout incurs an extra penalty of -20.

Spiral-v0 — An agent moves on a spiral trajectory in 2D space and must reach a randomly generated destination while avoiding five fixed obstacles (rocks). Actions adjust the radius of the spiral.

Usage

import gymnasium as gym
import uppaal_gym  # registers all environments

env = gym.make("BouncingBall-v0")
obs, info = env.reset(seed=42)

for _ in range(200):
    action = env.action_space.sample()
    obs, reward, terminated, truncated, info = env.step(action)
    if terminated or truncated:
        obs, info = env.reset()

env.close()

All environments expose two additional methods beyond the standard Gymnasium API:

# Check which actions are safe in a given state
safe_actions = env.allowed_actions(obs)

# Compute a transition without updating internal state (useful for planning)
next_state, reward, terminated = env.step_from(obs, action)

UPPAAL Models

The original UPPAAL model files (.xml) for each environment are included in the models/ directory. UPPAAL is available at uppaal.org.

Deviations from the original models

The gym environments are faithful adaptations but include deliberate deviations where necessary for use as RL benchmarks.

BouncingBall-v0 — The initial position range is [8, 10) rather than the original [7, 10). States in [7, 8) cannot be guaranteed safe even under a perfect strategy, so they are excluded to ensure the task is feasible.

CruiseControl-v0 — Two differences: (1) the sensor range is doubled from 100 to 200 to give the agent more time to react when the front car reappears; (2) the minimum velocity of the front car is −8 instead of −10, matching the observation space used in experiments.

DCDCBoostConverter-v0 — Several differences: (1) x1 and x2 are initialised at their target values (0.35 A, 15 V) rather than 0, since starting at 0 immediately violates the safety constraints; (2) the load resistance R is initialised at 73 Ω and may vary over [30, 200] Ω with fluctuations of ±30 per step, compared to [60, 80] Ω and ±10 in the original — this substantially increases task difficulty; (3) the safety region is widened to x1 ∈ [0, 4], x2 ∈ [14.5, 15.5] from the tighter query targets x1 ∈ [0, 0.7], x2 ∈ [14.8, 15.2] used in the original model.

OilPump-v0 — The consumption schedule, fluctuation range, inflow rate, latency, and time step all match the original exactly. The only deviation is in the termination condition: in the original model, a safety violation resets the oil volume to 10 and increments a death counter so the run continues; in the gym, a violation terminates the episode.

RandomWalk-v0 — No significant deviations. The UPPAAL model has been updated to use the same step sizes (Δd: 0.17 fast, 0.10 slow; Δt: 0.05 fast, 0.12 slow) and noise magnitude (±0.04) as the gym implementation. Action indices also match: 0 = slow, 1 = fast.

Citation

If you use uppaal-gym in your research, please cite:

@software{hoeeg-petersen_uppaal_gym_2026,
  author    = {Høeg-Petersen, Andreas Holck},
  title     = {uppaal-gym: Gymnasium Environments for UPPAAL Hybrid-System Benchmarks},
  year      = {2026},
  url       = {https://github.com/andreashhpetersen/uppaal-gym},
  version   = {1.0.0},
}

A Zenodo DOI will be added here after the first tagged release. To register: go to zenodo.org, sign in with GitHub, enable the repository, then create a GitHub release tagged v1.0.0. Zenodo mints a DOI automatically and the BibTeX above will update with it.

License

MIT — see LICENSE.