Theory Communication_C2KA
section ‹Notions of Communication for \CCKAabbrv \label{sec:communication}›
text ‹
Distributed systems contain a significant number of interactions among their constituent agents. Any interaction,
direct or indirect, of an agent with its neighbouring agents can be understood as a \emph{communication}~\<^cite>‹"Milner1989aa"›.
Therefore, any potential for communication between two system agents can be characterized by the existence of a communication
path allowing for the transfer of data or control from one agent to another. Potential for communication allows system
agents to have an \emph{influence} over each other. The study of agent influence allows for the
determination of the overall structure of the distributed system of which the agents comprise. A full treatment of the potential
for communication within distributed systems specified using \CCKAabbrv has been given in~\<^cite>‹"Jaskolka2015ab"›
and~\<^cite>‹"Jaskolka2014ac"› and is highlighted below.
Consider a distributed system with~$\Agent{A}, \Agent{B} \in \A$ such that~$\Agent{A} \neq \Agent{B}$. We write~$\agent{A}{a}$
where~$\Agent{A}$ is the name given to the agent and~$a \in \CKAset$ is the agent behaviour. For~$\agent{A}{a}$ and~$\agent{B}{b}$,
we write~$\Agent{A+B}$ to denote the agent~$\bigA{a+b}$. In a sense, we extend the operators on behaviours of~$\CKAset$ to their
corresponding agents.
Communication via stimuli from agent~$\Agent{A}$ to agent~$\Agent{B}$ is said to have taken place only when
a stimulus generated by~$\Agent{A}$ \emph{influences} (i.e., causes an observable change in, directly or indirectly) the behaviour
of~$\Agent{B}$. Note that it is possible that more than one agent is influenced by the generation of the same stimulus by another
agent in the system. Formally, we say that agent~$\agent{A}{a}$ has the \emph{potential for direct communication via stimuli} with
agent~$\agent{B}{b}$ (denoted by~$\STIMcommD{\Agent{A}}{\Agent{B}}$) if and only
if~$\biglnotation{\exists}{s,t}{s,t \in \STIMbasic \nAnd t \STIMle \lOut{a}{s} }{\lAct{b}{t} \neq b}$ where~$\STIMbasic$ is the
set of all basic stimuli. A stimulus is called \emph{basic} if it is indivisible with regard to the sequential composition
operator~$\STIMdot$ of a stimulus structure. Similarly, we say that agent~$\Agent{A}$ has the \emph{potential for communication
via stimuli with agent~$\Agent{B}$ using at most~$n$ basic stimuli} (denoted by~$\STIMcommN{\Agent{A}}{\Agent{B}}{n}$) if and only
if~$\biglnotation{\exists}{\Agent{C}}{\Agent{C} \in \A \nAnd \Agent{C} \neq \Agent{A} \nAnd \Agent{C} \neq \Agent{B}}{\STIMcommN{\Agent{A}}{\Agent{C}}{(n-1)} \nAnd \STIMcommD{\Agent{C}}{\Agent{B}}}$.
More generally, we say that agent~$\Agent{A}$ has the \emph{potential for communication via stimuli} with agent~$\Agent{B}$
(denoted by~$\STIMcomm{\Agent{A}}{\Agent{B}}$) if and only if~$\biglnotation{\exists}{n}{n \ge 1}{\STIMcommN{\Agent{A}}{\Agent{B}}{n}}$.
When~$\STIMcomm{\Agent{A}}{\Agent{B}}$, there is a sequence of stimuli of arbitrary length which allows for the transfer of data or
control from agent~$\Agent{A}$ to agent~$\Agent{B}$ in the system. To simplify the Isabelle theory, we do not implement
the potential for communication using at most~$n$ basic stimuli. Instead, we give the definition of potential for direct communication
via stimuli and the fact that~$\STIMcommD{\Agent{A}}{\Agent{B}} \Longrightarrow \STIMcomm{\Agent{A}}{\Agent{B}}$ as axioms because
these are the only properties that we use about potential for communication via stimuli.
Communication via shared environments from agent~$\Agent{A}$ to agent~$\Agent{B}$ (denoted by~$\ENVcomm{\Agent{A}}{\Agent{B}}$) is
said to have taken place only when~$\Agent{A}$ has the ability to alter an element of the environment that it shares with~$\Agent{B}$
such that~$\Agent{B}$ is able to observe the alteration that was made. Formally, we say that agent~$\agent{A}{a}$ has the
\emph{potential for direct communication via shared environments} with agent~$\agent{B}{b}$ (denoted by~$\ENVcommD{\Agent{A}}{\Agent{B}}$)
if and only if~$\dep{b}{a}$ where~$\depOp$ is a given dependence relation. More generally, agent~$\Agent{A}$ has the
\emph{potential for communication via shared environments} with agent~$\Agent{B}$ (denoted by~$\ENVcomm{\Agent{A}}{\Agent{B}}$) if and
only if~$\depTC{b}{a}$ where~$\depOpTC$ is the transitive closure of the given dependence relation. This means that if two agents respect
the given dependence relation, then there is a potential for communication via shared environments.
›
theory Communication_C2KA
imports Topology_C2KA
begin
text ‹
The locale \emph{communication-c2ka} extends \emph{topology-c2ka} to include aspects of potential for communication
among distributed system agents.
›
locale communication_c2ka = topology_c2ka +
fixes dcs :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "→⇩𝒮" 50)
and pcs :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "→⇩𝒮⇧+" 50)
and dce :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "→⇩ℰ" 50)
and pce :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "→⇩ℰ⇧+" 50)
and pdc :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "↝" 50)
and pfc :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "↝⇧+" 50)
and stimuli_connected :: "'a set ⇒ bool"
and universally_influential :: "'a::cka × 'a set ⇒ bool"
assumes dcs_def: "a →⇩𝒮 b ⟷
(∃ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,a) ∧ t ∘ b ≠ b)"
and pdc_def: "a ↝ b ⟷ (a →⇩𝒮 b ∨ a →⇩ℰ b)"
and zero_dce: "¬(0 →⇩ℰ a)"
and one_dce: "¬(1 →⇩ℰ a)"
and dce_zero: "¬(a →⇩ℰ 0)"
and dce_one: "¬(a →⇩ℰ 1)"
and sum_dce: "(A + B →⇩ℰ C) ⟷ (A →⇩ℰ C ∨ B →⇩ℰ C)"
and dce_sum: "(A →⇩ℰ B + C) ⟷ (A →⇩ℰ B ∨ A →⇩ℰ C)"
and dcs_pcs: "A →⇩𝒮 B ⟹ A →⇩𝒮⇧+ B"
and stimuli_connected_def: "stimuli_connected(𝒞) ⟷
(∀ X⇩1 X⇩2. X⇩1 ∩ X⇩2 = {} ∧ X⇩1 ∪ X⇩2 = 𝒞 ∧ X⇩1 ≠ {} ∧ X⇩2 ≠ {} ⟶
(∃ A B. A ∈ X⇩1 ∧ B ∈ X⇩2 ∧ (A →⇩𝒮⇧+ B ∨ B →⇩𝒮⇧+ A)))"
and universally_influential_def: "universally_influential(A,𝒞) ⟷
A ∈ 𝒞 ∧ (∀ B. B ∈ 𝒞 ∧ B ≠ A ⟶ A →⇩𝒮⇧+ B)"
begin
subsection ‹Stimuli-Connected Systems \& Universally Influential Agents \label{sub:stimuli_connected_universally_influential}›
text ‹
Two subsets~$X_1$ and~$X_2$ of~$\A$ form a partition of~$\A$ if and only if~$X_1 \cap X_2 = \STbot$ and~$X_1 \cup X_2 = \A$. A distributed system
of agents~$\A$ is called \emph{stimuli-connected} if and only if for every~$X_1$ and~$X_2$ nonempty that form a partition of~$\A$, we
have~$\lnotation{\exists}{\Agent{A},\Agent{B}}{\Agent{A} \in X_1 \nAnd \Agent{B} \in X_2}{\STIMcomm{\Agent{A}}{\Agent{B}} \Ors \STIMcomm{\Agent{B}}{\Agent{A}}}$.
Otherwise,~$\A$ is called \emph{stimuli-disconnected}. In a stimuli-connected system, every agent is a participant, either as the source or sink,
of at least one direct communication via stimuli.
›
text ‹
An agent~$\Agent{A} \in \A$ is called \emph{universally influential} if and only
if~$\biglnotation{\forall}{\Agent{B}}{\Agent{B} \in \A \STdiff \set{\Agent{A}}}{\STIMcomm{\Agent{A}}{\Agent{B}}}$.
A universally influential agent is able to generate some stimuli that influences the behaviour, either directly or
indirectly, of each other agent in the system.
›
text ‹
Lemma \emph{universally-influential-stimuli-connected} shows that the existence of a universally influential agent yields a stimuli-connected system.
›
lemma universally_influential_stimuli_connected:
"(∃ A. universally_influential(A,𝒞)) ⟶ stimuli_connected(𝒞)"
unfolding universally_influential_def stimuli_connected_def
proof (intro allI impI)
fix X⇩1 X⇩2
show "(∃A. A ∈ 𝒞 ∧ (∀B. B ∈ 𝒞 ∧ B ≠ A ⟶ A →⇩𝒮⇧+ B)) ⟹
X⇩1 ∩ X⇩2 = {} ∧ X⇩1 ∪ X⇩2 = 𝒞 ∧ X⇩1 ≠ {} ∧ X⇩2 ≠ {} ⟹
(∃ A B. A ∈ X⇩1 ∧ B ∈ X⇩2 ∧ (A →⇩𝒮⇧+ B ∨ B →⇩𝒮⇧+ A))"
proof -
assume "(∃A. A ∈ 𝒞 ∧ (∀B. B ∈ 𝒞 ∧ B ≠ A ⟶ A →⇩𝒮⇧+ B))"
from this obtain A where Aui: "A ∈ 𝒞 ∧ (∀B. B ∈ 𝒞 ∧ B ≠ A ⟶
A →⇩𝒮⇧+ B)" by auto
show "X⇩1 ∩ X⇩2 = {} ∧ X⇩1 ∪ X⇩2 = 𝒞 ∧ X⇩1 ≠ {} ∧ X⇩2 ≠ {} ⟹
(∃A B. A ∈ X⇩1 ∧ B ∈ X⇩2 ∧ (A →⇩𝒮⇧+ B ∨ B →⇩𝒮⇧+ A))"
proof -
assume partition:"X⇩1 ∩ X⇩2 = {} ∧ X⇩1 ∪ X⇩2 = 𝒞 ∧ X⇩1 ≠ {} ∧ X⇩2 ≠ {}"
show "(∃A B. A ∈ X⇩1 ∧ B ∈ X⇩2 ∧ (A →⇩𝒮⇧+ B ∨ B →⇩𝒮⇧+ A))"
proof cases
assume in1: "A ∈ X⇩1"
from partition obtain B where in2: "B ∈ X⇩2" by auto
have "A = B ⟹ False"
proof -
assume "A = B"
hence "A ∈ X⇩2" by (simp add: in2)
moreover have "A ∈ X⇩1" by (rule in1)
ultimately have "A ∈ X⇩1 ∩ X⇩2" by simp
hence "A ∈ {}" by (simp add: partition)
thus "False" by simp
qed
hence "A ≠ B" by auto
moreover have "B ∈ 𝒞"
proof -
from partition have "𝒞 = X⇩1 ∪ X⇩2" by auto
hence "X⇩2 ⊆ 𝒞" by simp
thus ?thesis by (auto simp add: in2)
qed
ultimately have "A →⇩𝒮⇧+ B" by (auto simp add: Aui in2)
thus ?thesis
by (rule_tac x="A" in exI, rule_tac x="B" in exI, simp add: in1 in2)
next
assume notin1: "A ∉ X⇩1"
moreover have "A ∈ 𝒞" by (simp add: Aui)
moreover have "X⇩1 ∪ X⇩2 = 𝒞" by (simp add: partition)
ultimately have in2: "A ∈ X⇩2" by auto
from partition obtain B where in1: "B ∈ X⇩1" by auto
have "B = A ⟹ False"
proof -
assume "B = A"
hence "B ∈ X⇩2" by (simp add: in2)
moreover have "B ∈ X⇩1" by (rule in1)
ultimately have "B ∈ X⇩1 ∩ X⇩2" by simp
hence "B ∈ {}" by (simp add: partition)
thus "False" by simp
qed
hence "B ≠ A" by auto
moreover have "B ∈ 𝒞"
proof -
from partition have "𝒞 = X⇩1 ∪ X⇩2" by auto
hence "X⇩1 ⊆ 𝒞" by simp
thus ?thesis by (auto simp add: in1)
qed
ultimately have "A →⇩𝒮⇧+ B" by (auto simp add: Aui in2)
thus ?thesis
by (rule_tac x="B" in exI, rule_tac x="A" in exI, simp add: in1 in2)
qed
qed
qed
qed
text ‹
Lemma \emph{fixed-no-stimcomm} shows that no agent has the potential for communication via stimuli with an agent that has a fixed point behaviour.
›
lemma fixed_no_stimcomm: "fixed(A) ⟶ (∀ B. ¬(B →⇩𝒮 A))"
unfolding fixed_def
proof (rule impI)
assume hyp: "∀s. s ≠ 𝔡 ⟶ s ∘ A = A"
have "∃ B. B →⇩𝒮 A ⟹ False"
proof -
assume "∃ B. B →⇩𝒮 A"
then obtain B where "B →⇩𝒮 A" by auto
hence "∃ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,B) ∧ t ∘ A ≠ A"
by (simp only: dcs_def)
then obtain s t where st: "s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,B) ∧ t ∘ A ≠ A"
by auto
hence "t ≠ 𝔡" by (auto simp only: zero_not_basic)
hence "t ∘ A = A" by (simp add: hyp)
thus False by (auto simp add: st)
qed
thus "(∀ B. ¬(B →⇩𝒮 A))" by auto
qed
subsection ‹Preserving the Potential for Communication under Non-Determinism \label{sub:non_determinism}›
subsubsection ‹Potential for Communication via Stimuli \label{ssub:pfc_stim}›
text ‹
The following results show how the potential for communication via stimuli can be preserved when non-determinism is introduced among agents.
Specifically, Lemma \emph{source-nondet-stimcomm} states that when non-determinism is added at the source of a potential communication path via stimuli, the potential
for communication via stimuli is always preserved. On the other hand, Lemma \emph{sink-nondet-stimcomm} states that when non-determinism is added at the sink of a
potential communication path via stimuli, the potential for communication is preserved only if there does not exist any basic stimulus that is
generated by the source that influences agent~$\Agent{B}$ and agent~$\Agent{C}$ to behave as a sub-behaviour of agent~$\Agent{B + C}$. This
condition ensures that agent~$\Agent{B + C}$ cannot have a fixed point behaviour.
›
lemma source_nondet_stimcomm: "(B →⇩𝒮 C) ⟹ ((A + B) →⇩𝒮 C)"
proof -
assume "B →⇩𝒮 C"
then obtain s t where st: "s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,B) ∧ t ∘ C ≠ C"
by (auto simp only: dcs_def)
show "(A + B) →⇩𝒮 C"
unfolding dcs_def
by (rule_tac x="s" in exI, rule_tac x="t" in exI, auto simp add: st inf_add_S_left)
qed
lemma comm_source_nondet_stimcomm: "(B →⇩𝒮 C) ⟹ ((B + A) →⇩𝒮 C)"
by (simp add: source_nondet_stimcomm algebra_simps)
lemma sink_sum_stimcomm: "(∃ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ∧
¬(t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C)) ⟹ (A →⇩𝒮 B + C)"
proof -
assume "∃ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ∧
¬(t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C)"
then obtain s t where st: "s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ∧
¬(t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C)" by auto
have "t ∘ (B + C) = B + C ⟹ False"
proof -
assume fixbc: "t ∘ (B + C) = B + C"
have "t ∘ B ≤⇩𝒦 t ∘ (B + C)"
by (simp, rule inf_add_K_right)
moreover have "t ∘ C ≤⇩𝒦 t ∘ (B + C)"
by (simp, rule inf_add_K_left)
ultimately have "t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C"
by (simp only: fixbc)
thus False by (simp only: st)
qed
thus "A →⇩𝒮 B + C"
unfolding dcs_def
by (rule_tac x="s" in exI, rule_tac x="t" in exI, auto simp only: st)
qed
lemma sink_nondet_stimcomm: "A →⇩𝒮 B ⟹ (∀ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A)
⟶ ¬(t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C)) ⟹ (A →⇩𝒮 B + C)"
proof (rule sink_sum_stimcomm)
assume h1: "A →⇩𝒮 B"
assume h2: "(∀ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ⟶
¬(t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C))"
show "∃ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ∧
¬(t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C)"
proof -
from h1 obtain s t where "s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ∧ t ∘ B ≠ B"
by (auto simp only: dcs_def)
from this h2 have "s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ∧
¬(t ∘ B ≤⇩𝒦 B + C ∧ t ∘ C ≤⇩𝒦 B + C)" by auto
thus ?thesis
by (rule_tac x="s" in exI, rule_tac x="t" in exI, auto)
qed
qed
subsubsection ‹Potential for Communication via Shared Environments \label{ssub:pfc_env}›
text ‹
Lemmas \emph{source-nondet-envcomm} and \emph{sink-nondet-envcomm} show how the potential for communication via shared environments is preserved when non-determinism is
introduced at the source or the sink of a potential communication path via shared environments.
›
lemma source_nondet_envcomm: "B →⇩ℰ C ⟹ (A + B) →⇩ℰ C"
by (simp add: sum_dce)
lemma sink_nondet_envcomm: "A →⇩ℰ B ⟹ A →⇩ℰ (B + C)"
by (simp add: dce_sum)
subsection ‹Preserving the Potential for Communication with Agent Behaviour Modifications\label{sub:preservation}›
text ‹
The following results identify the conditions constraining the modifications that can be made to the source or sink agent involved in a direct potential for communication to
preserve the communication in a distributed system. In this way, it demonstrates the conditions under which a modification to an agent behaviour can be made while maintaining
the communicating behaviour of the agents in the system.
Specifically, Lemma \emph{sink-seq-stimcomm} shows how the sequential composition of an additional behaviour on the left of a sink agent will not affect the potential for communication
provided that every stimulus that is generated by the source agent either does not fix the behaviour of the first component of the sequential composition, or causes the
first component of the sequential composition to generate a stimulus that does not fix the behaviour of the second component of the sequential composition. Alternatively,
Lemma \emph{nondet-right-source-communication} shows how non-determinism added on the right of a source agent will not affect the potential for communication provided that
the non-deterministic behaviours can be influenced by the source agent to stop being a sub-behaviour of the non-deterministic behaviour.
›
lemma sink_seq_stimcomm: "A →⇩𝒮 B
⟹ ∀ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ⟶ λ(t,C) = t ⟹ A;C →⇩𝒮 B"
proof -
assume "A →⇩𝒮 B"
then obtain s t where st: "s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ∧ t ∘ B ≠ B"
unfolding dcs_def by auto
assume "∀ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A) ⟶ λ(t,C) = t"
from this st have tfix: "λ(t,C) = t" by auto
have "λ(t,C) ≤⇩𝒮 λ(λ(s,A),C)" by (simp add: inf_S_next_stimulus st)
hence "t ≤⇩𝒮 λ (λ (s, A), C)" by (simp add: tfix)
thus "A;C →⇩𝒮 B"
unfolding dcs_def
by (rule_tac x="s" in exI, rule_tac x="t" in exI, simp add: st)
qed
lemma nondet_right_source_communication: "A ↝ C ∧ C ↝ B ⟹ (∀ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A)
⟶ ¬(t ∘ C ≤⇩𝒦 C + D ∧ t ∘ D ≤⇩𝒦 C + D)) ⟹ A ↝ C+D ∧ C+D ↝ B"
proof -
assume h1:"A ↝ C ∧ C ↝ B"
assume h2:"(∀ s t. s ∈ 𝒮⇩a ∧ t ∈ 𝒮⇩a ∧ t ≤⇩𝒮 λ(s,A)
⟶ ¬(t ∘ C ≤⇩𝒦 C + D ∧ t ∘ D ≤⇩𝒦 C + D))"
from h2 have hs: "A →⇩𝒮 C ⟹ A →⇩𝒮 C+D"
by (auto simp add: sink_nondet_stimcomm)
have "A ↝ C ⟹ A ↝ C+D"
unfolding pdc_def
using dce_sum hs by blast
moreover have "C ↝ B ⟹ C + D ↝ B"
unfolding pdc_def
using comm_source_nondet_stimcomm sum_dce by blast
ultimately show "A ↝ C+D ∧ C+D ↝ B"
by (simp add: h1)
qed
end
end