# Theory Stimuli

(* Title: C2KA Stimulus Structure Author: Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019 Maintainers: Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca> *) section ‹Stimulus Structure \label{sec:stimulus_structure}› text ‹ A stimulus constitutes the basis for behaviour. Because of this, each discrete, observable event introduced to a system, such as that which occurs through the communication among agents or from the system environment, is considered to be a stimulus which invokes a response from each system agent. A \emph{stimulus structure} is an idempotent semiring~$\STIMstructure$ with a multiplicatively absorbing~$\Dstim$ and identity~$\Nstim$. Within the context of stimuli,~$\STIMset$ is a set of stimuli which may be introduced to a system. The operator~$\STIMplus$ is interpreted as a choice between two stimuli and the operator~$\STIMdot$ is interpreted as a sequential composition of two stimuli. The element~$\Dstim$ represents the \emph{deactivation stimulus} which influences all agents to become inactive and the element~$\Nstim$ represents the \emph{neutral stimulus} which has no influence on the behaviour of all agents. The natural ordering relation~$\STIMle$ on a stimulus structure~$\stim$ is called the sub-stimulus relation. For stimuli~$s,t \in \STIMset$, we write~$s \STIMle t$ and say that~$s$ is a sub-stimulus of~$t$ if and only if~$s \STIMplus t = t$. › theory Stimuli imports Main begin text ‹ The class \emph{stimuli} describes the stimulus structure for \CCKAabbrv. We do not use Isabelle's built-in theories for groups and orderings to allow a different notation for the operations on stimuli to be consistent with~\cite{Jaskolka2015ab}. › class plus_ord = fixes leq::"'a ⇒ 'a ⇒ bool" ("(_/ ≤⇩_{𝒮}_)" [51, 51] 50) fixes add::"'a ⇒ 'a ⇒ 'a" (infixl "⊕" 65) assumes leq_def: "x ≤⇩_{𝒮}y ⟷ x ⊕ y = y" and add_assoc: "(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)" and add_comm: "x ⊕ y = y ⊕ x" begin notation leq ("'(≤')") and leq ("(_/ ≤⇩_{𝒮}_)" [51, 51] 50) end class stimuli = plus_ord + fixes seq_comp::"'a ⇒ 'a ⇒ 'a" (infixl "⊙" 70) fixes neutral :: 'a ("𝔫") and deactivation :: 'a ("𝔡") and basic :: "'a set" ("𝒮⇩_{a}") assumes stim_idem [simp]: "x ⊕ x = x" and seq_nl [simp]: "𝔫 ⊙ x = x" and seq_nr [simp]: "x ⊙ 𝔫 = x" and add_zero [simp]: "𝔡 ⊕ x = x" and absorbingl [simp]: "𝔡 ⊙ x = 𝔡" and absorbingr [simp]: "x ⊙ 𝔡 = 𝔡" and zero_not_basic: "𝔡 ∉ 𝒮⇩_{a}" begin lemma inf_add_S_right: "x ≤⇩_{𝒮}y ⟹ x ≤⇩_{𝒮}y ⊕ z" unfolding leq_def by (simp add: add_assoc [symmetric]) lemma inf_add_S_left: "x ≤⇩_{𝒮}y ⟹ x ≤⇩_{𝒮}z ⊕ y" by (simp add: add_comm inf_add_S_right) lemma leq_refl [simp]: "x ≤⇩_{𝒮}x" unfolding leq_def by simp end end

# Theory CKA

(* Title: C2KA Behaviour Structure (Concurrent Kleene Algebra) Author: Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019 Maintainers: Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca> *) section ‹Behaviour Structure \label{sec:behaviour_structure}› text ‹ Hoare et al.~\cite{Hoare2011aa} presented the framework of Concurrent Kleene Algebra (\CKAabbrv) which captures the concurrent behaviour of agents. The framework of \CKAabbrv is adopted to describe agent behaviours in distributed systems. For a \CKAabbrv~$\CKAstructure$,~$\CKAset$ is a set of possible behaviours. The operator~$+$ is interpreted as a choice between two behaviours, the operator~$\CKAseq$ is interpreted as a sequential composition of two behaviours, and the operator~$\CKApar$ is interpreted as a parallel composition of two behaviours. The operators~$\CKAiterSeq{\,}$ and~$\CKAiterPar{\,}$ are interpreted as a finite sequential iteration and a finite parallel iteration of behaviours, respectively. The element~$0$ represents the behaviour of the \emph{inactive agent} and the element~$1$ represents the behaviour of the \emph{idle agent}. Associated with a \CKAabbrv~$\cka$ is a natural ordering relation~$\CKAle$ related to the semirings upon which the \CKAabbrv is built which is called the sub-behaviour relation. For behaviours~$a,b \in \CKAset$, we write~$a \CKAle b$ and say that~$a$ is a sub-behaviour of~$b$ if and only if~$a + b = b$. › theory CKA imports Main begin no_notation rtrancl ("(_⇧^{*})" [1000] 999) notation times (infixl "*" 70) and less_eq ("'(≤⇩_{𝒦}')") and less_eq ("(_/ ≤⇩_{𝒦}_)" [51, 51] 50) text ‹ The class \emph{cka} contains an axiomatisation of Concurrent Kleene Algebras and a selection of useful theorems.› class join_semilattice = ordered_ab_semigroup_add + assumes leq_def: "x ≤ y ⟷ x + y = y" and le_def: "x < y ⟷ x ≤ y ∧ x ≠ y" and add_idem [simp]: "x + x = x" begin lemma inf_add_K_right: "a ≤⇩_{𝒦}a + b" unfolding leq_def by (simp add: add_assoc[symmetric]) lemma inf_add_K_left: "a ≤⇩_{𝒦}b + a" by (simp only: add_commute, fact inf_add_K_right) end class dioid = semiring + one + zero + join_semilattice + assumes par_onel [simp]: "1 * x = x" and par_oner [simp]: "x * 1 = x" and add_zerol [simp]: "0 + x = x" and annil [simp]: "0 * x = 0" and annir [simp]: "x * 0 = 0" class kleene_algebra = dioid + fixes star :: "'a ⇒ 'a" ("_⇧^{*}" [101] 100) assumes star_unfoldl: "1 + x * x⇧^{*}≤⇩_{𝒦}x⇧^{*}" and star_unfoldr: "1 + x⇧^{*}* x ≤⇩_{𝒦}x⇧^{*}" and star_inductl: "z + x * y ≤⇩_{𝒦}y ⟹ x⇧^{*}* z ≤⇩_{𝒦}y" and star_inductr: "z + y * x ≤⇩_{𝒦}y ⟹ z * x⇧^{*}≤⇩_{𝒦}y" class cka = kleene_algebra + fixes seq :: "'a ⇒ 'a ⇒ 'a" (infixl ";" 70) and seqstar :: "'a ⇒ 'a" ("_⇧^{;}" [101] 100) assumes seq_assoc: "x ; (y ; z) = (x ; y) ; z" and seq_rident [simp]: "x ; 1 = x" and seq_lident [simp]: "1 ; x = x" and seq_rdistrib [simp]: "(x + y);z = x;z + y;z" and seq_ldistrib [simp]: "x;(y + z) = x;y + x;z" and seq_annir [simp]: "x ; 0 = 0" and seq_annil [simp]: "0 ; x = 0" and seqstar_unfoldl: "1 + x ; x⇧^{;}≤⇩_{𝒦}x⇧^{;}" and seqstar_unfoldr: "1 + x⇧^{;}; x ≤⇩_{𝒦}x⇧^{;}" and seqstar_inductl: "z + x ; y ≤⇩_{𝒦}y ⟹ x⇧^{;}; z ≤⇩_{𝒦}y" and seqstar_inductr: "z + y ; x ≤⇩_{𝒦}y ⟹ z ; x⇧^{;}≤⇩_{𝒦}y" and exchange: "(a*b) ; (c*d) ≤⇩_{𝒦}(b;c) * (a;d)" begin interpretation cka: kleene_algebra plus less_eq less "1" "0" seq seqstar by (unfold_locales, simp_all add: seq_assoc seqstar_unfoldl seqstar_unfoldr seqstar_inductl seqstar_inductr) lemma par_comm: "a * b = b * a" proof - have "(b*a) ; (1*1) ≤⇩_{𝒦}(a;1) * (b;1)" by (simp only: exchange) hence "b * a ≤⇩_{𝒦}a * b" by (simp) hence "a * b ≤⇩_{𝒦}b * a ⟷ a * b = b * a" by (rule antisym_conv) moreover have "a * b ≤⇩_{𝒦}b * a" proof - have "(a*b) ; (1*1) ≤⇩_{𝒦}(b;1) * (a;1)" by (rule exchange) thus ?thesis by (simp) qed ultimately show ?thesis by (auto) qed lemma exchange_2: "(a*b) ; (c*d) ≤⇩_{𝒦}(a;c) * (b;d)" proof - have "(b*a) ; (c*d) ≤⇩_{𝒦}(a;c) * (b;d)" by (rule exchange) thus ?thesis by (simp add: par_comm) qed lemma seq_inf_par: "a ; b ≤⇩_{𝒦}a * b" proof - have "(1*a) ; (1*b) ≤⇩_{𝒦}(a;1) * (1;b)" by (rule exchange) thus ?thesis by simp qed lemma add_seq_inf_par: "a;b + b;a ≤⇩_{𝒦}a*b" proof - have "a;b ≤⇩_{𝒦}a*b" by (rule seq_inf_par) moreover have "b;a ≤⇩_{𝒦}b*a" by (rule seq_inf_par) ultimately have "a;b + b;a ≤⇩_{𝒦}a*b + b*a" by (simp add: add_mono) thus ?thesis by (simp add: par_comm) qed lemma exchange_3: "(a*b) ; c ≤⇩_{𝒦}a * (b;c)" proof - have "(a*b) ; (1*c) ≤⇩_{𝒦}(a;1) * (b;c)" by (rule exchange_2) thus ?thesis by simp qed lemma exchange_4: "a ; (b*c) ≤⇩_{𝒦}(a;b) * c" proof - have "(1*a) ; (b*c) ≤⇩_{𝒦}(a;b) * (1;c)" by (rule exchange) thus ?thesis by simp qed lemma seqstar_inf_parstar: "a⇧^{;}≤⇩_{𝒦}a⇧^{*}" proof - have "a ; a⇧^{*}≤⇩_{𝒦}a * a⇧^{*}" by (rule seq_inf_par) hence "1 + a ; a⇧^{*}≤⇩_{𝒦}1 + a * a⇧^{*}" by (simp add: add_left_mono) hence "1 + a ; a⇧^{*}≤⇩_{𝒦}a⇧^{*}" by (simp add: star_unfoldl order_trans) hence "a⇧^{;}; 1 ≤⇩_{𝒦}a⇧^{*}" by (rule seqstar_inductl) thus ?thesis by simp qed end end

# Theory C2KA

(* Title: C2KA: Communicating Concurrent Kleene Algebra Author: Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019 Maintainers: Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca> *) section ‹Communicating Concurrent Kleene Algebra \label{sec:ccka}› text ‹ \CCKAabbrv extends the algebraic foundation of \CKAabbrv with the notions of semimodules and stimulus structures to capture the influence of stimuli on the behaviour of system agents. A \CCKAabbrv is a mathematical system consisting of two semimodules which describe how a stimulus structure~$\stim$ and a \CKAabbrv~$\cka$ mutually act upon one another to characterize the response invoked by a stimulus on an agent behaviour as a next behaviour and a next stimulus. The \leftSemimodule{\stim}~$\ActSemimodule$ describes how the stimulus structure~$\stim$ acts upon the \CKAabbrv~$\cka$ via the mapping~$\actOp$. The mapping~$\actOp$ is called the \emph{next behaviour mapping} and it describes how a stimulus invokes a behavioural response from a given agent. From~$\ActSemimodule$, the next behaviour mapping~$\actOp$ distributes over~$+$ and~$\STIMplus$. Additionally, since~$\ActSemimodule$ is unitary, it is the case that the neutral stimulus has no influence on the behaviour of all agents and since~$\ActSemimodule$ is zero-preserving, the deactivation stimulus influences all agents to become inactive. The \rightSemimodule{\cka}~$\OutSemimodule$ describes how the \CKAabbrv~$\cka$ acts upon the stimulus structure~$\stim$ via the mapping~$\outOp$. The mapping~$\outOp$ is called the \emph{next stimulus mapping} and it describes how a new stimulus is generated as a result of the response invoked by a given stimulus on an agent behaviour. From~$\OutSemimodule$, the next stimulus mapping~$\outOp$ distributes over~$\STIMplus$ and~$+$. Also, since~$\OutSemimodule$ is unitary, it is the case that the idle agent forwards any stimulus that acts on it and since~$\OutSemimodule$ is zero-preserving, the inactive agent always generates the deactivation stimulus. A full account of \CCKAabbrv can be found in~\cite{Jaskolka2015ab,Jaskolka2013aa,Jaskolka2014aa}. › theory C2KA imports CKA Stimuli begin no_notation comp (infixl "∘" 55) and rtrancl ("(_⇧^{*})" [1000] 999) text ‹ The locale \emph{c2ka} contains an axiomatisation of \CCKAabbrv and some basic theorems relying on the axiomatisations of stimulus structures and \CKAabbrv provided in Sections~\ref{sec:stimulus_structure} and~\ref{sec:behaviour_structure}, respectively. We use a locale instead of a class in order to allow stimuli and behaviours to have two different types. › locale c2ka = fixes next_behaviour :: "'b::stimuli ⇒ 'a::cka ⇒ 'a" (infixr "∘" 75) and next_stimulus :: "('b::stimuli × 'a::cka) ⇒ 'b" ("λ") assumes lsemimodule1 [simp]: "s ∘ (a + b) = (s ∘ a) + (s ∘ b)" and lsemimodule2 [simp]: "(s ⊕ t) ∘ a = (s ∘ a) + (t ∘ a)" and lsemimodule3 [simp]: "(s ⊙ t) ∘ a = s ∘ (t ∘ a)" and lsemimodule4 [simp]: "𝔫 ∘ a = a" and lsemimodule5 [simp]: "𝔡 ∘ a = 0" and rsemimodule1 [simp]: "λ(s ⊕ t, a) = λ(s, a) ⊕ λ(t, a)" and rsemimodule2 [simp]: "λ(s, a + b) = λ(s, a) ⊕ λ(s, b)" and rsemimodule3 [simp]: "λ(s, a ; b) = λ(λ(s, a), b)" and rsemimodule4 [simp]: "λ(s, 1) = s" and rsemimodule5 [simp]: "λ(s, 0) = 𝔡" and cascadingaxiom [simp]: "s ∘ (a ; b) = (s ∘ a);(λ(s, a) ∘ b)" and cascadingoutputlaw: "a ≤⇩_{𝒦}c ∨ b = 1 ∨ (s ∘ a);(λ(s,c) ∘ b) = 0" and sequentialoutputlaw [simp]: "λ(s ⊙ t, a) = λ(s, t∘a) ⊙ λ(t, a)" and onefix: "s = 𝔡 ∨ s ∘ 1 = 1" and neutralunmodified: "a = 0 ∨ λ(𝔫, a) = 𝔫" begin text ‹ Lemmas \emph{inf-K-S-next-behaviour} and \emph{inf-K-S-next-stimulus} show basic results from the axiomatisation of \CCKAabbrv. › lemma inf_K_S_next_behaviour: "(a ≤⇩_{𝒦}b ∧ s ≤⇩_{𝒮}t) ⟹ (s ∘ a ≤⇩_{𝒦}t ∘ b)" unfolding Stimuli.leq_def CKA.leq_def proof - assume hyp: "a + b = b ∧ s ⊕ t = t" hence "s ∘ a + t ∘ b = s ∘ a + (s ⊕ t) ∘ b" by simp hence "s ∘ a + t ∘ b = s ∘ a + s ∘ b + t ∘ b" by (simp add: algebra_simps) moreover have "s ∘ (a + b) = s ∘ a + s ∘ b" by simp ultimately have "s ∘ a + t ∘ b = s ∘ (a + b) + t ∘ b" by simp hence "s ∘ a + t ∘ b = s ∘ b + t ∘ b" by (simp add: hyp) hence "s ∘ a + t ∘ b = (s ⊕ t) ∘ b" by simp thus "s ∘ a + t ∘ b = t ∘ b" by (simp add: hyp) qed lemma inf_K_S_next_stimulus: "a ≤⇩_{𝒦}b ∧ s ≤⇩_{𝒮}t ⟹ λ(s,a) ≤⇩_{𝒮}λ(t,b)" unfolding Stimuli.leq_def CKA.leq_def proof - assume hyp: "a + b = b ∧ s ⊕ t = t" hence "λ(s,a) ⊕ λ(t,b) = λ(s,a) ⊕ λ(s⊕t,b)" by simp hence "λ(s,a) ⊕ λ(t,b) = λ(s,a) ⊕ λ(s,b) ⊕ λ(t,b)" by (simp add: add_assoc) moreover have "λ(s,a+b) = λ(s,a) ⊕ λ(s,b)" by simp ultimately have "λ(s,a) ⊕ λ(t,b) = λ(s,a+b) ⊕ λ(t,b)" by simp hence "λ(s,a) ⊕ λ(t,b) = λ(s,b) ⊕ λ(t,b)" by (simp add: hyp) hence "λ(s,a) ⊕ λ(t,b) = λ(s⊕t,b)" by simp thus "λ(s,a) ⊕ λ(t,b) = λ(t,b)" by (simp add: hyp) qed text ‹ The following lemmas show additional results from the axiomatisation of \CCKAabbrv which follow from lemmas \emph{inf-K-S-next-behaviour} and \emph{inf-K-S-next-stimulus}. › lemma inf_K_next_behaviour: "a ≤⇩_{𝒦}b ⟹ s ∘ a ≤⇩_{𝒦}s ∘ b" by (simp add: inf_K_S_next_behaviour) lemma inf_S_next_behaviour: "s ≤⇩_{𝒮}t ⟹ s ∘ a ≤⇩_{𝒦}t ∘ a" by (simp add: inf_K_S_next_behaviour) lemma inf_add_seq_par_next_behaviour: "s ∘ (a;b + b;a) ≤⇩_{𝒦}s ∘ (a*b)" using inf_K_next_behaviour add_seq_inf_par by blast lemma inf_seqstar_parstar_next_behaviour: "s ∘ a⇧^{;}≤⇩_{𝒦}s ∘ a⇧^{*}" by (simp add: seqstar_inf_parstar inf_K_next_behaviour) lemma inf_S_next_stimulus: "s ≤⇩_{𝒮}t ⟹ λ(s,a) ≤⇩_{𝒮}λ(t,a)" by (simp add: inf_K_S_next_stimulus) lemma inf_K_next_stimulus: "a ≤⇩_{𝒦}b ⟹ λ(s,a) ≤⇩_{𝒮}λ(s,b)" by (simp add: inf_K_S_next_stimulus) lemma inf_add_seq_par_next_stimulus: "λ(s, a;b + b;a) ≤⇩_{𝒮}λ(s, a*b)" proof - have "a;b ≤⇩_{𝒦}a*b" by (rule seq_inf_par) moreover have "b;a ≤⇩_{𝒦}b*a" by (rule seq_inf_par) ultimately have "a;b + b;a ≤⇩_{𝒦}a*b + b*a" by (simp add: add_mono) hence "a;b + b;a ≤⇩_{𝒦}a*b" by (simp add: par_comm) thus "λ(s, a;b + b;a) ≤⇩_{𝒮}λ(s, a*b)" by (rule inf_K_next_stimulus) qed lemma inf_seqstar_parstar_next_stimulus: "λ(s, a⇧^{;}) ≤⇩_{𝒮}λ(s, a⇧^{*})" by (simp add: seqstar_inf_parstar inf_K_next_stimulus) end end

# Theory Topology_C2KA

(* Title: Notions of Topology for C2KA Author: Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019 Maintainers: Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca> *) section ‹Notions of Topology for \CCKAabbrv \label{sec:topology}› text ‹ Orbits, stabilisers, and fixed points are notions that allow us to perceive a kind of topology of a system with respect to the stimulus-response relationships among system agents. In this context, the term ``topology'' is used to capture the relationships (influence) and connectedness via stimuli of the agents in a distributed system. It intends to capture a kind of reachability in terms of the possible behaviours for a given agent. A \CCKAabbrv consists of two semimodules~$\ActSemimodule$ and~$\OutSemimodule$ for which we have a \leftAct{\stim}~$\lSact$ and a \rightAct{\cka}~$\rKact$. Therefore, there are two complementary notions of orbits, stabilisers, and fixed points within the context of agent behaviours and stimuli, respectively. In this way, one can use these notions to think about distributed systems from two different perspectives, namely the behavioural perspective provided by the action of stimuli on agent behaviours described by~$\ActSemimodule$ and the external event (stimulus) perspective provided by the action of agent behaviours on stimuli described by~$\OutSemimodule$. In this section, only the treatment of these notions with respect to the \leftSemimodule{\stim}~$\ActSemimodule$ and agent behaviours is provided. The same notions for the \rightSemimodule{\cka}~$\OutSemimodule$ and stimuli can be provided in a very similar way. When discussing the interplay between \CCKAabbrv and the notions of orbits, stabilisers, and fixed points, the partial order of sub-behaviours~$\CKAle$ is extended to sets in order to express sets of agent behaviours encompassing one another. For two subsets of agent behaviours~$A,B \STleq \CKAset$, we say that~$A$ \emph{is encompassed by}~$B$ (or~$B$ \emph{encompasses}~$A$), written~$\CKAencompass{A}{B}$, if and only if~$\biglnotation{\forall}{a}{a \in A}{\lnotation{\exists}{b}{b \in B}{a \CKAle b}}$. In essence,~$A \CKAenc B$ indicates that every behaviour contained within the set~$A$ is a sub-behaviour of at least one behaviour in the set~$B$. The encompassing relation~$\STIMenc$ for stimuli can be defined similarly. Throughout this section, let~$\ActSemimodule$ be the unitary and zero-preserving \leftSemimodule{\stim} of a \CCKAabbrv and let~$a \in \CKAset$. › theory Topology_C2KA imports C2KA begin no_notation comp (infixl "∘" 55) and rtrancl ("(_⇧^{*})" [1000] 999) text ‹ The locale \emph{topology-c2ka} extends the axiomatisation of \emph{c2ka} to support the notions of topology. › locale topology_c2ka = c2ka + fixes orbit :: "'a::cka ⇒ 'a::cka set" ("Orb") and strong_orbit :: "'a::cka ⇒ 'a::cka set" ("Orb⇩_{S}") and stabiliser :: "'a::cka ⇒ 'b::stimuli set" ("Stab") and fixed :: "'a::cka ⇒ bool" and encompassing_relation_behaviours :: "'a set ⇒ 'a set ⇒ bool" (infix "≪⇩_{𝒦}" 50) and encompassing_relation_stimuli :: "'b set ⇒ 'b set ⇒ bool" (infix "≪⇩_{𝒮}" 50) and induced :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "⊲" 50) and orbit_equivalent :: "'a::cka ⇒ 'a::cka ⇒ bool" (infix "∼⇩_{𝒦}" 50) assumes orb_def: "x ∈ Orb(a) ⟷ (∃s. (s ∘ a = x))" and orbs_def: "b ∈ Orb⇩_{S}(a) ⟷ Orb(b) = Orb(a)" and stab_def: "s ∈ Stab(a) ⟷ s ∘ a = a" and fixed_def: "fixed(a) ⟷ (∀s::'b. s≠𝔡 ⟶ s ∘ a = a)" and erb_def: "A ≪⇩_{𝒦}B ⟷ (∀a::'a. a ∈ A ⟶ (∃b. b ∈ B ∧ a ≤⇩_{𝒦}b))" and ers_def: "E ≪⇩_{𝒮}F ⟷ (∀a::'b. a ∈ E ⟶ (∃b. b ∈ F ∧ a ≤⇩_{𝒮}b))" and induced_def: "a ⊲ b ⟷ b ∈ Orb(a)" and orbit_equivalent_def: "a ∼⇩_{𝒦}b ⟷ Orb(a) = Orb(b)" begin subsection ‹Orbits \label{sub:orbits}› text ‹ The \emph{orbit} of~$a$ in~$\stim$ is the set given by~$\orb{a} = \sets{\lAct{a}{s}}{s \in \STIMset}$. The orbit of an agent~$a \in \CKAset$ represents the set of all possible behavioural responses from an agent behaving as~$a$ to any stimulus from~$\stim$. In this way, the orbit of a given agent can be perceived as the set of all possible future behaviours for that agent. › text ‹ Lemma \emph{inf-K-enc-orb} provides an isotonicity law with respect to the orbits and the encompassing relation for agent behaviours. › lemma inf_K_enc_orb: "a ≤⇩_{𝒦}b ⟹ Orb(a) ≪⇩_{𝒦}Orb(b)" unfolding erb_def orb_def using inf_K_next_behaviour by blast text ‹ The following lemmas provide a selection of properties regarding orbits and the encompassing relation for agent behaviours. › lemma enc_orb_add: "Orb(a) ≪⇩_{𝒦}Orb(a + b)" using inf_K_enc_orb inf_add_K_right by auto lemma enc_orb_exchange: "Orb((a*b) ; (c*d)) ≪⇩_{𝒦}Orb((a;c) * (b;d))" using inf_K_enc_orb exchange_2 by blast lemma enc_orb_seq_par: "Orb(a;b) ≪⇩_{𝒦}Orb(a*b)" using inf_K_enc_orb seq_inf_par by auto lemma enc_orb_add_seq_par: "Orb(a;b + b;a) ≪⇩_{𝒦}Orb(a*b)" using inf_K_enc_orb add_seq_inf_par by auto lemma enc_orb_parseq: "Orb((a*b);c) ≪⇩_{𝒦}Orb(a*(b;c))" using inf_K_enc_orb exchange_3 by blast lemma enc_orb_seqpar: "Orb(a;(b*c)) ≪⇩_{𝒦}Orb((a;b)*c)" using inf_K_enc_orb exchange_4 by blast lemma enc_orb_seqstar_parstar: "Orb(a⇧^{;}) ≪⇩_{𝒦}Orb(a⇧^{*})" using inf_K_enc_orb seqstar_inf_parstar by auto lemma enc_orb_union: "Orb(a) ≪⇩_{𝒦}Orb(c) ∧ Orb(b) ≪⇩_{𝒦}Orb(c) ⟷ Orb(a) ∪ Orb(b) ≪⇩_{𝒦}Orb(c)" unfolding erb_def by auto subsection ‹Stabilisers \label{sub:stabilisers}› text ‹ The \emph{stabiliser} of~$a$ in~$\stim$ is the set given by~$\stab{a} = \sets{s \in \STIMset}{\lAct{a}{s} = a}$. The stabiliser of an agent~$a \in \CKAset$ represents the set of stimuli which have no observable influence (or act as neutral stimuli) on an agent behaving as~$a$. › text ‹ Lemma \emph{enc-stab-inter-add} provides a property regarding stabilisers and the encompassing relation for stimuli. › lemma enc_stab_inter_add: "Stab(a) ∩ Stab(b) ≪⇩_{𝒮}Stab(a + b)" unfolding ers_def by (auto simp add: stab_def, rename_tac s, rule_tac x="s" in exI, simp) subsection ‹Fixed Points \label{sub:fixed_points}› text ‹ An element~$a \in \CKAset$ is called a \emph{fixed point} if~$\lnotation{\forall}{s}{s \in \STIMset \STdiff \set{\Dstim}}{\lAct{a}{s} = a}$.\linebreak When an agent behaviour is a fixed point, it is not influenced by any stimulus other than the deactivation stimulus~$\Dstim$. It is important to note that since~$\ActSemimodule$ is zero-preserving, every agent behaviour becomes inactive when subjected to the deactivation stimulus~$\Dstim$. Because of this, we exclude this special case when discussing fixed point agent behaviours. › lemma zerofix [simp]: "s ∘ 0 = 0" proof - have "0 = 𝔡 ∘ a" by simp hence "s ∘ 0 = s ∘ (𝔡 ∘ a)" by simp hence "s ∘ 0 = (s ⊙ 𝔡) ∘ a" by (simp only: lsemimodule3 [symmetric]) thus "s ∘ 0 = 0" by simp qed text ‹ The following lemmas provide a selection of properties regarding fixed agent behaviours. › lemma fixed_zero: "fixed(0)" unfolding fixed_def by simp lemma fixed_a_b_add: "fixed(a) ∧ fixed(b) ⟶ fixed(a + b)" unfolding fixed_def by simp lemma fix_not_deactivation: "s ∘ a = a ∧ λ(s,a) = 𝔡 ⟹ a = 0" proof - assume E: "s ∘ a = a ∧ λ(s,a) = 𝔡" hence "s ∘ (a;1) = a" by simp hence "(s∘a) ; (λ(s,a)∘1) = a" by (simp only: cascadingaxiom) hence "0 = a" by (simp add: E) thus ?thesis by auto qed lemma fixed_a_b_seq: "fixed(a) ∧ fixed(b) ⟶ fixed(a ; b)" unfolding fixed_def proof (rule impI) assume hyp: "(∀s. s ≠ 𝔡 ⟶ s ∘ a = a) ∧ (∀s. s ≠ 𝔡 ⟶ s ∘ b = b)" have C1: "(∀s. λ(s,a) = 𝔡 ⟶ s ≠ 𝔡 ⟶ s ∘ (a ; b) = a ; b)" proof - have E: "(∀s. s ≠ 𝔡 ∧ λ(s,a) = 𝔡 ⟶ s ∘ (a ; b) = 0)" by simp hence "(∀s. s ≠ 𝔡 ∧ λ(s,a) = 𝔡 ⟶ s ∘ a = a ∧ λ(s,a) = 𝔡)" by (simp add: hyp) moreover have "(∀s. s ∘ a = a ∧ λ(s,a) = 𝔡 ⟶ a = 0)" by (simp add: fix_not_deactivation) ultimately have "(∀s. s ≠ 𝔡 ∧ λ(s,a) = 𝔡 ⟶ a = 0)" by auto thus ?thesis by (auto simp add: E) qed moreover have C2: "(∀s. λ(s,a) ≠ 𝔡 ⟶ s ≠ 𝔡 ⟶ s ∘ (a ; b) = a ; b)" by (simp add: hyp) ultimately show "(∀s. s ≠ 𝔡 ⟶ s ∘ (a ; b) = a ; b)" by blast qed subsection ‹Strong Orbits and Induced Behaviours \label{sub:strong_orbits_and_induced_behaviours}› text ‹ The \emph{strong orbit} of~$a$ in~$\stim$ is the set given by~$\orbS{a} = \sets{b \in \CKAset}{\orb{b} = \orb{a}}$. Two agents are in the same strong orbit, denoted~$a \CKAsim b$ for~$a,b \in \CKAset$, if and only if their orbits are identical. This is to say when~$a \CKAsim b$, if an agent behaving as~$a$ is influenced by a stimulus to behave as~$b$, then there exists a stimulus which influences the agent, now behaving as~$b$, to revert back to its original behaviour~$a$. The influence of stimuli on agent behaviours is called the \emph{induced behaviours} via stimuli. Let~$a,b \in \CKAset$ be agent behaviours with~$a \neq b$. We say that~$b$ is \emph{induced by~$a$ via stimuli} (denoted by~$\induced{b}{a}$) if and only if~$\lnotation{\exists}{s}{s \in \STIMset}{\lAct{a}{s} = b}$. The notion of induced behaviours allows us to make some predictions about the evolution of agent behaviours in a given system by providing some insight into how different agents can respond to any stimuli. › text ‹ Lemma \emph{fixed-not-induce} states that if an agent has a fixed point behaviour, then it does not induce any agent behaviours via stimuli besides the inactive behaviour~$0$. › lemma fixed_not_induce: "fixed(a) ⟶ (∀b. b ≠ 0 ∧ b ≠ a ⟶ ¬(a ⊲ b))" proof - have "⋀s. s = 𝔡 ∨ s ≠ 𝔡 ⟹ (∀t. t ≠ 𝔡 ⟶ t ∘ a = a) ⟹ s ∘ a ≠ 0 ⟹ s ∘ a ≠ a ⟹ False" by (erule disjE, simp_all) hence "⋀s. (∀t. t ≠ 𝔡 ⟶ t ∘ a = a) ⟹ s ∘ a ≠ 0 ⟹ s ∘ a ≠ a ⟹ False" by simp thus ?thesis unfolding fixed_def induced_def orb_def by auto qed text ‹ Lemma \emph{strong-orbit-both-induced} states that all agent behaviours which belong to the same strong orbit are mutually induced via some (possibly different) stimuli. This is to say that if two agent behaviours are in the same strong orbit, then there exists inverse stimuli for each agent behaviour in a strong orbit allowing an agent to revert back to its previous behaviour. › lemma in_own_orbit: "a ∈ Orb(a)" unfolding orb_def by (rule_tac x="𝔫" in exI, simp) lemma strong_orbit_both_induced: "a ∼⇩_{𝒦}b ⟶ a ⊲ b ∧ b ⊲ a" unfolding orbit_equivalent_def induced_def by (blast intro: in_own_orbit) text ‹ Lemma \emph{strong-orbit-induce-same} states that if two agent behaviours are in the same strong orbit, then a third behaviour can be induced via stimuli by either of the behaviours within the strong orbit. This is to say that each behaviour in a strong orbit can induce the same set of behaviours (perhaps via different stimuli). › lemma strong_orbit_induce_same: "a ∼⇩_{𝒦}b ⟶ (a ⊲ c ⟷ b ⊲ c)" unfolding induced_def orbit_equivalent_def by simp end end

# Theory Communication_C2KA

(* Title: Notions of Communication for C2KA Author: Maxime Buyse <maxime.buyse at polytechnique.edu>, 2019 Maintainers: Maxime Buyse <maxime.buyse at polytechnique.edu> and Jason Jaskolka <jason.jaskolka at carleton.ca> *) 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