Description of Technical Contributions

1.

The issue of defining a process calculus which supports programming with explicit localities is investigated. We introduce a language which embeds the asynchronous Linda communication paradigm extended with explicit localities in a process calculus. We consider multiple tuple spaces that are distributed over a collections of sites and use localities to distribute/retrieve tuples and processes over/from these sites. The operational semantics of the language turns out to be useful for discussing the language design, e.g. the effects of scoping disciplines over mobile agents which maintain their connections to the located tuple spaces while moving along sites. The flexibility of the language is illustrated by a few examples.

2.

LLinda (Locality based Linda) is a variant of Linda which supports a programming paradigm where agents can migrate from one computing environment to another. In this paper, we define a type system for LLinda that permits statically checking access rights violations of mobile agents. Types are used to describe processes intentions (read, write, execute, ...) relatively to the different localities they are willing to interact with or they want to migrate to. The type system is used to determine the operations that processes want to perform at each locality, to check whether they comply with the declared intentions and whether they have the necessary rights to perform the intended operations at the specific localities.

3.

An automata-based verification environment for the $\pi$-calculus is developed. The environment takes a direct advantage of a general theory which allows to associate ordinary finite state automata to a wide class of $\pi$-calculus agents, so that equivalent automata are associated to equivalent agents. A key feature of the approach is the re-use of efficient algorithms and verification techniques (equivalence checkers and model checkers) which have been developed and implemented for ordinary automata. The verification environment has been implemented on top of an existing verification environment for process calculi: the JACK environment.

4.

Tiles are rewrite rules with side effects, reminiscent of both Plotkin SOS and Meseguer rewriting logic rules. They are well suited for modeling coordination languages, since they can be composed both statically and dynamically via possibly complex synchronization and workflow mechanisms. In this paper, we give a tile-based bisimilarity semantics for the asynchronous $\pi$-calculus of Honda and Tokoro and prove it equivalent to the ordinary semantics. Two kinds of tiles are provided: activity tiles and coordination tiles. Activity tiles specify the basic interactions sequential processes are able to perform, without considering the operational environment where they live. Instead, coordination tiles control the global evolution of programs.

5.

When concurrency is a primitive notion, models of process calculi usually include commuting diamonds and observations of causality links or of abstract locations. However it is still debatable if the existing approaches are natural, or rather if they are an ad hoc addition to the more basic interleaving semantics. In the paper a treatment of concurrent process calculi is proposed where the same operational and abstract concurrent semantics described in the literature now descend from general, uniform notions. More precisely we introduce a tile-based semantics for located CCS and we show it consistent with the ordinary concurrent (via permutation of transitions) and bisimilarity based location semantics. Tiles are rewrite rules with side effects, reminiscent of both Plotkin SOS and Meseguer rewriting logic rules. We argue that the tile model is particularly well suited for defining directly operational and abstract semantics of concurrent process calculi in a compositional style.

6.

In this paper we aim at describing a framework for specifying the behaviour of a wide class of rule-based computational systems. We gathered our inspiration both from the world of term rewriting, in particular from the rewriting logic approach, and of concurrency theory, the structural operational semantics, the context systems and the structured transition systems approaches among others. Our framework recollects many properties from these sources: First, it provides a compositional way to describe both the states and the sequences of transitions performed by a given system, taking into account their distributed nature. Second, a suitable notion of typed proof allows us to recast also those formalisms relying on the notions of synchronization and side-effects to determine the actual behaviour of a system. Moreover, both an operational and an observational semantics can be introduced: Operationally, those sequences of transitions are identified, that denote a family of ``computationally equivalent'' behaviours. Observationally, those states are identified, that denote a family of ``bisimilar'' configurations. Finally, and as a further abstraction step, our framework can be conveniently recasted using double-categories, recovering also its operational semantics.

7.

In this paper we propose a new approach to check history-preserving equivalence for Petri nets. Exploiting this approach, history-preserving bisimulation is proved decidable for the class of finite nets which are n-safe for some n. Moreover, since we map nets on ordinary transition systems, standard results and algorithms can be re-used, yielding for instance the possibility of deriving minimal realizations. The proposed approach can be applied also to other concurrent formalisms based on partial order semantics, like CCS with causality.

8.

In addition to ordinary places, called stable, zero-safe nets are equipped with zero places, which in a stable marking cannot contain any token. An evolution between two stable markings, instead, can be a complex computation called stable transaction, which may use zero places, but which is atomic when seen from stable places: no stable token generated in a transaction can be reused in the same transaction. Every zero-safe net has an ordinary Place-Transition net as its abstract counterpart, where only stable places are maintained, and where every transaction becomes a transition. The two nets allow us to look at the same system from both an abstract and a refined viewpoint. To achieve this result no new interaction mechanism is used, besides the ordinary token-pushing rules of nets. The refined zero-safe nets can be much smaller than their corresponding abstract P/T nets, since they take advantage of a transition synchronization mechanism. For instance, when transactions of unlimited length are possible in a zero safe net, the abstract net becomes infinite, even if the refined net is finite. In the second part of the paper two universal constructions - both following the Petri nets are monoids approach and the collective token philosophy - are used to give evidence of the naturality of our definitions. More precisely, the operational semantics of zero-safe nets is characterized as an adjunction, and the derivation of abstract P/T nets as a coreflection.