×

Partial order reduction for checking LTL formulae with the next-time operator. (English) Zbl 1380.68276

Summary: Partial order reduction (POR) has been one of the most successful techniques for reducing the state spaces in model checking concurrent asynchronous systems with respect to linear-time temporal logic (LTL) formulae. Conventional POR only support checking formulae without the next-time operator because these formulae are invariant under stuttering, thus are suitable for POR. In this article we introduce a novel POR technique for checking formulae with the next-time operator. This new technique enables model checking algorithms to use POR even if the formulae are not stutter invariant (SI). More precisely, it supports the full class of LTL formulae with the next-time operator. The core of our approach is a heuristic algorithm for detecting and extending SI components of Büchi automata (BA) during the translation from LTL formulae into BAs. Then, the detected component is used to direct the reduction of the state space of a system. In addition, an SI-component of a BA enables an improvement of LTL model checking algorithms based on the nested depth-first search. We show that our technique is efficient when the synchronous product of an SI-component and a system is large.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI