Structural Abstraction and Selective Refinement for Formal Verification

TL;DR

The paper addresses the challenge of safety verification for robot applications in complex environments by introducing structural abstraction via voxel grids. It presents a fully automated, CEGAR-inspired workflow that performs initial coarse abstractions and iteratively refines selectively based on counterexamples. The authors demonstrate that this selective refinement yields significant computational efficiency, finding counterexamples in minutes at high resolutions where direct model checking can take days or crash. The approach integrates with existing robot verification methodologies and provides a principled framework for guaranteeing over-approximation while preserving correctness.

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 (6)

• Figure 1: Environment model of the running example including gripper position (gray sphere) and trajectories (black lines)
• Figure 2: Voxel representation of a sphere in different resolutions -- left: sphere modeled in Blender online:Blender; middle: resolution $32 \times 32 \times 32$; right: resolution $8 \times 8 \times 8$
• Figure 3: Voxel representation of environment model of the running example --- left: modeled in Blender; middle: resolution $128 \times 128 \times 128$; right: resolution $32 \times 32 \times 32$
• Figure 4: Environment representation with more details added by selective refinement
• Figure 5: Verification workflow with selective refinement of structural abstractions