  We propose an automated method for proving termination of $\pi$-calculus
processes, based on a reduction to termination of sequential programs: we
translate a $\pi$-calculus process to a sequential program, so that the
termination of the latter implies that of the former. We can then use an
off-the-shelf termination verification tool to check termination of the
sequential program. Our approach has been partially inspired by Deng and
Sangiorgi's termination analysis for the $\pi$-calculus, and checks that there
is no infinite chain of communications on replicated input channels, by
converting such a chain of communications to a chain of recursive function
calls in the target sequential program. We have implemented an automated tool
based on the proposed method and confirmed its effectiveness.
