Termination Analysis for the $\pi$-Calculus by Reduction to Sequential Program Termination

TL;DR

This paper introduces an automated approach to prove termination of $ ext{pi}$-calculus processes by translating them into sequential programs and applying existing termination tools, simplifying the verification process.

Contribution

It presents a novel reduction-based method for $ ext{pi}$-calculus termination analysis, enabling the use of standard sequential program termination tools.

Findings

Successfully implemented an automated tool for the method.

Confirmed effectiveness through experiments.

Reduces $ ext{pi}$-calculus termination to sequential program termination.

Abstract

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.