Quelle  KBPs.thy

(*<*)
(*
 * 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}

  knowledge-based programs (KBPs) encodes the dependency of action on
  by a sequence of guarded commands, and a \emph{joint
 -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‹

  use a list of guarded commands just so we can reuse this definition
  others in algorithmic contexts; we would otherwise use a set as
  is no problem with infinite programs or actions, and we always
  the sequential structure.

  a KBP for an agent cannot directly evaluate the truth of
  arbitrary formula as it may depend on propositions that the agent
  no certainty about. For example, a card-playing agent cannot
  which cards are in the deck, despite being sure that those
  her hand are not. Conversely agent $a$ can evaluate formulas of the
  @{term "K φ"} as these depend only on the worlds the agent thinks
  possible.

  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‹

  JKBPs in the following sections are assumed to be subjective.

  syntactic restriction implies the desired semantic property, that
  can evaluate a guard at an arbitrary world that is compatible with
  given observation 🍋‹‹\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‹

  proof is by induction over the formula @{term "φ"}, using the
  of $S5_n$ Kripke structures in the knowledge cases.

  capture the fixed but arbitrary JKBP using a locale, and work in
  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‹

  action of the JKBP at a world is the list of all actions that are
  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‹

  of our machinery on Kripke structures lifts from the models
  of \S\ref{sec:kbps-logic-of-knowledge} through @{term
 jAction"}, due to the subjectivity requirement. In particular, the
  for agent $a$ behaves the same at worlds that $a$ cannot
  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‹

  the JKBP behaves the same on relevant generated models for all
 :

 ›

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‹

 , @{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}

  previous section showed how a JKBP can be interpreted statically,
  respect to a fixed Kripke structure. As we also wish to capture
  agents interact, we adopt the \emph{interpreted systems} and
 emph{contexts} of cite‹"FHMV:1995"›, which we term \emph{environments}
  cite‹"Ron:1996"›.

  \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}
  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}

  represent the possible evolutions of the system as finite sequences
  states, represented by a left-recursive type @{typ "'s Trace"} with
  @{term "tInit s"} and @{term "t ↝ s"}, equipped with
 {term "tFirst"}, @{term "tLast"}, @{term "tLength"} and @{term
 tMap"} functions.

  these traces requires us to determine the agents' actions
  a given state. To do so we need to find an appropriate S$5_n$
  for interpreting @{term "jkbp"}.

  that we want the agents to make optimal use of the information
  have access to, we allow these structures to depend on the entire
  of the system, suitably conditioned by what the agents can
 . We capture this notion of observation with a \emph{view}
 🍋‹"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}

  require views to be \emph{synchronous}, i.e. that agents be able to
  the time using their view by distinguishing two traces of
  lengths. As we will see in the next section, this guarantees
  the JKBP has an essentially unique implementation.

  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‹

  two principle synchronous views are the clock view and the
 -recall view which we discuss further in
 S\ref{sec:kbps-theory-views}. We will later derive an agent's
  view from an instantaneous observation of the global state in
 S\ref{sec:kbps-environments}.

  build a Kripke structure from a set of traces by relating traces
  yield the same view. To obtain an S$5_n$ structure we also need a
  to evaluate propositions: we apply @{term "envVal"} to the final
  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‹

  construction supplants the role of the \emph{local states} of
 🍋‹"FHMV:1995"›.

  following section shows how we can canonically interpret the JKBP
  respect to this structure.

 ›

section‹Canonical Structures›

text‹

 label{sec:kbps-canonical-kripke}

  goal in this section is to find the canonical set of traces for a
  JKBP in a particular environment. As we will see, this always
  with respect to synchronous views.

  inductively define an \emph{interpretation} of a JKBP with respect
  an arbitrary set of traces @{term "T"} by constructing a sequence
  sets of traces of increasing length:

 ›

fun jkbpTn :: "nat ==> 's Trace set ==> 's Trace set"(*<*)(\<open>jkbpT\<^bsub>_\<^esub>\<close>)(*>*) where
  "jkbpT T = { tInit s |s. s ∈ set envInit }"
| "jkbpT _n T = { t ↝ envTrans eact aact (tLast t) |t eact aact.
                             t ∈ jkbpT T ∧ eact ∈ set (envAction (tLast t))
                          ∧ (∀a. aact a ∈ set (jAction (mkM T) t a)) }"

text‹

  model reflects the failure of any agent to provide an action as
  of the entire system. In general @{term "envTrans"} may
  a scheduler and communication failure models.

  union of this sequence gives us a closure property:

 ›

definition jkbpT :: "'s Trace set ==> 's Trace set" where
  "jkbpT T ≡ ∪n. jkbpT 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‹

  say that a set of traces @{term "T"} \emph{represents} a JKBP if it
  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‹

  is the vicious cycle that we break using our assumption that the
  is synchronous. The key property of such views is that the
  of an epistemic formula is determined by the set of
  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 \<in> T and t \<in> 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‹

  implies that for a synchronous view we can inductively define the
 emph{canonical traces} of a JKBP. These are the traces that a JKBP
  when it is interpreted with respect to those very same
 . We do this by constructing the sequence ‹jkbpC_n› of
 emph{(canonical) temporal slices} similarly to @{term "jkbpT"}:

 ›

fun jkbpCn :: "nat ==> 's Trace set"(*<*)(\<open>jkbpC\<^bsub>_\<^esub>\<close>)(*>*) where
  "jkbpC = { tInit s |s. s ∈ set envInit }"
| "jkbpC _n = { t ↝ envTrans eact aact (tLast t) |t eact aact.
                             t ∈ jkbpC ∧ eact ∈ set (envAction (tLast t))
                          ∧ (∀a. aact a ∈ set (jAction (mkM jkbpC) t a)) }"

abbreviation MCn :: "nat ==> ('a, 'p, 's Trace) KripkeStructure"(*<*)(\<open>MC\<^bsub>_\<^esub>\<close>)(*>*) where
  "MC ≡ mkM jkbpC"
(*<*)

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‹

  canonical set of traces for a JKBP with respect to a joint view is
  set of canonical traces of all lengths.

 ›

definition jkbpC :: "'s Trace set" where
  "jkbpC ≡ ∪n. jkbpC"

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) 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‹

  can show that @{term "jkbpC"} represents the joint knowledge-based
  @{term "jkbp"} with respect to @{term "jview"}:

 ›

lemma jkbpC_jkbpCn_jAction_eq:
  assumes tCn: "t ∈ jkbpC"
  shows "jAction MC t = jAction MC t"
(*<*)
  using assms
  by - (rule sync_jview_jAction_eq, auto iff: jkbpC_traces_of_length)

(*>*)
text‹›

lemma jkbpTn_jkbpCn_represents: "jkbpT jkbpC = jkbpC"
  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‹

  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‹

 , at least with synchronous views, we are justified in talking
  \emph{the} representation of a JKBP in a given environment. More
  these results are also valid for the more general notion of
 emph{provides witnesses} as shown by 🍋‹‹Lemma 7.2.4› in "FHMV:1995"›
  🍋‹"DBLP:journals/dc/FaginHMV97"›: it requires only that if a
  knowledge formula is false on a trace then there is a trace
  the same length or less that bears witness to that effect. This is
  useful generalisation in asynchronous settings.

  next section shows how we can construct canonical representations
  JKBPs using automata.

 ›

(*<*)
end
(*>*)