
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.

In this paper we revisit some pioneering efforts to equip Petri nets with
compact operational models for expressing causality. The models we propose have
a bisimilarity relation and a minimal representative for each equivalence
class, and they can be fully explained as coalgebras on a presheaf category on
an index category of partial orders. First, we provide a settheoretic model in
the form of a a causal case graph, that is a labeled transition system where
states and transitions represent markings and firings of the net, respectively,
and are equipped with causal information. Most importantly, each state has a
poset representing causal dependencies among past events. Our first result
shows the correspondence with behavior structure semantics as proposed by
Trakhtenbrot and Rabinovich. Causal case graphs may be infinitelybranching and
have infinitely many states, but we show how they can be refined to get an
equivalent finitelybranching model. In it, states are equipped with
symmetries, which are essential for the existence of a minimal, often
finitestate, model. The next step is constructing a coalgebraic model. We
exploit the fact that events can be represented as names, and event generation
as name generation. Thus we can apply the FioreTuri framework: we model causal
relations as a suitable category of posets with action labels, and generation
of new events with causal dependencies as an endofunctor on this category. Then
we define a wellbehaved category of coalgebras. Our coalgebraic model is still
infinitestate, but we exploit the equivalence between coalgebras over a class
of presheaves and History Dependent automata to derive a compact
representation, which is equivalent to our settheoretical compact model.
Remarkably, state reduction is automatically performed along the equivalence.

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.

This volume contains the preproceedings of ICE'11, the 4th Interaction and
Concurrency Experience workshop, which was held in Reykjavik, Iceland on the
9th of June 2011 as a satellite event of DisCoTec'11.
The topic of ICE'11 was Reliable and Contractbased Interaction. Reliable
interactions are, e.g., those enjoying suitable logical, behavioural, or
security properties, or adhering to certain QoS standards. Contractbased
interactions are, e.g., those where the interacting entities are committed to
give certain guarantees whenever certain assumptions are met by their operating
environment.
The ICE procedure for paper selection allows for PC members to interact,
anonymously, with authors. During the review phase, each submitted paper is
published on a Wiki and associated with a discussion forum whose access is
restricted to the authors and to all the PC members not declaring a conflict of
interests. The PC members post comments and questions that the authors reply
to. Each paper was reviewed by four PC members, and altogether 8 papers (out of
12) were accepted for publication.
We were proud to host three invited talks by Rocco De Nicola (joint with
PACO), Simon Gay and Prakash Panangaden, whose abstracts are included in this
volume together with the regular papers.

This volume contains the proceedings of the 3rd Interaction and Concurrency
Experience (ICE 2010) workshop, which was held in Amsterdam, Netherlands on
10th of June 2010 as a satellite event of DisCoTec'10. Each year, the workshop
focuses on a specific topic: the topic of ICE 2010 was Guaranteed Interactions,
by which we mean, for example, guaranteeing safety, reactivity, quality of
service or satisfaction of analysis hypotheses.

We apply to logic programming some recently emerging ideas from the field of
reductionbased communicating systems, with the aim of giving evidence of the
hidden interactions and the coordination mechanisms that rule the operational
machinery of such a programming paradigm. The semantic framework we have chosen
for presenting our results is tile logic, which has the advantage of allowing a
uniform treatment of goals and observations and of applying abstract
categorical tools for proving the results. As main contributions, we mention
the finitary presentation of abstract unification, and a concurrent and
coordinated abstract semantics consistent with the most common semantics of
logic programming. Moreover, the compositionality of the tile semantics is
guaranteed by standard results, as it reduces to check that the tile systems
associated to logic programs enjoy the tile decomposition property. An
extension of the approach for handling constraint systems is also discussed.