Proving fiteness of CCS processes by non-standard semantics

We present a semantic method to check the finiteness of CCS terms. The method is interpretative, i.e. it is based on a non-standard CCS operational semantics. According to this semantics it is always possible, given a process p, to build a finite state transition system which, if a condition hold, is a finite representation of p; otherwise it is a suitable approximation of its semantic behaviour. The method is able to decide the finiteness of a CCS term in a larger number of cases than those capured by known syntactic criteria