Analysis of the reachability problem in fragments of the Pi-calculus - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Preprints, Working Papers, ... Year : 2010

Analysis of the reachability problem in fragments of the Pi-calculus

Abstract

The pi-calculus is one of the most important formalisms for analyzing and modelling concurrent systems. It is a simple but powerful tool for specifying and checking several properties in this kind of systems. An interesting property of any system is the ability to reach some special state where it has a particular behavior. In security systems this is extremely important, since we would like that a system does not reach a state where a secret becomes observable to potential attackers. This work studies the reachability problem in fragments of the pi-calculus and explores some expressiveness results beyond this problem. We prove the relation between local names and sequences of actions in CCS! processes. Using this result and the decidability of barbs from previous work we prove that the reachability problem for some fragments of pi-calculus is decidable. We also provide an algorithmic approach for solving this problem using the theory of well-structured transition systems in consequence we are able to verify this property in infinite state systems with a finite number of steps. Finally, we provide a small interpreter for CCS!, useful as an initial practical approach for checking properties in real life systems specified by this calculus
Fichier principal
Vignette du fichier
LuisFPinoBScThesis.pdf (428.27 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00546849 , version 1 (14-12-2010)

Identifiers

  • HAL Id : hal-00546849 , version 1

Cite

Luis Pino. Analysis of the reachability problem in fragments of the Pi-calculus. 2010. ⟨hal-00546849⟩
220 View
164 Download

Share

Gmail Facebook X LinkedIn More