Verify LTL with Fairness Assumptions Efficiently

TL;DR

This paper introduces an efficient algorithm for verifying LTL properties under fairness assumptions, significantly improving performance over traditional automata-based methods, and is implemented in NuSMV with promising experimental results.

Contribution

The paper presents a novel, efficient algorithm for LTL model checking with fairness assumptions that avoids large automata construction, extending to arbitrary fairness assumptions.

Findings

Algorithm outperforms automata-theoretic approach by several orders of magnitude in time and memory

Implementation in NuSMV demonstrates practical efficiency on various formulas

Approach effectively handles a broad class of fairness assumptions

Abstract

This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness assumptions and then extend the algorithm to handle arbitrary %fairness assumptions ones. Notably, by making use of some syntactic transformations, our algorithm avoids to construct corresponding B\"uchi automata for the whole fairness assumptions, which can be very large in practice. We implement our algorithm in NuSMV and consider a large selection of formulas. Our experiments show that in many cases our approach exceeds the automata-theoretic approach up to several orders of magnitude, in both time and memory.