On the Verification of Temporal Properties

We present a new algorithm that can be used for solving the model−checking problem for linear−time temporal logic. This algorithm can be viewed as the combination of two existing algorithms plus a new state representation technique introduced in this paper. The new algorithm is simpler than the traditional algorithm of Tarjan to check for maximal strongly connected components in a directed graph which is the classical algorithm used for model−checking. It has the same time complexity as Tarjan’s algorithm, but requires less memory. Our algorithm is also compatible with other important complexity management techniques, such as bit−state hashing and state space caching. Proc. IFIP, Symp. on Protocol Specification, Testing, and Verification. June 1993, Liege, Belgium. January 1, 1993 

• Type: Conference
• Year: 1993
• Where: PSTV
• Authors: Patrice Godefroid, Gerard J. Holzmann
• Keywords: Algorithm, Classical Algorithm, Hardware, PSTV 1993, Traditional Algorithm