# Abstraction and Learning for Infinite-State Compositional Verification

arXiv: https://arxiv.org/abs/1309.5140 · HTML: https://mlsanity.com/paper/1309.5140/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Sep 2013.

## Built on by (most cited first, 1 of 1)

- [Assumption Generation for the Verification of Learning-Enabled Autonomous Systems](https://mlsanity.com/paper/2305.18372/) (2023)

## Abstract (arXiv)

Despite many advances that enable the application of model checking techniques to the verification of large systems, the state-explosion problem remains the main challenge for scalability. Compositional verification addresses this challenge by decomposing the verification of a large system into the verification of its components. Recent techniques use learning-based approaches to automate compositional verification based on the assume-guarantee style reasoning. However, these techniques are only applicable to finite-state systems. In this work, we propose a new framework that interleaves abstraction and learning to perform automated compositional verification of infinite-state systems. We also discuss the role of learning and abstraction in the related context of interface generation for infinite-state components.