Counterexample-Preserving Reduction for Symbolic Model Checking

TL;DR

This paper introduces a novel reduction technique called Counterexample-Preserving Reduction (CePRe) that simplifies LTL formulas in model checking without losing counterexamples, thereby improving efficiency especially for symbolic models.

Contribution

The paper proposes CePRe, a new reduction method that preserves counterexamples and can be efficiently detected using SAT-solving, enhancing LTL model checking performance.

Findings

CePRe reduces LTL formulas while maintaining counterexamples.

The technique is effective with symbolic models and can be implemented with lightweight effort.

Experimental evaluation shows improved model checking efficiency with NuSMV.

Abstract

The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In our reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique "Counterexample-Preserving Reduction" (CePRe for short), and finally the proposed technquie is experimentally evaluated by adapting NuSMV.