
Assigning a satisfactory truly concurrent semantics to Petri nets with
confusion and distributed decisions is a long standing problem, especially if
one wants to resolve decisions by drawing from some probability distribution.
Here we propose a general solution based on a recursive, static decomposition
of (occurrence) nets in loci of decision, called structural branching cells
(scells). Each scell exposes a set of alternatives, called transactions. Our
solution transforms a given Petri net into another net whose transitions are
the transactions of the scells and whose places are those of the original net,
with some auxiliary structure for bookkeeping. The resulting net is
confusionfree, and thus conflicting alternatives can be equipped with
probabilistic choices, while nonintersecting alternatives are purely concurrent
and their probability distributions are independent. The validity of the
construction is witnessed by a tight correspondence with the recursively
stopped configurations of Abbes and Benveniste. Some advantages of our approach
are that: i) scells are defined statically and locally in a compositional way;
ii) our resulting nets faithfully account for concurrency.

Event structures are a widely accepted model of concurrency. In a seminal
paper by Nielsen, Plotkin and Winskel, they are used to establish a bridge
between the theory of domains and the approach to concurrency proposed by
Petri. A basic role is played by an unfolding construction that maps (safe)
Petri nets into a subclass of event structures where each event has a uniquely
determined set of causes, called prime event structures, which in turn can be
identified with their domain of configurations. At a categorical level, this is
nicely formalised by Winskel as a chain of coreflections. Contrary to prime
event structures, general event structures allow for the presence of
disjunctive causes, i.e., events can be enabled by distinct minimal sets of
events. In this paper, we extend the connection between Petri nets and event
structures in order to include disjunctive causes. In particular, we show that,
at the level of nets, disjunctive causes are well accounted for by persistent
places. These are places where tokens, once generated, can be used several
times without being consumed and where multiple tokens are interpreted
collectively, i.e., their histories are inessential. Generalising the work on
ordinary nets, Petri nets with persistence are related to a new class of event
structures, called locally connected, by means of a chain of coreflection
relying on an unfolding construction.

Variants of the must testing approach have been successfully applied in
Service Oriented Computing for analysing the compliance between (contracts
exposed by) clients and servers or, more generally, between two peers. It has
however been argued that multiparty scenarios call for more permissive notions
of compliance because partners usually do not have full coordination
capabilities. We propose two new testing preorders, which are obtained by
restricting the set of potential observers. For the first preorder, called
uncoordinated, we allow only sets of parallel observers that use different
parts of the interface of a given service and have no possibility of
intercommunication. For the second preorder, that we call individualistic, we
instead rely on parallel observers that perceive as silent all the actions that
are not in the interface of interest. We have that the uncoordinated preorder
is coarser than the classical must testing preorder and finer than the
individualistic one. We also provide a characterisation in terms of decorated
traces for both preorders: the uncoordinated preorder is defined in terms of
mustsets and Mazurkiewicz traces while the individualistic one is described in
terms of classes of filtered traces that only contain designated visible
actions and mustsets.

A quite flourishing research thread in the recent literature on
componentbased systems is concerned with the algebraic properties of different
classes of connectors. In a recent paper, an algebra of stateless connectors
was presented that consists of five kinds of basic connectors, namely symmetry,
synchronization, mutual exclusion, hiding and inaction, plus their duals, and
it was shown how they can be freely composed in series and in parallel to model
sophisticated 'glues'. In this paper we explore the expressiveness of stateful
connectors obtained by adding oneplace buffers or unbounded buffers to the
stateless connectors. The main results are: i) we show how different classes of
connectors exactly correspond to suitable classes of Petri nets equipped with
compositional interfaces, called nets with boundaries; ii) we show that the
difference between strong and weak semantics in stateful connectors is
reflected in the semantics of nets with boundaries by moving from the classic
step semantics (strong case) to a novel banking semantics (weak case), where a
step can be executed by taking some 'debit' tokens to be given back during the
same step; iii) we show that the corresponding bisimilarities are congruences
(w.r.t. composition of connectors in series and in parallel); iv) we show that
suitable monoidality laws, like those arising when representing stateful
connectors in the tile model, can nicely capture concurrency (in the sense of
step semantics) aspects; and v) as a side result, we provide a basic algebra,
with a finite set of symbols, out of which we can compose all P/T nets with
boundaries, fulfilling a long standing quest.

Contracts are a wellestablished approach for describing and analyzing
behavioral aspects of web service compositions. The theory of contracts comes
equipped with a notion of compatibility between clients and servers that
ensures that every possible interaction between compatible clients and servers
will complete successfully. It is generally agreed that real applications often
require the ability of exposing just partial descriptions of their behaviors,
which are usually known as abstract processes. We propose a formal
characterization of abstraction as an extension of the usual symbolic
bisimulation and we recover the notion of abstraction in the context of
contracts.