=Paper= {{Paper |id=Vol-3284/1841 |storemode=property |title=A Calculus for Subjective Communication |pdfUrl=https://ceur-ws.org/Vol-3284/1841.pdf |volume=Vol-3284 |authors=Marino Miculan,Matteo Paier |dblpUrl=https://dblp.org/rec/conf/ictcs/MiculanP22 }} ==A Calculus for Subjective Communication== https://ceur-ws.org/Vol-3284/1841.pdf

A Calculus for Subjective Communication
Marino Miculan1,2 , Matteo Paier1
1
University of Udine, Italy
2
Ca’ Foscari University of Venice, Italy

Abstract
In this paper we introduce Subjective Communication, a new interaction model for CAS and generalizing
the attribute-based communication introduced in the AbC calculus. In this model, a message is broad-
casted to every process, but each process can view the very same message in different ways, depending
on its attributes. To formalize this model, we introduce SCC, the Subjective Communication Calculus, for
which we propose two semantics: Direct SCC, particularly useful when dealing with an edge computing
communication paradigm, and Indirect SCC, more suited to a cloud-centric model. We then introduce a
stateless bisimilarity for our semantics, which we prove to be a congruence.

Keywords
Concurrency theory, Process algebra, Distributed Systems

1. 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].

Proceedings of the 23rd Italian Conference on Theoretical Computer Science, Rome, Italy, September 7-9, 2022
" marino.miculan@uniud.it (M. Miculan); paier.matteo@spes.uniud.it (M. Paier)
0000-0003-0755-3444 (M. Miculan)
© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
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 communi-
cations, 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.

2. 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.
Agent1 Agent2 Agent3
𝑣
Eval module Eval module Eval module
𝜆𝑋.𝑣 𝜆𝑋.𝑣 𝜆𝑋.𝑣 𝜆𝑋.𝑣

Shared communicatium medium

(a) The DSCC semantics.

Agent1 Agent2 Agent3
𝑣
𝜆𝑋.𝑣
Evaluation entity
𝜆𝑋.𝑣
Shared communicatium medium

(b) The ISCC semantics.
Figure 1: The DSCC and ISCC semantics. The dashed arrows represents the flow of information when
Agent1 sends a message, and only Agent2 is interested.

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 J𝑒KΓ , 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 J𝑒KΓ = ⊥. This means, for instance,
that in an arithmetic context J0 × 𝑥KΓ = ⊥, 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:
0 do nothing;
𝑃 |𝑄 interleave the execution of two processes;
𝑃 + 𝑄 non-deterministically choose a continuation;
𝜙?𝑃 : 𝑄 evaluate 𝜙, and if it is a boolean value it chooses 𝑃 or 𝑄, accordingly;
⟨𝑓 ⟩𝑃 broadcast a function from components to values (𝑓 : 𝒞 → 𝒱). Each receiver process
will get a value depending on itself;
(𝑥)𝑃 wait for the reception of a value. This construct allows for the substitution, in 𝑃 , of
the free name 𝑥 with the value received;
𝛼-equivalence 𝐶 ≡ 𝐷 if 𝐶 and 𝐷 are 𝛼-equivalent
Commutativity of | 𝑃 |𝑄 ≡ 𝑄|𝑃
Associativity of | 𝑃 |(𝑄|𝑅) ≡ (𝑃 |𝑄)|𝑅
Dead process 0|𝑃 ≡ 𝑃
Commutativity of ‖ 𝐶‖𝐷 ≡ 𝐷‖𝐶
Associativity of ‖ 𝐶‖(𝐷‖𝐸) ≡ (𝐶‖𝐷)‖𝐸
Commutativity of + 𝐶 + 𝐷 ≡ 𝐷 + 𝐶
Associativity of + 𝐶 + (𝐷 + 𝐸) ≡ (𝐶 + 𝐷) + 𝐸
Idempotency of + 𝐶 + 𝐶 ≡ 𝐶
Scope extrusion of 𝜈 (𝜈𝑥𝐶)‖𝐷 ≡ 𝜈𝑥(𝐶‖𝐷) if 𝑥 ∈
/ fn(𝐷)
Reordering of 𝜈 𝜈𝑥𝜈𝑦𝐶 ≡ 𝜈𝑦𝜈𝑥𝐶

Figure 2: Axioms of structural congruence.

𝐾(𝑒
⃗ ) call a process named 𝐾, instantiating the parameters with the list ⃗𝑒. This construct
enables looping of processes (using recursion);
[𝑙 := 𝑒]𝑃 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:
𝜙?𝑃 ≜ 𝐾(𝑥
⃗ ) where 𝐾(𝑥
⃗ ) ≜ 𝜙?𝑃 : 𝐾 and ⃗𝑥 = fv(𝑃 )
𝛼 𝛼
→𝐷 Γ′ : 𝑃 ′
Γ:𝑃 − →𝐷 Γ′ : 𝑃 ′
Γ:𝑃 −
Int 𝛼 Choice 𝛼
→𝐷 Γ′ : 𝑃 ′ |𝑄
Γ : 𝑃 |𝑄 − →𝐷 Γ′ : 𝑃 ′
Γ:𝑃 + 𝑄 −
𝛼 𝛼
→𝐷 Γ′ : 𝑃 ′
J𝜙KΓ = tt Γ : 𝑃 − →𝐷 Γ′ : 𝑄′
J𝜙KΓ = ff Γ : 𝑄 −
ExtTrue 𝛼 ExtFalse 𝛼
→𝐷 Γ′ : 𝑃 ′
Γ : (𝜙?𝑃 : 𝑄) − →𝐷 Γ′ : 𝑄′
Γ : (𝜙?𝑃 : 𝑄) −
J𝜙KΓ = ⊥ ?𝑓
SkipExt SkipZero Γ : 0 −
−→𝐷 Γ : 0
?𝑓
Γ : (𝜙?𝑃 : 𝑄) −
−→𝐷 Γ : (𝜙?𝑃 : 𝑄)
!𝑓 ?𝑔
Output Γ : ⟨𝑓 ⟩𝑃 −→𝐷 Γ : 𝑃 SkipOutput Γ : ⟨𝑓 ⟩𝑃 −
−→𝐷 Γ : ⟨𝑓 ⟩𝑃
𝑓 (Γ : (𝑥)𝑃 ) = 𝑣 ̸= ⊥ 𝑓 (Γ : (𝑥)𝑃 ) = ⊥
Input SkipInput
?𝑓 ?𝑓
Γ : (𝑥)𝑃 −
−→𝐷 Γ : 𝑃 [𝑣/𝑥] Γ : (𝑥)𝑃 −
−→𝐷 Γ : (𝑥)𝑃
𝛼
→𝐷 Γ′ : 𝑃 ′
J𝑒KΓ = 𝑣 ̸= ⊥ Γ[𝑙 ↦→ 𝑣] : 𝑃 − J𝑒KΓ = ⊥
Update 𝛼 SkipUpdate
?𝑓
→𝐷 Γ′ : 𝑃 ′
Γ : [𝑙 := 𝑒]𝑃 − Γ : [𝑙 := 𝑒]𝑃 −
−→𝐷 Γ : [𝑙 := 𝑒]𝑃
!𝑓 ?𝑓 𝛼
𝐶 −→𝐷 𝐶 ′ 𝐷−
−→𝐷 𝐷 ′ Γ : 𝑃 [𝑒 ⃗] −
⃗ /𝑥 →𝐷 𝐶
Comm Call 𝛼 𝐾(𝑥
⃗) ≜ 𝑃
!𝑓
𝐶‖𝐷 −→𝐷 𝐶 ′ ‖𝐷′ ⃗) −
Γ : 𝐾(𝑒 →𝐷 𝐶
𝛼 𝛼
→𝐷 𝐶 ′
𝐶− 𝐶 ≡ 𝐶′ 𝐶′ −
→𝐷 𝐷′ 𝐷′ ≡ 𝐷
Res Cong 𝛼
[𝑥]𝛼 𝐶−
→𝐷 𝐷
𝜈𝑥𝐶 −−−→𝐷 𝜈𝑥𝐶 ′

Figure 3: Operational semantics of DSCC.

fork duplicates a process which continues as different threads:

!𝑃 ≜ 𝐾(𝑥 ⃗ ) ≜ 𝑃 |𝐾(𝑥
⃗ ) 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 : (. . . (𝑥 = 𝑒𝑥𝑝𝑟𝑛 )?𝑃𝑛 : 𝑄) . . . )

2.1. 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
!𝑓
→𝐷 𝐶𝑖′ then
regardless the particular component ordering. Formally, for any 𝐶1 , . . . , 𝐶𝑛 , if 𝐶𝑖 −
′ ′ ′ ′
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).

2.2. 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 medi-
ated, 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.
𝛼 𝛼
→𝐼 Γ′ : 𝑃 ′
Γ:𝑃 − →𝐼 Γ′ : 𝑃 ′
Γ:𝑃 −
Int 𝛼 Choice 𝛼
→𝐼 Γ′ : 𝑃 ′ |𝑄
Γ : 𝑃 |𝑄 − →𝐼 Γ′ : 𝑃 ′
Γ:𝑃 + 𝑄 −
𝛼 𝛼
→𝐼 Γ′ : 𝑃 ′
J𝜙KΓ = tt Γ : 𝑃 − →𝐼 Γ′ : 𝑄′
J𝜙KΓ = ff Γ : 𝑄 −
ExtTrue 𝛼 ExtFalse 𝛼
→𝐼 Γ′ : 𝑃 ′
Γ : (𝜙?𝑃 : 𝑄) − →𝐼 Γ′ : 𝑄′
Γ : (𝜙?𝑃 : 𝑄) −
J𝜙KΓ = ⊥ ?𝑣
SkipExt SkipZero Γ : 0 −
−→𝐼 Γ : 0
?𝑣
Γ : (𝜙?𝑃 : 𝑄) −
−→𝐼 Γ : (𝜙?𝑃 : 𝑄)
!𝑓 ?𝑣
Output Γ : ⟨𝑓 ⟩𝑃 −→𝐼 Γ : 𝑃 SkipOutput Γ : ⟨𝑓 ⟩𝑃 −
−→𝐼 Γ : ⟨𝑓 ⟩𝑃
𝑣 ̸= ⊥ 𝑣=⊥
Input SkipInput
?𝑣 ?𝑣
Γ : (𝑥)𝑃 −
−→𝐼 Γ : 𝑃 [𝑣/𝑥] Γ : (𝑥)𝑃 −
−→𝐼 Γ : (𝑥)𝑃
𝛼
J𝑒KΓ = 𝑣 ̸= ⊥ →𝐼 Γ′ : 𝑃 ′
Γ[𝑙 ↦→ 𝑣] : 𝑃 − J𝑒KΓ = ⊥
Update 𝛼 SkipUpdate
?𝑣
Γ : [𝑙 := 𝑒]𝑃 −
→𝐼 Γ′ : 𝑃 ′ Γ : [𝑙 := 𝑒]𝑃 −
−→𝐼 Γ : [𝑙 := 𝑒]𝑃
!𝑓 ?𝑣 𝛼
𝐶 −→𝐼 𝐶 ′ 𝐷−
−→𝐼 𝐷′ 𝑓 (𝐷) = 𝑣 Γ : 𝑃 [𝑒 ⃗] −
⃗ /𝑥 →𝐼 𝐶
Comm Call 𝛼 𝐾(𝑥
⃗) ≜ 𝑃
!𝑓
𝐶‖𝐷 −→𝐼 𝐶 ′ ‖𝐷′ ⃗) −
Γ : 𝐾(𝑒 →𝐼 𝐶
𝛼 𝛼
→𝐼 𝐶 ′
𝐶− 𝐶 ≡ 𝐶′ →𝐼 𝐷′
𝐶′ − 𝐷′ ≡ 𝐷
Res Cong 𝛼
[𝑥]𝛼 𝐶−
→𝐼 𝐷
𝜈𝑥𝐶 −−−→𝐼 𝜈𝑥𝐶 ′

Figure 4: Operational semantics of ISCC.

m m m m m

Figure 5: A smart vineyard. Each dot represents a vine (with the associated watering valve), each m
represents a moisture sensor. The circles are the reach of each sensor

3. 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 commu-
nicate 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:

𝐶𝑣𝑎𝑙𝑣𝑒 (𝑛, 𝑥, 𝑦) = Γ𝑣𝑎𝑙𝑣𝑒 :!(𝑃𝑣𝑎𝑙𝑣𝑒 |𝑃𝑠𝑒𝑛𝑑𝑆𝑡𝑎𝑡𝑢𝑠 )
Γ𝑣𝑎𝑙𝑣𝑒 = {𝑡𝑦𝑝𝑒 ↦→ valve, 𝑦𝑎𝑟𝑑 ↦→ 𝑛, 𝑥 ↦→ 𝑥, 𝑦 ↦→ 𝑦, 𝑤𝑎𝑡𝑒𝑟 ↦→ ff}
𝑃𝑣𝑎𝑙𝑣𝑒 = (𝑚𝑠𝑔)case 𝑚𝑠𝑔 of
open → [𝑤𝑎𝑡𝑒𝑟 := tt]0;
close → [𝑤𝑎𝑡𝑒𝑟 := ff]0;
end
𝑃𝑠𝑒𝑛𝑑𝑆𝑡𝑎𝑡𝑢𝑠 = ⟨𝑓𝑠𝑒𝑛𝑑𝑆𝑡𝑎𝑡𝑢𝑠 ⟩0
⎧(︁ )︁
valve,𝑡ℎ𝑖𝑠.𝑦𝑎𝑟𝑑,
⎨
𝑡ℎ𝑖𝑠.𝑥,𝑡ℎ𝑖𝑠.𝑦,𝑡ℎ𝑖𝑠.𝑤𝑎𝑡𝑒𝑟 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
(moist, 𝑦𝑎𝑟𝑑, 𝑥, 𝑦, ℎ) → 𝐾𝑙𝑜𝑔𝑀 𝑜𝑖𝑠𝑡𝑢𝑟𝑒 (𝑦𝑎𝑟𝑑, 𝑥, 𝑦, ℎ);
(valve, 𝑦𝑎𝑟𝑑, 𝑥, 𝑦, 𝑠) → 𝐾𝑙𝑜𝑔𝑉 𝑎𝑙𝑣𝑒𝑆𝑡𝑎𝑡𝑢𝑠 (𝑦𝑎𝑟𝑑, 𝑥, 𝑦, 𝑠);
end

where 𝐾𝑙𝑜𝑔𝑀 𝑜𝑖𝑠𝑡𝑢𝑟𝑒 saves the moisture reading in a database and 𝐾𝑙𝑜𝑔𝑉 𝑎𝑙𝑣𝑒𝑆𝑡𝑎𝑡𝑢𝑠 does the same
with the valve status.

4. 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 envi-
ronments on a par with processes. More precisely, a strong bisimulation for DSCC (similary for
ISCC) is a relation 𝑅 ⊆ 𝒞 × 𝒞, such that for all (𝐶1 , 𝐶2 ) ∈ 𝑅:
𝛼 𝛼
→𝐷 𝐶1′ there exists 𝐶2′ such that 𝐶2 −
• for all 𝛼 such that 𝐶1 − →𝐷 𝐶2′ and (𝐶1′ , 𝐶2′ ) ∈ 𝑅;
𝛼 𝛼
→𝐷 𝐶2′ there exists 𝐶1′ such that 𝐶1 −
• for all 𝛼 such that 𝐶2 − →𝐷 𝐶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 −→ be any of − →𝐷 , −
→𝐼 :

Definition 1 (Stateless Bisimilarity). A symmetric relation 𝑅𝑠𝑙 ⊆ 𝒫 𝑛 × 𝒫 𝑛 is a stateless
⃗ ,𝑄
bisimulation if for all (𝑃 ⃗ ) ∈ 𝑅𝑠𝑙 :

1. for all Γ1 , . . . , Γ𝑛 and 𝑃1′ , . . . , 𝑃𝑛′ such that
𝛼
→ Γ′1 : 𝑃1′ ‖ . . . ‖Γ′𝑛 : 𝑃𝑛′
Γ1 : 𝑃1 ‖ . . . ‖Γ𝑛 : 𝑃𝑛 −

there exist 𝑄′1 , . . . , 𝑄′𝑛 such that (𝑃⃗ ′ , 𝑄
⃗ ′ ) ∈ 𝑅 and
𝑠𝑙

𝛼
→ Γ′1 : 𝑄′1 ‖ . . . ‖Γ′𝑛 : 𝑄′𝑛
Γ1 : 𝑄1 ‖ . . . ‖Γ𝑛 : 𝑄𝑛 −

2. for all Δ1 , . . . , Δ𝑛 and 𝑄′1 , . . . , 𝑄′𝑛 such that
𝛼
→ Δ′1 : 𝑄′1 ‖ . . . ‖Δ′𝑛 : 𝑄′𝑛
Δ1 : 𝑄1 ‖ . . . ‖Δ𝑛 : 𝑄𝑛 −

there exist 𝑃1′ , . . . , 𝑃𝑛′ such that (𝑃⃗ ′ , 𝑄
⃗ ′ ) ∈ 𝑅 and
𝑠𝑙

𝛼
→ Δ′1 : 𝑃1′ ‖ . . . ‖Δ′𝑛 : 𝑃𝑛′
Δ1 : 𝑃1 ‖ . . . ‖Δ𝑛 : 𝑃𝑛 −

Two processes 𝑃 and 𝑄 are stateless bisimilar, written 𝑃 ∼𝑠𝑙 𝑄, if there exists a stateless
bisimulation 𝑅𝑠𝑙 such that (𝑃, 𝑄) ∈ 𝑅𝑠𝑙 .

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.
5. 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].

Acknowledgments
This work has been supported by the Italian MIUR project PRIN 2017FTXR7S IT MATTERS
(Methods and Tools for Trustworthy Smart Systems).
References
[1] V. Andrikopoulos, A. Bucchiarone, S. Gómez Sáez, D. Karastoyanova, C. A. Mezzina, To-
wards modeling and execution of collective adaptive systems, in: International Conference
on Service-Oriented Computing, Springer, 2013, pp. 69–81.
[2] Miller, J. H, S. E. Page, Complex adaptive systems: An introduction to computational
models of social life, Princeton university press, 2009.
[3] Y. A. Alrahman, R. De Nicola, M. Loreti, On the power of attribute-based communication,
in: International Conference on Formal Techniques for Distributed Objects, Components,
and Systems, Springer, 2016, pp. 1–18.
[4] R. De Nicola, M. Loreti, R. Pugliese, F. Tiezzi, A formal approach to autonomic systems
programming: the SCEL language, ACM Transactions on Autonomous and Adaptive
Systems (TAAS) 9 (2014) 1–29.
[5] K. V. Prasad, A calculus of broadcasting systems, Science of Computer Programming 25
(1995) 285–327.
[6] M. Miculan, M. Pasqua, A calculus for attribute-based memory updates, in: A. Cerone, P. C.
Ölveczky (Eds.), Theoretical Aspects of Computing – ICTAC 2021, Springer International
Publishing, Cham, 2021, pp. 366–385.
[7] M. Miculan, M. Pasqua, Distributed programming of smart systems with event-condition-
action rules (short paper), in: U. Dal Lago, D. Gorla (Eds.), 23rd Italian Conference on
Theoretical Computer Science (ICTCS), Proceedings, CEUR Workshop Proceedings, 2022.
[8] A. M. Pitts, Nominal logic, a first order theory of names and binding, Information and
computation 186 (2003) 165–193.
[9] M. J. Gabbay, The 𝜋-calculus in FM, in: Thirty Five Years of Automating Mathematics,
Springer, 2003, pp. 247–269.
[10] M. R. Mousavi, M. A. Reniers, J. F. Groote, Notions of bisimulation and congruence formats
for sos with data, Information and Computation 200 (2005) 107–147.
[11] B. Klin, Bialgebras for structural operational semantics: An introduction, Theoretical
Computer Science 412 (2011) 5043–5069.
[12] M. Miculan, A categorical model of the Fusion calculus, Electr. Notes Theor. Comput. Sci.
218 (2008) 275–293.
[13] M. Miculan, K. Yemane, A unifying model of variables and names, in: V. Sassone (Ed.),
Foundations of Software Science and Computational Structures, 8th International Con-
ference, FOSSACS 2005, Proceedings, volume 3441 of Lecture Notes in Computer Science,
Springer, 2005, pp. 170–186.
[14] T. Brengos, M. Miculan, M. Peressotti, Behavioural equivalences for coalgebras with
unobservable moves, J. Log. Algebraic Methods Program. 84 (2015) 826–852.
[15] M. Miculan, M. Peressotti, GSOS for non-deterministic processes with quantitative aspects,
in: N. Bertrand, L. Bortolussi (Eds.), Proc. QAPL 2014, volume 154 of EPTCS, 2014, pp.
17–33.
[16] M. Miculan, M. Peressotti, Structural operational semantics for non-deterministic processes
with quantitative aspects, Theor. Comput. Sci. 655 (2016) 135–154.
[17] G. Bacci, D. Grohmann, M. Miculan, Dbtk: A toolkit for directed bigraphs, in: Proc. CALCO,
volume 5728 of Lecture Notes in Computer Science, Springer, 2009, pp. 413–422.