
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.

Coordination is essential for dynamic distributed systems whose components
exhibit interactive and autonomous behaviors. Spatially distributed, locally
interacting, propagating computational fields are particularly appealing for
allowing components to join and leave with little or no overhead. Computational
fields are a key ingredient of aggregate programming, a promising software
engineering methodology particularly relevant for the Internet of Things. In
our approach, space topology is represented by a fixed graphshaped field,
namely a network with attributes on both nodes and arcs, where arcs represent
interaction capabilities between nodes. We propose a SMuC calculus where
mucalculus like modal formulas represent how the values stored in neighbor
nodes should be combined to update the present node. Fixpoint operations can be
understood globally as recursive definitions, or locally as asynchronous
converging propagation processes. We present a distributed implementation of
our calculus. The translation is first done mapping SMuC programs into normal
form, purely iterative programs and then into distributed programs. Some key
results are presented that show convergence of fixpoint computations under fair
asynchrony and under reinitialization of nodes. The first result allows nodes
to proceed at different speeds, while the second one provides robustness
against certain kinds of failure. We illustrate our approach with a case study
based on a disaster recovery scenario, implemented in a prototype simulator
that we use to evaluate the performance of a recovery strategy.

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.

Soft Constraint Logic Programming is a natural and flexible declarative
programming formalism, which allows to model and solve reallife problems
involving constraints of different types.
In this paper, after providing a slightly more general and elegant
presentation of the framework, we show how we can apply it to the emobility
problem of coordinating electric vehicles in order to overcome both energetic
and temporal constraints and so to reduce their running cost. In particular, we
focus on the journey optimization subproblem, considering sequences of trips
from a user's appointment to another one. Solutions provide the best
alternatives in terms of time and energy consumption, including route sequences
and possible charging events.

We present a formal model to represent and solve the unicast/multicast
routing problem in networks with Quality of Service (QoS) requirements. To
attain this, first we translate the network adapting it to a weighted graph
(unicast) or andor graph (multicast), where the weight on a connector
corresponds to the multidimensional cost of sending a packet on the related
network link: each component of the weights vector represents a different QoS
metric value (e.g. bandwidth, cost, delay, packet loss). The second step
consists in writing this graph as a program in Soft Constraint Logic
Programming (SCLP): the engine of this framework is then able to find the best
paths/trees by optimizing their costs and solving the constraints imposed on
them (e.g. delay < 40msec), thus finding a solution to QoS routing problems.
Moreover, csemiring structures are a convenient tool to model QoS metrics. At
last, we provide an implementation of the framework over scalefree networks
and we suggest how the performance can be improved.

In this paper we compare three different formalisms that can be used in the
area of models for distributed, concurrent and mobile systems. In particular we
analyze the relationships between a process calculus, the Fusion Calculus,
graph transformations in the Synchronized Hyperedge Replacement with Hoare
synchronization (HSHR) approach and logic programming. We present a translation
from Fusion Calculus into HSHR (whereas Fusion Calculus uses Milner
synchronization) and prove a correspondence between the reduction semantics of
Fusion Calculus and HSHR transitions. We also present a mapping from HSHR into
a transactional version of logic programming and prove that there is a full
correspondence between the two formalisms. The resulting mapping from Fusion
Calculus to logic programming is interesting since it shows the tight analogies
between the two formalisms, in particular for handling name generation and
mobility. The intermediate step in terms of HSHR is convenient since graph
transformations allow for multiple, remote synchronizations, as required by
Fusion Calculus semantics.

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.