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.