Theory Labeled_Transition_Systems

(* License: LGPL *)

section ‹Labeled Transition Systems›

theory Labeled_Transition_Systems
  imports Main
begin

subsection ‹Base LTS›

text ‹
  The locale ‹LTS› represents a labeled transition system consisting of a set of states $\mathcal{P}$, a set of actions $\Sigma$, and a transition relation $\mapsto \subseteq \mathcal{P}\times\Sigma\times\mathcal{P}$.
  We formalize the sets of states and actions by the type variables ‹'s› and ‹'a›. An LTS is then determined by the transition relation ‹step›.
›

locale lts =
  fixes step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› (‹_ ↦ _ _› [70,70,70] 80)
begin

text ‹One may lift \<^term>‹step› to sets of states, written as ‹P ↦S α Q›.›
abbreviation step_setp (‹_ ↦S _ _› [70,70,70] 80) where
  ‹P ↦S α Q ≡ (∀q ∈ Q. ∃p ∈ P. p ↦ α q) ∧ (∀p ∈ P. ∀q. p ↦ α q ⟶ q ∈ Q)›

text ‹The set of ‹α›-derivatives for a set of states ‹P›.›
definition step_set :: ‹'s set ⇒ 'a ⇒ 's set› where
  ‹step_set P α ≡ { q . ∃p ∈ P. p ↦ α q }›

text ‹The set of possible ‹α›-steps for a set of states ‹P› is an instance of \<^term>‹step› lifted to sets of steps.›
lemma step_set_is_step_set: ‹P ↦S α (step_set P α)›
  using step_set_def by force

text ‹The lifted \<^term>‹step_setp› (‹P ↦S α Q›) is therefore this set ‹Q›.›
lemma step_set_eq:
  assumes ‹P ↦S α Q›
  shows ‹Q = step_set P α›
  using assms step_set_is_step_set by fastforce

end ― ‹of locale ‹lts››

subsection ‹Labeled Transition Systems with Silent Steps›

text ‹
  We formalize labeled transition systems with silent steps as an extension of ordinary labeled transition systems with a fixed internal action ‹τ›.
›

locale lts_tau =
  lts step
    for step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› (‹_ ↦ _ _› [70,70,70] 80) +
    fixes τ :: 'a
begin

text ‹
  The paper \<^cite>‹bj2023silentStepSpectroscopyArxiv› introduces a transition $p \xrightarrow{(\alpha)}p'$ if $p \xrightarrow{\alpha} p'$, or if $\alpha = \tau$ and $p = p'$.
  We define \<^term>‹soft_step› analogously and provide the notation ‹p ↦a α p'›.
›
abbreviation soft_step (‹_ ↦a _ _› [70,70,70] 80) where
  ‹p ↦a α q ≡ p ↦α q ∨ (α = τ ∧ p = q)›

inductive silent_reachable :: ‹'s ⇒ 's ⇒ bool›  (infix ‹↠› 80)
  where
    refl: ‹p ↠ p› |
    step: ‹p ↠ p''› if ‹p ↦ τ p'› and ‹p' ↠ p''›

text ‹If ‹p'› is silent-reachable from ‹p› and there is a ‹τ›-transition from ‹p'› to ‹p''› then ‹p''› is silent reachable from ‹p›.›
lemma silent_reachable_append_τ: ‹p ↠ p' ⟹ p' ↦ τ p'' ⟹ p ↠ p''›
proof (induct rule: silent_reachable.induct)
  case (refl p)
  then show ?case using silent_reachable.intros by blast
next
  case (step p p' p'')
  then show ?case using silent_reachable.intros by blast
qed

text ‹The relation \<^term>‹silent_reachable› is transitive.›
lemma silent_reachable_trans:
  assumes
    ‹p ↠ p'›
    ‹p' ↠ p''›
  shows
    ‹p ↠ p''›
using assms silent_reachable.intros(2)
  by (induct, blast+)

text ‹The relation ‹silent_reachable_loopless› is a variation of \<^term>‹silent_reachable› that does not use self-loops.›
inductive silent_reachable_loopless :: ‹'s ⇒ 's ⇒ bool›  (infix ‹↠L› 80)
  where
    ‹p ↠L p› |
    ‹p ↠L p''› if ‹p ↦ τ p'› and ‹p' ↠L p''› and ‹p ≠ p'›

text ‹If a state ‹p'› is \<^term>‹silent_reachable› from ‹p› it is also \<^term>‹silent_reachable_loopless›.›
lemma silent_reachable_impl_loopless:
  assumes ‹p ↠ p'›
  shows ‹p ↠L p'›
  using assms
proof(induct rule: silent_reachable.induct)
  case (refl p)
  thus ?case by (rule silent_reachable_loopless.intros(1))
next
  case (step p p' p'')
  thus ?case proof(cases ‹p = p'›)
    case True
    thus ?thesis using step.hyps(3) by auto
  next
    case False
    thus ?thesis using step.hyps silent_reachable_loopless.intros(2) by blast
  qed
qed

lemma tau_chain_reachabilty:
  assumes ‹∀i < length pp - 1.  pp!i ↦ τ pp!(Suc i)›
  shows ‹∀j < length pp. ∀i ≤ j. pp!i ↠ pp!j›
proof safe
  fix j i
  assume ‹j < length pp› ‹i ≤ j›
  thus ‹pp!i ↠ pp!j›
  proof (induct j)
    case 0
    then show ?case
      using silent_reachable.refl by blast
  next
    case (Suc j)
    then show ?case
    proof (induct i)
      case 0
      then show ?case using assms silent_reachable_append_τ
        by (metis Suc_lessD Suc_lessE bot_nat_0.extremum diff_Suc_1)
    next
      case (Suc i)
      then show ?case using silent_reachable.refl assms silent_reachable_append_τ
        by (metis Suc_lessD Suc_lessE  diff_Suc_1 le_SucE)
    qed
  qed
qed

text ‹A state ‹p› can reach ‹p'› weakly by performing an ‹α›-transition, possibly proceeded and followed by any number of ‹τ›-transitions.›
definition weak_step (‹_ ↠↦↠ _ _› [70, 70, 70] 80) where
  ‹p  ↠↦↠ α p' ≡ if α = τ
                    then p ↠ p'
                    else ∃p1 p2. p ↠ p1 ∧ p1 ↦ α p2 ∧ p2 ↠ p'›

lemma silent_prepend_weak_step: ‹p ↠ p' ⟹ p' ↠↦↠ α p'' ⟹ p ↠↦↠ α p''›
  unfolding weak_step_def using silent_reachable_trans[of p p'] by fastforce

text ‹A sequence of \<^term>‹weak_step›s from one state ‹p› to another ‹p'›.›
inductive weak_step_sequence :: ‹'s ⇒ 'a list ⇒ 's ⇒ bool› (‹_ ↠↦↠$ _ _› [70,70,70] 80) where
  ‹p ↠↦↠$ [] p'› if ‹p ↠ p'› |
  ‹p ↠↦↠$ (α#rt) p''› if ‹p ↠↦↠ α p'› ‹p' ↠↦↠$ rt p''›

lemma weak_step_sequence_trans:
  assumes ‹p ↠↦↠$ tr_1 p'› and ‹p' ↠↦↠$ tr_2 p''›
  shows ‹p ↠↦↠$ (tr_1 @ tr_2) p''›
  using assms weak_step_sequence.intros(2)
proof induct
  case (1 p p')
  then show ?case
    by (metis weak_step_sequence.simps append_Nil silent_prepend_weak_step silent_reachable_trans)
next
  case (2 p α p' rt p'')
  then show ?case by fastforce
qed

text ‹The weak traces of a state are all possible sequences of weak transitions that can be performed.›
abbreviation weak_traces :: ‹'s ⇒ 'a list set›
  where ‹weak_traces p ≡ {tr. ∃p'. p ↠↦↠$ tr p'}›

text ‹The empty trace is in \<^term>‹weak_traces› for all states.›
lemma empty_trace_allways_weak_trace:
  shows ‹[] ∈ weak_traces p›
  using silent_reachable.intros(1) weak_step_sequence.intros(1) by fastforce

text ‹‹τ› can be prepended to any weak trace.›
lemma prepend_τ_weak_trace:
  assumes ‹tr ∈ weak_traces p›
  shows ‹(τ # tr) ∈ weak_traces p›
  using assms silent_reachable.intros(1) mem_Collect_eq
    weak_step_sequence.intros(2) weak_step_def by fastforce

lemma silent_prepend_weak_traces:
  assumes
    ‹p ↠ p'›
    ‹tr ∈ weak_traces p'›
  shows
    ‹tr ∈ weak_traces p›
  using assms
proof -
  assume ‹p ↠ p'›
     and ‹tr ∈ weak_traces p'›
  hence ‹∃p''. p' ↠↦↠$ tr p''› by auto
  then obtain p'' where ‹p' ↠↦↠$ tr p''› by auto
  from ‹p' ↠↦↠$ tr p''›
    and ‹p ↠ p'›
  have ‹p ↠↦↠$ tr p''›
    by (metis append_self_conv2 weak_step_sequence.intros(1) weak_step_sequence_trans)
  hence ‹∃p''. p ↠↦↠$ tr p''› by auto
  then show ‹tr ∈ weak_traces p›
    by blast
qed

text ‹If there is an ‹α›-transition from ‹p› to ‹p'›, and ‹p'› has a weak trace ‹tr›, then the sequence ‹(α # tr)› is a valid (weak) trace of ‹p›.›
lemma step_prepend_weak_traces:
  assumes
    ‹p ↦ α p'›
    ‹tr ∈ weak_traces p'›
  shows
    ‹(α # tr) ∈ weak_traces p›
  using assms
proof -
  from ‹tr ∈ weak_traces p'›
  have ‹∃p''. p' ↠↦↠$ tr p''› by auto
  then obtain p'' where ‹p' ↠↦↠$ tr p''› by auto
  with ‹p ↦ α p'›
  have ‹p ↠↦↠$ (α # tr) p''›
    by (metis lts_tau.silent_reachable.intros(1) lts_tau.silent_reachable_append_τ
        lts_tau.weak_step_def lts_tau.weak_step_sequence.intros(2))
  then have ‹∃p''. p ↠↦↠$ (α # tr) p''› by auto
  then show ‹(α # tr) ∈ weak_traces p› by auto
qed

text ‹A state is weakly trace pre-ordered to another other, ‹weakly_trace_preordered›
denoted by ‹≲WT› if all its traces can also be observed from the second process.›
definition weakly_trace_preordered (infix ‹≲WT› 60) where
  ‹p ≲WT q ≡ weak_traces p ⊆ weak_traces q›

definition weakly_trace_equivalent (infix ‹≃WT› 60) where
  ‹p ≃WT q ≡ p ≲WT q ∧ q ≲WT p›

text ‹Just like \<^term>‹step_setp›, one can lift \<^term>‹silent_reachable› to sets of states.›
abbreviation silent_reachable_setp (infix ‹↠S› 80) where
  ‹P ↠S P' ≡ ((∀p' ∈ P'. ∃p ∈ P. p ↠ p') ∧ (∀p ∈ P. ∀p'. p ↠ p' ⟶ p' ∈ P'))›

definition silent_reachable_set :: ‹'s set ⇒ 's set› where
  ‹silent_reachable_set P ≡ { q . ∃p ∈ P. p ↠ q }›

lemma sreachable_set_is_sreachable: ‹P ↠S (silent_reachable_set P)›
  using silent_reachable_set_def by auto

lemma sreachable_set_eq:
  assumes ‹P ↠S Q›
  shows ‹Q = silent_reachable_set P›
  using sreachable_set_is_sreachable assms by fastforce

text ‹We likewise lift \<^term>‹soft_step› to sets of states.›
abbreviation soft_step_setp (‹_ ↦aS _ _› [70,70,70] 80) where
  ‹P ↦aS α Q ≡ (∀q ∈ Q. ∃p ∈ P. p ↦a α q) ∧ (∀p ∈ P. ∀q. p ↦a α q ⟶ q ∈ Q)›

definition soft_step_set :: ‹'s set ⇒ 'a ⇒ 's set› where
  ‹soft_step_set P α ≡ { q . ∃p ∈ P. p ↦a α q }›

lemma soft_step_set_is_soft_step_set:
  ‹P ↦aS α (soft_step_set P α)›
  using soft_step_set_def by auto

lemma exactly_one_soft_step_set:
  ‹∃!Q. P ↦aS α Q›
proof -
  from soft_step_set_is_soft_step_set
  have ‹P ↦aS α (soft_step_set P α)›
    and ‹⋀Q. P ↦aS α Q ⟹ Q = (soft_step_set P α)›
    by fastforce+
  show ‹∃!Q. P ↦aS α Q›
  proof
    from ‹P ↦aS α (soft_step_set P α)›
    show ‹P ↦aS α (soft_step_set P α)› .
  next
    from ‹⋀Q. P ↦aS α Q ⟹ Q = (soft_step_set P α)›
    show ‹⋀Q. P ↦aS α Q ⟹ Q = (soft_step_set P α)› .
  qed
qed

lemma soft_step_set_eq:
  assumes ‹P ↦aS α Q›
  shows ‹Q = soft_step_set P α›
  using exactly_one_soft_step_set soft_step_set_is_soft_step_set assms
  by fastforce

text ‹A state is stable if it cannot make any further internal steps.›
abbreviation ‹stable_state p ≡ ∀p'. ¬(p ↦ τ p')›

lemma stable_state_stable:
  assumes ‹stable_state p› ‹p ↠ p'›
  shows ‹p = p'›
  using assms(2,1) by (cases, blast+)

definition stability_respecting :: ‹('s ⇒ 's ⇒ bool) ⇒ bool› where
  ‹stability_respecting R ≡ ∀ p q. R p q ∧ stable_state p ⟶
    (∃q'. q ↠ q' ∧ R p q' ∧ stable_state q')›

end ― ‹of locale ‹lts_tau››

end