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)›
abbreviation no_special_action :: ‹'a ⇒ bool›
where ‹no_special_action α
≡ α ≠ τ ∧ α ≠ t ∧ α ≠ t_ε ∧ (∀ X. α ≠ ε[X])›
lemma 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
end