.

The pi-calculus [61] is one the most influential formalisms for modelling and analyzing the behaviour of concurrent systems. This calculus provides a language in which the structure of terms represents the structure of processes together with an operational semantics to represent computational steps. For example, the parallel composition term P | Q, which is built from the terms P and Q, represents the process that results from the parallel execution of the processes P and Q. Similarly, the restriction (v x)P represents a process P with local resource x. The replication !P can be thought of as abbreviating the parallel composition P | P | . . . of an unbounded number of P processes. As for other language-based formalisms (e.g., logic, formal grammars and the pi-calculus) a fundamental part of the research in process calculi involves the study of the expressiveness of fragments or variants of a given process calculus. In this dissertation we shall study the expressiveness of some variants of the pi-calculus focusing on the role of the terms used to represent local and infinite behaviour, namely restriction and replication. The first part of this dissertation is devoted to the expressiveness of the zero-adic variant of the (polyadic) pi-calculus, i.e., CCS with replication (CCS!) [21]. Busi et al [22] show that CCS! is Turing powerful [22]. The result is obtained by encoding Random Access Machines (RAMs) in CCS!. The encoding is said to be non-faithful because it may move from a state which can lead to termination into a divergent one which do not correspond to any configuration of the encoded RAM. I.e., the encoding is not termination preserving. In this dissertation we shall study the existence of faithful encodings into CCS! of models of computability strictly less expressive than Turing Machines. Namely, grammars of Types 1 (Context Sensitive Languages), 2 (Context Free Languages) and 3 (Regular Languages) in the Chomsky Hierarchy. We provide faithful encodings of Type 3 grammars. We show that it is impossible to provide a faithful encoding of Type 2 grammars and that termination-preserving CCS! processes can generate languages which are not Type 2. We finally conjecture that the languages generated by termination-preserving CCS! processes are Type 1 . We also observe that the encoding of RAMs [22] and several encoding of Turing-powerful formalisms in pi-calculus variants may generate an unbounded number of restrictions during the simulation of a given machine. This unboundedness arises from having restrictions under the scope of replication (or recursion) as in e.g., !(v x)P or μX.(v x)(P | X). This suggests that such an interplay between these operators is fundamental for Turing completeness. We shall also study the expressive power of restriction and its interplay with replication. We do this by considering several syntactic variants of CCS! which differ from each other in the use of restriction with respect to replication. We consider three syntactic variations of CCS! which do not allow the generation of unbounded number of restrictions: C2 is the fragment of CCS! not allowing restrictions under the scope of a replication, C3 is the restriction-free fragment of CCS!. The third variant is C4 which extends C2 with Phillips' priority guards [76]. We shall show that the use of an unboundedly many restrictions in CCS! is necessary for obtaining Turing expressiveness in the sense of Busi et al [22]. We do this by showing that there is no encoding of RAMs into C2 which preserves and reflects convergence. We also prove that up to failures equivalence, there is no encoding from CCS! into C2 nor from C2 into C3. Thus up to failures equivalence, we cannot encode a process with an unbounded number of restrictions into one with a bounded number of restrictions, nor one with a bounded number of restrictions into a restriction-free process. As lemmata for the above results we prove that convergence is decidable for C2 and that language equivalence is decidable for C3 but undecidable for C2. As corollary it follows that convergence is decidable for restriction-free CCS. Finally, we show the expressive power of priorities by providing a faithful encoding of RAMs in C4 thus bearing witness to the expressive power of Phillips' priority guards [76]. The second part of this dissertation is devoted to expressiveness of the asynchronous monadic pi-calculus, A [15, 47]. In [70] the authors studied the expressivenessn of persistence in Api [15, 47] wrt weak barbed congruence. The study is incomplete because it ignores divergence. We shall present an expressiveness study of persistence in Api wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [70],,we consider Api and three sub-languages of it, each capturing one source of persistence: the persistent-input Api-calculus (PIA), the persistent-output Api-calculus (POA) and the persistent Api-calculus (PA). In [70] the authors showed encodings from Api into the semi-persistent calculi (i.e., POA and PIA) correct wrt weak barbed congruence. We show that, under some general conditions related to compositionality of the encoding and preservation of the infinite behaviour, there cannot be an encoding from Api into a (semi)-persistent calculus preserving the must testing semantics. We also prove that convergence and divergence are decidable for POA (and PA). As a consequence there is no encoding preserving and reflecting divergence or convergence from Api into POA (and PA). This study fills a gap on the expressiveness study of persistence in A in [70].

<p>In this thesis we investigate two operational models of name-passing calculi: one based on coalgebra, and one based on enriched automata. We develop a semantic framework for modelling the open bisimulation in <i>π</i>-calculus, hyperbisimulation in Fusion calculus, and the first semantic interpretation of <i>FOλ</i>⁽<i>nabla</i>⁾ logic.</p><p>We consider a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of <i>atoms</i>. The key aspect of this model is to consider functors over the category of irreflexive and symmetric finite relations. The models previously proposed for the separate notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter.</p><p>Moreover, the new model admits a definition of <i>distinction-aware</i> simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu's <i>FOλ</i>⁽<i>nabla</i>⁾ logic. <i>FOλ</i>⁽<i>nabla</i>⁾ logic is designed for reasoning about operational semantics of languages with binding.</p><p>On the operational level, a contribution of the thesis is to extend an automata-based model for a variety of name-passing calculi with their associated notion of equivalence. HD-automata, a syntax-independent operational model, has been successfully applied for modelling e.g. early and late bisimulation in <i>π</i>-calculus and hyperbisimulation in Fusion calculus. However, current HD-automata are not adequate for modelling open bisimulation because they can not handle distinction-preserving substitutions. We solve this technical problem by integrating the notion of distinction into the definition of named sets, the basic building blocks of HD-automata. Finally, we discuss the relationship between HD-automata with distinctions, and <b>D</b>-LTS. </p>

Concurrency is concerned with systems of multiple computing agents that interact with each other. Bisimilarity is one of the main representatives of these. Concurrent Constrain Programming (ccp) is a formalism that combines the traditional and algebraic view of process calculi with a declarative one based upon first-order logic. The standard definition of bisimilarity is not completely satisfactory for ccp since it yields an equivalence that is too fine grained. By building upon recent foundational investigations, we introduce a labeled transition semantics and a novel notion of bisimilarity that is fully abstract w.r.t. the observational equivalence in ccp. When the state space of a system is finite, the ordinary notion of bisimilarity can be computed via the partition refinement algorithm, but unfortunately, this algorithm does not work for ccp bisimilarity. Hence, we provide an algorithm that allows us to verify strong bisimilarity for ccp, modifying the algorithm by using a pre-refinement and a partition function based on the irredundant bisimilarity. Weak bisimilarity is a central behavioral equivalence in process calculi and it is obtained from the strong case by taking into account only the actions that are observable in the system. Typically the standard partition refinement can also be used for deciding weak bisimilarity simply by using Milner's reduction from weak to strong; a technique referred to as saturation. We demonstrate that the above-mentioned saturation technique does not work for ccp. We give a reduction that allows us to use the ccp partition refinement algorithm for deciding this equivalence.

A psi-calculus is an extension of the pi-calculus with nominal data types for data structures, logical assertions, and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Expressiveness and therefore modelling convenience significantly exceed those of other formalisms: psi-calculi can capture the same phenomena as other extensions of the pi-calculus, and can be more general, e.g. by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions. Ample comparisons to related calculi are provided and a few significant applications are discussed. The labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. Minimal requirements on the nominal data and logic are established in order to prove general algebraic properties of psi-calculi. The purity of the semantics is on par with the pi-calculus. The theory of weak bisimulation is established, where the tau actions are unobservable. The notion of barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of weak barbs in all static contexts. It is proved that weak barbed equivalence coincides with weak bisimulation equivalence. A symbolic transition system and bisimulation equivalence is presented, and shown fully abstract with respect to bisimulation congruence in the non-symbolic semantics. The symbolic semantics is necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means processes are bisimilar in the symbolic setting if they are bisimilar in the original semantics. Psi-calculi remove the necessity of proving general properties every time a new mobile process calculus is defined. By properly instantiating the framework the properties are guaranteed to hold, thus removing the need to do tedious and error-prone proofs.

In this thesis we investigate two operational models of name-passing calculi: one based on coalgebra, and one based on enriched automata. We develop a semantic framework for modelling the open bisimulation in π-calculus, hyperbisimulation in Fusion calculus, and the first semantic interpretation of FOλ(nabla) logic. We consider a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of atoms. The key aspect of this model is to consider functors over the category of irreflexive and symmetric finite relations. The models previously proposed for the separate notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter. Moreover, the new model admits a definition of distinction-aware simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu's FOλ(nabla) logic. FOλ(nabla) logic is designed for reasoning about operational semantics of languages with binding. On the operational level, a contribution of the thesis is to extend an automata-based model for a variety of name-passing calculi with their associated notion of equivalence. HD-automata, a syntax-independent operational model, has been successfully applied for modelling e.g. early and late bisimulation in π-calculus and hyperbisimulation in Fusion calculus. However, current HD-automata are not adequate for modelling open bisimulation because they can not handle distinction-preserving substitutions. We solve this technical problem by integrating the notion of distinction into the definition of named sets, the basic building blocks of HD-automata. Finally, we discuss the relationship between HD-automata with distinctions, and D-LTS.

Les comportements des processus concurrents peuvent être exprimés en utilisant des calculs de processus, des langages formels simples qui permettent de démontrer des résultats mathématiques précis sur les interactions entre processus. Un exemple très simple est CCS, un autre exemple est le pi-calcul, plus expressif grâce à un mécanisme de communication de canaux. Dans ce dernier, on peut instaurer un système de types (pour raffiner l'analyse aux environnements plus contraints) et encoder le lambda-calcul (qui représente les calculs séquentiels).Certains de ces calculs, comme CCS ou des variantes du pi-calcul comme les calculs de fusions, ont une certaine propriété de symétrie. On utilise dans un premier temps cette symétrie comme un outil, pour prouver que deux encodages du lambda-calcul dans le pi-calcul sont en fait équivalents.Cette preuve nécessitant un système de types et une forme de symétrie, on se pose la question de l'existence d'un système de types pour les autres calculs symétriques, notamment les calculs de fusion, à laquelle on répond par la négative avec un théorème d'impossibilité.En analysant ce théorème, on découvre un contrainte fondamentale de ces calculs qui empêche l'utilisation des types, à savoir la présence d'une notion de relation d'équivalence entre les canaux de communication. Le relâchement de cette contrainte pour obtenir une relation de pré-ordre engendre un calcul intéressant qui recouvre des notions importantes du pi-calcul, absentes dans les calculs de fusion : les types et les noms privés. La première partie de la thèse se concentre sur l'étude de ce calcul.La deuxième partie de la thèse se concentre sur la bisimulation, une méthode pour établir l'équivalence de deux agents dans des langages d'ordre supérieur, par exemple le pi-calcul ou le lambda-calcul. Une amélioration de cette méthode est la théorie des techniques modulo, très puissante, mais qui malheureusement s'applique uniquement aux systèmes de premier ordre, comme les automates ou CCS.Cette thèse s'applique alors à décrire les langages d'ordre supérieur en tant que systèmes du premier ordre. On récupère ainsi la théorie générale des techniques modulo pour ces langages, en prouvant correctes la correspondance induite et les techniques spécifiques à chaque langage. On détaille les tenants et aboutissants de cette approche, pour fournir les outils nécessaires à son utilisation pour d'autres langages d'ordre supérieur. / The behaviours of concurrent processes can be expressed using process calculi, which are simple formal languages that let us establish precise mathematical results on the behaviours and interactions between processes. A very simple example is CCS, another one is the pi-calculus, which is more expressive thanks to a name-passing mechanism. The pi-calculus supports the addition of type systems (to refine the analysis to more subtle environments) and the encoding of the lambda-calculus (which represents sequential computations).Some of these calculi, like CCS or variants of the pi-calculus such as fusion calculi, enjoy a property of symmetry. First, we use this symmetry as a tool to prove that two encodings of the lambda-calculus in the pi-calculus are in fact equivalent.This proof using a type system and a form of symmetry, we wonder if other existing symmetric calculi can support the addition of type systems. We answer negatively to this question with an impossibility theorem.Investigating this theorem leads us to a fundamental constraint of these calculi that forbids types: they induce an equivalence relation on names. Relaxing this constraint to make it a preorder relation yields another calculus that recovers important notions of the pi-calculus, that fusion calculi do not satisfy: the notions of types and of privacy of names. The first part of this thesis focuses on the study of this calculus, a pi-calculus with preorders on names.The second part of this thesis focuses on bisimulation, a proof method for equivalence of agents in higher-order languages, like the pi- or the lambda-calculi. An enhancement of this method is the powerful theory of bisimulations up to, which unfortunately only applies for first-order systems, like automata or CCS.We then proceed to describe higher-order languages as first-order systems. This way, we inherit the general theory of up-to techniques for these languages, by proving correct the translations and up-to techniques that are specific to each language. We give details on the approach, to provide the necessary tools for future applications of this method to other higher-order languages.

Concurrence est concernée par les systèmes informatiques des agents multiples qui interagissent les uns avec les autres. Bisimilarité est l'un des principales représentantes de ces derniers. Programmation concurrente par contraintes (ccp) est un formalisme qui combine le point de vue traditionnel des formules algébriques et opérationnelles des calculs de processus avec une notion déclarative basée sur logique. La définition standard de bisimilarité n'est pas complètement satisfaisante pour ccp car il donne une équivalence qui est trop à grain fin. Nous introduisons une sémantique de transitions étiquetées et une notion de bisimilarité totalement abstraite à l'équivalence observationnelle en ccp. Lorsque l'espace d'état d'un système est fini, la notion ordinaire de bisimilarité peut être calculé par l'algorithme de partition de raffinement, mais, cet algorithme ne fonctionne pas pour la bisimilarité de ccp. Par conséquent, nous fournissons un algorithme que nous permet de vérifier bisimilarité forte pour ccp, en utilisant un pré-raffinement et une fonction de partition basée sur la bisimilarité irredondante. Bisimilarité faible est une équivalence comportementale obtenue en prenant en compte uniquement les actions qui sont observables dans le système. Typiquement, le raffinement de partition standard peut être utilisé pour décider bisimilarité faible simplement en utilisant la réduction de Milner allant de faible à forte. Nous démontrons que, en raison de ses impliquées transitions étiquetées, la technique mentionnée ci-dessus ne fonctionne pas pour ccp. Nous donnons une réduction qui nous permet d'utiliser cet algorithme pour ccp pour décider cette équivalence.

Le concept de réversibilité est ancien, mais il soulève de nos jours beaucoup d'intérêt. Il est en effet exploité dans de nombreux domaines tels que la conception de circuits, le débogage et le test de programmes, la simulation et l'informatique quantique. L'idée d'un modèle de programmation réversible peut se montrer particulièrement intéressante pour la construction de systèmes sûrs de fonctionnement, ne serait-ce que parce que plusieurs techniques connues pour la construction de tels systèmes exploitent une forme ou une autre de retour en arrière ou de reprise. Nous poursuivons dans cette thèse l'étude entreprise avec CCS réversible par Vincent Danos et Jean Krivine, en définissant un pi-calcul d'ordre supérieur réversible (rhopi). Nous prouvons que le modèle obtenu est causalement cohérent, et que l'on peut encoder fidèlement rhopi dans une variante du pi-calcul d'ordre supérieur. Nous définissons également une primitive de reprise à grain fin qui permet de contrôler le retour en arrière dans une exécution concurrente. Nous spécifions formellement la sémantique de cette primitive, et nous montrons qu'elle possède de bonnes propriétés, y compris en présence d'opérations de reprise concurrentes. Enfin nous définissons un algorithme concurrent implantant cette primitive de reprise et ous montrons que cet algorithme respecte la sémantique définie. / Reversible computing has a long history. Nowadays, reversible computing is attracting increasing interest because of its potential applications in diverse fields, including hardware design, biological modelling, program debugging and testing and quantum computing. Of particular interest is the application of reversible computation notions to the study of programming abstractions for dependable systems, because several techniques used to build dependable systems rely on some forms of undo or rollback. We continue, in this thesis, the study undertaken on reversible CCS by Vincent Danos and Jean Krivine, by defining a reversible higher-order pi-calculus (rhopi). We prove that reversibility in our calculus is causally consistent and that one can encode faithfully rhopi into a variant of HOpi. Moreover we design a fine-grained rollback primitive able to control the rollback of a concurrent execution. We give a formal specification of this primitive and show that it enjoys good properties, even in presence of concurrent conflicting rollbacks. We then devise a concurrent algorithm implementing such primitive and show that the algorithm respects the defined semantics.

The work presented in this document in an account of my work as a PhD student at LIX, Ecole Polytechnique, in the COMETE team under the supervision of Catuscia Palamidessi. During these studies, I have been in interested in the various aspects of concurrency covered by the COMETE team activities. The initial goal of my thesis was to investigate the aspects related to process calculi based formalisms to express and analyze Security Protocols. The ultimate goal was to makes some advances towards the automatic verification of security properties. In particular, I was interested in information-hiding protocols which require no cryptography, but normally use randomized mechanisms and therefore exhibit probabilistic behavior. Information hiding protocols are used typically in networks, and they are run by parties that reside in different locations of the system, and therefore interact asynchronously. The first work that I did was to try to give a correct meaning to the various notions of formal asynchronous communications used in various models, in particular between the field of concurrency and the field of distributed computing, where this was a recurrent question. These results are presented in the first part of this document. Being interested in the formal aspects of information-hiding problems, I took part in the preparation of the journal version of [BP09], and started preparing an automated probabilistic anonymity checker based on the formalism presented in this document. This lead to an initial draft of an implementation presented in http://vamp.gforge.inria.fr/. The formalism for this analysis is presented in the fourth part of this document. Another aspect of the verification of information hiding properties is that it requires to compute the probabilities of the possible outcomes for each scheduler. For this reason, this application quickly turned out to be highly inefficient. However, in an asynchronous system, a lot of transitions are confluent, which means that when evaluating a process, it is only necessary to choose one of the two confluent branches. Hence, I have worked on formalizing the possible optimizations based on the possible confluent computations. This work is presented in the second part of the document. Another interesting aspects of probabilistic protocols is the possibility to con- sider infinite runs. By doing such consideration, it is possible to verify the correction of some probabilistic protocols. For instance, in the case of the Crowds routing protocol, presented in Section 5.3, the protocol is considered correct because the probability of running into an infinite execution is null, hence the message will eventually be delivered. For this reason, I got interested in extending the meaning of a asynchronous probabilistic computations to the case of an infinite execution. As a matter of fact, the combination of infinite computation, confluence and probability is not easy to treat in the general case. The problem of confluence in concurrency is solved in an elegant way in an asyn- chronous paradigm called Concurrent Constraint Programming (CCP). Hence, I decided to study infinite computations in a probabilistic version of CCP. The problem, however, is that the meaning of the result of an infinite probabilistic computation was still an open problem also in that context. Hence, I studied a possible way to define this result, using the notion of valuations and sober spaces, and applied it to give a denotational semantics to probabilistic CCP, including infinite computations. This work is presented in the third part of the document. I have chosen a specific order for the various parts of this document that follows the various formal models that are used, in order to present each result along with the corresponding formalism. * In the first and second parts, I present the formal concurrent models, and in the particular asynchronous ones. * In the third part, I present the probabilistic CCP. This part also presents mathematic structures for the representation of infinite probabilistic executions. * Eventually, an application of both asynchronous and probabilistic models to the case of probabilistic information hiding is presented in the fourth part.