Finite approximations for model checking non-finite-state processes

In this paper we present a verification framework to check properties of full CCS terms. These properties are expressed in an action-based logie, and the proof technique is model checking, based on the transition system corresponding 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 cases we only bave 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 particolar notion of approximation, suitable in proving liveness and safety properties of the process terms. Then we show that the class of provable properties might also depend on the way chains of approximations are built and we provide a set of notions to compare and choose among different approximation chains.