Skip to Main content Skip to Navigation
Reports

On the Decidability of Fragments of the Asynchronous Pi-Calculus

Roberto M. Amadio 1 Charles Meyssonnier
1 MIMOSA - Migration and mobility : semantics and applications
CRISAM - Inria Sophia Antipolis - Méditerranée , Université de Provence - Aix-Marseille 1, MINES ParisTech - École nationale supérieure des mines de Paris
Abstract : We study the decidability of a reachability problem for various fragments of the asynchronous $\pi$-calculus. We consider the combination of three main features: name generation, name mobility, and unbounded control. We show that the combination of name generation with either name mobility or unbounded control leads to an undecidable fragment. On the other hand, we prove that name generation without name mobility and with bounded control is decidable by reduction to the coverability problem for Petri Nets.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00072346
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:28:53 PM
Last modification on : Wednesday, October 14, 2020 - 3:46:41 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:44:52 PM

Identifiers

  • HAL Id : inria-00072346, version 1

Citation

Roberto M. Amadio, Charles Meyssonnier. On the Decidability of Fragments of the Asynchronous Pi-Calculus. RR-4241, INRIA. 2001. ⟨inria-00072346⟩

Share

Metrics

Record views

265

Files downloads

332