
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.

Spatial aspects of computation are becoming increasingly relevant in Computer
Science, especially in the field of collective adaptive systems and when
dealing with systems distributed in physical space. Traditional formal
verification techniques are well suited to analyse the temporal evolution of
programs; however, properties of space are typically not taken into account
explicitly. We present a topologybased approach to formal verification of
spatial properties depending upon physical space. We define an appropriate
logic, stemming from the tradition of topological interpretations of modal
logics, dating back to earlier logicians such as Tarski, where modalities
describe neighbourhood. We lift the topological definitions to the more general
setting of closure spaces, also encompassing discrete, graphbased structures.
We extend the framework with a spatial surrounded operator, a propagation
operator and with some collective operators. The latter are interpreted over
arbitrary sets of points instead of individual points in space. We define
efficient model checking procedures, both for the individual and the collective
spatial fragments of the logic and provide a proofofconcept tool.

Collective Adaptive Systems (CAS) consist of a large number of spatially
distributed heterogeneous entities with decentralised control and varying
degrees of complex autonomous behaviour that may be competing for shared
resources even when collaborating to reach common goals. It is important to
carry out thorough quantitative modelling and analysis and verification of
their design to investigate all aspects of their behaviour before they are put
into operation. This requires combinations of formal methods and applied
mathematics which moreover scale to largescale CAS. The primary goal of
FORECAST is to raise awareness in the software engineering and formal methods
communities of the particularities of CAS and the design and control problems
which they bring.

In open systems, i.e. systems operating in an environment that they cannot
control and with components that may join or leave, behaviors can arise as side
effects of intensive components interaction. Finding ways to understand and
design these systems and, most of all, to model the interactions of their
components, is a difficult but important endeavor. To tackle these issues, we
present AbC, a calculus for attributebased communication. An AbC system
consists of a set of parallel agents each of which is equipped with a set of
attributes. Communication takes place in an implicit multicast fashion, and
interactions among agents are dynamically established by taking into account
"connections" as determined by predicates over the attributes of agents. First,
the syntax and the semantics of the calculus are presented, then expressiveness
and effectiveness of AbC are demonstrated both in terms of modeling scenarios
featuring collaboration, reconfiguration, and adaptation and of the possibility
of encoding channelbased interactions and other interaction patterns.
Behavioral equivalences for AbC are introduced for establishing formal
relationships between different descriptions of the same system.

In this paper we present CARMA, a language recently defined to support
specification and analysis of collective adaptive systems. CARMA is a
stochastic process algebra equipped with linguistic constructs specifically
developed for modelling and programming systems that can operate in openended
and unpredictable environments. This class of systems is typically composed of
a huge number of interacting agents that dynamically adjust and combine their
behaviour to achieve specific goals. A CARMA model, termed a collective,
consists of a set of components, each of which exhibits a set of attributes. To
model dynamic aggregations, which are sometimes referred to as ensembles, CARMA
provides communication primitives that are based on predicates over the
exhibited attributes. These predicates are used to select the participants in a
communication. Two communication mechanisms are provided in the CARMA language:
multicastbased and unicastbased. In this paper, we first introduce the basic
principles of CARMA and then we show how our language can be used to support
specification with a simple but illustrative example of a sociotechnical
collective adaptive system.

The interplay between process behaviour and spatial aspects of computation
has become more and more relevant in Computer Science, especially in the field
of collective adaptive systems, but also, more generally, when dealing with
systems distributed in physical space. Traditional verification techniques are
well suited to analyse the temporal evolution of programs; properties of space
are typically not explicitly taken into account. We propose a methodology to
verify properties depending upon physical space. We define an appropriate
logic, stemming from the tradition of topological interpretations of modal
logics, dating back to earlier logicians such as Tarski, where modalities
describe neighbourhood. We lift the topological definitions to a more general
setting, also encompassing discrete, graphbased structures. We further extend
the framework with a spatial until operator, and define an efficient model
checking procedure, implemented in a proofofconcept tool.

Two of the most studied extensions of trace and testing equivalences to
nondeterministic and probabilistic processes induce distinctions that have been
questioned and lack properties that are desirable. Probabilistic
tracedistribution equivalence differentiates systems that can perform the same
set of traces with the same probabilities, and is not a congruence for parallel
composition. Probabilistic testing equivalence, which relies only on extremal
success probabilities, is backward compatible with testing equivalences for
restricted classes of processes, such as fully nondeterministic processes or
generative/reactive probabilistic processes, only if specific sets of tests are
admitted. In this paper, new versions of probabilistic trace and testing
equivalences are presented for the general class of nondeterministic and
probabilistic processes. The new trace equivalence is coarser because it
compares execution probabilities of single traces instead of entire trace
distributions, and turns out to be compositional. The new testing equivalence
requires matching all resolutions of nondeterminism on the basis of their
success probabilities, rather than comparing only extremal success
probabilities, and considers success probabilities in a tracebytrace fashion,
rather than cumulatively on entire resolutions. It is fully backward compatible
with testing equivalences for restricted classes of processes; as a
consequence, the tracebytrace approach uniformly captures the standard
probabilistic testing equivalences for generative and reactive probabilistic
processes. The paper discusses in full details the new equivalences and
provides a simple spectrum that relates them with existing ones in the setting
of nondeterministic and probabilistic processes.

A novel, scalable, onthefly modelchecking procedure is presented to verify
bounded PCTL properties of selected individuals in the context of very large
systems of independent interacting objects. The proposed procedure combines
onthefly model checking techniques with deterministic meanfield
approximation in discrete time. The asymptotic correctness of the procedure is
shown and some results of the application of a prototype implementation of the
FlyFast modelchecker are presented.

In the paper "Relating Strong Behavioral Equivalences for Processes with
Nondeterminism and Probabilities" to appear in TCS, we present a comparison of
behavioral equivalences for nondeterministic and probabilistic processes. In
particular, we consider strong trace, failure, testing, and bisimulation
equivalences. For each of these groups of equivalences, we examine the
discriminating power of three variants stemming from three approaches that
differ for the way probabilities of events are compared when nondeterministic
choices are resolved via deterministic schedulers. The established
relationships are summarized in a socalled spectrum. However, the equivalences
we consider in that paper are only a small subset of those considered in the
original spectrum of equivalences for nondeterministic systems introduced by
Rob van Glabbeek. In this companion paper we we enlarge the spectrum by
considering variants of trace equivalences (completedtrace equivalences),
additional decoratedtrace equivalences (failuretrace, readiness, and
readytrace equivalences), and variants of bisimulation equivalences (kernels
of simulation, completedsimulation, failuresimulation, and readysimulation
preorders). Moreover, we study how the spectrum changes when randomized
schedulers are used instead of deterministic ones.

We present a spectrum of tracebased, testing, and bisimulation equivalences
for nondeterministic and probabilistic processes whose activities are all
observable. For every equivalence under study, we examine the discriminating
power of three variants stemming from three approaches that differ for the way
probabilities of events are compared when nondeterministic choices are resolved
via deterministic schedulers. We show that the first approach  which compares
two resolutions relatively to the probability distributions of all considered
events  results in a fragment of the spectrum compatible with the spectrum of
behavioral equivalences for fully probabilistic processes. In contrast, the
second approach  which compares the probabilities of the events of a
resolution with the probabilities of the same events in possibly different
resolutions  gives rise to another fragment composed of coarser equivalences
that exhibits several analogies with the spectrum of behavioral equivalences
for fully nondeterministic processes. Finally, the third approach  which only
compares the extremal probabilities of each event stemming from the different
resolutions  yields even coarser equivalences that, however, give rise to a
hierarchy similar to that stemming from the second approach.