Finite approximations for model checking non-finite-state processes

In this paper we present a verification framework to check properties of fu ll CCS terms. These properties are expressed in an action-based logic, and the proof technique is model checking, based on the transition system corre sponding to the CCS term. Our approach also allows some kinds of properties to be proved if the transition systems are infinite. Of course, in these c ases we only have a semi-decision method. The idea is to use (a sequence of ) finite-state transition systems which approximate the, possibly infinite, transition system corresponding to a term. To this end we define a particu lar notion of approximation, suitable in proving liveness and safety proper ties of the process terms. Then we show that the class of provable properti es might also depend on the way chains of approximations are built and we p rovide a set of notions to compare and choose among different approximation chains.