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 broadcasted to every process, but each process can view the very same message in diferent 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.
However, there is a tension between the objective nature of messages and the fact that the same message can be accessed diferently by agents with diferent 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 diferent 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, diferent agents can experience the same message in diferent 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, diferent agents may obtain diferent 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 diferent 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. . . Eval module
. . .
(a) The DSCC semantics.
(b) The ISCC semantics.
.
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 JKΓ, 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 JKΓ = ⊥. 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 ≡
(⃗) 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 diferent 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.
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( ) Γ:→−
Γ′ : ′ Γ: + →− Γ′ : ′ ExtFalse J KΓ = ff Γ:→−
Γ′ :′ Γ:( ? :)→− Γ′ :′ SkipZero Γ:→0−− ?
Γ:0 SkipOutput Γ:⟨⟩→−− ?
Γ:⟨⟩ fork duplicates a process which continues as diferent threads:
! ≜ (⃗) where (⃗) ≜ |(⃗) and ⃗ = fv( ) case allows for choosing among multiple continuations via pattern-matching (this is useful when we need to perform diferent 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 rules for this semantics are in Fig. 3.
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 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 [
Rule Cong, finally, allows our system to be written in diferent, 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 diferent subsets of the system. Without the Skip rules, a system could get stuck in two cases: 1. if two diferent 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. there exist 1′, . . . , ′− 1, ′+1, . . . ′ such that 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 ! ! 1‖2‖3‖ . . . ‖→− 1′‖2′‖3′‖ . . . ‖′ 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 diferent from the
DSCC one. In particular, the associated labels are
∈ ∪ {! | : → }.
As for DSCC these labels denotes diferent 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. snifing 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 diferent. 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 is given the value returned by the application of the output function to itself. perform an input, the two of them are able to continue in parallel as ′‖′, provided that to Γ : →−
Γ′ : ′ Γ : + →− Γ′ : ′ ExtFalse J KΓ = ff Γ : →−
Γ′ : ′ Γ : ( ? : )→− Γ′ : ′
SkipZero Γ : →0−− ? Γ : 0 SkipOutput Γ : ⟨ ⟩→−− ?
Γ : ⟨ ⟩ 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 diferent 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)‖ . . . ‖ ()‖
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 ⎪ ⎪ .⎪⎪ )⎪ ⎪⎪ ,⎪⎪ ,⎪⎪⎪⎪⎨close ,⎪ ⎪⎪ ⎪ ⎪ ⎪(︁ (⎪⎪⎪ ⎪⎪ ⎪ ⎪ ⎩⊥ moist,ℎ., )︁ ℎ.,ℎ.,ℎ.ℎ if if
ℎ.ℎ < ℎ.ℎ ∧ = valve ∧ = ℎ. ∧ √︀(ℎ. − )2 + (ℎ. − )2 < ℎ.ℎ
ℎ.ℎ > ℎ.ℎ ∧ = valve ∧ = ℎ. ∧ √︀(ℎ. − )2 + (ℎ. − )2 < ℎ.ℎ Here we see that the same message () can be interpreted in diferent 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.
end = ⟨⟩0 = (). = Γ :! Γ = { ↦→ console} = ()case of
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; ⎧(︁ ⎨ ℎ.,ℎ.,ℎ. 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: (moist, , , , ℎ) → (, , , ℎ); (valve, , , , ) → (, , , ); end where saves the moisture reading in a database and does the same with the valve status.
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′) ∈ .
be any o→f− →,−
: 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 [
Γ′1 : 1′ ‖ . . . ‖Γ′ : ′ Γ1 : 1‖ . . . ‖Γ : →−
Γ′1 : ′1‖ . . . ‖Γ′ : ′ there exist 1′ , . . . , ′ such that (⃗ ′, ⃗′) ∈ and Δ1 : 1‖ . . . ‖Δ : →−
Δ′1 : ′1‖ . . . ‖Δ′ : ′ Δ1 : 1‖ . . . ‖Δ : →−
Δ′1 : 1′ ‖ . . . ‖Δ′ : ′ bisimulation such that (, ) ∈ .
Two processes and are stateless bisimilar, written ∼ , if there exists a stateless 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 [
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 diferent 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 [
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 [
Finally, it is interesting to develop a prototypal implementation of SCC, in order to evaluate
the practical diferences of the two semantics. To this end, we will leverage the experience from
the implementation of SCEL, AbC and the AbU calculus [
This work has been supported by the Italian MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems).