Rapport 04-2002
Roberto M. Amadio and Charles Meyssonnier
On decidability of the control reachability problem in the asynchronous pi-calculus
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).
Petri Nets, pi-calculus, control reachability.
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).
Réseaux de Petri, pi-calcul, accessibilité du contrôle.
@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}, }