Structural Abstraction and Selective Refinement for Formal Verification

Christoph Luckeneder; Hermann Kaindl; Ralph Hoch

REVIEW 3 major objections 4 minor 19 references

Structural Abstraction and Selective Refinement for Formal Verification

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that a model-checking workflow can find the same collision a direct high-resolution run would find, in minutes rather than days, by starting from coarse voxels and refining only those a counterexample points to.

desk verdict A sound and honest extension of CEGAR to structural voxel abstraction; the efficiency claim is promising but needs stronger empirical backing. read the letter →

arxiv 2505.22982 v1 pith:LAMDSGX6 submitted 2025-05-29 cs.RO cs.SE

Christoph Luckeneder , Ralph Hoch , Hermann Kaindl This is my paper

classification cs.ROcs.SE

keywords structuralabstractionselectiverefinementmodelcheckingvoxelgridcounterexample-guidedformalverificationrobotsafetyover-approximation

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper proposes a way to make formal safety verification of robot environments drastically faster. The environment is represented as voxels—same-sized cubes marking occupied space—and verification starts at a coarse resolution; whenever the model checker reports a collision, its counterexample is parsed automatically to find the one voxel responsible, and only that voxel is refined into eight finer voxels. The authors claim this loop finds the same real collision that a direct run at the finest resolution would find, in a few minutes where the direct run crashed after days. If correct, it makes model checking practical for realistic robot workspaces without a human having to guess which parts of the environment need detail.

What carries the argument

The load-bearing object is the abstract voxel. A coarse voxel is marked SOLID if and only if at least one of the maximum-resolution voxels inside it is SOLID, which ensures that any collision visible at the finest granularity remains visible at the coarser granularity. The load-bearing mechanism is the selective-refinement loop: each counterexample from the model checker is parsed to locate the violating voxel, that voxel is replaced by eight voxels at the next higher resolution using the finest grid as ground truth, and the mixed-resolution environment is fed back into the model checker. The voxel grid's indexing scheme lets the tool compute which finest voxels belong to any coarse voxel, so refinement is exact and automatic. This combination—over-approximating abstraction plus counterexample-driven local refinement—is what allows the workflow to reach a real counterexample quickly.

What would settle it

Place a thin obstacle, thinner than one voxel at the maximum resolution, exactly between voxel cells on the robot's path; if the workflow reports no collision while the robot physically intersects the obstacle, the over-approximation assumption fails.

Watch

Extended reading notes

Core claim

The central claim is that behavioral abstraction—the usual counterexample-guided route—is not needed to get counterexample-guided speedups in robot verification; structural abstraction of the environment alone suffices. The paper defines an abstract voxel as SOLID whenever any of the finer voxels it contains is SOLID, which makes the coarse environment model an over-approximation of the fine one for collision properties. The workflow then alternates model-checker runs with automatic counterexample analysis: the log is parsed to identify the specific voxel whose SOLID status violates the property at a given step, that voxel is split into $2\times2\times2$ children filled with data from the finest voxel grid, and the loop repeats. In the reported collision scenario with a maximum resolution of $128\times128\times128$, starting from base resolutions 2, 4, 8, or 16, the workflow terminates with a counterexample of length 80 in roughly 3 to 14 minutes, while a direct run at resolution 128 crashed after a couple of days.

Load-bearing premise

The whole safety guarantee rests on the input voxel grid being an over-approximation of the real environment: if a real obstacle is thinner than one voxel and falls between grid cells, a collision in the real world could slip through undetected.

Editorial extensions

If this is right

Verification can start from a deliberately coarse environment model and still converge to the same real counterexample as the finest model, because the abstraction is an over-approximation.
The workflow is fully automatic after the base and maximum resolutions are chosen; no human judgment about which regions matter is needed.
Coarser base resolutions produce the largest time savings in the tested collision scenario, at the price of more refinement iterations.
In near-miss and obviously-safe scenarios, the workflow still terminates in reasonable time, although the speed advantage shrinks when no real counterexample exists and many refinements are needed.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Beyond the paper: the same refinement scheme should carry over to octree or multi-level voxel representations, provided the relationship between coarse and fine cells is computable; the paper notes this generality but does not demonstrate it.
Beyond the paper: refining all voxels that overlap the robot at the violating time step, rather than one voxel per counterexample, would cut the number of model-checker runs, as the paper's own observation of up to six violating voxels at one position suggests.
Beyond the paper: the workflow's guarantee is only as strong as the pipeline that builds the finest voxel grid; integrating it with an over-approximating voxelization of point clouds or CAD models is a testable extension.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The paper does one real thing: it transplants CEGAR-style abstraction and refinement from behavioral models to structural environment models, specifically voxel grids, for robot safety verification. The over-approximation argument is simple and correct: joining voxels and marking the abstract voxel SOLID if any constituent is SOLID preserves all collisions. The workflow is fully automated and the paper honestly distinguishes spurious from real counterexamples. That is a genuine, if modest, contribution.

What is good: The formal soundness of the abstraction step holds up. The empirical results, while narrow, are suggestive. For the pick-and-place scenario, the workflow finds a collision at max resolution 128 in minutes, while a direct nuXmv run reportedly crashed after days. The paper also explores three scenarios (collision, near-miss, safe) and sweeps base-resolution. The authors are transparent about the one load-bearing assumption: the input voxel grid must itself over-approximate the real environment, otherwise no safety guarantee follows. They state this in the Discussion and note it applies to direct model checking as well. That is an honest limitation, not a hidden one.

Soft spots: The baseline crash is anecdotal; there are no memory numbers, no timeout threshold, no replication. All runtimes are single measurements without variance. The scenario is a single fixed trajectory, so the generality of the speedup is unmeasured. The base-resolution is set by educated guessing, though the sensitivity table helps. The refinement loop refines one voxel per counterexample, which the authors themselves note is inefficient in cases where multiple voxels at the same robot position cause the violation. These are all fixable in a revised version with more robust benchmarking.

Bottom line: This is a solid paper for the formal verification and robot safety community. It does not reshape the field, but it addresses a practical bottleneck. The central argument holds up; the weaknesses are in the empirical evidence, not the logic. I would send it to peer review and would cite it if I worked on voxel-based verification. Bring it to reading group if you want a clean example of a sound abstraction-refinement loop.

Recommendation: review it.

Referee Report

3 major / 4 minor

Summary. This paper proposes a verification workflow for robot collision-avoidance properties that uses structural abstraction of voxel-grid environment models. Starting from a user-provided high-resolution (Max) voxel grid, the workflow creates a coarse Base-resolution grid by marking each abstract voxel as SOLID if any of its constituent Max-resolution voxels is SOLID, then repeatedly runs the nuXmv model checker on the abstract environment, parses any counterexample to identify the offending voxel, refines that voxel to the next finer resolution, and repeats until the property holds or a Max-resolution voxel is the counterexample. The approach is evaluated on a pick-and-place scenario taken from Rathmair et al. [2], with three variants (collision, near-miss, obviously safe) and a sweep over Base- and Max-resolutions. The headline result is that a counterexample for Max-resolution 128 is found in a few minutes, whereas a direct model-checker run at that resolution reportedly crashed after a couple of days. The paper includes a discussion of limitations, including the fact that the input voxel grid must itself over-approximate the real environment for a real-world safety guarantee.

Significance. If the efficiency and soundness claims hold, the paper makes a practical contribution: it demonstrates that a simple, fully automated structural abstraction can make high-resolution voxel-based model checking feasible for a realistic robot scenario, with no change to the behavioral model. The over-approximation construction for the collision property is sound and is maintained under refinement, since each refined voxel is recomputed from the original Max-resolution voxels. The paper is honest about the property-dependence of the abstraction and about the residual risk at the input-voxelization stage. Strengths include the availability of an executable artefact, the transparent parameter sweep over Base-resolution, and the explicit separation of the structural-abstraction correctness from the environment-modeling assumption. The main caveats are that the runtime comparison rests on single runs and an anecdotal crash baseline, and that the workflow's correctness relative to the Max-resolution model is argued informally rather than stated as a theorem.

major comments (3)

[VI, last paragraph] The final paragraph of Section VI concedes that the workflow can only guarantee detection of collisions with the real environment if the input Max-resolution voxel grid over-approximates the real environment, but no procedure or test is provided to establish this. This is load-bearing for the paper's safety-verification framing: binvox's default voxelization is not in general an over-approximation (e.g., a thin obstacle can fall between voxel centers and produce no SOLID voxel), so a verified 'pass' of the workflow does not by itself certify the real environment. Please either extend the workflow with a conservative voxelization step (e.g., marking a voxel SOLID whenever the occupied region intersects the voxel, or prove that the chosen voxelizer does this), or explicitly restrict the claims in the abstract and conclusion to 'relative to the provided voxel grid' and remove the real-environment safety guarantee wording.
[IV, Tables I and II] The central efficiency claim is supported only by single runs: Table I gives one time per resolution for direct model checking, Table II gives one time per Base-resolution for the proposed workflow, and the 'crash after a couple of days' baseline for resolution 128 is anecdotal, with no specification of whether the crash was due to memory exhaustion, a timeout, or a tool failure. Since runtimes are the paper's main quantitative evidence, please report repeated runs with error bars or at least state explicitly that each data point is a single measurement, and document the crash conditions for the 128-resolution baseline. In addition, Table IV contains an unresolved 'xxx d' entry; this should be replaced by the actual measured value or explicitly marked as not measured.
[III-C] The workflow is described procedurally, but the paper does not state a correctness theorem linking the workflow's outcome to the property on the Max-resolution model. The over-approximation argument ensures that a pass in an abstract model implies a pass in the Max-resolution model, and a counterexample at a Max-resolution voxel is real in the Max-resolution model, but termination and completeness of the iterative refinement are only argued informally. Please add a short formal statement that (i) each refinement preserves over-approximation, (ii) the workflow terminates, and (iii) the final verdict is sound and complete with respect to the Max-resolution grid. This would strengthen the 'formal verification' claim.

minor comments (4)

[II-D] The text refers to 'Clark et al. [10]'; the correct spelling is 'Clarke et al.' as used in the reference list.
[III-B] The sentence 'the model-checker is more likely to encounter states where the atomic prepositions x of a property like φ=AG(x) becomes false' should read 'atomic propositions'.
[V] In the Related Work section, 'enterely' should be 'entirely' and 'course voxels' should be 'coarse voxels'.
[IV] The repeated odd spacing in terms such as 'V oxel-resolution' may be a LaTeX artifact from the PDF extraction, but please check that the typeset manuscript renders these terms as 'Voxel-resolution' consistently.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the workflow's results are produced by model-checker runs with base-resolution swept as an independent variable; self-citations are background and the Section VI over-approximation caveat is a soundness limitation, not a circular step.

full rationale

The paper does not derive any predicted quantity from a fitted parameter or from a self-citation chain. Its central abstraction rule (Section III-B) is a constructive definition: an abstract voxel is SOLID if any composed voxel is SOLID, and the paper argues this preserves over-approximation for the collision property; this is a standard abstraction construction rather than a conclusion smuggled from its own premise. Runtime results (Tables II-V) come from the authors' own implementation invoking nuXmv, with Base-resolution swept as an independent variable rather than tuned to force the reported speedups. The citations to [1] and [2] supply the running example and the no-selective-refinement baseline, but the claimed efficiency advantage is measured against a direct nuXmv run that crashed, not against a number imported from those references. Section VI explicitly concedes the load-bearing caveat: 'since the voxel grid provided to the workflow is already an abstraction of the real environment, it would have to be made sure that it is generated in such a way that this abstraction is an "over-approximation" of the real environment. Unless this is ensured, however, the workflow cannot guarantee that a collision in the real environment is detected.' This is a genuine soundness limitation about the input voxelization, but it is not a circular derivation: the workflow's claims are relative to the Max-resolution grid, and the paper does not disguise that limitation as a result. No equation or fitted value in the paper reduces by construction to another quantity being predicted.

Assumptions & free parameters 1 free parameters · 3 assumptions · 0 invented entities

The central claim rests on the over-approximation property of the voxel abstraction, the assumption that the input max-resolution grid over-approximates the physical environment, and the correctness of the nuXmv model checker. The Base-resolution is a user-chosen parameter swept in the experiments, not fitted.

free parameters (1)

Base-resolution = varied as 2, 4, 8, 16, 32, 64
A user-chosen parameter that sets the coarsest voxel resolution at the start of the workflow. It directly affects the number of refinements and total runtime, and is swept in Tables II-V rather than fitted to data.

assumptions (3)

domain assumption An abstract voxel is SOLID if at least one of its constituent voxels at Max-resolution is SOLID.
This guarantees over-approximation for collision detection, as argued in Section III-B. The property checked is AG(visited voxels are not SOLID), so marking more voxels SOLID can only add spurious counterexamples, never hide real ones.
domain assumption The input Max-resolution voxel grid over-approximates the real physical environment.
Acknowledged in Section VI: 'since the voxel grid provided to the workflow is already an abstraction of the real environment, it would have to be made sure that it is generated in such a way that this abstraction is an "over-approximation" of the real environment.' The workflow cannot detect collisions that are absent from the input grid.
domain assumption nuXmv correctly implements the semantics of the ACTL* properties and counterexample generation assumed by the workflow.
The entire refinement loop depends on the model checker's output being a genuine counterexample of the abstract model. This is a standard tool assumption, not verified in the paper.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Structural Abstraction and Selective Refinement for Formal Verification." pith.science (2026). https://pith.science/paper/LAMDSGX6

@misc{pith2026250522982,
  author       = {Pith},
  title        = {Pith review of: Structural Abstraction and Selective Refinement for Formal Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/LAMDSGX6}},
  note         = {Machine review of arXiv:2505.22982}
}

read the original abstract

Safety verification of robot applications is extremely challenging due to the complexity of the environment that a robot typically operates in. Formal verification with model-checking provides guarantees but it may often take too long or even fail for complex models of the environment. A usual solution approach is abstraction, more precisely behavioral abstraction. Our new approach introduces structural abstraction instead, which we investigated in the context of voxel representation of the robot environment. This kind of abstraction leads to abstract voxels. We also propose a complete and automated verification workflow, which is based on an already existing methodology for robot applications, and inspired by the key ideas behind counterexample-guided abstraction refinement (CEGAR) - performing an initial abstraction and successively introducing refinements based on counterexamples, intertwined with model-checker runs. Hence, our approach uses selective refinement of structural abstractions to improve the runtime efficiency of model-checking. A fully-automated implementation of our approach showed its feasibility, since counterexamples have been found for a realistic scenario with a fairly high (maximal) resolution in a few minutes, while direct model-checker runs led to a crash after a couple of days.

Figures

Figures reproduced from arXiv: 2505.22982 by the authors.

**Figure 2.** Voxel representation of a sphere in different resolutions – left: sphere [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗

**Figure 3.** Voxel representation of environment model of the running example — [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗

Figures from the paper (3 more)

**Figure 4.** Figure 4: Environment representation with more details added by selective [PITH_FULL_IMAGE:figures/full_fig_p004_4.png]

**Figure 5.** Figure 5: Verification workflow with selective refinement of structural abstrac [PITH_FULL_IMAGE:figures/full_fig_p005_5.png]

**Figure 6.** Figure 6: Evolution of the voxel grid with Base-resolution [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

19 extracted references · 19 canonical work pages

[2]

Formal Verification of Safety Properties of Collaborative Robotic Applications including Variability,

M. Rathmair, C. Luckeneder, T. Haspl, B. Reiterer, R. Hoch, M. Hofbaur, and H. Kaindl, “Formal Verification of Safety Properties of Collaborative Robotic Applications including Variability,” in2021 30th IEEE Interna- tional Conference on Robot & Human Interactive Communication (RO- MAN). Vancouver, BC, Canada: IEEE, Aug. 2021, pp. 1283–1288

work page 2021
[1]

Approaches to cyber-physical (model) model- checking,

C. Luckeneder, “Approaches to cyber-physical (model) model- checking,” Doctoral Dissertation, TU Wien, Dec. 2023

work page 2023
[3]

P. Min. (2023) Binvox 3D mesh voxelizer, keywords: V oxelization, voxelisation, 3D model. https://www.patrickmin.com/binvox/. [Online]. Available: https://www.patrickmin.com/binvox/

work page 2023
[4]

(2023) nuXmv: The nuXmv model checker

Fondazione Bruno Kessler. (2023) nuXmv: The nuXmv model checker. https://nuxmv.fbk.eu/. [Online]. Available: https://nuxmv.fbk.eu/

work page 2023
[5]

The nuXmv symbolic model checker,

R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuXmv symbolic model checker,” inComputer Aided Verification, A. Biere and R. Bloem, Eds. Cham: Springer International Publishing, 2014, pp. 334–342

work page 2014
[6]

B. O. Community,Blender - a 3D modelling and rendering package, Blender Foundation, Stichting Blender Foundation, Amsterdam, 2023. [Online]. Available: http://www.blender.org

work page 2023
[7]

P. Min. (2023) Viewvox 3D voxel model viewer. https://www.patrickmin.com/viewvox/. [Online]. Available: https: //www.patrickmin.com/viewvox/

work page 2023
[8]

Model checking and ab- straction,

E. M. Clarke, O. Grumberg, and D. E. Long, “Model checking and ab- straction,”ACM Transactions on Programming Languages and Systems, vol. 16, no. 5, pp. 1512–1542, Sep. 1994

work page 1994

Show all 19 references

[9]

Counterexample- Guided Abstraction Refinement,

E. Clarke, O. Grumberg, S. Jha, Y . Lu, and H. Veith, “Counterexample- Guided Abstraction Refinement,” inComputer Aided Verification, G. Goos, J. Hartmanis, J. van Leeuwen, E. A. Emerson, and A. P. Sistla, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2000, vol. 1855, p...

2000
[10]

Counterexample-guided abstraction refinement for symbolic model checking,

——, “Counterexample-guided abstraction refinement for symbolic model checking,”Journal of the ACM (JACM), vol. 50, no. 5, pp. 752– 794, 2003

2003
[11]

Verification of hybrid systems based on counterexample-guided abstrac- tion refinement,

E. Clarke, A. Fehnker, Z. Han, B. Krogh, O. Stursberg, and M. Theobald, “Verification of hybrid systems based on counterexample-guided abstrac- tion refinement,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2003, pp...

2003
[12]

Abstraction and counterexample-guided refinement in model checking of hybrid systems,

E. Clarke, A. Fehnker, Z. Han, B. Krogh, J. Ouaknine, O. Stursberg, and M. Theobald, “Abstraction and counterexample-guided refinement in model checking of hybrid systems,”International Journal of Foundations of Computer Science, vol. 14, no. 04, pp. 583–604, 2003. [Online]. A...

2003 doi
[13]

The morgan kaufmann series,

C. Ericson, “The morgan kaufmann series,” inReal-Time Collision Detection, 2005, pp. i–i

2005
[14]

GPU-accelerated generation and ren- dering of multi-level voxel representations of solid models,

G. Young and A. Krishnamurthy, “GPU-accelerated generation and ren- dering of multi-level voxel representations of solid models,”Computers & Graphics, vol. 75, pp. 11–24, Oct. 2018

2018
[15]

Direct 3D printing of multi-level voxel models,

S. Ghadai, A. Jignasu, and A. Krishnamurthy, “Direct 3D printing of multi-level voxel models,”Additive Manufacturing, vol. 40, p. 101929, Apr. 2021

2021
[16]

Structural Abstraction of Software Verification Conditions,

D. Babi ´c and A. J. Hu, “Structural Abstraction of Software Verification Conditions,” inComputer Aided Verification, W. Damm and H. Her- manns, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2007, vol. 4590, pp. 366–378

2007
[17]

Two methods for exploiting abstraction in systems,

P. A. Fishwick and K. Lee, “Two methods for exploiting abstraction in systems,”AI, Simulation and Planning in High Autonomous Systems, pp. 257–264, 1996

1996
[18]

Unsupervised learning for cuboid shape abstrac- tion via joint segmentation from point clouds,

K. Yang and X. Chen, “Unsupervised learning for cuboid shape abstrac- tion via joint segmentation from point clouds,”ACM Transactions on Graphics, vol. 40, no. 4, pp. 1–11, Aug. 2021

2021
[19]

Lazy abstraction,

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, “Lazy abstraction,” inConference Record of POPL 2002: The 29th SIGPLAN- SIGACT Symposium on Principles of Programming Languages, Portland, OR, USA, January 16-18, 2002, J. Launchbury and J. C. Mitchell, Eds. ACM, 2002, pp. ...

2002

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.

[1] [2]

Formal Verification of Safety Properties of Collaborative Robotic Applications including Variability,

M. Rathmair, C. Luckeneder, T. Haspl, B. Reiterer, R. Hoch, M. Hofbaur, and H. Kaindl, “Formal Verification of Safety Properties of Collaborative Robotic Applications including Variability,” in2021 30th IEEE Interna- tional Conference on Robot & Human Interactive Communication (RO- MAN). Vancouver, BC, Canada: IEEE, Aug. 2021, pp. 1283–1288

work page 2021

[2] [1]

Approaches to cyber-physical (model) model- checking,

C. Luckeneder, “Approaches to cyber-physical (model) model- checking,” Doctoral Dissertation, TU Wien, Dec. 2023

work page 2023

[3] [3]

P. Min. (2023) Binvox 3D mesh voxelizer, keywords: V oxelization, voxelisation, 3D model. https://www.patrickmin.com/binvox/. [Online]. Available: https://www.patrickmin.com/binvox/

work page 2023

[4] [4]

(2023) nuXmv: The nuXmv model checker

Fondazione Bruno Kessler. (2023) nuXmv: The nuXmv model checker. https://nuxmv.fbk.eu/. [Online]. Available: https://nuxmv.fbk.eu/

work page 2023

[5] [5]

The nuXmv symbolic model checker,

R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuXmv symbolic model checker,” inComputer Aided Verification, A. Biere and R. Bloem, Eds. Cham: Springer International Publishing, 2014, pp. 334–342

work page 2014

[6] [6]

B. O. Community,Blender - a 3D modelling and rendering package, Blender Foundation, Stichting Blender Foundation, Amsterdam, 2023. [Online]. Available: http://www.blender.org

work page 2023

[7] [7]

P. Min. (2023) Viewvox 3D voxel model viewer. https://www.patrickmin.com/viewvox/. [Online]. Available: https: //www.patrickmin.com/viewvox/

work page 2023

[8] [8]

Model checking and ab- straction,

E. M. Clarke, O. Grumberg, and D. E. Long, “Model checking and ab- straction,”ACM Transactions on Programming Languages and Systems, vol. 16, no. 5, pp. 1512–1542, Sep. 1994

work page 1994