Proving finiteness 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 processp, to build a finite state transition system which, if a condition holds, is a finite representation ofp; 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 captured by known syntactic criteria.This work has been partially funded by Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo.