(*<*) (* * Knowledge-based programs. * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com. * License: BSD *) theory KBPs imports Kripke Traces begin (*>*) section‹Knowledge-based Programs› text ‹ \label{sec:kbps-theory-kbps-semantics} A knowledge-based programs (KBPs) encodes the dependency of action on knowledge by a sequence of guarded commands, and a \emph{joint knowledge-based program} (JKBP) assigns a KBP to each agent: › record ('a, 'p, 'aAct) GC = guard :: "('a, 'p) Kform" action :: "'aAct" type_synonym ('a, 'p, 'aAct) KBP = "('a, 'p, 'aAct) GC list" type_synonym ('a, 'p, 'aAct) JKBP = "'a ⇒ ('a, 'p, 'aAct) KBP" text‹ We use a list of guarded commands just so we can reuse this definition and others in algorithmic contexts; we would otherwise use a set as there is no problem with infinite programs or actions, and we always ignore the sequential structure. Intuitively a KBP for an agent cannot directly evaluate the truth of an arbitrary formula as it may depend on propositions that the agent has no certainty about. For example, a card-playing agent cannot determine which cards are in the deck, despite being sure that those in her hand are not. Conversely agent $a$ can evaluate formulas of the form @{term "❙K⇩a φ"} as these depend only on the worlds the agent thinks is possible. Thus we restrict the guards of the JKBP to be boolean combinations of \emph{subjective} formulas: › fun subjective :: "'a ⇒ ('a, 'p) Kform ⇒ bool" where "subjective a (Kprop p) = False" | "subjective a (Knot f) = subjective a f" | "subjective a (Kand f g) = (subjective a f ∧ subjective a g)" | "subjective a (Kknows a' f) = (a = a')" | "subjective a (Kcknows as f) = (a ∈ set as)" text‹ All JKBPs in the following sections are assumed to be subjective. This syntactic restriction implies the desired semantic property, that we can evaluate a guard at an arbitrary world that is compatible with a given observation \<^citep>‹‹\S3› in "DBLP:journals/dc/FaginHMV97"›. › lemma S5n_subjective_eq: assumes S5n: "S5n M" assumes subj: "subjective a φ" assumes ww': "(w, w') ∈ relations M a" shows "M, w ⊨ φ ⟷ M, w' ⊨ φ" (*<*) using subj ww' proof(induct φ rule: subjective.induct[case_names Kprop Knot Kand Kknows Kcknows]) case (Kcknows a as φ) hence "(w, w') ∈ (⋃a∈set as. relations M a)⇧^{+}" by auto with Kcknows S5n show ?case by (auto dest: S5n_tc_rels_eq) qed (auto dest: S5n_rels_eq[OF S5n]) (*>*) text‹ The proof is by induction over the formula @{term "φ"}, using the properties of $S5_n$ Kripke structures in the knowledge cases. We capture the fixed but arbitrary JKBP using a locale, and work in this context for the rest of this section. › locale JKBP = fixes jkbp :: "('a, 'p, 'aAct) JKBP" assumes subj: "∀a gc. gc ∈ set (jkbp a) ⟶ subjective a (guard gc)" context JKBP begin text‹ The action of the JKBP at a world is the list of all actions that are enabled at that world: › definition jAction :: "('a, 'p, 'w) KripkeStructure ⇒ 'w ⇒ 'a ⇒ 'aAct list" where "jAction ≡ λM w a. [ action gc. gc ← jkbp a, M, w ⊨ guard gc ]" text‹ All of our machinery on Kripke structures lifts from the models relation of \S\ref{sec:kbps-logic-of-knowledge} through @{term "jAction"}, due to the subjectivity requirement. In particular, the KBP for agent $a$ behaves the same at worlds that $a$ cannot distinguish amongst: › lemma S5n_jAction_eq: assumes S5n: "S5n M" assumes ww': "(w, w') ∈ relations M a" shows "jAction M w a = jAction M w' a" (*<*) proof - { fix gc assume "gc ∈ set (jkbp a)" with subj have "subjective a (guard gc)" by auto with S5n ww' have "M, w ⊨ guard gc = M, w' ⊨ guard gc" by - (rule S5n_subjective_eq, simp_all) } thus ?thesis unfolding jAction_def by - (rule arg_cong[where f=concat], simp) qed (*>*) text‹ Also the JKBP behaves the same on relevant generated models for all agents: › lemma gen_model_jAction_eq: assumes S: "gen_model M w = gen_model M' w" assumes w': "w' ∈ worlds (gen_model M' w)" assumes M: "kripke M" assumes M': "kripke M'" shows "jAction M w' = jAction M' w'" (*<*) unfolding jAction_def by (auto iff: gen_model_eq[OF M M' S w']) (*>*) text‹ Finally, @{term "jAction"} is invariant under simulations: › lemma simulation_jAction_eq: assumes M: "kripke M" assumes sim: "sim M M' f" assumes w: "w ∈ worlds M" shows "jAction M w = jAction M' (f w)" (*<*) unfolding jAction_def using assms by (auto iff: sim_semantic_equivalence) (*>*) end section‹Environments and Views› text‹ \label{sec:kbps-theory-environments} The previous section showed how a JKBP can be interpreted statically, with respect to a fixed Kripke structure. As we also wish to capture how agents interact, we adopt the \emph{interpreted systems} and \emph{contexts} of \<^cite>‹"FHMV:1995"›, which we term \emph{environments} following \<^cite>‹"Ron:1996"›. A \emph{pre-environment} consists of the following: \begin{itemize} \item @{term "envInit"}, an arbitrary set of initial states; \item The protocol of the environment @{term "envAction"}, which depends on the current state; \item A transition function @{term "envTrans"}, which incorporates the environment's action and agents' behaviour into a state change; and \item A propositional evaluation function @{term "envVal"}. \end{itemize} We extend the @{term "JKBP"} locale with these constants: › locale PreEnvironment = JKBP jkbp for jkbp :: "('a, 'p, 'aAct) JKBP" + fixes envInit :: "'s list" and envAction :: "'s ⇒ 'eAct list" and envTrans :: "'eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's" and envVal :: "'s ⇒ 'p ⇒ bool" text‹ \label{sec:kbps-views} We represent the possible evolutions of the system as finite sequences of states, represented by a left-recursive type @{typ "'s Trace"} with constructors @{term "tInit s"} and @{term "t ↝ s"}, equipped with @{term "tFirst"}, @{term "tLast"}, @{term "tLength"} and @{term "tMap"} functions. Constructing these traces requires us to determine the agents' actions at a given state. To do so we need to find an appropriate S$5_n$ structure for interpreting @{term "jkbp"}. Given that we want the agents to make optimal use of the information they have access to, we allow these structures to depend on the entire history of the system, suitably conditioned by what the agents can observe. We capture this notion of observation with a \emph{view} \<^citep>‹"Ron:1996"›, which is an arbitrary function of a trace: › type_synonym ('s, 'tview) View = "'s Trace ⇒ 'tview" type_synonym ('a, 's, 'tview) JointView = "'a ⇒ 's Trace ⇒ 'tview" text‹ \label{sec:kbps-synchrony} We require views to be \emph{synchronous}, i.e. that agents be able to tell the time using their view by distinguishing two traces of different lengths. As we will see in the next section, this guarantees that the JKBP has an essentially unique implementation. We extend the @{term "PreEnvironment"} locale with a view: › locale PreEnvironmentJView = PreEnvironment jkbp envInit envAction envTrans envVal for jkbp :: "('a, 'p, 'aAct) JKBP" and envInit :: "'s list" and envAction :: "'s ⇒ 'eAct list" and envTrans :: "'eAct ⇒ ('a ⇒ 'aAct) ⇒ 's ⇒ 's" and envVal :: "'s ⇒ 'p ⇒ bool" + fixes jview :: "('a, 's, 'tview) JointView" assumes sync: "∀a t t'. jview a t = jview a t' ⟶ tLength t = tLength t'" text‹ The two principle synchronous views are the clock view and the perfect-recall view which we discuss further in \S\ref{sec:kbps-theory-views}. We will later derive an agent's concrete view from an instantaneous observation of the global state in \S\ref{sec:kbps-environments}. We build a Kripke structure from a set of traces by relating traces that yield the same view. To obtain an S$5_n$ structure we also need a way to evaluate propositions: we apply @{term "envVal"} to the final state of a trace: › definition (in PreEnvironmentJView) mkM :: "'s Trace set ⇒ ('a, 'p, 's Trace) KripkeStructure" where "mkM T ≡ ⦇ worlds = T, relations = λa. { (t, t') . {t, t'} ⊆ T ∧ jview a t = jview a t' }, valuation = envVal ∘ tLast ⦈" (*<*) context PreEnvironmentJView begin lemma mkM_kripke[intro, simp]: "kripke (mkM T)" unfolding mkM_def by (rule kripkeI) fastforce lemma mkM_S5n[intro, simp]: "S5n (mkM T)" unfolding mkM_def by (intro S5nI equivI) (bestsimp intro: equivI refl_onI symI transI)+ lemma mkM_simps[simp]: "worlds (mkM T) = T" "⟦ (t, t') ∈ relations (mkM T) a ⟧ ⟹ jview a t = jview a t'" "⟦ (t, t') ∈ relations (mkM T) a ⟧ ⟹ t ∈ T" "⟦ (t, t') ∈ relations (mkM T) a ⟧ ⟹ t' ∈ T" "valuation (mkM T) = envVal ∘ tLast" unfolding mkM_def by simp_all lemma mkM_rel_length[simp]: assumes tt': "(t, t') ∈ relations (mkM T) a" shows "tLength t' = tLength t" proof - from tt' have "jview a t = jview a t'" by simp thus ?thesis by (bestsimp dest: sync[rule_format]) qed (*>*) text‹ This construction supplants the role of the \emph{local states} of \<^citet>‹"FHMV:1995"›. The following section shows how we can canonically interpret the JKBP with respect to this structure. › section‹Canonical Structures› text‹ \label{sec:kbps-canonical-kripke} Our goal in this section is to find the canonical set of traces for a given JKBP in a particular environment. As we will see, this always exists with respect to synchronous views. We inductively define an \emph{interpretation} of a JKBP with respect to an arbitrary set of traces @{term "T"} by constructing a sequence of sets of traces of increasing length: › fun jkbpTn :: "nat ⇒ 's Trace set ⇒ 's Trace set"(*<*)("jkbpT⇘_⇙")(*>*) where "jkbpT⇘0⇙ T = { tInit s |s. s ∈ set envInit }" | "jkbpT⇘Suc n⇙ T = { t ↝ envTrans eact aact (tLast t) |t eact aact. t ∈ jkbpT⇘n⇙ T ∧ eact ∈ set (envAction (tLast t)) ∧ (∀a. aact a ∈ set (jAction (mkM T) t a)) }" text‹ This model reflects the failure of any agent to provide an action as failure of the entire system. In general @{term "envTrans"} may incorporate a scheduler and communication failure models. The union of this sequence gives us a closure property: › definition jkbpT :: "'s Trace set ⇒ 's Trace set" where "jkbpT T ≡ ⋃n. jkbpT⇘n⇙ T" (*<*) lemma jkbpTn_length: "t ∈ jkbpTn n T ⟹ tLength t = n" by (induct n arbitrary: t, auto) lemma jkbpT_tLength_inv: "⟦ t ∈ jkbpT T; tLength t = n ⟧ ⟹ t ∈ jkbpTn n T" unfolding jkbpT_def by (induct n arbitrary: t) (fastforce simp: jkbpTn_length)+ lemma jkbpT_traces_of_length: "{ t ∈ jkbpT T . tLength t = n } = jkbpTn n T" using jkbpT_tLength_inv unfolding jkbpT_def by (bestsimp simp: jkbpTn_length) (*>*) text‹ We say that a set of traces @{term "T"} \emph{represents} a JKBP if it is closed under @{term "jkbpT"}: › definition represents :: "'s Trace set ⇒ bool" where "represents T ≡ jkbpT T = T" (*<*) lemma representsI: "jkbpT T = T ⟹ represents T" unfolding represents_def by simp lemma representsD: "represents T ⟹ jkbpT T = T" unfolding represents_def by simp (*>*) text‹ This is the vicious cycle that we break using our assumption that the view is synchronous. The key property of such views is that the satisfaction of an epistemic formula is determined by the set of traces in the model that have the same length. Lifted to @{term "jAction"}, we have: › (*<*) lemma sync_tLength_eq_trc: assumes "(t, t') ∈ (⋃a∈as. relations (mkM T) a)⇧^{*}" shows "tLength t = tLength t'" using assms by (induct rule: rtrancl_induct) auto lemma sync_gen_model_tLength: assumes traces: "{ t ∈ T . tLength t = n } = { t ∈ T' . tLength t = n }" and tT: "t ∈ { t ∈ T . tLength t = n }" shows "gen_model (mkM T) t = gen_model (mkM T') t" apply(rule gen_model_subset[where T="{ t ∈ T . tLength t = n }"]) apply simp_all (* t ∈ T and t ∈ T' *) prefer 4 using tT apply simp prefer 4 using tT traces apply simp apply (unfold mkM_def)[1] using tT traces apply (auto)[1] using tT apply (auto dest: sync_tLength_eq_trc[where as=UNIV] kripke_rels_trc_worlds)[1] using tT traces apply (auto dest: sync_tLength_eq_trc[where as=UNIV] kripke_rels_trc_worlds)[1] done (*>*) lemma sync_jview_jAction_eq: assumes traces: "{ t ∈ T . tLength t = n } = { t ∈ T' . tLength t = n }" assumes tT: "t ∈ { t ∈ T . tLength t = n }" shows "jAction (mkM T) t = jAction (mkM T') t" (*<*) apply (rule gen_model_jAction_eq[where w=t]) apply (rule sync_gen_model_tLength) using assms apply (auto intro: gen_model_world_refl) done (*>*) text‹ This implies that for a synchronous view we can inductively define the \emph{canonical traces} of a JKBP. These are the traces that a JKBP generates when it is interpreted with respect to those very same traces. We do this by constructing the sequence ‹jkbpC⇩_{n}› of \emph{(canonical) temporal slices} similarly to @{term "jkbpT⇘n⇙"}: › fun jkbpCn :: "nat ⇒ 's Trace set"(*<*)("jkbpC⇘_⇙")(*>*) where "jkbpC⇘0⇙ = { tInit s |s. s ∈ set envInit }" | "jkbpC⇘Suc n⇙ = { t ↝ envTrans eact aact (tLast t) |t eact aact. t ∈ jkbpC⇘n⇙ ∧ eact ∈ set (envAction (tLast t)) ∧ (∀a. aact a ∈ set (jAction (mkM jkbpC⇘n⇙) t a)) }" abbreviation MCn :: "nat ⇒ ('a, 'p, 's Trace) KripkeStructure"(*<*)("MC⇘_⇙")(*>*) where "MC⇘n⇙ ≡ mkM jkbpC⇘n⇙" (*<*) lemma jkbpCn_step_inv: "t ↝ s ∈ jkbpCn (Suc n) ⟹ t ∈ jkbpCn n" by (induct n arbitrary: t, (fastforce simp add: Let_def)+) lemma jkbpCn_length[simp]: "t ∈ jkbpCn n ⟹ tLength t = n" by (induct n arbitrary: t, (fastforce simp add: Let_def)+) lemma jkbpCn_init_inv[intro]: "tInit s ∈ jkbpCn n ⟹ s ∈ set envInit" by (frule jkbpCn_length) auto lemma jkbpCn_tFirst_init_inv[intro]: "t ∈ jkbpCn n ⟹ tFirst t ∈ set envInit" by (induct n arbitrary: t) (auto iff: Let_def) (*>*) text‹ The canonical set of traces for a JKBP with respect to a joint view is the set of canonical traces of all lengths. › definition jkbpC :: "'s Trace set" where "jkbpC ≡ ⋃n. jkbpC⇘n⇙" abbreviation MC :: "('a, 'p, 's Trace) KripkeStructure" where "MC ≡ mkM jkbpC" (*<*) lemma jkbpCn_jkbpC_subset: "jkbpCn n ⊆ jkbpC" unfolding jkbpC_def by blast lemma jkbpCn_jkbpC_inc[intro]: "t ∈ jkbpCn n ⟹ t ∈ jkbpC" unfolding jkbpC_def by best lemma jkbpC_tLength_inv[intro]: "⟦ t ∈ jkbpC; tLength t = n ⟧ ⟹ t ∈ jkbpCn n" unfolding jkbpC_def by (induct n arbitrary: t, (fastforce simp add: Let_def)+) lemma jkbpC_traces_of_length: "{ t ∈ jkbpC . tLength t = n } = jkbpCn n" unfolding jkbpC_def by bestsimp lemma jkbpC_prefix_closed[dest]: "t ↝ s ∈ jkbpC ⟹ t ∈ jkbpC" apply (drule jkbpC_tLength_inv) apply simp apply (auto iff: Let_def jkbpC_def) done lemma jkbpC_init[iff]: "tInit s ∈ jkbpC ⟷ s ∈ set envInit" unfolding jkbpC_def apply rule apply fast apply (subgoal_tac "tInit s ∈ jkbpCn 0") apply simp apply (rule_tac x=0 in exI) apply simp_all done lemma jkbpC_jkbpCn_rels: "⟦ (u, v) ∈ relations MC a; tLength u = n ⟧ ⟹ (u, v) ∈ relations (MC⇘n⇙) a" unfolding mkM_def by (fastforce dest: sync[rule_format]) lemma jkbpC_tFirst_init_inv[intro]: "t ∈ jkbpC ⟹ tFirst t ∈ set envInit" unfolding jkbpC_def by blast (*>*) text‹ We can show that @{term "jkbpC"} represents the joint knowledge-based program @{term "jkbp"} with respect to @{term "jview"}: › lemma jkbpC_jkbpCn_jAction_eq: assumes tCn: "t ∈ jkbpC⇘n⇙" shows "jAction MC t = jAction MC⇘n⇙ t" (*<*) using assms by - (rule sync_jview_jAction_eq, auto iff: jkbpC_traces_of_length) (*>*) text‹› lemma jkbpTn_jkbpCn_represents: "jkbpT⇘n⇙ jkbpC = jkbpC⇘n⇙" by (induct n) (fastforce simp: Let_def jkbpC_jkbpCn_jAction_eq)+ text‹› theorem jkbpC_represents: "represents jkbpC" (*<*) using jkbpTn_jkbpCn_represents by (simp add: representsI jkbpC_def jkbpT_def) (*>*) text‹ We can show uniqueness too, by a similar argument: › theorem jkbpC_represents_uniquely: assumes repT: "represents T" shows "T = jkbpC" (*<*) proof - { fix n have "{ t ∈ T . tLength t = n } = { t ∈ jkbpC . tLength t = n }" proof(induct n) case 0 from repT have F: "{t ∈ T. tLength t = 0} = jkbpTn 0 T" by - (subst jkbpT_traces_of_length[symmetric], simp add: representsD) thus ?case by (simp add: jkbpC_traces_of_length) next case (Suc n) hence indhyp: "{t ∈ T. tLength t = n} = jkbpCn n" by (simp add: jkbpC_traces_of_length) (* F and H are very similar. *) from repT have F: "⋀n. jkbpTn n T = {t ∈ T. tLength t = n}" by - (subst jkbpT_traces_of_length[symmetric], simp add: representsD) from indhyp F have G: "jkbpTn n T = jkbpCn n" by simp from repT have H: "⋀n. {t ∈ T. tLength t = n} = {t ∈ jkbpTn n T. tLength t = n}" by (subst representsD[OF repT, symmetric], auto iff: jkbpT_traces_of_length jkbpTn_length) from F indhyp have ACTS: "⋀t. t ∈ jkbpTn n T ⟹ jAction (mkM T) t = jAction (MCn n) t" by - (rule sync_jview_jAction_eq[where n="n"], auto) show ?case apply (auto iff: Let_def ACTS G H jkbpC_traces_of_length) apply blast+ done qed } thus ?thesis by auto qed (*>*) end (* context PreEnvironmentJView *) text‹ Thus, at least with synchronous views, we are justified in talking about \emph{the} representation of a JKBP in a given environment. More generally these results are also valid for the more general notion of \emph{provides witnesses} as shown by \<^citet>‹‹Lemma 7.2.4› in "FHMV:1995"› and \<^citet>‹"DBLP:journals/dc/FaginHMV97"›: it requires only that if a subjective knowledge formula is false on a trace then there is a trace of the same length or less that bears witness to that effect. This is a useful generalisation in asynchronous settings. The next section shows how we can construct canonical representations of JKBPs using automata. › (*<*) end (*>*)