Deciding Bisimulation Equivalences for a Class of Non-Finite-State Programs

AbstractTraditionally, many automatic program verification techniques have been applicable only to finite-state programs. In this paper we extend some of these techniques to a class of infinite-state programs that, in addition to having a finite-state control component, may read, store, and write but not perform any other computations on data. Such programs are data-independent in the sense that their behavior does not depend on the actual data values supplied. We consider the problems of deciding strong equivalence and observation equivalence, defined by bisimulations (as in CCS), between such programs. These equivalences have major applications in verification of communication protocols. We present reductions of these problems to the problem of deciding strong equivalence and observation equivalence between finite-state programs, for which polynomial time algorithms exist. The equivalence problems on data-independent programs are shown to be NP-hard in the size of the programs