On the Expressiveness of Pure Mobile Ambients

We consider the Pure Ambient Calculus, which is Cardelli and Gordon's Ambient Calculus (or more precisely its safe version by Levi and Sangiorgi) restricted to its mobility primitives, and we focus on its expressive power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As an example, we give an encoding of the synchronous π-calculus into pure ambients and we state an operational correspondence result. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language: the π-Calculus with Explicit Substitutions and Channels, which is a syntactic extension of the π-calculus with a specific operational semantics.     

Ambient Petri Nets

Both the Ambient Calculus by L. Cardelli and the Elementary Object Systems by R. Valk model the behaviour of mobile systems. The Ambient Calculus is based on the concept of ambient, which is an environment with a given name that is delimited by a boundary, where some internal processes are executed. The main property of these ambients is that they can be moved to a new location thus modeling mobility. Elementary Object Systems are two-level net systems composed of a system net and one or more object nets, which can be seen as high-level token objects of the system net modeling the execution of mobile processes. This paper intends to contribute to the relationship between both frameworks by defining a multilevel extension of Elementary Object Systems, which will be used to provide a denotational semantics of a new process algebra called APBC (Ambient Petri Box Calculus). Such process algebra is an extension of the Petri Box Calculus that includes both ambients and their mobility capabilities, which conversely can be also interpreted as an extension of the Ambient Calculus with the main operations from the PBC.     

Predicate μ-Calculus for Mobile Ambients

Ambient logics have been proposed to describe properties for mobile agents which may evolve over time as well as space. This paper takes a predicate-based approach to extending an ambient logic with recursion, yielding a predicate μ-calculus in which fixpoint formulas are formed using predicate variables. An algorithm is developed for model checking finite-control mobile ambients against formulas of the logic, providing the first decidability result for model checking a spatial logic with recursion.     

The Calculus of Context-aware Ambients

We present the Calculus of Context-aware Ambients (CCA in short) for the modelling and verification of mobile systems that are context-aware. This process calculus is built upon the calculus of mobile ambients and introduces new constructs to enable ambients and processes to be aware of the environment in which they are being executed. This results in a powerful calculus where both mobility and context-awareness are first-class citizens. We present the syntax and a formal semantics of the calculus. We propose a new theory of equivalence of processes which allows the identification of systems that have the same context-aware behaviours. We prove that CCA encodes the π-calculus which is known to be a universal model of computation. Finally, we illustrate the pragmatics of the calculus through many examples and a real-world case study of a context-aware hospital bed.     

Separation of synchronous and asynchronous communication via testing

One of the early results concerning the asynchronous π$\pi$-calculus which significantly contributed to its popularity is the capability of encoding the output prefix of the (choiceless) π$\pi$-calculus in a natural and elegant way. Encodings of this kind were proposed by Honda and Tokoro, by Nestmann and (independently) by Boudol. We investigate whether the above encodings preserve De Nicola and Hennessy’s testing semantics. In this sense, it turns out that, under some general conditions, no encoding of the output prefix is able to preserve the must testing. This negative result is due to (a) the non-atomicity of the sequences of steps which are necessary in the asynchronous π$\pi$-calculus to mimic synchronous communication, and (b) testing semantics’ sensitivity to divergence.     

Tile Formats for Located and Mobile Systems

Standard SOS formats are limited in their ability to define the operational semantics of process calculi with concurrency, causality, and mobility, and with bound names and name generation mechanisms. In this paper we describe a general approach, based on the tile model, to the definition of the operational semantics of process calculi. By providing tile systems for located CCS and asynchronous π-calculus we demonstrate that the proposed approach is more suited than SOS to provide a uniform treatment of concurrency and mobility within a compositional framework.     

A taxonomy of process calculi for distribution and mobility

In this paper, we comparatively analyze some mainstream calculi for mobility and distribution, together with some of their variants: asynchronous π-calculus, distributed π-calculus, and some dialects of Mobile/Boxed/Safe ambients. In particular, we focus on their relative expressive power, i.e. we try to encode every language in the other while respecting some reasonable properties. According to the possibility or the impossibility for such results, we set up a taxonomy of these languages. Our study enables understanding, for every pair of calculi, which features of one can be rendered in the other and how this is possible, or which features cannot be rendered and why this is impossible.     

χ-演算与π-演算的语义比较研究

Through the comparison of syntactic structure,operational semantics and algebraic semantics between χ-calculus and π-calculus, this paper concludes that χ-calculus has more succinct syntactic structure,more explicit operational semantics,more intuitionistic algebraic semantics and more favorable algebraic property. And a translation from π-calculus to χ-calculus is presented.     

On the expressive power of KLAIM-based calculi

We study the expressive power of variants of KLAIM, an experimental language with programming primitives for network-aware programming that combines the process algebra approach with the coordination-oriented one. KLAIM has proved to be suitable for programming a wide range of distributed applications with agents and code mobility, and has been implemented on the top of a runtime system written in Java. In this paper, the expressivity of its constructs is tested by distilling from it a few, more and more foundational, languages and by studying the encoding of each of them into a simpler one. The expressive power of the considered calculi is finally tested by comparing one of them with asynchronous π$\pi$-calculus.     

A CPS encoding of name-passing in Higher-order mobile embedded resources

We present an encoding of the synchronous π$\pi$-calculus in the calculus of Higher-order mobile embedded resources (Homer), a pure higher-order calculus with mobile processes in nested locations, defined as a simple, conservative extension of the core process-passing subset of Thomsen's Plain CHOCS. We prove that our encoding is fully abstract with respect to barbed bisimulation and sound with respect to barbed congruence. Our encoding demonstrates that higher-order process-passing together with mobile resources in, possibly local, named locations are sufficient to express π$\pi$-calculus name-passing. The encoding uses a novel continuation passing style to facilitate the encoding of synchronous communication.     

On the Expressive Power of Joint Input

The join-calculus was introduced as an ‘extended subset’ of the asynchronous π-calculus by amalgamating the three operators for input, restriction, and replication into a single operator, called definition, but with the additional capability to describe the atomic joint reception of values from two different channels. In this paper, we just extend the asynchronous π-calculus with joint input. By studying its expressive power, using slight variations of previously investigated choice encodings, we also conclude on the expressiveness of the join-calculus.     

Calculi for interaction

Action structures have previously been proposed as an algebra for both the syntax and the semantics of interactive computation. Here, a class of concrete action structures calledaction calculi is identified, which can serve as a non-linear syntax for a wide variety of models of interactive behaviour. Each action in an action calculus is represented as an assembly ofmolecules; the syntactic binding ofnames is the means by which molecules are bound together. A graphical form,action graphs, is used to aid presentation. One action calculus differs from another only in its generators, calledcontrols. Action calculi generalise a previously defined action structure PIC for the π- calculus. Several extensions to PIC are given as action calculi, giving essentially the same power as the π-calculus. An action calculus is also given for the typed λ-calculus, and for Petri nets parametrized on their places and transitions. An equational characterization of action calculi is given: each action calculusA is the quotient of a term algebra by certain equations. The terms are generated by a set of operators, including those basic to all action structures as well as the controls specific toA; the equations are the basic axioms of action structures together with four additional axiom schemata.     

On the expressive power of movement and restriction in pure mobile ambients

Pure mobile ambients is a process calculus suitable to focus on issues related to mobility, abstracting away from aspects concerning process communication. However, it incorporates name restriction (i.e. the (νn) binder) and ambient movement (i.e. the in and out capabilities) that can be seen as characteristics adapted, or directly borrowed, from the tradition of communication-based process calculi. For this reason, we retain that it is worth to investigate whether or not these features can be removed from pure mobile ambients without losing expressive power.To this aim, we consider two variants of pure mobile ambients which differ in the way infinite processes can be defined; the former exploits process replication, while the latter is more general and permits recursive process definition. We analyse whether or not the elimination of ambient movement and/or name restriction reduces the expressive power of these two calculi, using the decidability of process termination as a yardstick. We prove that name restriction can be removed from both calculi without reducing the expressive power. On the other hand, the elimination of both ambient movement and name restriction strictly reduces the expressive power of both calculi. As far as the elimination of only ambient movement is concerned, we prove an interesting discrimination result: process termination is undecidable under recursive process definition, while it turns out to be decidable under process replication.     

Interaction Nets vs. the ρ-calculus: Introducing Bigraphical Nets

The ρ-calculus generalises both term rewriting and the λ-calculus in a uniform framework. Interaction nets are a form of graph rewriting which proved most successful in understanding the dynamics of the λ-calculus, the prime example being the implementation of optimal β-reduction. It is thus natural to study interaction net encodings of the ρ-calculus as a first step towards the definition of efficient reduction strategies. We give two interaction net encodings which bring a new understanding to the operational semantics of the ρ-calculus; however, these encodings have some drawbacks and to overcome them we introduce bigraphical nets—a new paradigm of computation inspired by Lafont's interactions nets and Milner's bigraphs.     

Parametric synchronizations in mobile nominal calculi

We present and compare P-PRISMA and F-PRISMA, two parametric calculi that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). In particular, P-PRISMA is based on name transmission (P-SAM), like π-calculus, and thus exploits directional (input–output) communication only, while F-PRISMA is based on name fusion (F-SAM), like Fusion calculus, and thus exploits a more symmetric form of communication. However, P-PRISMA and F-PRISMA can easily accommodate many other high-level synchronization mechanisms than the basic ones available in π-calculus and Fusion, hence allowing for the development of a general meta-theory of mobile calculi. We define for both the labeled operational semantics and a form of strong bisimilarity, showing that the latter is compositional for any SAM. We also discuss reduction semantics and weak bisimilarity. We give several examples based on heterogeneous SAMs, we investigate the case studies of π-calculus and Fusion calculus giving correspondence theorems, and we show how P-PRISMA can be encoded in F-PRISMA. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.     

Interaction in Time and Space

Distributed π-calculus and ambient calculus are extended with timers which may trigger timeout recovery processes. Timers provide a useful notion of relative time with respect to the interaction in a distributed system. The rather flat notion of space in timed distributed π-calculus is improved by considering a hierarchical representation of space in timed mobile ambients. Some basic results are proven, making sound both formal approaches. An easily understood example is used for both extensions, showing how it is possible to describe a non-monotonic behaviour and use a decentralized control to coordinate the interacting components in time and space.     

On the Expressive Power of Klaim-based Calculi

In this work, we study the expressive power of variants of Klaim, an experimental language with programming primitives for global computing that combines the process algebra approach with the coordination-oriented one. Klaim has proved to be suitable for programming a wide range of distributed applications with agents and code mobility, and has been implemented on the top of a runtime system based on Java. The expressivity of its constructs is tested by distilling from it some (more and more foundational) calculi and studying the encoding of each of the considered languages into a simpler one. An encoding of the asynchronous π-calculus into one of these calculi is also presented.