Encoding Distributed Areas and Local Communication into the π-Calculus

We show how the π-calculus can express local communications within a distributed system, through an encoding of the local area π-calculus, an enriched system that explicitly represents names which are known universally but always refer to local information. Our translation replaces point-to-point communication with a system of shared local ethers; we prove that this preserves and reflects process behaviour. We give an example based on an internet service dæmon, and investigate some limitations of the encoding.     

Objects in the π-Calculus

Two semantics for a parallel object-oriented programming language are presented. One is a two-level transitional semantics in which the global behaviour of a system is derived directly from the possible actions of its constituent objects. The other is by translation into the π-calculus. A close correspondence between the semantics is established.     

Dynamic Channel Screening in the Higher Order π-Calculus

Recently programming languages have been designed to support mobile code, i.e. higher-order code that is transferred from a remote location or domain and executed within the local environment. This may expose the internal interfaces and objects within a location to attacks by mobile code. In this work, we propose an extension of notations based on the Higher-Order π-calculus with primitive operators, called screening operators, whose role is to protect internal interfaces by dynamically restricting the visibility of channels. The usefulness of these operators is illustrated by applications involving resource access control. We show how restrictions on resource access control can be enforced dynamically in terms of screening operators, and contrast it with an alternative approach in which restrictions on the behaviour of processes are based on the notion of process type [17] and intended to be checked statically.     

A First-Order Syntax for the π-Calculus in Isabelle/HOL using Permutations

A formalized theory of alpha-conversion for the π-calculus in Isabelle/HOL is presented. Following a recent proposal by Gabbay and Pitts, substitutions are modelled in terms of permutations, and alpha-equivalence is defined over all but finitely many names. In contrast to the work by Gabbay and Pitts, however, standard universal and existential quantification are used instead of introducing a new binder.Further, a classification of the various approaches to formalizing languages with binders is presented. Strengths and weaknesses are pointed out, and suggestions for possible applications are made.     

On discrete lower π-strategies

Two-person zero-sum differential games of survival are investigated. It is assumed that player I, as well as player II, can employ during the course of the game any lower π-strategy [2], π(t_i) being a finite partition of [t₀, ∞). The concept of a discrete lower π-strategy is introduced and it is shown that if player I (II) confines himself to the space of discrete lower π-strategies, being a subset of the space of lower π-strategies, then he will be able to force the same lower (upper) value as if he could employ any lower π-strategy. Since we do not use any deep facts about differential games, the results contained here might be extended to continuous games.     

Strong normalisation in the π-calculus

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes.     

Using Assumptions to Distribute Alternation Free μ-Calculus Model Checking

In this work we extend the approach used in [6] to perform distributed-memory AFMC model checking. The part of a system held in one computer is modeled as a Kripke structure with border states. Moreover, we use assumptions about the truth of a formula in each state. Each process then repeatedly executes a slight modification of a standard sequential algorithm and exchanges its results with other processes. In the paper we define the AFMC semantics for structures with border states and assumptions, present the distributed algorithm and show the main ideas behind the proof of its correctness. Complexity and experimental results are provided as well.     

Low voltage fast response display using dual π‐cells with quarter‐wave thickness

In this paper, a design for a fast response display consisting of dual π‐cells is investigated. The thickness of each liquid crystal cell layer is only half of a single LC cell device with the same retardation change, which results in about one quarter of the response time for a single π‐cell device. While this result is obviously anticipated, an additional advantage is that a good viewing angle can be achieved by using negative C plates, which allows a lower cost device with a more uniform black state across the area of the display than the case of a single cell compensated by a discotic compensator. We also propose a solution to solve parallax issue from two‐layer structure of liquid crystal cell, and it opens a window of opportunity for a device with two‐layer structure.     

On the decidability of fragments of the asynchronous π-calculus

We study the decidability of a reachability problem for various fragments of the asynchronous π-calculus. We consider the combination of three main features: name generation, name mobility, and unbounded control. We show that the combination of name generation with either name mobility or unbounded control leads to an undecidable fragment. On the other hand, we prove that name generation without name mobility and with bounded control is decidable by reduction to the coverability problem for Petri Nets.     

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π.     

Factors affecting the dynamics of a π‐cell (Invited Paper)

Abstract— The basic factors related to the dynamics of a π‐cell device are reviewed. Specifically, the director dynamics are studied for the case of a periodic drive voltage that is sometimes referred to as “impulse drive.” It is found for this type of drive waveform the desired bend state is more stable against the twisting effect of transverse electric fields found in AMLCD devices. This effect causes the reduction in light transmission due to “impulse drive” to be smaller in π‐cell devices than is expected to be found in other AMLCD modes.     

Fair Π

In this paper, we define fair computations in the π-calculus [Milner, R., Parrow, J. & Walker, D., A Calculus of Mobile Processes, Part I and II, Information and Computation 100 (1992) 1–78]. We follow Costa and Stirling's approach for CCS-like languages [Costa, G. & Stirling, C., A Fair Calculus of Communicating Systems, Acta Informatica 21 (1984) 417–441, Costa, G. & Stirling, C., Weak and Strong Fairness in CCS, Information and Computation 73 (1987) 207–244] but exploit a more natural labeling method of process actions to filter out unfair process executions. The new labeling allows us to prove all the significant properties of the original one, such as unicity, persistence and disappearance of labels. It also turns out that the labeled π-calculus is a conservative extension of the standard one. We contrast the existing fair testing [Brinksma, E., Rensink, A. & Vogler, W., Fair Testing, Proc. of CONCUR'95, LNCS, 962 (1995) 313–327, Natarajan, V. & Cleaveland, R., Divergence and Fair Testing, Proc. of ICALP '95, LNCS, 944 (1995) 648–659] with those that naturally arise by imposing weak and strong fairness as defined by Costa and Stirling. This comparison provides the expressiveness of the various fair testing-based semantics and emphasizes the discriminating power of the one already proposed in the literature.     

σ-Automata and Chebyshev-polynomials

A σ-automaton is an additive, binary cellular automaton on a graph. For product graphs such as a grids and cylinders, reversibility and periodicity properties of the corresponding σ-automaton can be expressed in terms of a binary version of Chebyshev polynomials. We will give a detailed analysis of the divisibility properties of these polynomials and apply our results to the study of σ-automata.     

A hierarchy of deterministic context-free ω-languages

Twenty years ago, Klaus. W. Wagner came up with a hierarchy of ω-regular sets that actually bears his name. It turned out to be exactly the Wadge hierarchy of the sets of ω-words recognized by deterministic finite automata. We describe the Wadge hierarchy of context-free ω-languages, which stands as an extension of Wagner's work from automata to pushdown automata.