#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"
}