Theory Mapping_for_Transition_Systems

(*<*)
theory Mapping_for_Transition_Systems
  imports
    Labelled_Transition_Systems_with_TimeOuts
begin
(*>*)

section ‹A Mapping for Transition Systems›
text ‹\label{sec:mapping_lts}›

text ‹Let $\mathbb{T} = (\Proc, \Act, \rightarrow)$ be an \LTSt{}. Let $A = \Act \!\setminus\! \{\tau, t\}$.

In reference to van~Glabbeek's $\theta_X$-operators, I introduce a family of operators $\vartheta_X$ with similar but not identical semantics. Additionally, I introduce the operator $\vartheta$ that places a process in an indeterminate environment.

Furthermore, I introduce a family of special actions $\varepsilon_X$ for $X \subseteq A$ that represent a triggered environment stabilising into an environment~$X$, as well as a special action $t_\varepsilon$ that represents a time-out of the environment.

We assume that $t_\varepsilon \notin \Act$ and $\forall X \subseteq A.\; \varepsilon_X \notin \Act$. 

Then we define $\mathbb{T}_\vartheta = (\Proc_\vartheta, \Act_\vartheta, \rightarrow_\vartheta)$ with
\begin{align*}
    \Proc_\vartheta &= \{ \vartheta(p) \mid p \in \Proc \} \cup \{ \vartheta_X(p) \mid p \in \Proc \wedge X \subseteq A \}, \\
    \Act_\vartheta &= \Act \cup \{t_\varepsilon\} \cup \{ \varepsilon_X \mid X \subseteq A \},
\end{align*}
and $\rightarrow_\vartheta$ defined by the following rules:
\vspace{2\baselineskip}

\begin{tabular}{c c}
$\displaystyle
(1)\,\frac{p \xrightarrow{\tau} p'}{\vartheta(p) \xrightarrow{\tau}_\vartheta \vartheta(p')}
$
&
$\displaystyle
(2)\,\frac{}{\vartheta(p) \xrightarrow{\varepsilon_X}_\vartheta \vartheta_X(p)} \; X \subseteq A
$
\\[2.5em]
$\displaystyle
(3)\,\frac{p \xrightarrow{a} p'}{\vartheta_X(p) \xrightarrow{a}_\vartheta \vartheta(p')} \; a \in X
$
&
$\displaystyle
(4)\,\frac{p \xrightarrow{\tau} p'}{\vartheta_X(p) \xrightarrow{\tau}_\vartheta \vartheta_X(p')}
$
\\[2.5em]
$\displaystyle
(5)\,\frac{p \not\xrightarrow{\alpha} \text{ for all } \alpha \in X \cup \{\tau\}}
{\vartheta_X(p) \xrightarrow{t_\varepsilon}_\vartheta \vartheta(p)}
$
&
$\displaystyle
(6)\,\frac{p \not\xrightarrow{\alpha} \text{ for all } \alpha \in X \cup \{\tau\} \quad\; p \xrightarrow{t} p'}
{\vartheta_X(p) \xrightarrow{t}_\vartheta \vartheta_X(p')}
$
\end{tabular}
\vspace{2\baselineskip}

These rules mirror the clauses of the definition of SRBs (cf.\@ \cref{sec:reactive_bisimilarity}):

\begin{enumerate}[nosep]
    \item $\tau$-transitions can be performed regardless of the environment,
    \item indeterminate environments can stabilise into arbitrary stable \linebreak environments~$X$ for $X \subseteq A$,
    \item facilitated visible transitions can be performed and can trigger a change in the environment,
    \item $\tau$-transitions cannot be observed by the environment and hence cannot trigger a change,
    \item if the underlying system is idle, the environment may time-out and turn into an indeterminate/triggered environment,
    \item if the underlying system is idle and has a $t$-transition, the transition may be performed and is not observable by the environment.
\end{enumerate}

\example{%
The \LTSt{} on the left (with $\Act = \{a,\tau,t\}$) gets mapped to the LTS on the right. States that have no incoming or outgoing transitions other than $\varepsilon_X$ or $t_\varepsilon$ are omitted. Note how $\vartheta(p_4)$ is not reachable from $\vartheta(p)$.

\phantomsection
\label{fig:mapping_example}
\scalebox{.9}{\vbox{\lts{
    \node[state]    (P)                             {$p$};
    \node[state]    (Q) [below left of=P]           {$p_1$};
    \node[state]    (R) [below right of=P]          {$p_2$};
    \node[state]    (S) [below left of=R]           {$p_3$};
    \node[state]    (T) [below right of=R]          {$p_4$};
    
    \path   (P) edge node[above left]               {$a$}               (Q)
                edge node[above right]              {$t$}               (R)
            (R) edge node[above left]               {$\tau$}            (S)
                edge node[above right]              {$a$}               (T);


    \node[state]    (Pt) [right of=P, xshift=4.5cm] {$\vartheta(p)$};
    \node[state]    (Pa) [below left of=Pt]         {$\vartheta_{\{a\}}(p)$};
    \node[state]    (Pe) [below right of=Pt]        {$\vartheta_\emptyset(p)$};
    \node[state]    (Rt) [right of=Pe]              {$\vartheta(p_2)$};
    \node[state]    (Qt) [below of=Pa]              {$\vartheta(p_1)$};
    \node[state]    (Re) [below of=Pe]              {$\vartheta_\emptyset(p_2)$};
    \node[state]    (Se) [below of=Re]              {$\vartheta_\emptyset(p_3)$};
    \node[state]    (Ra) [below of=Rt,xshift=1.8cm] {$\vartheta_{\{a\}}(p_2)$};
    \node[state]    (Tt) [right of=Ra,xshift=.7cm]  {$\vartheta(p_4)$};
    \node[state]    (Sa) [below of=Ra]              {$\vartheta_{\{a\}}(p_3)$};
    \node[state]    (St) [right of=Se,yshift=-2cm]  {$\vartheta(p_3)$};
    
    \path   (Pt)    edge node[above left]           {$\varepsilon_{\{a\}}$}     (Pa)
            (Pt)    edge node[left]                 {$\varepsilon_\emptyset$}   (Pe)
            (Pe)    edge[bend right] node[right]    {$t_\varepsilon$}           (Pt)
            (Pa)    edge node[left]                 {$a$}                       (Qt)
            (Pe)    edge node[left]                 {$t$}                       (Re)
            (Re)    edge node[left]                 {$\tau$}                    (Se)
            (Rt)    edge node[right]                {$\varepsilon_{\{a\}}$}     (Ra)
            (Rt)    edge node[left]                 {$\varepsilon_\emptyset$}   (Re)
            (Ra)    edge node[above]                {$a$}                       (Tt)
            (Ra)    edge node[left]                 {$\tau$}                    (Sa)
            (Se)    edge node[above]                {$t_\varepsilon$}           (St)
            (St)    edge[bend left] node[left]      {$\varepsilon_\emptyset$}   (Se)
            (Sa)    edge node[above]                {$t_\varepsilon$}           (St)
            (St)    edge[bend right] node[right]    {$\varepsilon_{\{a\}}$}   (Sa)
            (Rt)    edge node[right]                {$\tau$}                    (St);
            
    \coordinate [below of=Qt,yshift=10pt] (Qc);
    \coordinate [below of=Tt,yshift=10pt] (Tc);
            
    \draw [dotted,->,shorten >= 7pt] (Qt) to[bend right] node[left] {$\varepsilon_{\dots}$} (Qc);
    \draw [dotted,->,shorten <= 7pt] (Qc) to[bend right] node[right] {$t_\varepsilon$} (Qt);
    \draw [dotted,->,shorten >= 7pt] (Tt) to[bend right] node[left] {$\varepsilon_{\dots}$} (Tc);
    \draw [dotted,->,shorten <= 7pt] (Tc) to[bend right] node[right] {$t_\varepsilon$} (Tt);
}}}}
\vspace{-1cm}›


subsection ‹Isabelle›

subsubsection ‹Formalising \boldmath{$\Proc_\vartheta$} and \boldmath{$\Act_\vartheta$}›

text ‹We specify another locale based on lts_timeout›, where the aforementioned special actions and operators are considered; we call it lts_timeout_mappable›. 
Since $\Proc \cap \Proc_\vartheta = \emptyset$, we introduce a new type variable 'ss› for $\Proc_\vartheta$; we use 'a› for both $\Act$ and $\Act_\vartheta$.
We formalise the family of special actions $\varepsilon_X$ as a mapping ε[_] :: 'a set ⇒ 'a›, and the environment operators $\vartheta$/$\vartheta_X$ as a single mapping θ?[_](_) :: 'a set option ⇒ 's ⇒ 'ss›.

As for lts_timeout› in \cref{sec:LTSt}, we require that all special actions are distinct, formalised by the first set of assumptions distinctness_special_actions›.

As an operator, the term $\vartheta_X(p)$ simply refers to the state $p$ in an environment~$X$; when understood as a mapping, we have to be more careful, since θ?[Some X](p)› is now itself a state. Specifically, we have to assume that θ?[_](_)› is injective (when restricted to domains where \linebreak X ⊆ visible_actions›, because $\vartheta_X$ is only defined for those $X \subseteq A$). Otherwise, we might have θ?[None](p) = θ?[None](q)› for p ≠ q›, which is problematic if e.g.\@ p› has a τ›-transition, but q› does not.
The restricted injectivity of θ?[_](_)› is formalised as the set of assumptions injectivity_theta›.

The same is required for the mapping ε[_]›, as formalised in the last clause of the set of assumptions distinctness_special_actions› (the restricted injectivity of ε[_]› is part of the requirement that all special actions must be distinct). Again, we only require injectivity for the mapping restricted to the domain visible_actions›. If we required that ε[_] :: 'a set ⇒ 'a› were injective over its entire domain 'a set›, we would run into problems, since such a function cannot exist by Cantor's theorem.

That such mappings exist is intuitively clear, whence there were no ambiguities when defining them as operators in the prosaic/mathematical section above. Formalising these mappings in HOL, however, is not so straight\-forward: as operators, we assume that they are only defined for certain parameters; in HOL, every mapping must be total. For now, we simply assume that such total functions that formalise these operators exist. Doing this significantly improves the readability of following sections, since we must only consider the relevant properties of the mappings given by the assumptions. In \cref{chap:example_instantiation}, I give examples for these mappings and show that, together with these, any lts_timeout› can be interpreted as an lts_timeout_mappable›, i.e.\@ every \LTSt{} $\mathbb{T}$ can be mapped to an LTS $\mathbb{T}_\vartheta$.

Lastly, we formalise our requirements $t_\varepsilon \notin \Act$ and $\forall X \subseteq A.\; \varepsilon_X \notin \Act$ as the last set of assumptions no_epsilon_in_tran›. Technically, these assumptions only state that the $\varepsilon$-actions do not label any transition of $\mathbb{T}$. However, we can assume that 
$\Act = \{ \alpha \mid \exists p, p'.\; p \xrightarrow{\alpha} p' \}$, 
since actions that do not label any transitions are not relevant to the behaviour of an LTS.›

locale lts_timeout_mappable = lts_timeout tran τ t 
  for tran :: "'s  'a  's  bool" 
      ("_ _ _" [70, 70, 70] 80) 
    and τ :: 'a 
    and t :: 'a +
  fixes t_ε :: 'a 
    and stabilise :: 'a set  'a 
      (ε[_]) 
    and in_env :: 'a set option  's  'ss 
      (θ?[_]'(_'))
  assumes
    distinctness_special_actions:
    τ  t τ  t_ε t  t_ε
    ε[X]  τ ε[X]  t ε[X]  t_ε 
    X  visible_actions  ε[X] = ε[Y]  X = Y
    and
    
    injectivity_theta:
    θ?[None](p)  θ?[Some X](q)
    (θ?[None](p) = θ?[None](q))  p = q
    X  visible_actions  
      (θ?[Some X](p) = θ?[Some Y](q))  X = Y  p = q
    and

    no_epsilon_in_tran:
    ¬ p ε[X] q
    ¬ p t_ε q
begin

text ‹We can now define abbreviations with notations that correspond more closely to our operators defined above.›

abbreviation triggered_env :: 's  'ss 
  (θ'(_'))
  where θ(p)  θ?[None](p)
abbreviation stable_env :: 'a set  's  'ss 
  (θ[_]'(_'))
  where θ[X](p)  θ?[Some X](p)

(* This abbreviation and this lemma are not important for the thesis document. *)
(*<*)
abbreviation‹tag unimportant› no_special_action :: 'a  bool›
  where no_special_action α 
     α  τ  α  t  α  t_ε  ( X. α  ε[X])

lemma‹tag (proof) unimportant› special_actions_invisible:
  assumes X  visible_actions› α  X
  shows ‹no_special_action α
  using assms(1) assms(2) no_epsilon_in_tran(1) no_epsilon_in_tran(2) visible_actions_def by auto
(*>*)

subsubsection ‹Formalising \boldmath{$\rightarrow_\vartheta$}›
text ‹We formalise the transition relation of our mapping, given above by the structural operational rules, as a function tran_theta›.% 
\footnote{We use the notation _ ⟼θ_ _› instead of the more obvious _ ⟼θ_ _› simply because of better readability.}

We use the inductive› command, because it allows us to define separate clauses (as opposed to the definition› command). Technically speaking, however, this inductive definition only has base cases, since none of the premises involves θ.

It should be easy to see that the clauses below correspond directly to the rules above. Like in previous sections, we have to take extra care to handle the requirement X ⊆ visible_actions›.›

inductive tran_theta :: 'ss  'a  'ss  bool› 
  (‹_ θ_ _› [70, 70, 70] 70)
  where 
    triggered_tau:
      p τ q  θ(p) θτ θ(q)
  | env_stabilise: X  visible_actions  
      θ(p) θε[X] θ[X](p)
  | tran_visible: X  visible_actions  
      a  X  p a q  θ[X](p) θa θ(q)
  | stable_tau: X  visible_actions  
      p τ q  θ[X](p) θτ θ[X](q)
  | env_timeout: X  visible_actions  
      idle p X  θ[X](p) θt_ε θ(p)
  | sys_timeout: X  visible_actions  
      idle p X  p t q  θ[X](p) θt θ[X](q)

subsubsection ‹Note on Metavariable usage›

text ‹If not referenced directly by $\vartheta(p)$ or $\vartheta_X(p)$, arbitrary states of a mapped LTS range over $P, Q, P', Q', \dots$, where $P$ and $P'$ are used for states connected by some transition (i.e.\@ $P \xrightarrow{\alpha}_\vartheta P'$), whereas $P$ and $Q$ are used for states possibly related by some equivalence (e.g.\@ $P \leftrightarrow_r Q$).›

text ‹\pagebreak›
subsubsection ‹Generation Lemmas›

text ‹Lastly, we derive a set of generation lemmas, i.e.\@ lemmas that allow us to reason backwards: if we know P ⟼θα P'› and some other information about P› and/or α›, we can deduce some information about the other variables as well as the transitions of the original \LTSt{}.›

lemma generation_triggered_transitions:
  assumes θ(p) θα P'
  shows (X. α = ε[X]  P' = θ[X](p)  X  visible_actions) 
     (α = τ  (p'. p τ p'))
  using iffD1[OF tran_theta.simps assms]
  by (smt (z3) injectivity_theta(1,2))

lemma generation_stable_transitions:
  assumes θ[X](p) θα P'
  shows α = t_ε  ( p'. p α p'  (α  X  α = τ  α = t))
  using iffD1[OF tran_theta.simps assms]
  by (smt injectivity_theta(1,3) lts_timeout_mappable_axioms)

lemma generation_triggered_tau:
  assumes θ(p) θτ P'
  shows  p'. P' = θ(p')  p τ p'
  using iffD1[OF tran_theta.simps assms]
  using distinctness_special_actions(4) injectivity_theta(1) injectivity_theta(2) by blast
  
lemma generation_env_stabilise:
  assumes P θε[X] P'
  shows  p. P = θ(p)  P' = θ[X](p) 
  using iffD1[OF tran_theta.simps assms(1)] 
  by (smt (z3) distinctness_special_actions(6) distinctness_special_actions(7) no_epsilon_in_tran(1))

lemma generation_tran_visible:
  assumes θ[X](p) θa P' a  visible_actions›
  shows a  X  ( p'. P' = θ(p')  p a p')
  using iffD1[OF tran_theta.simps assms(1)]
proof (elim disjE, goal_cases)
  case 1
  then obtain p' where θ[X](p) = θ(p') by blast
  hence False using injectivity_theta(1) by metis
  thus ?case by simp
next
  case 2
  then show ?case by (metis injectivity_theta(1))
next
  case 3
  hence X  visible_actions› by (metis injectivity_theta(3))
  with 3 show ?case using injectivity_theta(3) by blast
next
  case 4
  hence False using visible_actions_def assms(2) by simp
  thus ?case by simp
next
  case 5
  then show ?case using assms(2) no_epsilon_in_tran(2) visible_actions_def by auto
next
  case 6
  hence False using visible_actions_def assms(2) by simp
  thus ?case by simp
qed

lemma generation_stable_tau:
  assumes θ[X](p) θτ P'
  shows  p'. P' = θ[X](p')  p τ p'
  using iffD1[OF tran_theta.simps assms]
proof (elim disjE, goal_cases)
  case 1
  then obtain p' where θ[X](p) = θ(p') by blast
  hence False using injectivity_theta(1) by metis
  thus ?case by simp
next
  case 2
  hence False using distinctness_special_actions by blast
  thus ?case by simp
next
  case 3
  then show ?case using visible_actions_def by fastforce
next
  case 4
  hence X  visible_actions› by (metis injectivity_theta(3))
  with 4 show ?case using injectivity_theta(3) by blast
next
  case 5
  hence False using distinctness_special_actions by blast
  thus ?case by simp
next
  case 6
  hence False using lts_timeout_axioms lts_timeout_def by force
  thus ?case by simp
qed
  
lemma generation_env_timeout:
  assumes θ[X](p) θt_ε P'
  shows P' = θ(p)  idle p X
  using iffD1[OF tran_theta.simps assms] distinctness_special_actions
  by (smt injectivity_theta(3) insertCI no_epsilon_in_tran(2))+

lemma generation_sys_timeout:
  assumes θ[X](p) θt P'
  shows  p'. P' = θ[X](p')  idle p X  p t p'
  using iffD1[OF tran_theta.simps assms]
proof (elim disjE, goal_cases)
  case 1
  then obtain p' where θ[X](p) = θ(p') by blast
  hence False using injectivity_theta(1) by metis
  thus ?case ..
next
  case 2
  hence False using distinctness_special_actions by blast
  thus ?case ..
next
  case 3
  then show ?case using visible_actions_def by auto
next
  case 4
  hence False using lts_timeout_axioms lts_timeout_def by force
  thus ?case ..
next
  case 5
  hence False using distinctness_special_actions by blast
  thus ?case ..
next
  case 6
  hence X  visible_actions› by (metis injectivity_theta(3))
  with 6 show ?case using injectivity_theta(3) by blast
qed

end ― ‹of locale lts_timeout_mappable›
(*<*)
end ― ‹of ‹theory››
(*>*)