Editors: Maurice ter Beek, Marjan Sirjani

A recurrent task in coordinated systems is managing (estimating, predicting,or controlling) signals that vary in space, such as distributed sensed data orcomputation outcomes. Especially in large-scale settings, the problem can beaddressed through decentralised and situated computing systems: nodes canlocally sense, process, and act upon signals, and coordinate with neighbours toimplement collective strategies. Accordingly, in this work we devisedistributed coordination strategies for the estimation of a spatial phenomenonthrough collaborative adaptive sampling. Our design is based on the idea ofdynamically partitioning space into regions that compete and grow/shrink toprovide accurate aggregate sampling. Such regions hence define a sort ofvirtualised space that is "fluid", since its structure adapts in response topressure forces exerted by the underlying phenomenon. We provide an adaptivesampling algorithm in the field-based coordination framework, and prove it isself-stabilising and locally optimal. Finally, we verify by simulation that theproposed algorithm effectively carries out a spatially adaptive sampling whilemaintaining a tuneable trade-off between accuracy and efficiency.

We tackle the problem of establishing the soundness of approximatebisimilarity with respect to PCTL and its relaxed semantics. To this purpose,we consider a notion of bisimilarity inspired by the one introduced byDesharnais, Laviolette, and Tracol, and parametric with respect to anapproximation error $\delta$, and to the depth $n$ of the observation alongtraces. Essentially, our soundness theorem establishes that, when a state $q$satisfies a given formula up-to error $\delta$ and steps $n$, and $q$ isbisimilar to $q'$ up-to error $\delta'$ and enough steps, we prove that $q'$also satisfies the formula up-to a suitable error $\delta"$ and steps $n$. Thenew error $\delta"$ is computed from $\delta$, $\delta'$ and the formula, andonly depends linearly on $n$. We provide a detailed overview of our soundnessproof. We extend our bisimilarity notion to families of states, thus obtainingan asymptotic equivalence on such families. We then consider an asymptoticsatisfaction relation for PCTL formulae, and prove that asymptoticallyequivalent families of states asymptotically satisfy the same formulae.

We introduce a meta-model based on formal languages, dubbed formalchoreographic languages, to study message-passing systems. Our framework allowsus to generalise standard constructions from the literature and to comparethem. In particular, we consider notions such as global view, local view, andprojections from the former to the latter. The correctness of local viewsprojected from global views is characterised in terms of a closure property. Weconsider a number of communication properties -- such as (dead)lock-freedom --and give conditions on formal choreographic languages to guarantee them.Finally, we show how formal choreographic languages can capture existingformalisms; specifically we consider communicating finite-state machines,choreography automata, and multiparty session types. Notably, formalchoreographic languages, differently from most approaches in the literature,can naturally model systems exhibiting non-regular behaviour.

Existing models for the analysis of concurrent processes tend to focus onfail-stop failures, where processes are either working or permanently stopped,and their state (working/stopped) is known. In fact, systems are often affectedby grey failures: failures that are latent, possibly transient, and may affectthe system in subtle ways that later lead to major issues (such as crashes,limited availability, overload). We introduce a model of actor-based systemswith grey failures, based on two interlinked layers: an actor model, given asan asynchronous process calculus with discrete time, and a failure model thatrepresents failure patterns to inject in the system. Our failure model capturesnot only fail-stop node and link failures, but also grey failures (e.g.,partial, transient). We give a behavioural equivalence relation based on weakbarbed bisimulation to compare systems on the basis of their ability to recoverfrom failures, and on this basis we define some desirable properties ofreliable systems. By doing so, we reduce the problem of checking reliabilityproperties of systems to the problem of checking bisimulation.