2021/09/01 by Tsubasa Shoshi, Shoshi, Tsubasa, Takuma Ishikawa +9
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2109.00311
openalex publication_date 2021/09/01 · openalex created_date 2021/09/13 · openalex updated_date 2026/07/28
We propose an automated method for proving termination of π-calculus processes, based on a reduction to termination of sequential programs: we translate a π-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 π-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.