Grid-World

A large grid-world navigation benchmark: a robot routes to a goal across a 49 × 478 obstacle map. This is BehaVerify’s standard scalability demonstrator — the same shape used in the Serbinowska–Johnson fast-forwarding paper to show the tool verifying thousands of behavior-tree nodes.

Location

examples/grid_world_big/

Files included:

  • grid_world_big.tree — the behavior-tree model.

  • template_fake_network_SCALE.tree — scalable template used to generate bigger / smaller variants of the same problem.

  • mapFilled_49_478_6.png + obstaclesFilled_49_478_6.txt — the obstacle map rendered as an image and as a text file.

  • command.sh / run_smv.sh / time_command.sh — canonical invocation scripts (including the time-it variant used in the reproducibility experiments).

Features exercised

  • Large integer-ranged blackboard. pos_x and pos_y take hundreds of distinct values each; the fast-forwarding encoding keeps the state space linear in map size rather than quadratic in tree size.

  • Obstacle avoidance logic expressed as a selector with per-direction guard checks.

  • Sub-tree inlining. The navigate-to-goal sub-tree is inserted at multiple sites (each direction), showing the insert { name } pattern.

  • Invariant + CTL specifications asserting obstacle-freedom and eventual goal-reachability.

Canonical invocation

Formal verification (requires nuXmv on PATH):

python -m behaverify nuxmv \
    examples/grid_world_big/grid_world_big.tree \
    ../grid_out/ \
    --generate --invar --ctl --nuxmv_path ../nuXmv \
    --recursion_limit 5000

Or run the bundled script, which sets the right paths and invokes nuXmv directly:

cd examples/grid_world_big
bash run_smv.sh

Python simulation:

python -m behaverify python \
    examples/grid_world_big/grid_world_big.tree \
    ../grid_out_py/ --max_iter 1000

What to look for

  • INVARSPEC asserting that (pos_x, pos_y) is always obstacle-free. The verifier reports true.

  • CTLSPEC asserting that the goal cell is always eventually reachable (AG (EF at_goal)). The verifier reports true for maps whose obstacle configuration leaves a connected path; flipping an obstacle to block the only route produces a counter-example that can be rendered with Generation Modes (trace mode).

Scaling

template_fake_network_SCALE.tree lets you instantiate a smaller or larger variant of the same tree by substituting the grid dimension parameters. The FM 2026 scalability chart in REPRODUCIBILITY/2026_FM/ was generated by varying this template across 31, 127, 511, and 2055 leaf nodes.

References

  • Serbinowska, Johnson. BehaVerify: Verifying Temporal Logic Specifications for Behavior Trees. SEFM 2022, LNCS 13550. https://doi.org/10.1007/978-3-031-17108-6_19

  • Reproducibility bundle: third_party/behaverify/REPRODUCIBILITY/2026_FM/.