Technical Report CS-2000-03

Title: Static Analysis for State-Space Reductions Preserving Temporal Logics
Authors: Karen Yorav, Orna Grumberg
Abstract: In this paper we present two methods that use static analysis of parallel programs to create reduced models for them. Our algorithms examine the control-flow graph of a program (the syntax) and create a smaller transition system than would have been created otherwise. The smaller transition system is equivalent to the original transition system of the program with respect to temporal logic specifications. The two methods are orthogonal in their approach. The first, called {\em path reduction}, reduces the state-space by compressing computation paths. This method reduces the number of steps each computation takes. The second method, called {\em dead variable reduction}, reduces according to the variable domains. It identifies classes of equivalent states which differ only on variable values (and not the program counter) and uses a representative for each class. Our target is not only to be able to reduce according to both approaches, but also to find out which approach is more useful. Our algorithms are based on syntactic manipulation of expressions, thus enabling us to handle programs with variables over finite as well as infinite domains. Both methods can easily be combined with either explicit state or symbolic methods (and with each other). We used the Murphi verifier to test the amount of reduction achieved by both methods. We let Murphi perform a DFS search and compared the sizes of the original and reduced transition systems, for several examples and according to both reductions. The results show that path reduction gives significant reductions, while the effects of dead-variable reduction are less impressive. We discuss the differences between the approaches, and the reasons for these results.
CopyrightThe above paper is copyright by the Technion, Author(s), or others. Please contact the author(s) for more information

Remark: Any link to this technical report should be to this page (, rather than to the URL of the PDF files directly. The latter URLs may change without notice.

To the list of the CS technical reports of 2000
To the main CS technical reports page

Computer science department, Technion