Introduction

Collective Adaptive Systems (CAS) are systems consisting of many interacting components ("agents") which exhibit complex behaviours depending on their attributes, objectives and actions [1]. Such systems consist of both physical and virtual entities, often geographically distributed, and are capable to react to changes in the environment they operate in. Usually, a CAS component contains three main blocks: Knowledge, that contains local and global data and information; Policies, that define how different entities should interact, combine and compute; Processes, that describe how the component progresses. Global behaviour of the system emerge from the interaction between the components [2].

In these scenarios, new robust engineering techniques and programming paradigms, with solid theoretical foundations, are sought. However, traditional interaction models based on channels or point-to-point communication, as formalised in calculi such as CCS and 𝜋-calculus, appear to be inadequate and non-scalable; hence, new formal models for CAS are currently being investigated. An important example is AbC [3], a calculus inspired by SCEL [4] and based on attribute-based communication. In this model, communication is broadcast-based, as in CBS [5], but the receivers are dynamically identified by means of predicates: only the nodes whose state satisfies a given property will actually receive the message. Thus, attribute-based communication frees the nodes from knowing each other's identities, allowing for a scalable, decoupled interaction. In fact, attribute-based communication has been integrated also in declarative programming paradigms, e.g. ECA rule-based languages for "smart" systems [6,7].

However, there is a tension between the objective nature of messages and the fact that the same message can be accessed differently by agents with different knowledge. This is evident in the case of messages containing restricted names (akin secret keys): an agent receives a "restricted", projected version of the message, where the unknown names have been removed.

In this paper, we solve this tension by renouncing to the idea that messages have an absolute, "platonistic" meaning whose shadows is all what different agents can observed. Instead, we embrace the empiricistic principle that a message has no meaning on its own, but can be "experienced" by an observer-and clearly, different agents can experience the same message in different ways, according to their knowledge, processes, policies. We call this model subjective communication, since the meaning of a message is not fixed a priori: when a communication occurs, the very same message is delivered to all nodes, but the actual value received by each of them depends on their internal state.

In order to model and reason about concurrent systems interacting via subjective communications, in this paper we introduce the Subjective Communication Calculus SCC. In this calculus, each agent is composed by an internal state and a process, defining its behaviour. A component can broadcast a message, which is actually a (partial) function from components to values. Every component receives such function and evaluates it on itself; thus, different agents may obtain different values from the very same function-or nothing at all. This model generalizes attribute-based communication: a message that in AbC is discarded by a node corresponds to a message whose evaluation on that node's state is undefined.

Given this definition of subjective communication, we need to specify where is the control logic that decides how to modify or filter the messages that an agent will receive. We found two possibilities, yielding two different semantics. One possibility is that the agent itself checks each message and decides how to interpret it (i.e. it evaluates the function on itself, Fig. 1a); the other is that an external entity enforces this check, and then passes the evaluated message (i.e. the return value) to the agent (Fig. 1b). These possibilities, which we Direct Subjective Communication (DSCC, Section 2.1) and Indirect Subjective Communication (ISCC, Section 2.2), respectively, correspond to two common approaches to "smart" computation, namely, edge vs cloud computing.

Furthermore, we give the definition of stateless bisimilarity over processes, and prove that it is compositional for both direct and indirect semantics. Synopsis. In Section 2 we introduce syntax and the two semantics of SCC. An extended example is presented in Section 3. Stateless bisimilarity for SCC is introduced and studied in Section 4. Some conclusions are drawn in Section 5.

A calculus for Subjective Communication

In this section we introduce the syntax and two operational semantics for SCC We define a (collective) system 𝐶 as a collection of parallel components of the form Γ : 𝑃 , where 𝑃 is a process and Γ : 𝒜 → 𝒱 is an environment i.e. a map from a set 𝒜 of attribute identifiers to values 𝒱, representing the current internal state of the component. The special ⊥ represents undefined. Processes are the building blocks of components: they define the behaviour of the component itself, whereas the environment defines the memory. We assume a set of expressions 𝑒 ∈ ℰ and a set of predicates 𝜙 ∈ Φ over a fixed set of term variables 𝒳 . The evaluation of an expression 𝑒 w.r.t. store Γ is denoted as 𝑒 Γ , which yields a value 𝑣 (possibly ⊥). We do not enforce an expression syntax to remain more general. The evaluation is defined as usual, with the requirement that it is defined only on ground expressions, i.e. expressions with no free variable; thus: if fv(𝑒) ̸ = ∅ then 𝑒 Γ = ⊥. This means, for instance, that in an arithmetic context 0 × 𝑥 Γ = ⊥, instead of 0 as one may expect. The evaluation is extended to logical predicates as usual.

The complete syntax of SC is defined in terms of processes and components:

𝒫 𝑃, 𝑄 ::= 0 ⃒ ⃒ 𝑃 |𝑄 ⃒ ⃒ 𝑃 + 𝑄 ⃒ ⃒ 𝜙?𝑃 : 𝑄 ⃒ ⃒ ⟨𝑓 ⟩𝑄 ⃒ ⃒ (𝑥)𝑃 ⃒ ⃒ 𝐾(𝑒 ⃗) ⃒ ⃒ [𝑙 := 𝑒]𝑃 𝒞 𝐶 ::= Γ : 𝑃 ⃒ ⃒ 𝐶‖𝐶 ⃒ ⃒ 𝜈𝑥𝐶

The behaviour of a single component is defined by a process which can: 𝐾(𝑒 ⃗) call a process named 𝐾, instantiating the parameters with the list 𝑒 ⃗. This construct enables looping of processes (using recursion);

0

[𝑙 := 𝑒]𝑃 update its local memory, by updating the cell identified by the label 𝑙 with the value of 𝑒 (if not ⊥).

Components can be assembled into systems:

Γ : 𝑃 is a single component, with a process 𝑃 running on a store Γ.

𝐶‖𝐶 is a parallel of multiple components;

𝜈𝑥𝐶 is a system with a fresh, local name, a la 𝜋-calculus.

Processes and systems are taken up-to a congruence expressing the fact that they can be denoted in different but equivalent ways. This is useful both to simplify the writing of some semantic rules (e.g. the rules for 𝑃 + 𝑄 and 𝐶‖𝐷) and to simplify the modelling of systems. The axioms are mostly standard (see Fig. 2). The congruence axioms for the commutativity and associativity of |, ‖ and +, for the the idempotency of + and for the reordering of 𝜈 are the usual. The rule for the scope extrusion is like in 𝜋-calculus. The rule for the elimination of a dead process simplifies our terms. In particular, it states that 0 can be removed if it runs in parallel with another process.

Notice that we do not have an axiom in the form Γ : 0‖𝐶 ≡ 𝐶 because we do not allow a component to "disappear" from the system, even if its process is done: a component usually represents a physical object, which is not destroyed if the software component in it terminates.

Some common operations can be introduced as syntactic shorthands:

awareness is a blocking test, i.e. the process stops until the predicate becomes true. This is equivalent to a busy-waiting in a classical programming language: fork duplicates a process which continues as different threads:

𝜙?𝑃 ≜ 𝐾(𝑥 ⃗ ) where 𝐾(𝑥 ⃗ ) ≜ 𝜙?𝑃 : 𝐾 and 𝑥 ⃗ = fv(𝑃 ) Int Γ : 𝑃 𝛼 − →𝐷 Γ ′ : 𝑃 ′ Γ : 𝑃 |𝑄 𝛼 − →𝐷 Γ ′ : 𝑃 ′ |𝑄 Choice Γ : 𝑃 𝛼 − →𝐷 Γ ′ : 𝑃 ′ Γ : 𝑃 + 𝑄 𝛼 − →𝐷 Γ ′ : 𝑃 ′ ExtTrue 𝜙 Γ = tt Γ : 𝑃 𝛼 − →𝐷 Γ ′ : 𝑃 ′ Γ : (𝜙?𝑃 : 𝑄) 𝛼 − →𝐷 Γ ′ : 𝑃 ′ ExtFalse 𝜙 Γ = ff Γ : 𝑄 𝛼 − →𝐷 Γ ′ : 𝑄 ′ Γ : (𝜙?𝑃 : 𝑄) 𝛼 − →𝐷 Γ ′ : 𝑄 ′ SkipExt 𝜙 Γ = ⊥ Γ : (𝜙?𝑃 : 𝑄) ?𝑓 − − →𝐷 Γ : (𝜙?𝑃 : 𝑄) SkipZero Γ : 0 ?𝑓 − − →𝐷 Γ : 0 Output Γ : ⟨𝑓 ⟩𝑃 !𝑓 − →𝐷 Γ : 𝑃 SkipOutput Γ : ⟨𝑓 ⟩𝑃 ?𝑔 − − →𝐷 Γ : ⟨𝑓 ⟩𝑃 Input 𝑓 (Γ : (𝑥)𝑃 ) = 𝑣 ̸ = ⊥ Γ : (𝑥)𝑃 ?𝑓 − − →𝐷 Γ : 𝑃 [𝑣/𝑥] SkipInput 𝑓 (Γ : (𝑥)𝑃 ) = ⊥ Γ : (𝑥)𝑃 ?𝑓 − − →𝐷 Γ : (𝑥)𝑃 Update 𝑒 Γ = 𝑣 ̸ = ⊥ Γ[𝑙 ↦ → 𝑣] : 𝑃 𝛼 − →𝐷 Γ ′ : 𝑃 ′ Γ : [𝑙 := 𝑒]𝑃 𝛼 − →𝐷 Γ ′ : 𝑃 ′ SkipUpdate 𝑒 Γ = ⊥ Γ : [𝑙 := 𝑒]𝑃 ?𝑓 − − →𝐷 Γ : [𝑙 := 𝑒]𝑃 Comm 𝐶 !𝑓 − →𝐷 𝐶 ′ 𝐷 ?𝑓 − − →𝐷 𝐷 ′ 𝐶‖𝐷 !𝑓 − →𝐷 𝐶 ′ ‖𝐷 ′ Call Γ : 𝑃 [𝑒 ⃗/𝑥 ⃗ ] 𝛼 − →𝐷 𝐶 Γ : 𝐾(𝑒 ⃗) 𝛼 − →𝐷 𝐶 𝐾(𝑥 ⃗ ) ≜ 𝑃 Res 𝐶 𝛼 − →𝐷 𝐶 ′ 𝜈𝑥𝐶 [𝑥]𝛼 − −− →𝐷 𝜈𝑥𝐶 ′ Cong 𝐶 ≡ 𝐶 ′ 𝐶 ′ 𝛼 − →𝐷 𝐷 ′ 𝐷 ′ ≡ 𝐷 𝐶 𝛼 − →𝐷 𝐷!𝑃 ≜ 𝐾(𝑥 ⃗ ) where 𝐾(𝑥 ⃗ ) ≜ 𝑃 |𝐾(𝑥 ⃗ ) and 𝑥 ⃗ = fv(𝑃 )

case allows for choosing among multiple continuations via pattern-matching (this is useful when we need to perform different actions based on the value of a received message):

case 𝑥 of 𝑒𝑥𝑝𝑟 1 → 𝑃 1 ; 𝑒𝑥𝑝𝑟 2 → 𝑃 2 ; . . . ; 𝑒𝑥𝑝𝑟 𝑛 → 𝑃 𝑛 ; default → 𝑄 end ≜ (𝑥 = 𝑒𝑥𝑝𝑟 1 )?𝑃 1 : ((𝑥 = 𝑒𝑥𝑝𝑟 2 )?𝑃 2 : (. . . (𝑥 = 𝑒𝑥𝑝𝑟 𝑛 )?𝑃 𝑛 : 𝑄) . . . )

Semantics for Direct Subjective Communication

The operational (system) semantics of DSCC is given by a labelled transition relation 𝐶 𝛼 − → 𝐷 𝐶 ′ , whose labels are 𝛼 ∈ {?𝑓, !𝑓 | 𝑓 : 𝒞 → 𝒱}. ?𝑓 is used for inputs, !𝑓 is used for outputs. The rules for this semantics are in Fig. 3.

Rules prefixed with Skip are needed to have a proper broadcast communication: a component is always able to perform an input action, possibly ignoring the message and remaining itself. Without these rules, our systems would stop communicating if a component does not want to input something or if two components try simultaneously to perform an output. In other words, at each step a system can only perform a single communication; if two components need to send two messages, these cannot occur in parallel but will be interleaved.

Rule Int is the standard rule for handling interleaving of the actions of two processes. Rule Choice represents the nondeterministic choice between the subprocesses 𝑃 and 𝑄, i.e. that 𝑃 + 𝑄 can choose to continue as any of 𝑃 or 𝑄.

Rules ExtTrue and ExtFalse evaluate a predicate 𝜙 in Γ; if this returns tt the process 𝜙?𝑃 : 𝑄 proceeds as 𝑃 , if it is ff it proceeds as 𝑄, otherwise it does not change.

Rule SkipExt enables a component to perform an input (discarding the value) even if the evaluation of a predicate 𝜙 under the environment Γ is not possible (e.g. in the case 𝜙 is not ground). Rule SkipZero represents the trivial fact that an inactive (dead) component can always receive something in a broadcast.

Rule Output performs an output action, broadcasting a function 𝑓 and continuing as 𝑃 . Rule SkipOutput enables a component that wants to output something also to receive a function and remain itself. This is useful if more than a component, in a parallel system, is trying to perform an output at once; then, these components perform their outputs in turns.

Rules Input and SkipInput evaluate a received function. If the evaluation yields a value 𝑣 ̸ = ⊥, the substitution [𝑣/𝑥] is done to the continuation process 𝑃 . If the evaluation of the received function yields ⊥, the component is forced to discard the input and to remain itself.

Rule Update evaluates the expressions 𝑒 in Γ. If the result is a value (̸ = ⊥), it applies the attribute update to the store. Then the component performs an action with an 𝛼 label if the component Γ[𝑙 ↦ → 𝑣] : 𝑃 (𝑃 under the updated environment) can do so. Rule SkipUpdate, as usual, forces a component that wants to update the store to discard any arriving inputs.

Rule Comm enables parallel systems to communicate. In particular, it states that if there is a system 𝐶 that wants to perform an output in parallel with a system 𝐷 that is able to perform an input (any system is able to do so, given the Skip rules), the two of them are able to continue in parallel as 𝐶 ′ ‖𝐷 ′ .

Rule Call expands the definition of a process constant, by instantiating the formal parameters (in a call-by-name fashion).

Rule Res defines the behaviour of components under name restriction. Since 𝑥 is bound in 𝜈𝑥𝐶, it can not be visible in the label either. To this end, we use the name binding operation provided by Nominal Sets [8,9]. In particular, with the notation [𝑥]𝛼 we denote the label obtained by binding 𝑥 in 𝛼: if 𝛼 =?𝑓 then [𝑥]𝛼 =?𝑥.𝑓 ; if 𝛼 =!𝑓 then [𝑥]𝛼 =!𝑥.𝑓 . Notice that 𝑥 is a local name, bound to the label 𝛼, so fn([𝑥]𝛼) = fn(𝛼) ∖ {𝑥}.

Rule Cong, finally, allows our system to be written in different, but equivalent ways, in order to be in the correct shape for performing the action.

Notice that the semantics does not allow for parallel broadcasts, even if these actually involve different subsets of the system. Without the Skip rules, a system could get stuck in two cases:

1. if two different components try to broadcast simultaneously; 2. if a component does not want to perform an input, in presence of a broadcast.

In both these cases, we would not have a rule that enables us to join the components with the parallel operator ‖, since Comm requires the two parallel components to make, respectively, an output and an input transition.

Moreover, without the congruence axioms and Cong, we would not be able to use Comm if, e.g., we have a system 𝐶‖𝐷 where 𝐶 wants to input and 𝐷 wants to output (we do not have the symmetric Comm rule).

The following Lemma 1 proves that the semantics behaves well, in the sense that a component executing a broadcast will always succeed in every system. Lemma 1. Given 𝑛 parallel components, of which one wants to output, the broadcast succeeds regardless the particular component ordering. Formally, for any 𝐶 1 , . . . , 𝐶 𝑛 , if

𝐶 𝑖 !𝑓 − → 𝐷 𝐶 ′ 𝑖 then there exist 𝐶 ′ 1 , . . . , 𝐶 ′ 𝑖−1 , 𝐶 ′ 𝑖+1 , . . . 𝐶 ′ 𝑛 such that 𝐶 1 ‖𝐶 2 ‖𝐶 3 ‖ . . . ‖𝐶 𝑛 !𝑓 − → 𝐷 𝐶 ′ 1 ‖𝐶 ′ 2 ‖𝐶 ′ 3 ‖ . . . ‖𝐶 ′ 𝑛 Proof.

For the congruence axioms of commutativity and associativity of the system parallel ‖ we have:

𝐶 1 ‖𝐶 2 ‖𝐶 3 ‖ . . . ‖𝐶 𝑛 ≡ (. . . (𝐶 𝑖 ‖𝐶 1 )‖𝐶 2 )‖𝐶 3 )‖ . . . ‖𝐶 𝑖−1 )‖𝐶 𝑖+1 )‖ . . . ‖𝐶 𝑛 )

Now, all of 𝐶 1 , 𝐶 2 , 𝐶 3 , . . . , 𝐶 𝑖−1 , 𝐶 𝑖+1 , . . . , 𝐶 𝑛 may perform an input, using either Input or a Skip rule. Then, 𝐶 𝑖 and 𝐶 1 may proceed using Comm. Since the conclusion exhibits an output label, we can again use Comm alongside 𝐶 2 and we can iterate the process until we reach 𝐶 𝑛 (with a total of 𝑛 − 1 application of Comm).

Semantics for Indirect Subjective Communication

The operational (system) semantics of ISCC is given by a labelled transition relation 𝐶 𝛼 − → 𝐼 𝐶 ′ , different from the DSCC one. In particular, the associated labels are 𝛼 ∈ 𝒱 ∪ {!𝑓 | 𝑓 : 𝒞 → 𝒱}. As for DSCC these labels denotes different actions: ?𝑣 is used for inputs, !𝑓 is used for outputs.

Notice that, contrary to the DSCC specification, here the communication is somewhat mediated, hence the name Indirect Subjective Communication. This means that a component is no longer required to get and execute a function (fundamentally a piece of code) to obtain a value; instead, the broadcasted function is collected by an external mediating entity that evaluates them on the behalf of the SC recipients. We do not discuss here how such an entity should work: we just need to know that it must have access to the stores of all agents.

An interesting thing to notice is that in this setting the agent does not need to be trusted, since it will receive only the values that it is meant to receive. This prevents e.g. sniffing of messages or unwanted behaviours by byzantine components. Suppose there is a DSCC agent that "looks into" the received function prior to evaluation: such an agent may be able to gather information that must be kept secret. With the ISCC semantics this is no longer possible, since the component will be given only the relevant result.

The rules for ISCC are in Fig. 4, and may look similar to the ones for DSCC, but of course the transition relation is different. They have, however, the same role in the two semantics, so that we can omit explaining them again here.

Rule Input, in ISCC, performs the substitution [𝑣/𝑥] to the continuation process 𝑃 , if the component is given a value 𝑣 that is not ⊥. Rule SkipInput is similar: a component, when it is given ⊥, discards the input and remains itself.

Rule Comm, like in DSCC, enables parallel systems to communicate. Here, however, is this rule that evaluates the output function 𝑓 to yield a value 𝑣. In particular, the rule states that if there is a system 𝐶 that wants to perform an output in parallel with a system 𝐷 that is able to perform an input, the two of them are able to continue in parallel as 𝐶 ′ ‖𝐷 ′ , provided that to 𝐷 is given the value returned by the application of the output function to 𝐷 itself.

Update 𝑒 Γ = 𝑣 ̸ = ⊥ Γ[𝑙 ↦ → 𝑣] : 𝑃 𝛼 − →𝐼 Γ ′ : 𝑃 ′ Γ : [𝑙 := 𝑒]𝑃 𝛼 − →𝐼 Γ ′ : 𝑃 ′ SkipUpdate 𝑒 Γ = ⊥ Γ : [𝑙 := 𝑒]𝑃 ?𝑣 − − →𝐼 Γ : [𝑙 := 𝑒]𝑃 Comm 𝐶 !𝑓 − →𝐼 𝐶 ′ 𝐷 ?𝑣 − − →𝐼 𝐷 ′ 𝑓 (𝐷) = 𝑣 𝐶‖𝐷 !𝑓 − →𝐼 𝐶 ′ ‖𝐷 ′ Call : 𝑃 [𝑒 ⃗/𝑥 ⃗ ] 𝛼 − →𝐼 𝐶 Γ : 𝐾(𝑒 ⃗) 𝛼 − →𝐼 𝐶 𝐾(𝑥 ⃗ ) ≜ 𝑃 Res 𝐶 𝛼 − →𝐼 𝐶 ′ 𝜈𝑥𝐶 [𝑥]𝛼 − −− →𝐼 𝜈𝑥𝐶 ′ Cong 𝐶 ≡ 𝐶 ′ 𝐶 ′ 𝛼 − →𝐼 𝐷 ′ 𝐷 ′ ≡ 𝐷 𝐶 𝛼 − →𝐼 𝐷

Example: a Vineyard Irrigation System

Let us consider a scenario where a winegrower wants to optimize the irrigation of some vineyards. Their main goals are: 1) to irrigate each vine with the correct amount of water; 2) to know if the soil "behaves well", i.e. if it neither causes water stagnation nor it dries too quickly; 3) to know, at every time, each watering valve status (i.e. if it is opened or closed). Each yard is divided into zones; each zone has a moisture sensor and a certain number of vines, each with its watering valve (see Fig. 5). Additionally, each sensor and actuator knows its position (a Cartesian coordinate, e.g., (𝑟𝑜𝑤, 𝑐𝑜𝑙𝑢𝑚𝑛)), fixed at deployment. The coordinates are not unique among different yards. The winegrower has a console terminal that collects the watering data and reports them in some graphical way (e.g. it shows a heat-map).

A traditional, centralised way to implement a management system for this scenario is to use a central server (possibly in the cloud) that gathers all the relevant data and remotely open and closes the valves according to some policies, in order to maintain the desired moisture level. On the other hand, there is the possibility of using a distributed, edge-computing paradigm, where the computation is moved near the source of the data. This should reduce latency and increase reliability, at the cost of increasing the computational resources required on the nodes.

With our paradigm we can implement both: DSCC is well-suited for a truly distributed system, where reliability is the main goal; ISCC is better suited when security is essential. When modelling the system we can abstract from the particular implementation: switching between the two semantics can be easily done at any point of the design.

We can model the scenario as a SC system as follows:

𝐶 𝑦𝑎𝑟𝑑 (𝑛𝑎𝑚𝑒) = 𝐶 𝑣𝑎𝑙𝑣𝑒 (𝑛𝑎𝑚𝑒, 𝑥 𝑣1 , 𝑦 𝑣1 )‖ . . . ‖𝐶 𝑣𝑎𝑙𝑣𝑒 (𝑛𝑎𝑚𝑒, 𝑥 𝑣𝑛 , 𝑦 𝑣𝑛 )‖ 𝐶 𝑚𝑜𝑖𝑠𝑡 (𝑛𝑎𝑚𝑒, 𝑥 ℎ1 , 𝑦 ℎ1 )‖ . . . ‖𝐶 𝑚𝑜𝑖𝑠𝑡 (𝑛𝑎𝑚𝑒, 𝑥 ℎ𝑚 , 𝑦 ℎ𝑚 ) 𝐶 𝑦𝑎𝑟𝑑𝑠 = 𝜈𝑛 1 𝐶 𝑦𝑎𝑟𝑑 (𝑛 1 )‖ . . . ‖𝜈𝑛 𝑘 𝐶 𝑦𝑎𝑟𝑑 (𝑛 𝑘 )‖𝐶 𝑐𝑜𝑛𝑠𝑜𝑙𝑒

The construct 𝜈𝑘(𝐶 1 ‖𝐶 2 ) creates a secret 𝑘 (i.e., a nonce), that 𝐶 1 and 𝐶 2 can use to communicate without interfering with other components; this allows to logically separate messages that involve only some components, yielding a cleaner "communication environment".

The moisture sensor acts as a local controller for the zone, communicating a message which commands the nearby watering valves, and notifying the moisture level to the console:

𝐶 𝑚𝑜𝑖𝑠𝑡 (𝑛, 𝑥, 𝑦) = Γ 𝑚𝑜𝑖𝑠𝑡 :!⟨𝑓 𝑚𝑜𝑖𝑠𝑡 ⟩0 Γ 𝑚𝑜𝑖𝑠𝑡 = {𝑡𝑦𝑝𝑒 ↦ → moisture, 𝑦𝑎𝑟𝑑 ↦ → 𝑛, 𝑥 ↦ → 𝑥, 𝑦 ↦ → 𝑦, 𝑟𝑒𝑎𝑐ℎ ↦ → 2, ℎ ↦ → NaN, ℎ 𝑚𝑖𝑛 ↦ → 0.4, ℎ 𝑚𝑎𝑥 ↦ → 0.5}

where ℎ bound to the output of a physical moisture sensor and 𝑓 𝑚𝑜𝑖𝑠𝑡 is defined as follows:

𝑓 𝑚𝑜𝑖𝑠𝑡 = 𝜆(𝑡𝑦𝑝𝑒, 𝑦𝑎𝑟𝑑, 𝑥, 𝑦). ⎧ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎪ ⎩ open if 𝑡ℎ𝑖𝑠.ℎ < 𝑡ℎ𝑖𝑠.ℎ 𝑚𝑖𝑛 ∧ 𝑡𝑦𝑝𝑒 = valve ∧ 𝑦𝑎𝑟𝑑 = 𝑡ℎ𝑖𝑠.𝑦𝑎𝑟𝑑 ∧ √︀ (𝑡ℎ𝑖𝑠.𝑥 − 𝑥) 2 + (𝑡ℎ𝑖𝑠.𝑦 − 𝑦) 2 < 𝑡ℎ𝑖𝑠.𝑟𝑒𝑎𝑐ℎ close if 𝑡ℎ𝑖𝑠.ℎ > 𝑡ℎ𝑖𝑠.ℎ 𝑚𝑎𝑥 ∧ 𝑡𝑦𝑝𝑒 = valve ∧ 𝑦𝑎𝑟𝑑 = 𝑡ℎ𝑖𝑠.𝑦𝑎𝑟𝑑 ∧ √︀ (𝑡ℎ𝑖𝑠.𝑥 − 𝑥) 2 + (𝑡ℎ𝑖𝑠.𝑦 − 𝑦) 2 < 𝑡ℎ𝑖𝑠.𝑟𝑒𝑎𝑐ℎ (︁ moist,𝑡ℎ𝑖𝑠.𝑦𝑎𝑟𝑑, 𝑡ℎ𝑖𝑠.𝑥,𝑡ℎ𝑖𝑠.𝑦,𝑡ℎ𝑖𝑠.ℎ )︁ if 𝑡𝑦𝑝𝑒 = console ⊥ otherwise

Here we see that the same message (𝑓 𝑚𝑜𝑖𝑠𝑡 ) can be interpreted in different ways:

1. a valve (𝑡𝑦𝑝𝑒 = valve) close to the sensor will evaluate it as a command to open or close;

2. the console (𝑡𝑦𝑝𝑒 = console) be evaluated as a tuple that contains all the information needed to insert in a log file the current moisture value read by the particular sensor;

3. anyone else will evaluate it as ⊥, meaning that no value is passed to the process.

To complete our system we need to define the components for the irrigation valves and the console. The valve acts on the water dripper according to the command received from the local controller. It also updates the console with the current status of the valve (to e.g. raise an alert if a valve is stuck open).

The valve component is programmed as follows:

)︁ if 𝑡𝑦𝑝𝑒 = console ⊥ otherwise

The console simply logs in a database the values obtained from the moisture sensors and the watering valves. This component is defined as:

𝐶 𝑐𝑜𝑛𝑠𝑜𝑙𝑒 = Γ 𝑐𝑜𝑛𝑠𝑜𝑙𝑒 :!𝑃 𝑐𝑜𝑛𝑠𝑜𝑙𝑒 Γ 𝑐𝑜𝑛𝑠𝑜𝑙𝑒 = {𝑡𝑦𝑝𝑒 ↦ → console} 𝑃 𝑐𝑜𝑛𝑠𝑜𝑙𝑒 = (𝑚𝑠𝑔)case 𝑚𝑠𝑔 of

Stateless Bisimulation

As for similar foundational calculi, SCC is intended to be also a basis for the investigation of theoretical aspects of the Subjective Communication model. As an example along this line, in this section we introduce a behavioural equivalence for processes.

In SCC, components carry (local) data (the environments or stores), which may be updated by processes. We can easily define a notion of strong bisimilarity on components and systems by applying directly the original notion of strong bisimilarity, treating attributes in the environments on a par with processes. More precisely, a strong bisimulation for DSCC (similary for ISCC) is a relation 𝑅 ⊆ 𝒞 × 𝒞, such that for all (𝐶 1 , 𝐶 2 ) ∈ 𝑅:

• for all 𝛼 such that 𝐶 1 𝛼 − → 𝐷 𝐶 ′ 1 there exists 𝐶 ′ 2 such that 𝐶 2 𝛼 − → 𝐷 𝐶 ′ 2 and (𝐶 ′ 1 , 𝐶 ′ 2 ) ∈ 𝑅;

• for all 𝛼 such that 𝐶 2

𝛼 − → 𝐷 𝐶 ′ 2 there exists 𝐶 ′ 1 such that 𝐶 1 𝛼 − → 𝐷 𝐶 ′ 1 and (𝐶 ′ 1 , 𝐶 ′ 2 ) ∈ 𝑅.

Two systems are strongly bisimilar if there exists a strong bisimulation relating them. However, this notion of bisimilarity is not very satisfactory, because systems can be strongly bisimilar even if their environments are not the same; e.g., Γ 1 : 0 and Γ 2 : 0 are strongly bisimilar for any Γ 1 , Γ 2 . In fact, in most applications we need to observe and compare (local) environments in a finer way; e.g., a closed valve is not equivalent to an open one. Therefore, in this paper, we restrict ourselves to comparing processes with respect to the same environments, in order to ensure that, when starting from the same state, they yield the same state.

Our behavioural equivalence is an adaptation of the stateless bisimulation given in [10]. Two process terms are stateless bisimilar if, for all identical data states, they can mimic transitions of each other and the resulting process terms are again stateless bisimilar, i.e. it compares components for all identical environments and allows all sort of changes after the transition. More formally, let Compositionality of stateless bisimilarity makes it particularly useful when, in a parallel system, we want to replace a component: if the new "part" is stateless bisimilar to the old one, the component (and the whole system) is guaranteed to behave the same.

Proposition 1. Stateless bisimilarity is a congruence for both DSCC and ISCC.

Proof. Follows from [10, Th. 14] and the fact that DSCC and ISCC are in process-tyft format [10]. Rule Cong is not strictly in process-tyft format, but we can omit it from the system by taking process up-to congruence, as two congruent components exhibit the same transitions.

Conclusion

In this paper we have introduced the Subjective Communication Calculus SCC, a formal model for Collective Adaptive Systems with subjective communication. In this paradigm, messages are (partial) functions from components to values; each component may obtain a different value (or nothing at all) from the very same message, according to its specific state and perspective.

We have presented two operational semantics for SCC. On one hand, we have introduced Direct Subjective Communication (DSCC), where each agent receives the message function and evaluates it; this semantics is akin to "edge computing", where the burden of computation is moved towards the node of the CAS. On the other hand, in Indirect Subjective Communication (ISCC) the broadcasted function is evaluated by some mediating middleware; this semantics can be seen as the counterpart of usual cloud-based computing, where messages are collected and elaborated by some central node (possibly in the cloud). For both these semantics we have given the definition of stateless bisimilarity, and proved that it is a congruence. In order to showcase the expressive power of the paradigm, we have provided an example inspired to real-world application scenario, i.e., a smart irrigation system for a vineyard.

Future work. We plan to give a categorical bialgebraic semantics for SCC [11], from which we expect to derive a canonical compositional LTS and behavioural equivalence, which we plan to compare with that examined in Section 4. Since the components contain states and local names and variables, we plan to follow the approach adopted for the Fusion calculus in [12,13]. It is interesting also to investigate behavioural equivalences where some steps are unobservable from the point of view of some participant; to this end we plan to adopt and extend the approach presented in [14]. Afterwards, we plan to consider also quantitative aspects (e.g. execution times, energy consumptions); to this end, the results of [15,16] could be useful.

There are other interesting types of bisimilarities for semantics with data: in particular we recall the notions of initially stateless bisimilarity and statebased bisimilarity. We cannot, however, apply the general results from [10] as we have done for stateless bisimilarity since our transition system specifications are not in sfisl format (for initially stateless bisimilarity) or sbsf format (for statebased bisimilarity). It is still an open question whether initially stateless or statebased bisimilarities are congruences for our specifications.

Finally, it is interesting to develop a prototypal implementation of SCC, in order to evaluate the practical differences of the two semantics. To this end, we will leverage the experience from the implementation of SCEL, AbC and the AbU calculus [3,4,6]. An alternative approach is to encode SCC as a bigraphic reactive system, in order to reuse existing toolkits [17].