Dam, Mads (1994) *On the Decidability of Process Equivalences for the pi-calculus.* [SICS Report]

Postscript 81Kb |

## Abstract

We present general results for showing process equivalences applied to the finite control fragment of the pi-calculus decidable. Firstly a Finite Reachability Theorem states that up to finite name spaces and up to a static normalisation procedure, the set of reachable agent expressions is finite. Secondly a Boundedness Lemma shows that no potential computations are missed when name spaces are chosen large enough, but finite. We show how these results lead to decidability for a number of pi-calculus equivalences such as strong or weak, late or early bismulation equivalence. Furthermore, for strong late equivalence we show how our techniques can be used to adapt the well-known Paige-Tarjan algorithm. Strikingly this results in a single exponential running time not much worse than the running time for the case of for instance CCS. Our results considerably strengthens previous results on decidable equivalences for parameter-passing process calculi.

Item Type: | SICS Report |
---|---|

Uncontrolled Keywords: | Program Verification, Mobile Processes, Process Equivalence, Bisimulation Equivalence |

ID Code: | 2140 |

Deposited By: | Vicki Carleson |

Deposited On: | 22 Oct 2007 |

Last Modified: | 18 Nov 2009 16:00 |

Repository Staff Only: item control page