Axiomatisations and Types for Probabilistic and Mobile Processes - Archive ouverte HAL Access content directly
Theses Year : 2005

Axiomatisations and Types for Probabilistic and Mobile Processes

Axiomatisations et types pour des processus probabilistes et mobiles

(1)
1
Yuxin Deng
  • Function : Author
  • PersonId : 840711

Abstract

The focus of this thesis are the theoretical foundations for reasoning about algorithms and protocols for modern distributed systems. Two important features of models for these systems are probability and typed mobility: probabilities can be used to quantify unreliable or unpredictable behaviour and types can be used to guarantee secure behaviour in systems with a mobile structure. In this thesis we develop algebraic and type-based techniques for behavioural reasoning on probabilistic and mobile processes.

In the first part of the thesis we study the algebraic theory of a process calculus which combines both nondeterministic and probabilistic behaviour in the style of Segala and Lynch's probabilistic automata. We consider various strong and weak behavioural equivalences, and we provide complete axiomatisations for finite-state processes, restricted to guarded recursion in the case of the weak equivalences.

In the second part of the thesis we investigate the algebraic theory of the $\pi$-calculus under the effect of capability types, which are one of the most useful forms of types in mobile process calculi. Capability types allow one to distinguish between the capability to read from a channel, to write to a channel, and to both read and write. They also give rise to a natural and powerful subtyping relation. We consider two variants of typed bisimilarity, both in their late and in their early version. For both of them, we give complete axiomatisations on the closed finite terms. For one of the two variants, we provide a complete axiomatisation for the open finite terms.

In the last part of the thesis we develop a type-based technique for verifying the termination property of some mobile processes. We provide four type systems to guarantee this property. The type systems are obtained by successive refinements of the types of the simply typed $\pi$-calculus. The termination proofs take advantage of techniques from term rewriting systems. These type systems can be used for reasoning about the terminating behaviour of some non-trivial examples: the encodings of primitive recursive functions, the protocol for encoding separate choice in terms of parallel composition, a symbol table implemented as a dynamic chain of cells.

These results lay out the foundations for further study of more advanced models which may combine probabilities with types. They also highlight the robustness of the algebraic and type-based techniques for behavioural reasoning.
Cette th`ese se concentre sur des bases th´eoriques utiles pour l'analyse d'algorithmes et de protocoles
pour des syst`emes r´epartis modernes. Deux caract´eristiques importantes des mod`eles pour
ces syst`emes sont les probabilit´es et la mobilit´e typ´ee : des probabilit´es peuvent ˆetre utilis´ees pour
quantifier des comportements incertains ou impr´evisibles, et des types peuvent ˆetre utilis´es pour
garantir des comportements sˆurs dans des syst`emes mobiles. Dans cette th`ese nous d´eveloppons
des techniques alg´ebriques et des techniques bas´ees sur les types pour l'´etude comportementale des
processus probabilistes et mobiles.

Dans la premi`ere partie de la th`ese nous ´etudions la th´eorie alg´ebrique d'un calcul de processus
qui combine les comportements non-d´eterministe et probabiliste dans le mod`ele des automates probabilistes
propos´es par Segala et Lynch. Nous consid´erons diverses ´equivalences comportementales
fortes et faibles, et nous fournissons des axiomatisations compl`etes pour des processus `a ´etats finis,
limit´ees `a la r´ecursion gard´ee dans le cas des ´equivalences faibles.

Dans la deuxi`eme partie de la th`ese nous ´etudions la th´eorie alg´ebrique du -calcul en pr´esence
des types de capacit´es, qui sont tr`es utiles dans les calculs de processus mobiles. Les types de
capacit´es distinguent la capacit´e de lire sur un canal, la capacit´e d'´ecrire sur un canal, et la capacit´e
de lire et d'´ecrire `a la fois. Ils introduisent ´egalement une relation de sous-typage naturelle et
puissante. Nous consid´erons deux variantes de la bisimilarit´e typ´ee, dans leurs versions retard´ees
et anticip´ees. Pour les deux variantes, nous donnons des axiomatisations compl`etes pour les termes
ferm´es. Pour une des deux variantes, nous fournissons une axiomatisation compl`ete pour tous les
termes finis.

Dans la derni`ere partie de la th`ese nous d´eveloppons des techniques bas´ees sur les types pour
v´erifier la propri´et´e de terminaison de certains processus mobiles. Nous fournissons quatre syst`emes
de types pour garantir cette propri´et´e. Les syst`emes de types sont obtenus par des am´eliorations
successives des types du -calcul simplement typ´e. Les preuves de terminaison utilisent des techniques
employ´ees dans les syst`emes de r´e´ecriture. Ces syst`emes de types peuvent ˆetre utilis´es pour
raisonner sur le comportement de terminaison de quelques exemples non triviaux : les codages des
fonctions r´ecursives primitives, le protocole pour coder le choix s´epar´e en terme de composition
parall`ele, une table de symboles implement´ee comme une chaˆıne dynamique de cellules.

Ces r´esultats ´etablissent des bases pour une future ´etude de mod`eles plus avanc´es qui peuvent
combiner des probabilit´es avec des types. Ils soulignent ´egalement la robustesse des techniques
alg´ebriques et de celles bas´ees sur les types pour le raisonnement comportemental.
Fichier principal
Vignette du fichier
main.pdf (1.15 Mo) Télécharger le fichier
Loading...

Dates and versions

tel-00155225 , version 1 (16-06-2007)

Identifiers

  • HAL Id : tel-00155225 , version 1

Cite

Yuxin Deng. Axiomatisations and Types for Probabilistic and Mobile Processes. Modeling and Simulation. École Nationale Supérieure des Mines de Paris, 2005. English. ⟨NNT : ⟩. ⟨tel-00155225⟩
111 View
179 Download

Share

Gmail Facebook Twitter LinkedIn More