Résumé de rapport du LIF


Rapport 04-2002
Roberto M. Amadio and Charles Meyssonnier
On decidability of the control reachability problem in the asynchronous pi-calculus


Téléchargement / Download : pdf 248k , ps.gz 224k , bibtex

Abstract

We study the decidability of the control 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 with unique receiver and bounded input (a condition weaker than bounded control) is decidable by reduction to the coverability problem for Petri Nets with transfer (and back).

Keywords

Petri Nets, pi-calculus, control reachability.

Résumé

Nous étudions la décidabilité d'un problème d'accessibilité pour plusieurs fragments du pi-calcul asynchrone. Nous considérons la combinaison de trois aspects principaux : la génération de noms, la mobilité de noms et le contrôle non borné. Nous montrons que la combinaison de la génération de noms avec ou bien la mobilité de noms ou bien le contrôle non borné induit un fragment indécidable. D'autre part, nous démontrons que la génération de noms avec recepteur unique et avec input borné (une condition plus faible que le contrôle borné) est décidable par réduction au problème de couverture pour les Réseaux de Petri avec transfert (et vice versa).

Mots clés

Réseaux de Petri, pi-calcul, accessibilité du contrôle.

Bibtex

@TECHREPORT{04-2002,
    AUTHOR	= {Roberto M. Amadio and Charles Meyssonnier},
    TITLE	= {{On decidability of the control reachability problem in the asynchronous pi-calculus}},
    INSTITUTION	= {{LIF}},
    ADDRESS	= {Marseille, France},
    TYPE	= {Research report},
    NUMBER	= {04-2002},
    MONTH	= {May},
    YEAR	= {2002},
    NOTE	= {http://pageperso.lif.univ-mrs.fr/~edouard.thiel/RESP/Rapports/04-2002.html},
}

[css]   [GenRap] [xhtml] Direction : François Denis - Secrétariat de direction : Martine Quessada
Tel. 04 91 11 36 00 - Fax : 04 91 11 36 02 - Mel. Martine.Quessada@cmi.univ-mrs.fr

webmaster - La dernière mise à jour de cette page date du 04 septembre 2008