Theory LTS

text ‹\newpage›
section ‹LTS \label{sect:LTS}›
theory LTS
  imports Main
begin

subsection ‹Labelled Transition Systems›

text ‹
The locale @{term ‹LTS›} represents a labelled 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}$ (cf. \cite[defintion 1]{bisping2023lineartimebranchingtime}).
We formalize the sets of states and actions by the type variables ‹'s› and ‹'a›. An LTS is then determined by the transition relation @{term ‹step›}.
Due to technical limitations we use the notation ‹p ↦α p'› which has same meaing as $p \xrightarrow{\alpha} p'$ has in \cite{bisping2023lineartimebranchingtime}.

›

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›. We define ‹P ↦S α Q› to be true if and only if for all states ‹q› in ‹Q› there exists
a state ‹p› in ‹P› such that ‹p ↦ α q› and for all ‹p› in ‹P› and for all ‹q›, if ‹p ↦ α q› then ‹q› is in ‹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 possible ‹α›-steps for a set of states ‹P› are all ‹q› such that there is a state ‹p› in ‹P› with ‹p ↦ α q›.›
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 ‹For a set of states ‹P› and an action ‹α› there exists exactly one ‹Q› such that ‹P ↦S α Q›.›
lemma exactly_one_step_set: ‹∃!Q. P ↦S α Q›
proof -
  from step_set_is_step_set
  have ‹P ↦S α (step_set P α)›
    and ‹⋀Q. P ↦S α Q ⟹ Q = (step_set P α)›
    by fastforce+
  then show ‹∃!Q. P ↦S α Q›
    by blast
qed

text ‹The lifted @{term ‹step›} (‹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 exactly_one_step_set by fastforce

end (*<*) (* locale LTS *) (*>*)

subsection ‹Labelled Transition Systems with Silent Steps›

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

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

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

text ‹A state ‹p› is @{term ‹silent_reachable›}, represented by the symbol ‹↠›, from another state ‹p'› iff there exists a path of ‹τ›-transitions.
from ‹p'› to ‹p›.›
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 @{term ‹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 ‹In the following, we define @{term ‹weak_step›} as a new notion of transition relation between states. A state ‹p› can reach
‹p'› 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''›
proof (cases ‹α = τ›)
  case True
  assume ‹p ↠ p'›
     and ‹p' ↠↦↠ α p''›
     and ‹α = τ›
  hence ‹p' ↠↦↠ τ p''› by auto
  then have ‹p' ↠ p''› unfolding weak_step_def by auto
  with ‹p ↠ p'›
  have ‹p ↠ p''› using silent_reachable_trans
    by blast
  then have ‹p ↠↦↠ τ p''› unfolding weak_step_def by auto
  with ‹α = τ›
  show ‹p ↠↦↠ α p''› by auto
next
  case False
  assume ‹p ↠ p'›
    and ‹p' ↠↦↠ α p''›
    and ‹α ≠ τ›
  then have ‹∃p1 p2. p' ↠ p1 ∧ p1 ↦ α p2 ∧ p2 ↠ p''›
    using weak_step_def by auto
  then obtain p1 and p2 where ‹p' ↠ p1› and ‹p1 ↦ α p2› and ‹p2 ↠ p''› by auto

  from ‹p ↠ p'› and ‹p' ↠ p1›
  have ‹p ↠ p1› by (rule silent_reachable_trans)

  with ‹p1 ↦ α p2› and ‹p2 ↠ p''› and ‹α ≠ τ›
  show ‹p ↠↦↠ α p''›
    using weak_step_def by auto
qed

text ‹A sequence of @{term ‹weak_step›}'s from one state ‹p› to another ‹p'› is called a @{term ‹weak_step_sequence›}
That means that ‹p'› can be reached from ‹p› with that sequence of steps.›
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 LTS_Tau.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 or all possible sequences of weak transitions that can be performed.
In the context of labelled transition systems, weak traces capture the observable behaviour of a state.›
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 ‹Since @{term ‹weak_step›}'s can be proceeded and followed by any number ‹τ›-transitions and the empty
@{term ‹weak_step_sequence›} also allows ‹τ›-transitions, ‹τ› can be prepended to a weak trace of a state.›
lemma prepend_τ_weak_trace:
  assumes ‹tr ∈ weak_traces p›
  shows ‹(τ # tr) ∈ weak_traces p›
  using silent_reachable.intros(1)
    and weak_step_def
    and assms
    and mem_Collect_eq
    and weak_step_sequence.intros(2)
  by fastforce

text ‹If state ‹p'› is reachable from state ‹p› via a sequence of ‹τ›-transitions and there exists a weak trace ‹tr› starting from ‹p'›,
then ‹tr› is also a weak trace starting from ‹p›.›
lemma silent_prepend_weak_traces:
  assumes ‹p ↠ p'›
      and ‹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'›
      and ‹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 ‹One of the behavioural pre-orders/equivalences that we talk about is trace pre-order/equivalence.
This is the modal characterization for one state is weakly trace pre-ordered to the other, @{term ‹weakly_trace_preordered›}
denoted by ‹≲WT›, and two states are weakly trace equivalent, @{term ‹weakly_trace_equivalent›} denoted ‹≃WT›.›
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 exactly_one_sreachable_set: ‹∃!Q. P ↠S Q›
proof -
  from sreachable_set_is_sreachable
  have ‹P ↠S (silent_reachable_set P)› .

  have ‹⋀Q. P ↠S Q ⟹ Q = (silent_reachable_set P)›
  proof -
    fix Q
    assume ‹P ↠S Q›

    with sreachable_set_is_sreachable
    have ‹∀q ∈ Q. q ∈ (silent_reachable_set P)›
      by meson

    from ‹P ↠S Q›
     and sreachable_set_is_sreachable
    have ‹∀q ∈ (silent_reachable_set P). q ∈ Q›
      by meson

    from ‹∀q ∈ Q. q ∈ (silent_reachable_set P)›
     and ‹∀q ∈ (silent_reachable_set P). q ∈ Q›
    show ‹Q = (silent_reachable_set P)› by auto
  qed

  with ‹P ↠S (silent_reachable_set P)›
  show ‹∃!Q. P ↠S Q›
    by blast
qed


lemma sreachable_set_eq:
  assumes ‹P ↠S Q›
  shows ‹Q = silent_reachable_set P›
  using exactly_one_sreachable_set 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

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 (* locale LTS_Tau *)

end (* theory LTS *)