Model Checking for Linear Temporal Logic: An Efficient Implementation

: This report provides evidence to support the claim that model checking for linear temporal logic (LTL) is 'practically efficient.' Two implementations of a linear temporal logic model checker is described. One is based on transforming the model checking problem into a satisfiability problem; the other checks an LTL formula for a finite model by computing the cross- product of the finite state transition graph of the program with a structure containing all possible models for the property. An experiment was done with a set of mutual exclusion algorithms and tested safety and liveness under fairness for these algorithms. (CP)