Theory HM_Logic_with_TimeOuts
theory HM_Logic_with_TimeOuts
imports
Reactive_Bisimilarity
"HOL-Library.Countable_Set_Type"
begin
section ‹Hennessy-Milner Logic with Time-Outs›
text ‹\label{sec:HMLt}›
text ‹In @{cite ‹section 3› rbs}, van~Glabbeek extends Hennessy-Milner logic by a family of new modal operators $\langle X \rangle \varphi$ for $X \subseteq A$, as well as additional satisfaction relations $\vDash_X$ for $X \subseteq A$. Intuitively, $p \vDash \langle X \rangle \varphi$ means that $p$ is idle when placed in an environment~$X$ \emph{and} $p$ can perform a $t$-transition into a state that satisfies $\varphi$; $p \vDash_X \varphi$ means that $p$ satisfies $\varphi$ in environments~$X$.
I will refer to this extension as \emph{Hennessy-Milner Logic with Time-Outs} (\HMLt{}) and to $\langle X \rangle$ for $X \subseteq A$ as the \emph{time-out--possibility operators} (to be distinguished from the ordinary possibility operators $\langle \alpha \rangle$ for $\alpha \in \Act$).
The precise semantics are given by the following inductive definition of the satisfaction relation @{cite ‹section 3› rbs} (notation adapted):
\begin{tabular}{l l l}
$p \vDash \bigwedge_{i \in I} \varphi_i$
& \text{if}
& $\forall i \in I.\; p \vDash \varphi_i$ \\
$p \vDash \neg\varphi$
& \text{if}
& $p \not\vDash \varphi$ \\
$p \vDash \langle \alpha \rangle \varphi$ \quad with $\alpha \in A \cup \{\tau\}$
& \text{if}
& $\exists p'.\; p \xrightarrow{\alpha} p' \wedge p' \vDash \varphi$ \\
$p \vDash \langle X \rangle \varphi$ \quad with $X \subseteq A$
& \text{if}
& $\mathcal{I}(p) \cap (X \cup \{\tau\}) = \emptyset \wedge \exists p'.\; p \xrightarrow{t} p' \wedge p' \vDash_X \varphi$ \\[1em]
$p \vDash_X \bigwedge_{i \in I} \varphi_i$
& \text{if}
& $\forall i \in I.\; p \vDash_X \varphi_i$ \\
$p \vDash_X \neg\varphi$
& \text{if}
& $p \not\vDash_X \varphi$ \\
$p \vDash_X \langle a \rangle \varphi$ \quad with $a \in A$
& \text{if}
& $a \in X \wedge \exists p'.\; p \xrightarrow{a} p' \wedge p' \vDash \varphi$ \\
$p \vDash_X \langle \tau \rangle \varphi$
& \text{if}
& $\exists p'.\; p \xrightarrow{\tau} p' \wedge p' \vDash_X \varphi$ \\[0.5em]
$p \vDash_X \varphi$
& \text{if}
& $\mathcal{I}(p) \cap (X \cup \{\tau\}) = \emptyset \wedge p \vDash \varphi$
\end{tabular}›
text ‹The same intuitions regarding triggered and stable environments as for the definition of strong reactive bisimulations in \cref{sec:strong_bisimilarity} hold. $\vDash$ expresses that a property holds in indeterminate environments and $\vDash_X$ that a property holds in stable environments~$X$. The last clause expresses the possibility of stable environments timing out into triggered environments.
Van~Glabbeek then also proves that \HMLt{} characterises strong reactive/$X$-bisimilarity, i.e.\@ that
$p \leftrightarrow_r q \iff (\forall \varphi .\; p \vDash \varphi \longleftrightarrow q \vDash \varphi)$ and
$p \leftrightarrow_r^X q \iff (\forall \varphi .\; p \vDash_X \varphi \longleftrightarrow q \vDash_X \varphi)$,
where $\varphi$ are formulas of \HMLt{}.
A replication of the proof of this characterisation, however, is not part of this thesis.
›
subsection ‹Isabelle›
text ‹The following formalisation is analogous to the one in \cref{sec:HML}.›
datatype ('a)HMLt_formula =
HMLt_conj ‹('a)HMLt_formula cset›
| HMLt_neg ‹('a)HMLt_formula›
| HMLt_poss ‹'a› ‹('a)HMLt_formula›
| HMLt_time ‹'a set› ‹('a)HMLt_formula›
notation cin (‹_ ∈⇩c _› [100, 100] 100)
text ‹In order to formalise the semantics, I combined both the usual satisfaction relation $\vDash$ and the environment satisfaction relations $\vDash_X$ into one predicate, which is formalised by the function ‹HMLt_sat› below, where ‹p ⊫?[None] φ› corresponds to $p \vDash \varphi$ and ‹p ⊫?[Some X] φ› corresponds to $p \vDash_X \varphi$.
Note that, in Isabelle code, I use the symbol ‹⊫› for all satisfaction relations in the context of \HMLt{}, whereas I use ‹⊨› for satisfaction relations in the context of ordinary HML.
This notational nuance will be important when we examine the relationship between the satisfaction relations of \HMLt{} and HML in the context of the reduction in \cref{sec:reduction_satisfaction}.
The first four clauses of my formalisation are clearly direct translations of the clauses for the satisfaction relation $\vDash$ above. It is less easy to see that the next four clauses do, in fact, correspond to the five clauses for $\vDash_X$.
First, each of the four clauses below includes the requirement that ‹X› is a subset of the visible actions; in the original definition, the satisfaction relations $\vDash_X$ are only defined for those $X$ to begin with.
Next, the clause for ‹p ⊫?[Some X] (HMLt_poss α φ)› combines the original clauses for $p \vDash_X \langle a \rangle \varphi$ and $p \vDash_X \langle \tau \rangle \varphi$.
Lastly and most importantly, the last clause of the original definition, stating that $p \vDash_X \varphi$ if $p$ is idle in environments~$X$ and $p \vDash \varphi$, is added disjunctively to the cases ‹p ⊫?[Some X] (HMLt_poss α φ)› and ‹p ⊫?[Some X] (HMLt_time Y φ)›; the latter case is not part of the original definition and can only be true by virtue of the last clause of the original definition, wherefore this is the only way for this case in the function definition below to be true.
I will show below that this is sufficient to assure that my satisfaction function satisfies the last clause of the original definition, i.e.\@ that it is not required to be added disjunctively to the cases ‹p ⊫?[Some X] (HMLt_conj Φ)› and ‹p ⊫?[Some X] (HMLt_neg φ)›.›
context lts_timeout begin
function HMLt_sat :: ‹'s⇒'a set option⇒('a)HMLt_formula ⇒ bool›
(‹_ ⊫?[_] _› [50, 50, 50] 50)
where
‹(p ⊫?[None] (HMLt_conj Φ)) =
(∀ φ. φ ∈⇩c Φ ⟶ p ⊫?[None] φ)›
| ‹(p ⊫?[None] (HMLt_neg φ)) =
(¬ p ⊫?[None] φ)›
| ‹(p ⊫?[None] (HMLt_poss α φ)) =
((α ∈ visible_actions ∪ {τ}) ∧
(∃ p'. p ⟼α p' ∧ p' ⊫?[None] φ))›
| ‹(p ⊫?[None] (HMLt_time X φ)) =
((X ⊆ visible_actions) ∧ (idle p X) ∧
(∃ p'. p ⟼t p' ∧ p' ⊫?[Some X] φ))›
| ‹(p ⊫?[Some X] (HMLt_conj Φ)) = (X ⊆ visible_actions ∧
(∀ φ. φ ∈⇩c Φ ⟶ p ⊫?[Some X] φ))›
| ‹(p ⊫?[Some X] (HMLt_neg φ)) = (X ⊆ visible_actions ∧
(¬ p ⊫?[Some X] φ))›
| ‹(p ⊫?[Some X] (HMLt_poss α φ)) = (X ⊆ visible_actions ∧
(((α ∈ X) ∧ (∃ p'. p ⟼α p' ∧ p' ⊫?[None] φ)) ∨
((α = τ) ∧ (∃ p'. p ⟼τ p' ∧ p' ⊫?[Some X] φ)) ∨
((idle p X) ∧ (p ⊫?[None] (HMLt_poss α φ)))))›
| ‹(p ⊫?[Some X] (HMLt_time Y φ)) = (X ⊆ visible_actions ∧
((idle p X) ∧ (p ⊫?[None] (HMLt_time Y φ))))›
using HMLt_formula.exhaust
by (metis (no_types, hide_lams) not_Some_eq prod_cases3, fast+)
text ‹The well-founded relation used for the termination proof of the satisfaction function is considerably more difficult due to the last line of the definition containing the same formula on both sides of the implication (as opposed to the other lines of the definition, where the premises only contain subformulas of the formula in the conclusion). We define two relations ‹R› and ‹S›, prove their well-foundedness separately, and show that ‹R O S ⊆ R› (where ‹O› is relation composition), yielding that the union of ‹R› and ‹S› is well-founded using the theorem @{thm wf_union_compatible}. Further details are omitted from the thesis document.›
inductive_set HMLt_wf_rel_1 :: ‹('s × 'a set option × ('a)HMLt_formula) rel› where
‹φ ∈⇩c Φ ⟹ ((p, XoN, φ), (p', XoN', HMLt_conj Φ)) ∈ HMLt_wf_rel_1› |
‹((p, XoN, φ), (p', XoN', HMLt_neg φ)) ∈ HMLt_wf_rel_1› |
‹((p, XoN, φ), (p', XoN', HMLt_poss α φ)) ∈ HMLt_wf_rel_1› |
‹((p, XoN, φ), (p', XoN', HMLt_time X φ)) ∈ HMLt_wf_rel_1›
lemma HMLt_wf_rel_1_is_wf: ‹wf HMLt_wf_rel_1›
unfolding wf_def
proof (rule allI, rule impI, rule allI)
fix P::‹'s × 'a set option × ('a)HMLt_formula ⇒ bool› and t::‹'s × 'a set option × ('a)HMLt_formula›
obtain p XoN φ where ‹t = (p, XoN, φ)›
using prod_cases3 by blast
assume ‹∀x. (∀y. (y, x) ∈ HMLt_wf_rel_1 ⟶ P y) ⟶ P x›
hence ‹P (p, XoN, φ)›
apply (induct φ arbitrary: p XoN)
apply (smt (verit) HMLt_wf_rel_1_def case_prodD case_prodE' mem_Collect_eq HMLt_formula.distinct(1,3,5) HMLt_formula.inject(1) HMLt_wf_rel_1p.simps HMLt_wf_rel_1p_HMLt_wf_rel_1_eq cin.rep_eq prod_cases3)
apply (smt (verit) HMLt_wf_rel_1_def case_prodD case_prodE' mem_Collect_eq HMLt_formula.distinct(1,7,9) HMLt_formula.inject(2) HMLt_wf_rel_1.simps surj_pair)
apply (smt (verit) HMLt_wf_rel_1_def case_prodD case_prodE' mem_Collect_eq HMLt_formula.distinct(3,7,11) HMLt_formula.inject(3) HMLt_wf_rel_1.simps surj_pair)
apply (smt (verit, del_insts) HMLt_formula.distinct(5,9,12) HMLt_formula.inject(4) HMLt_wf_rel_1.simps HMLt_wf_rel_1_def case_prodD case_prodE' mem_Collect_eq)
done
thus ‹P t› using ‹t = (p, XoN, φ)› by simp
qed
inductive_set HMLt_wf_rel_2 :: ‹('s × 'a set option × ('a)HMLt_formula) rel› where
‹((p, None, φ), (p, Some X, φ)) ∈ HMLt_wf_rel_2›
lemma HMLt_wf_rel_2_is_wf: ‹wf HMLt_wf_rel_2›
by (simp add: HMLt_wf_rel_2.simps wf_def)
abbreviation HMLt_wf_rel where ‹HMLt_wf_rel ≡ (HMLt_wf_rel_1 ∪ HMLt_wf_rel_2)›
lemma HMLt_wf_rel_is_wf: ‹wf HMLt_wf_rel›
proof (rule wf_union_compatible[OF HMLt_wf_rel_1_is_wf HMLt_wf_rel_2_is_wf], standard)
fix tup
assume ‹tup ∈ HMLt_wf_rel_1 O HMLt_wf_rel_2›
then obtain a c where ‹(a, c) = tup› ‹(a, c) ∈ HMLt_wf_rel_1 O HMLt_wf_rel_2› by blast
with relcomp.simps obtain b where ‹(a, b) ∈ HMLt_wf_rel_1› ‹(b, c) ∈ HMLt_wf_rel_2› by blast
from ‹(b, c) ∈ HMLt_wf_rel_2› obtain p X φ where ‹b = (p, None, φ)› ‹c = (p, Some X, φ)›
by (metis HMLt_wf_rel_2.cases surj_pair)
have ‹(a, (p, None, φ)) ∈ HMLt_wf_rel_1› using ‹(a, b) ∈ HMLt_wf_rel_1› ‹b = (p, None, φ)› by simp
have ‹(a, (p, Some X, φ)) ∈ HMLt_wf_rel_1›
using ‹(a, (p, None, φ)) ∈ HMLt_wf_rel_1›
proof (induct a)
case (fields p' XoN φ')
then show ?case
by (induct φ' arbitrary: p' XoN, (simp add: HMLt_wf_rel_1.simps)+)
qed
thus ‹tup ∈ HMLt_wf_rel_1›
using ‹(a, c) = tup› ‹c = (p, Some X, φ)› by fastforce
qed
termination HMLt_sat using HMLt_wf_rel_is_wf by (standard, (simp add: HMLt_wf_rel_1.intros HMLt_wf_rel_2.intros)+)
text ‹We can now introduce the more readable notation (more closely corresponding to the notation in @{cite rbs}) through abbreviations.›
abbreviation HMLt_sat_triggered :: ‹'s⇒('a)HMLt_formula ⇒ bool›
("_ ⊫ _" [50, 50] 50)
where ‹p ⊫ φ ≡ p ⊫?[None] φ›
abbreviation HMLt_sat_stable :: ‹'s⇒'a set⇒('a)HMLt_formula ⇒ bool›
("_ ⊫[_] _" [70, 70, 70] 80)
where ‹p ⊫[X] φ ≡ p ⊫?[Some X] φ›
text ‹Lastly, we show (by induction over ‹φ›) that the function ‹HMLt_sat› does indeed satisfy the last clause of the original definition.›
lemma idle_sat_lemma:
assumes
‹idle p X›
‹X ⊆ visible_actions›
shows
‹(p ⊫ φ) = (p ⊫[X] φ)›
proof (induct φ)
case (HMLt_conj Φ)
then show ?case
by (meson assms(2) cin.rep_eq HMLt_sat.simps(1,5))
next
case (HMLt_neg φ)
then show ?case
by (simp add: assms(2))
next
case (HMLt_poss α φ)
show ?case
proof
assume ‹p ⊫ HMLt_poss α φ›
with assms show ‹p ⊫[X] HMLt_poss α φ› using HMLt_sat.simps(7) by blast
next
assume ‹p ⊫[X] HMLt_poss α φ›
hence ‹α ∈ X ∧ (∃p'. p ⟼α p' ∧ p' ⊫ φ) ∨ α = τ ∧ (∃p'. p ⟼τ p' ∧ p' ⊫[X] φ) ∨ idle p X ∧ p ⊫ HMLt_poss α φ›
using HMLt_sat.simps(7) by simp+
thus ‹p ⊫ HMLt_poss α φ› using ‹idle p X›
by (meson UnCI assms(2) idle_no_derivatives singletonI)
qed
next
case (HMLt_time Y φ)
then show ?case using HMLt_sat.simps(8) assms by blast
qed
proposition
assumes
‹X ⊆ visible_actions›
‹idle p X›
‹p ⊫ φ›
shows
‹p ⊫[X] φ›
using idle_sat_lemma[OF assms(2,1)] assms(3) ..
text ‹As the last clause of van Glabbeek's definition is the main disparity to the function definition of ‹HMLt_sat›, this proposition gives confidence that the function does indeed formalise the original definition.›
end
end