#NumberTR-PDS-2004-002

#Title
On Reducing the Global State Graph for Verification of Distributed Computations

#Author
Arindam Chakraborty
Vijay K. Garg

#Abstract
Correct distributed programs are very hard to write and reason about. Verification 
of distributed programs with respect to their specifications is thus very important
to ensure that a distributed system works as expected. Model checking has emerged 
as a technique used to verify the correctness of programs. However model checking 
techniques suffer from the global state explosion problem - finite state models of 
distributed and concurrent systems grow exponentially in size as the number of com-
ponents in the system increases. Even though work has been done to reduce the size 
of the global state graph generated by model checking algorithms, current research 
has mainly focussed on finite-state transition graphs. In the context of distribut-
ed computations, additional advantage can be derived from the fact that the global 
state graph forms a distributive lattice. We present a generic technique using cong-
ruences to reduce the global state graph of distributed programs, by using lattice 
theoretic properties of the graph. Our state space reduction technique is generic in
the sense that it integrates seamlessly with any model checking algorithm.

#Bib
@techreport{TR-PDS-2004-002,
  author =   "Arindam Chakraborty and Vijay K. Garg",
  title =   "On Reducing the Global State Graph for Verification of Distributed Computations",
  instituition = "The University of Texas at Austin",
  year =   "2004",
  number =  "TR-PDS-2004-002",
  note =  "available via ftp or WWW at maple.ece.utexas.edu
    as technical report TR-PDS-2004-002"
}