Artefact for "What a LiDAR-Inertial Filter's Covariance Is Worth to a Verified Planner: Measured versus Reported Localisation Uncertainty in an Exact Navigation Guarantee"

Abstract

Simulator configuration, Point-LIO patch and commit, the 33 recorded runs' error files and logs, the PRISM models and every table's CSV for the paper "What a LiDAR-Inertial Filter's Covariance Is Worth to a Verified Planner: Measured versus Reported Localisation Uncertainty in an Exact Navigation Guarantee" (S. Phetmanee, Thammasat University, 2026; under submission to iFS 2027). The paper measures what a LiDAR-inertial odometry filter's reported covariance is worth to a verified planner. In simulation (MuJoCo, a Unitree Go2 carrying a simulated Unitree L2) Point-LIO is run through three scene classes (cluttered room, featureless corridor, open field) at two speeds with five seeds, scored against exact ground truth (ATE, RPE/m, absolute and windowed NEES), and both the measured error and the filter's own covariance are carried into an exact PRISM-checked legged-navigation MDP and into an automatic emergency braking model. Every number in the paper descends from a CSV or JSON in this package; nothing is typed by hand. Sensor parameters are declared assumptions, recorded in each run's _meta.json. Contents (the package mirrors the repository layout so every script runs unchanged). papers/lio-measured-guarantee/exp1/: pre-registered plan and adversarial review; data/ with the 33 runs (per-message error, reported sigma, NEES, covariance block; eval and meta JSON; grid log); summarise.py -> summary.csv, tests.csv (Table 1, Mann-Whitney tests); bridge.py -> sigma_table.csv, guarantee_shift.csv, invariants.csv, the 65 generated PRISM MDPs and their PRISM 4.10.1 logs (Tables 2-3, Fig. 3); figures.py; results.md. papers/lio-measured-guarantee/exp2/: bridge_aeb.py, the 37 AEB models and logs, aeb_shift.csv, invariants.csv (I1-AEB: k = 0 reproduces the oracle to 1e-9). papers/verified-legged-nav/exp1/, missions/M006-EDGECHECKER/ and papers/edge-model-checker/oracle/: the S1 and AEB generators, properties and oracle values reused unchanged. experiments/go2-sim-steve/: scenes (MuJoCo XML), simulated L2 + IMU, recorder, evaluator, Point-LIO config/launch/replay scripts, the covariance-export patch script, point_lio_commit.txt (unitreerobotics/point_lio_unilidar @ 18ed5976), point_lio.patch (the full working tree diff), the sim_l2 vs unilidar_l2 config diff, compute host bootstrap and grid driver. README.md with reproduction commands, LICENSE (MIT code, CC BY 4.0 data, GPL-2.0 for the Point-LIO-derived files), CITATION.cff, SHA256SUMS. Findings the package supports: the filter is overconfident in every scene and run (windowed NEES 6-30 against 3; error/sigma > 1 in 30 of 30 runs); the measured uncertainty is 1.6-4.7 times the reported one and moves the exact guarantee further, with the same sign, in all 60 instantiations; the pre-registered scene order of drift per metre is refuted; the AEB guarantee does not move at the measured error (below the 1 m cell size). Not included: the rosbags (never left the compute host), the Point-LIO sources (clone the recorded commit and apply the patch), the go2 walker package and the MuJoCo Menagerie Go2 model, and the house figure-style module. Requirements for the downstream steps: Python 3 with numpy, scipy, pyyaml; PRISM 4.10.1 (path in config.yaml). Recording additionally needs MuJoCo 3, rosbags, ROS 1 Noetic and the items above.