Termination Analysis for the pi-Calculus by Reduction to Sequential Program Termination
summary
Proposes an automated reduction that translates pi-calculus processes into sequential C programs so termination of the C program implies termination of the process; replicated inputs become functions and outputs become function calls while non-replicated inputs map to nondeterministic instantiation. Refinement channel types recover value constraints via CHC generation and solving (Spacer/hoist templates) so finite-value chains prove termination. Implementation emits C and uses Ultimate Optimizer for termination; prototype verifies many benchmarks, beats TyPiCal on several, but fails four cases due to multi-channel synchronization.
AI-written summary · about
chapters (11)
- 0:00Termination analysis intro
- 1:27Research motivation
- 1:50Pi-calculus basics
- 4:25Pi-calculus example
- 4:47Translation to sequential
- 6:53Termination correspondence
- 8:03Soundness proof
- 12:28Refinement types for input
- 16:37Refinement type constraints
- 19:05Implementation results
- 21:41Related work
related talks
19mCommutativity Simplifies Proofs of Parameterized Programs
31mTermination in Concurrency, Revisited
23mTranslating Concepts of the Futhark Programming Language into an Extended Pi-Calculus
21mA Semantic Logical Relation for Termination of Intuitionistic Linear Logic Session Types
21mFair Termination of Binary Sessions
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
23mProbabilistic Refinement Session Types
54mReasoning about Progress of Concurrent Objects