Structural Abstraction and Selective Refinement for Formal Verification

• URL: http://arxiv.org/abs/2505.22982v1
• Date: Thu, 29 May 2025 01:44:47 GMT
• Title: Structural Abstraction and Selective Refinement for Formal Verification
• Authors: Christoph Luckeneder, Ralph Hoch, Hermann Kaindl,
• Abstract summary: Safety verification of robot applications is extremely challenging due to the complexity of the environment that a robot typically operates in.<n>A usual solution approach is abstraction, more precisely behavioral abstraction.<n>We propose structural abstraction instead, which we investigated in the context of voxel representation of the robot environment.
• Score: 0.5735035463793008
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
  Auto is a fully automated method that integrates a closed-loop self-validation process within a dual-system framework.<n>The effectiveness of Auto was validated across 8 distinct scenarios, where it demonstrated a significant 10.1% improvement over SOTA methods.
  arXiv  Detail & Related papers  (2025-07-06T08:35:22Z)
• Unlocking Smarter Device Control: Foresighted Planning with a World Model-Driven Code Execution Approach [83.21177515180564]
  We propose a framework that prioritizes natural language understanding and structured reasoning to enhance the agent's global understanding of the environment.<n>Our method outperforms previous approaches, particularly achieving a 44.4% relative improvement in task success rate.
  arXiv  Detail & Related papers  (2025-05-22T09:08:47Z)
• Contract Based Program Models for Software Model Checking [0.0]
  We propose a formalism previously developed for the purposes of compositional model checking.<n>We describe how we envisage the work flow and tool chain to support the proposed verification approach in the context of embedded, safety-critical software written inC.
  arXiv  Detail & Related papers  (2025-03-14T09:34:59Z)
• Model Checking for Closed-Loop Robot Reactive Planning [0.0]
  We show how model checking can be used to create multistep plans for a differential drive wheeled robot so that it can avoid immediate danger. Using a small, purpose built model checking algorithm in situ we generate plans in real-time in a way that reflects the egocentric reactive response of simple biological agents.
  arXiv  Detail & Related papers  (2023-11-16T11:02:29Z)
• On the Trade-off Between Efficiency and Precision of Neural Abstraction [62.046646433536104]
  Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics.
  arXiv  Detail & Related papers  (2023-07-28T13:22:32Z)
• Learning minimal representations of stochastic processes with variational autoencoders [52.99137594502433]
  We introduce an unsupervised machine learning approach to determine the minimal set of parameters required to describe a process. Our approach enables for the autonomous discovery of unknown parameters describing processes.
  arXiv  Detail & Related papers  (2023-07-21T14:25:06Z)
• Neural Abstractions [72.42530499990028]
  We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models.
  arXiv  Detail & Related papers  (2023-01-27T12:38:09Z)
• Learning Dynamic Abstract Representations for Sample-Efficient Reinforcement Learning [22.25237742815589]
  In many real-world problems, the learning agent needs to learn a problem's abstractions and solution simultaneously. This paper presents a novel top-down approach for constructing state abstractions while carrying out reinforcement learning.
  arXiv  Detail & Related papers  (2022-10-04T23:05:43Z)
• Toward Certified Robustness Against Real-World Distribution Shifts [65.66374339500025]
  We train a generative model to learn perturbations from data and define specifications with respect to the output of the learned model. A unique challenge arising from this setting is that existing verifiers cannot tightly approximate sigmoid activations. We propose a general meta-algorithm for handling sigmoid activations which leverages classical notions of counter-example-guided abstraction refinement.
  arXiv  Detail & Related papers  (2022-06-08T04:09:13Z)
• Automated Repair of Process Models with Non-Local Constraints Using State-Based Region Theory [0.19499120576896226]
  State-of-the-art process discovery methods construct free-choice process models from event logs. We propose a novel approach for enhancing free-choice process models by adding non-free-choice constructs discovered a-posteriori via region-based techniques.
  arXiv  Detail & Related papers  (2021-06-26T21:14:04Z)
• Model-Invariant State Abstractions for Model-Based Reinforcement Learning [54.616645151708994]
  We introduce a new type of state abstraction called textitmodel-invariance. This allows for generalization to novel combinations of unseen values of state variables. We prove that an optimal policy can be learned over this model-invariance state abstraction.
  arXiv  Detail & Related papers  (2021-02-19T10:37:54Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.