Model Checking for Linear Temporal Logic: An Efficient Implementation

摘要

This report provides evidence to support the claim that model checking for lineartemporal 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. Keywords: Mathematical logic; Linear algebraic equations; Model-checking algorithms; Computer program verification. (CP)