The link-calculus homepage

"Increased expressiveness is not a theoretical luxury, but an eminently practical goal, since formal specification languages should describe as simply and naturally as possible the widest possible class of systems" -- José Meseguer

Link-calculus - without mobility - Core Network Algebra (CNA) (subsumes CCS)
Traditionally in process algebras, communication is based on send/receive synchronisation on specific channels. In link-calculus, instead, action prefixes are given in terms of links that record the source (input) and the target (output) ends of each hop of interactions. Links can be combined in link chains in order to describe how information can be routed across processes before arriving at destination. Thus, communication is inherently multiparty. Link-calculus also allows for uncomplete interactions by the way of virtual links, i.e. free spaces in a link-chain that can eventually accept other processes to interact with.

Link-calculus - with mobility (subsumes pi-calculus)
The interaction mechanism is the one described for CNA. Here, interactions make use of a data tuple. Each participant can provide data or variables to be members of the data tuple. Thus, all participants are peers, as they can send and receive data in the same interaction.

chained Core Network Algebra (cCNA) The generalisation of link prefixes to chain prefixes is very expressive to encode some simple patterns of interaction directly in the action prefixes, thus enhancing the modelling power.

Some results

Membranes as processes

The link-calculus interaction mechanism forms link chains composed by link prefixes. This allows us to encode membranes, or more in general localities as processes that participate to the interaction. In fact, membranes play an active role in the process interaction: they allow or block the interaction depending on how processes are located.
It follows that calculi with membranes are intrinsecally multiparty. This figure shows how the movement of an ambient into another one is realized as a three-party interaction.

Bisimilarity is a congruence

Notably, bisimilarity equivalence is a congruence also w.r.t. substitutions and prefixing. Basically, this is due to the fact that in link-calculus these two processes:

are not bisimilar, whereas, e.g., in CCS the following holds:
but when b is replaced by a the two processes are no longer bisimilar, because the first can perform a silent action.

Rougly, we can say that link bisimulatio(without mobility) is somehow less restrictive than CCS strong bisimulation and more restrictive than CCS weak bisimulation.

Communication backbone

Thanks to the expressivity of the chained link-calculus (cCNA), it is possible to divide the processes involved in an interaction in two sets: the set of processes providing the links that define the so-called backbone of the interaction, defining the whole path to follow from end to end and the set of processes providing those solid links that fill the virtual links in the backbone.

Symbolic Link Modal Logic

The symbolic Link Modal Logic, defined on top of the symbolic semantics for the link-calculus, is a smooth extension of the Hennessy-Milner logic which is able to characterize the (symbolic) transitions of CNA processes. Moreover, similar to CCS, link bisimilar processes (without mobility) satisfy the same formulas in this logic.