Verena: Solving Partially Observable Safety Games

Verena is written in Python and uses Z3 for symbolic reasoning and SimSat for strategy extraction. We provide a Docker image, or you can install natively on Ubuntu 24.04.

The full evaluation requires Z3 and SimSat, both provided by the Docker image and native install script.

Platforms

Verena was built and tested on Linux x86_64 (Intel Xeon E5-2640 v3, 64 GB RAM). Native installation is supported on Ubuntu 24.04.

Each benchmark case needs up to 64 GiB of memory. The full Table 3 evaluation runs 45 cases across 6 methods, so a machine with at least 64 GB RAM is recommended. Kick-the-tires and Table 1 need only 8 GB. No network access (after setup), GPU, or multi-machine setup is required.

Documentation

Below, we provide an overview of the Verena project's directory structure:

• solver/ implements the synthesis pipeline.
  • synthesizer.py is the top-level entry point orchestrating all pipeline stages.
  • forward_planner.py implements forward planning for candidate strategies.
  • template_miner.py and automatic_templates.py mine and manage templates for invariant candidates.
  • fixpoints.py implements the fixpoint computation for winning regions.
  • beliefs.py and belief_map.py track and manipulate belief states.
  • memory.py and observations.py handle memory abstractions and observation models.
  • policy.py defines strategy representations.
  • options.py contains solver configuration options.
• examples/ contains benchmark games grouped by paper family.
  • game.py defines the Game interface that all benchmarks implement.
  • uav/ contains 1D and 2D UAV altitude-tracking games.
  • robot/ contains robot navigation games with sensor and delay variations.
  • cca/ contains congestion control games (RTT-based and timestep-based).
  • lander/ contains Mars powered-lander games.
  • finite_action/ contains bakery, parts, and robot games with finite action spaces.
• artifact/ contains the evaluation harness.
  • install_dependencies.sh installs native dependencies and builds the strategy backend.
  • reproduce_table1.py, reproduce_figure3.py, reproduce_table3.py are the experiment entry points.
  • run_suite.py runs a benchmark suite from a JSON manifest.
  • plot_results.py generates comparison tables and figures.
  • benchmarks/ contains JSON configurations and expected outcomes for each family.

Usage

--help is available on every runner. Below is an example running one benchmark with the native installation:

$ artifact/.venv/bin/python artifact/reproduce_table1.py \
    --family uav --case UAV-1D --output results/smoke

The strategy is saved to results/smoke/uav/original/UAV-1D/strategy.sexpr. To define a new game, see Reusing Verena on a New Game.

Getting Started with Docker

Prerequisites:

• Docker with at least 64 GiB memory and 20 GiB free disk.
• Building the image requires internet access; no GitHub credentials are needed.

To begin, build the image and create an output directory:

$ docker build -t verena-ae .
$ mkdir -p results

The image contains the repository at /opt/verena and all solver dependencies. Create a named container from the image:

$ docker run -it --name verena -v "$PWD/results:/opt/verena/results" verena-ae bash

Inside the container, run all commands from /opt/verena directly (no separate installation needed). Results written to results/ are visible on the host. If you exit, docker start -ai verena returns to the same container; a new docker run starts clean.

You can move forward to the section Step-by-Step Evaluation Instructions.

Getting Started with Native Ubuntu 24.04

Clone the repository, then run from its root:

$ bash artifact/install_dependencies.sh --system-deps
$ mkdir -p results

This installs the Python environment at artifact/.venv/ and builds the strategy backend.

You can move forward to the section Step-by-Step Evaluation Instructions.

Step-by-Step Evaluation Instructions

0. Enter the environment as described above.

1. Verify the environment

$ bash artifact/install_dependencies.sh --check

Expect Dependencies and all three experiment entry points are ready.

2. Kick the tires

Run a single fast benchmark to confirm the full pipeline works:

$ artifact/.venv/bin/python artifact/reproduce_table1.py \
    --family uav --case UAV-1D --output results/kick

This normally takes a few seconds. Check results/kick/uav/original-runner.log for UAV-1D: solved and results/kick/uav/original/results.json for outcome: "realizable" and strategy_extracted: true. The case directory contains strategy.sexpr and run.log.

3. Run the full evaluation

The full evaluation could take several hours to complete. The details for each experiment are presented in the following table:

Experiment	Scope	Est. Serial Runtime	Output directory
Table 1 / RQ1	30 cases: UAV, Robot, CCA, Lander	33 min	results/table1/
Figure 3 / RQ2	15 cases: Bakery, Parts, finite-action Robot	26 min	results/figure3/
Table 3 / RQ3	45 cases x 6 methods	Several hours	results/table3/

Serial runtimes are from an Intel Xeon E5-2640 v3 with a 300-second per-case limit, including timeouts.

Run the experiments:

$ artifact/.venv/bin/python artifact/reproduce_table1.py --output results/table1
$ artifact/.venv/bin/python artifact/reproduce_figure3.py --output results/figure3
$ artifact/.venv/bin/python artifact/reproduce_table3.py --output results/table3

For a subset, append --family NAME or --case NAME; Table 1 and Table 3 require one selected family when selecting cases. Table 3 also accepts --method NAME (see Ablations).

Parallelism and resource limits

Defaults are one job, 300 seconds and 64 GiB per case. The time limit includes strategy extraction. Figure 3 and the Table 3 ablations accept --jobs N; memory limits apply per worker. Table 1 has no --jobs option, and Table 3's original column always runs sequentially regardless of --jobs. Use one job for timing comparisons. Append --timeout SECONDS or --memory-gib GIB to override.

The three experiments are independent and can run concurrently in separate terminal sessions. On a 28-core machine this brings the full evaluation down to roughly 1.5 hours.

4. Evaluate the claims presented in the paper

Each experiment writes results.json, results.csv, and summary.json, with per-case logs and strategies underneath its output directory. Plot the completed results without rerunning synthesis:

$ artifact/.venv/bin/python artifact/plot_results.py \
    --table1 results/table1 --figure3 results/figure3 --table3 results/table3 \
    --style paper --output results/plots

Paper item	What to compare	Generated report
Table 1	Solved counts, realizable/unrealizable split, mean/median/max solving time by family	table1.pdf, table1-comparison.csv
Figure 3	Verena and SPIAR runtime scaling as the action count increases within each family	figure3.pdf, figure3-comparison.csv, figure3-points.csv
Table 3	Solved counts for the full algorithm and each ablation	table3.pdf, table3-comparison.csv

SPIAR is private, so we provide artifact/spiar-figure3.csv with results measured on translated Verena games using the same machine and experiment configuration described above. Figure 3 uses this CSV automatically.

Note that the final results may vary depending on hardware and solver nondeterminism. Counts should match; compare timings only roughly.

Result statuses. A realizable case is solved only after strategy extraction succeeds; an unrealizable case has no winning strategy. The possible statuses are:

• solved: synthesis completed and the outcome matches the expected label (if one is set).
• timeout: the time budget expired before synthesis finished.
• inconclusive: the configured search ended without proving either realizability or unrealizability. This does not establish unrealizability.
• mismatch: synthesis completed, but the outcome disagrees with the manifest's expected label. For example, a suffix-memory ablation may report unrealizable for a case labeled realizable, because the restricted memory abstraction is too coarse to find a winning strategy. The runner counts a mismatch as unsolved.

RQ4: Learned Memory Templates (Sec. 7.4)

RQ4 examines the memory templates that Verena's template miner learns for the CCA benchmarks. No separate runner is needed: the Table 1 run already produces the relevant output. After running table1, inspect the per-case run.log files under results/table1/cca/original/. Each log prints the mined templates at each generalization level, with lines like Level 0 templates: and Level 1 templates: followed by the Z3 formulas. The templates for RTT-no_buffer-converge and RTT-no_buffer-jitter-converge correspond to the interval and pending-probe structures discussed in Section 7.4.

Ablations

Table 3 accepts the following method names via --method:

Paper method	--method	Configuration
Verena Original	original	Full synthesis pipeline
Trivial Support	trivial-support	Backward safety computation with trivial support
Support AsWin	support-as-win	Use the mined support directly as the candidate winning region
Suffix Mem(1), Mem(2), Mem(3)	suffix-1, suffix-2, suffix-3	Keep an observation suffix of the corresponding length

For example, run Support AsWin on the UAV family:

$ artifact/.venv/bin/python artifact/reproduce_table3.py \
    --family uav --method support-as-win --output results/uav-support-as-win

Reusing Verena on a New Game

1. Define the game

Create a game file (e.g. examples/uav/my_uav.py) using the Game interface. Declare the actions, observable variables, and latent (hidden) variables, then provide Z3 formulas for initial states, safety, allowed actions, and transitions:

from z3 import And, BoolVal
from examples.game import Game


class MyUAV(Game):
    def __init__(self):
        super().__init__()
        self.actions = {"cmd": "Real"}
        self.observable_states = {"obs": "Real"}
        self.latent_states = {"alt": "Real"}
        self.states = {**self.observable_states, **self.latent_states}

    def initial(self, s):
        return s["alt"] == 500

    def safety(self, s):
        return And(s["alt"] >= 450, s["alt"] <= 550)

    def enable_action(self, a):
        return BoolVal(True)

    def transition_env(self, s, s_p, a):
        return And(
            s["alt"] + a["cmd"] - 25 <= s_p["alt"],
            s_p["alt"] <= s["alt"] + a["cmd"] + 25,
            s_p["alt"] - 25 <= s_p["obs"],
            s_p["obs"] <= s_p["alt"] + 25,
        )

Here, alt is the hidden altitude and obs is its noisy observation. The UAV starts at altitude 500 and must stay within [450, 550], despite wind and sensor errors of up to 25. The arguments s, s_p, and a map variable names to Z3 expressions for the current state, next state, and action.

2. Configure the experiment

Save a JSON manifest (e.g. artifact/benchmarks/my_uav.json):

{
  "family": "Custom UAV",
  "paper": {},
  "instances": [
    {
      "name": "my_uav",
      "module": "examples.uav.my_uav",
      "class": "MyUAV",
      "args": [0, true, 5, 1, false],
      "strategy_backend": "skeleton-qe"
    }
  ]
}

• module and class identify the game; optional kwargs supplies constructor arguments.
• args sets the starting planning depth, numeric compatibility flag, generalization threshold, bad-template threshold, and safety-template mining flag.
• strategy_backend: "skeleton-qe" extracts and checks a strategy using quantifier elimination.
• Optional synthesis_options: {"export_winning_region": true} also saves the winning region and checked initial memory values.

3. Run and find the strategy

$ artifact/.venv/bin/python artifact/run_suite.py \
    --manifest artifact/benchmarks/my_uav.json \
    --case my_uav --timeout 300 --memory-gib 64 \
    --output results/my-uav-run

Check results/my-uav-run/results.json for status: "solved", outcome: "realizable", and strategy_extracted: true. The case directory contains:

• strategy.sexpr: symbolic action and memory-update functions.
• strategy-verification.json: strategy verification results.
• initial-memory.json: checked initial memory (when export_winning_region is enabled).
• run.log: synthesis progress and diagnostics.