Static Analysis for State-Space Reductions Preserving Temporal Logics

摘要

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 path reduction, reduces the state-space by compressing computation paths. This method reduces the number of steps each computation takes. The second method, called 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. We also consider a refinement of the dead variable reduction, based on partially dead variables, which may result in a greater reduction. 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 and the reduction based on partially dead variables give significant reductions, while the effect of fully dead variables is less impressive. We discuss the differences between the approaches, and the reasons for these results.