Automatic verification of finite-state concurrent systems using temporal logic specifications

TLDR

The authors propose an efficient procedure for verifying finite‑state concurrent systems against propositional branching‑time temporal logic specifications, adaptable to fairness, offering a practical alternative to manual proofs or mechanical theorem provers. The method efficiently verifies such systems by checking specifications against the global state graph, with an adaptation for fairness. The algorithm runs in linear time with respect to both specification size and global state graph size, and experiments show that state machines with several hundred states are verified in seconds.

Abstract

We give an efficient procedure for verifying that a finite-state concurrent system meets a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm has complexity linear in both the size of the specification and the size of the global state graph for the concurrent system. We also show how this approach can be adapted to handle fairness. We argue that our technique can provide a practical alternative to manual proof construction or use of a mechanical theorem prover for verifying many finite-state concurrent systems. Experimental results show that state machines with several hundred states can be checked in a matter of seconds.