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.     

State-oriented Noninterference for CCS

We address the question of typing noninterference (NI) in the calculus CCS, in such a way that Milner's translation into CCS of a standard parallel imperative language preserves both an existing NI property and the associated type system. Recently, Focardi, Rossi and Sabelfeld have shown that a variant of Milner's translation, restricted to the sequential fragment of the language, maps a time-sensitive NI property to that of Persistent Bisimulation-based Non Deducibility on Compositions (PBNDC) on CCS. However, since CCS was not equipped with a type system, the question of whether the translation preserves types could not be addressed. We extend Focardi, Rossi and Sabelfeld's result by showing that a slightly simpler variant of Milner's translation preserves a time-insensitive NI property on the full parallel language, by mapping it again to PBNDC. As a by-product, we formalise a folklore result, namely that Milner's translation preserves a behavioural equivalence on programs. We present a simple type system ensuring PBNDC on CCS, inspired by existing type systems for the π-calculus. Unfortunately, this type system as it stands is too restrictive to grant the expected type preservation result. We sketch a solution to overcome this problem.     

Efficient Stochastic Simulation of Biological Systems with Multiple Variable Volumes

The application of concurrent calculi to the formalisation of biological systems constitutes a promising approach to the analysis in silico of biological phenomena. The Gillespie algorithm is one of the main models exploited for their stochastic simulation. While the original algorithm considers only one fixed-volume compartment, the simulation of biological systems often requires multi-compartment semantics. In this paper we present an enhanced formulation of an extended version of the algorithm which handles multiple compartments with varying volumes. The presented algorithm is used as basis for the implementation of an extension of the stochastic π-Calculus, called Sπ@, which allows an intuitive and concise formalisation of such systems. The algorithm is also efficient in presence of a high number of compartments and reactions, therefore Sπ@ represents the starting point for the development of an effective tool for the simulation of biological systems with dynamical structure even in presence of computationally expensive phenomena like diffusion.     

Towards coalgebraic behaviourism

In this paper we show that it is possible to model observable behaviour of coalgebras independently from their internal dynamics, but within the general framework of representing behaviour by a map into a “final” coalgebra.In the first part of the paper we characterise Set-endofunctors F with the property that bisimilarity of elements of F-coalgebras coincides with having the same observable behaviour. We show that such functors have the final coalgebra of a rather simple nature, and preserve some weak pullbacks. We also show that this is the case if and only if F-bisimilarity corresponds to logical equivalence in the finitary fragment of the coalgebraic logic.In the second part of the paper, we present a construction of a “final” coalgebra that captures the observable behaviour of F-coalgebras. We keep the word “final” quoted since the object we are going to construct need not belong to the original category. The construction is carried out for arbitrary Set-endofunctor F, throughout the construction we remain in Set, but the price to pay is the introduction of new morphisms. The paper concludes with a hint to a possible application to modelling weak bisimilarity for coalgebras.     

On the Expressive Power of Polyadic Synchronisation in π-calculus

We extend the π-calculus with polyadic synchronisation, a generalisation of the communication mechanism which allows channel names to be composite. We show that this operator embeds nicely in the theory of π-calculus, and makes it possible to derive divergence-free encodings of distributed calculi. We give a separation result between the π-calculus with polyadic synchronisation (^eπ) and the original calculus, in the style of an analogous result given by Palamidessi for mixed choice. We encode Local Area π showing how to control the local use of resources in ^eπ.     

Fidelity of Gaussian Channels

A noisy Gaussian channel is defined as a channel in which an input field mode is subjected to random Gaussian displacements in phase space. We introduce the quantum fidelity of a Gaussian channel for pure and mixed input states, and we derive a universal scaling law of the fidelity for pure initial states. We also find the maximum fidelity of a Gaussian channel over all input states. Quantum cloning and continuous-variable teleportation are presented as physical examples of Gaussian channels to which the fidelity results can be applied.Presented at the 36th Symposium on Mathematical Physics, “Open Systems & Quantum Information”, Toruń, Poland, June 9–12, 2004.Supported in part by US O.ce of Naval Research Grant No. N00014–03–1–0426.Supported in part by KBN Grant No. PBZ–Min–008/P03/03     

Can LCF be topped? Flat lattice models of typed λ-calculus

Plotkin ((1977) Theoret. Comput. Sci. 5: 223–256) examines the denotational semantics of PCF (essentially typed λ-calculus with arithmetic and looping). The standard Scott semantics V is computationally adequate but not fully abstract; with the addition of some parallel facilities, it becomes fully abstract, and with the addition of an existential operator, denotationally universal. We consider carrying out the same program for , the Scott models built from flat lattices rather than flat cpo's. Surprisingly, no computable extension of PCF can be denotationally universal; perfectly reasonable semantic values such as supremum and Plotkin's “parallel or” cannot be definable. There is an unenlightening fully abstract extension _A (approx), based on Gödel numbering and syntactic analysis. Unfortunately, this is the best we can do; operators defined by PCF-style rules cannot give a fully abstract language. (There is a natural and desirable property, operational extensionality, which prevents full abstraction with respect to .) However, we show that Plotkin's program can be carried out for a nonconfluent evaluator.     

Iterated Function Systems and Control Languages

Valuations—morphisms from (Σ*, ·, e) to ((0, ∞), ·, 1)—are a generalization of Bernoulli morphisms introduced by Eilenberg [“Automata, Languages, and Machines”, Academic Press, New York, 1974]. Here, we show how to generalize the notion of entropy (of a language) in order to obtain new formulas to determine the Hausdorff dimension of fractal sets (also in Euclidean spaces), especially defined via regular (ω-)languages. By doing this, we can sharpen and generalize earlier results in two ways: first, we treat the case where the underlying basic iterated function system contains noncontractive mappings and, second, we obtain results valid for nonregular languages as well.     

Mobile Objects as Mobile Processes

Obliq is a lexically scoped, distributed, object-based programming language. In Obliq, the migration of an object is proposed as creating a clone of the object at the target site, whereafter the original object is turned into an alias for the clone. Obliq has only an informal semantics, so there is no proof that this style of migration is safe, i.e., transparent to object clients. In previous work, we introduced Ø, an abstraction of Obliq, where, by lexical scoping, sites have been abstracted away. We used Ø in order to exhibit how the semantics behind Obliq's implementation renders migration unsafe. We also suggested a modified semantics that we conjectured instead to be safe. In this paper, we rewrite our modified semantics of Ø in terms of the π-calculus, and we use it to formally prove the correctness of object surrogation, the abstraction of object migration in Ø.     

Language Simplification through Error-Correcting and Grammatical Inference Techniques

In many language processing tasks, most of the sentences generally convey rather simple meanings. Moreover, these tasks have a limited semantic domain that can be properly covered with a simple lexicon and a restricted syntax. Nevertheless, casual users are by no means expected to comply with any kind of formal syntactic restrictions due to the inherent spontaneous nature of human language. In this work, the use of error-correcting-based learning techniques is proposed to cope with the complex syntactic variability which is generally exhibited by natural language. In our approach, a complex task is modeled in terms of a basic finite state model, F, and a stochastic error model, E. F should account for the basic (syntactic) structures underlying this task, which would convey the meaning. E should account for general vocabulary variations, word disappearance, superfluous words, and so on. Each natural user sentence is thus considered as a corrupted version (according to E) of some simple sentence of L(F). Adequate bootstrapping procedures are presented that incrementally improve the structure of F while estimating the probabilities for the operations of E. These techniques have been applied to a practical task of moderately high syntactic variability, and the results which show the potential of the proposed approach are presented.     

On the Power of Multiple Reads in a Chip

A chip algorithm is called r-multilective if it reads its input bits r times. In this paper we relate the r-bound communication complexity of a language L and the area requirement for an r-multilective chip algorithm of a related language . More specifically Improving known lower bounds on the r-bound communication complexity of certain languages, we obtain several hierarchies of r-multilective languages depending on the parameter r. For example, if 0 < r < s, then there are constants 0 < c, c′ such that for infinitely many n there is a language L_n {0, 1}ⁿ such that there is an s-multilective algorithm recognizing L_n using area at most c log n and any r-multilective algoerithm recognizing L_n requires area at least c′n/log n. Similar results have been known only for s = 2 and r = 1 and have been open in other cases.     

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.     

On the Expressiveness of Chi, Update, and Fusion calculi

Chi and Update calculi [9,17] have been independently introduced in order to model mobile systems. The two calculi are very close to each other and represent an evolution of π-calculus [15]. More recently a (non-straightforward) polyadic version of the Update calculus, the Fusion calculus, has been proposed [18].In the paper we give a fully abstract encoding from an asynchronous variant of Chi and Update calculi to asynchronous π-calculus [11,4]. This proves that, at least for their asynchronous variants, Chi and Update calculi are not more expressive than π-calculus. A similar result can be proved for the Fusion calculus.     

Languages Defined with Modular Counting Quantifiers

We prove that a regular language defined by a boolean combination of generalized Σ₁-sentences built using modular counting quantifiers can be defined by a boolean combination of Σ₁-sentences in which only regular numerical predicates appear. The same statement, with “Σ₁” replaced by “first-order,” is equivalent to the conjecture that the nonuniform circuit complexity class ACC is strictly contained in NC¹. The argument introduces some new techniques, based on a combination of semigroup theory and Ramsey theory, which may shed some light on the general case.     

Infinitary logics and 0–1 laws

We investigate the infinitary logic L_∞ω^ω, in which sentences may have arbitrary disjunctions and conjunctions, but they involve only finite numbers of distinct variables. We show that various fixpoint logics can be viewed as fragments of L_∞ω^ω, and we describe a game-theoretic characterization of the expressive power of the logic. Finally, we study asymptotic probabilities of properties expressible in L_∞ω^ω on finite structures. We show that the 0–1 law holds for L_∞ω^ω, i.e., the asymptotic probability of every sentence in this logic exists and is equal to either 0 or 1. This result subsumes earlier work on asymptotic probabilities for various fixpoint logics and reveals the boundary of 0–1 laws for infinitary logics.     

Collecting Statistics over Runtime Executions

By collecting statistics over runtime executions of a program we can answer complex queries, such as “what is the average number of packet retransmissions” in a communication protocol, or “how often does process P₁ enter the critical section while process P₂ waits” in a mutual exclusion algorithm. We present an extension to linear-time temporal logic that combines the temporal specification with the collection of statistical data. By translating formulas of this language to alternating automata we obtain a simple and efficient query evaluation algorithm. We illustrate our approach with examples and experimental results.     

Analytic evaluation of contention protocols used in distributed real-time systems

The probability of a station failing to deliver packets before their deadlines, called theprobability of dynamic failure, P _dyn, is an important measure for the communication subsystem of a distributed real-time system. Another closely-related performance measure is the -bounded delivery time,T , which is defined as the least time needed to deliver a packet with probability greater than 1–. UsingP _dyn andT , we comparatively evaluate four contention protocols often used in distributed real-time systems: (i) the token passing protocol and its priority-based variation (called thetoken scheduling protocol), and (ii) theP _i-persistent protocol and a priority-based variation thereof. The communication subsystem equipped with different contention protocols is modeled first as embedded Markov chains. Then, we derive the probability distributions of access delay, from whichP _dyn andT can be calculated. The blocking probability,Q _i, can also be derived from the access delay distribution. These measures are derived first under the assumption of a single buffer at each station. The single-buffer model is then extended to the multiple-buffer case. The effects of buffer size onP _dyn,T , andQ _i, and the performance improvement with multiple buffers are analyzed over a wide range of network traffic.The work reported in this paper was supported in part by the ONR under Grant N00014-92-J—1080. Any opinions, findings, and conclusions or recommendations expressed in this paper are those of the authors and do not necessarily reflect the views of the ONR.     

Structured coalgebras and minimal HD-automata for the -calculus

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.