Proving fineteness of CCS processes by non-standard semantics

In this paper we present a semantic method to check the finiteness of CCS expressions. The method is interpretative, i.e. it is based on a non-standard operational semantics of CCS. According to this semantics it is always possible, given a process p, to build a finite state transition system which, if some condition holds, is a finite representation of p; otherwise it is a suitable approximation of its semantic behavior. The method is able to decide the finiteness of a CCS expression in a large number of cases which are not captured by the known syntactic criteria.