Infinite State Model Checking by Learning Transitive Relations
Florian Frohn, Jürgen Giesl
TL;DR
The paper tackles safety verification for infinite-state systems by extending the analyzed model with learned transitive relations, reducing the reachability diameter $D$ so that safety reduces to checking the absence of error states within $D$ steps. It introduces Transitive Relation Learning (TRL), a bounded-model-checking-based framework that unrolls transitions, detects loops, and learns transitive (often disjunctive) relations via transitive projections and conjunctive variable projections, guided by blocking clauses to bias the search toward learned relations. For linear integer arithmetic, TP is instantiated via a recurrence-analysis-inspired procedure that uses CVP to compute concise, state-transition descriptions; TRL can also prove unsafety by applying acceleration to learned transitions. Empirical results in LoAT show TRL is highly competitive with state-of-the-art interpolation-based methods, while avoiding interpolation fragility and offering complementary proof power, with open-source availability for broader use.
Abstract
We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until constantly many steps suffice to cover all reachable states, irrespective of the initial state. Then we can prove safety by checking that no error state is reachable in D steps. To deduce transitive relations, we use recurrence analysis. While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with projections. An empirical evaluation of the implementation of our approach in our tool LoAT shows that it is highly competitive with the state of the art.