Ensuring termination by typability

A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed π-calculus processes. The systems are obtained by successive refinements of the types of the simply typed π-calculus. For all (but one of) the type systems we also present upper bounds to the number of steps well-typed processes take to terminate. The termination proofs use techniques from term rewriting systems. We show the usefulness of the type systems on 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.     

Trust and Partial Typing in Open Systems of Mobile Agents

We present a partially typed semantics for Dπ, a distributed π-calculus. The semantics is designed for mobile agents in open distributed systems in which some sites may harbor malicious intentions. Nonetheless, the semantics guarantees traditional type-safety properties at good locations by using a mixture of static and dynamic type-checking. We show how the semantics can be extended to allow trust between sites, improving performance and expressiveness without compromising type safety.     

Molecular interaction

We introduce and study abstract structures which are suitable for expressing molecular interaction. The abstract structures are able to manage shared resources and to describe the use of shared resources. We show that these structures can provide an interpretation of the π-calculus, a known calculus of communicating concurrent systems. We briefly describe DNA methylation by using the π-calculus. Molecular interactions during DNA methylation imply changes of conformation and other modifications; these changes can be modelled by substitutions. Formally, we use some notions and results of the concurrency theory, particularly related to the π-calculus and multiset semantics.     

Electronic passports – from secure specifications to secure implementations

For some years more and more countries have been introducing electronic passports. A reason for that is the need of higher security of travel documents in an age where people fear terrorism and crime. There are the US requirements for VISA Waiver countries to issue biometric enabled Passports and the European Commission's decision for a chip based storage of facial image and fingerprints in passports issued by EU member states. In this article standards for ePassports in terms of security and the implementations of security mechanisms are analysed.     

Constructing and visualizing chemical reaction networks from pi-calculus models

The π-calculus, in particular its stochastic version the stochastic π-calculus, is a common modeling formalism to concisely describe the chemical reactions occurring in biochemical systems. However, it remains largely unexplored how to transform a biochemical model expressed in the stochastic π-calculus back into a set of meaningful reactions. To this end, we present a two step approach of first translating model states to reaction sets and then visualizing sequences of reaction sets, which are obtained from state trajectories, in terms of reaction networks. Our translation from model states to reaction sets is formally defined and shown to be correct, in the sense that it reflects the states and transitions as they are derived from the continuous time Markov chain-semantics of the stochastic π-calculus. Our visualization concept combines high level measures of network complexity with interactive, table-based network visualizations. It directly reflects the structures introduced in the first step and allows modelers to explore the resulting simulation traces by providing both: an overview of a network’s evolution and a detail inspection on demand.     

Maintenance of mobile system ambients using a process calculus

We propose a formal method to maintain mobile systems placed on dynamically changing environments in this paper. Recently about 200 million people use mobile phones and mobile terminals, and mobile systems have been very popular. Remarkable features of mobile systems like mobile telephone systems and intelligent transport systems (ITSs) are dynamical linking and effects of environments to behavior of systems. To formally specify these systems, π-calculus is extended using the notion of a field, which is a formalization of constraints on communication among processes. Our goal is to find recovering damaged environments for preservation of connectivity among processes using this extension even if accidents occur.     

Discrete-event modeling of multi-agent systems with broadcasting-based parallel composition

Multi-agent systems have been widely used in logistics and manufacturing. In this paper we develop an automaton-based modeling framework for a special type of multi-agent systems, where agents are instantiated from a finite number of finite-state automaton templates, and interactions among agents are characterized via cooperative synchronization and broadcasting. To describe the compositional behavior of all agents, we propose a novel broadcasting-based parallel composition rule and show that it is commutative and associative. The effectiveness of this modeling framework and the parallel composition rule is illustrated in a simple multi-agent system.     

From Flow Logic to static type systems for coordination languages

Coordination languages are often used to describe open-ended systems. This makes it challenging to develop tools for guaranteeing the security of the coordinated systems and the correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper, we show how the insights from the Flow Logic approach can be used to construct a type system for statically ensuring secure access to tuple spaces and safe process migration for an extension of the language Klaim.     

Distributed system contract monitoring

Runtime verification of distributed systems poses various challenges. A pivotal challenge is the choice of howto distribute the monitors themselves across the system.On one hand, centralised monitoringmay result in increased communication overhead and information exposure across locations, while, on the other hand, systems with dynamic topologies and properties are difficult to address using static monitor choreographies. In this paper we present mDPi, a location-aware π-calculus extension for reasoning about the distributed monitoring scenario.We also define numerousmonitoring strategies for a regular expression-based logic, including a novel approach in which monitors migrate to ensure local monitoring. Finally, we present a number of results which emerge from this formalism, justifying our approach.     

Countering overlapping rectangle privacy attack for moving kNN queries

An important class of LBSs is supported by the moving k nearest neighbor (MkNN) query, which continuously returns the k nearest data objects for a moving user. For example, a tourist may want to observe the five nearest restaurants continuously while exploring a city so that she can drop in to one of them anytime. Using this kind of services requires the user to disclose her location continuously and therefore may cause privacy leaks derived from the user's locations. A common approach to protecting a user's location privacy is the use of imprecise locations (e.g., regions) instead of exact positions when requesting LBSs. However, simply updating a user's imprecise location to a location-based service provider (LSP) cannot ensure a user's privacy for an MkNN query: continuous disclosure of regions enable LSPs to refine more precise location of the user. We formulate this type of attack to a user's location privacy that arises from overlapping consecutive regions, and provide the first solution to counter this attack. Specifically, we develop algorithms which can process an MkNN query while protecting the user's privacy from the above attack. Extensive experiments validate the effectiveness of our privacy protection technique and the efficiency of our algorithm.     

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 UTP approach for rTiMo

rTiMo is a real-time version of  TiMo (Timed Mobility), which is a process algebra for mobile distributed systems. In this paper, we investigate the denotational semantics for rTiMo. A trace variable tr is introduced to record the communications among processes as well as the location where the communication action takes place. Based on the formalized model, we study a set of algebraic laws, especially the laws about the migration and communication with real-time constraints. In order to facilitate the algebraic reasoning about the parallel expansion laws, we enrich rTiMo with a form of guarded choice. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.     

Analyzing the dynamics of stigmergetic interactions through pheromone games

The concept of stigmergy provides a simple framework for interaction and coordination in multi-agent systems. However, determining the global system behavior that will arise from local stigmergetic interactions is a complex problem. In this paper we propose to use Game Theory to analyze stigmergetic interactions. We show that a system where agents coordinate by sharing local pheromone information can be approximated by a limiting pheromone game in which different pheromone vectors represent player strategies. This game view allows us to use established methods and solution concepts from game theory to describe the properties of stigmergy based systems. Our goal is to provide a new framework to aid in the understanding and design of pheromone interactions. We demonstrate how we can use this system to determine the long term system behavior of a simple pheromone model, by analyzing the convergence properties of the pheromone update rule in the approximating game. We also apply this model to cases where multiple colonies of agents concurrently optimize different objectives. In this case a limiting colony game can be linked to colony level interactions to characterize the global system behavior.     

I-index for quantifying an urban location's irreplaceability

A location's irreplaceability refers to the degree of difficulty with which it can be replaced by other locations. For example, the irreplaceability of airports, hospitals, and ATMs varies, and that between hospitals is also different. They differ in both the number of users and the extent of service area. Quantifying the location's irreplaceability provides guidance for urban planning, such as siting of public resources. Existing methods for quantifying an urban location's irreplaceability do not consider human activity at the location, therefore the revealed irreplaceability may deviate from the resident's perceptions. To address this issue, we use origin-destination flows to reflect human activity. We propose a flow-based locational measure, I-index, to quantify the location's irreplaceability. It can be viewed as ‘H-index of flow’ where we regard locations as scientists, flows as papers. I-index of a location is the maximum value of i such that at least i flows with a length of at least α 1 i meters have reached this location, where α is the conversion factor that can be determined adaptively from the flow dataset. I-index elegantly combines the flow volume and length into a single value. The effectiveness of the I-index is validated by simulation experiments. Two case studies show that the hospital's irreplaceability strongly correlates with the hospital bypass behavior and locations with strongly mixed urban functions are more irreplaceable. The implications for urban planning are further discussed.     

Making data-centric storage adaptive and cost-optimal

We present an adaptive and cost-optimal mechanism called Tug-of-War (ToW) for data storage and query mechanism in wireless sensor networks. ToW is based on the concept of data-centric storage (DCS), where a unique home location is used to store events of a given type so that queries of the event type can be directed to the location without flooding. However, rather than using just a single home location, the mechanism can dynamically adjust the number of home locations according to the event and query rates ratio so as to minimize the total communication cost. We also generalize the framework so that different schemes can be used to construct home locations as well as to ensure rendezvous of events and queries, thereby to fine-tune the system performance.     

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.