Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF

TL;DR

This paper introduces a CEGAR-based method that reduces invariant checking of NRA transition systems to LRA with EUF, enabling the use of efficient linear model checking techniques.

Contribution

It presents a novel incremental reduction approach leveraging differential calculus to handle NRA by translating it into LRA with EUF for model checking.

Findings

Empirical results confirm the approach's effectiveness.

Reduction enables the use of mature LRA model checkers.

Potential for improved NRA invariant checking performance.

Abstract

Model checking invariant properties of designs, represented as transition systems, with non-linear real arithmetic (NRA), is an important though very hard problem. On the one hand NRA is a hard-to-solve theory; on the other hand most of the powerful model checking techniques lack support for NRA. In this paper, we present a counterexample-guided abstraction refinement (CEGAR) approach that leverages linearization techniques from differential calculus to enable the use of mature and efficient model checking algorithms for transition systems on linear real arithmetic (LRA) with uninterpreted functions (EUF). The results of an empirical evaluation confirm the validity and potential of this approach.