Theory HM_Logic_infinitary
theory HM_Logic_infinitary
imports
Strong_Bisimilarity
begin
chapter ‹Infinitary Hennessy-Milner Logic›
text ‹\label{chap:HML_infinitary}›
text ‹We will show that a modal characterisation of strong bisimilarity is possible without any assumptions about the cardinality of derivative sets ‹Der(p, α)›, using infinitary HML (with conjunction of arbitrary cardinality).
Instead of formalising formulas under a conjunction as a countable set,%
\footnote{Note that it is not possible to define a type with a constructor depending on a set of the type itself, i.e.\@ ‹HML_conj ‹('a)HML_formula set›› would not yield a valid type.}
we use an index set of arbitrary type ‹I :: 'x set› and a mapping \linebreak ‹F :: 'x ⇒ ('a,'x)HML_formula› so that each element of ‹I› is mapped to a formula. This closely resembles the semantics of $\bigwedge_{i \in I} \varphi_i$. Instead of using partial mappings ‹F :: 'x ⇒ ('a,'x)HML_formula option›, I included a constructor ‹HML_true› and implicitly assume that ‹F› maps to ‹HML_true› for all objects of type ‹'x› that are not elements of ‹I›.›
datatype ('a,'x)HML_formula =
HML_true
| HML_conj ‹'x set› ‹'x ⇒ ('a,'x)HML_formula›
| HML_neg ‹('a,'x)HML_formula›
| HML_poss ‹'a› ‹('a,'x)HML_formula›
subsubsection ‹Satisfaction Relation›
text ‹Data types cannot be used with variable parameter types ‹'x› in concrete contexts; so when using our data type in the ‹context lts›, we use the type of processes ‹'s› as the type for conjunction index sets.
\pagebreak
Since this suffices to proof the modal characterisation, we can conclude that it suffices for the cardinality of conjunction to be equal to the cardinality of the set of processes $\Proc$. As we can deduce from the part of the proof where formula conjunction is used, a weaker requirement would be to allow for conjunction of cardinality equal to $\displaystyle\max_{\substack{p\in\Proc \\ \alpha\in\Act}} |\text{Der}(p, \alpha)|$.
\vspace{1\baselineskip}
The remainder of this appendix follows the same structure as that in \cref{sec:HML}. The explanations from there mostly apply here as well.›
context lts begin
function satisfies :: ‹'s ⇒ ('a, 's) HML_formula ⇒ bool›
(‹_ ⊨ _› [50, 50] 50)
where
‹(p ⊨ HML_true) = True›
| ‹(p ⊨ HML_conj I F) = (∀ i ∈ I. p ⊨ (F i))›
| ‹(p ⊨ HML_neg φ) = (¬ p ⊨ φ)›
| ‹(p ⊨ HML_poss α φ) = (∃ p'. p ⟼α p' ∧ p' ⊨ φ)›
using HML_formula.exhaust by (auto, blast)
inductive_set HML_wf_rel :: ‹('s × ('a, 's) HML_formula) rel›
where
‹φ = F i ∧ i ∈ I ⟹ ((p, φ), (p, HML_conj I F)) ∈ HML_wf_rel›
| ‹((p, φ), (p, HML_neg φ)) ∈ HML_wf_rel›
| ‹((p, φ), (p', HML_poss α φ)) ∈ HML_wf_rel›
lemma HML_wf_rel_is_wf: ‹wf HML_wf_rel›
unfolding wf_def
proof (rule allI, rule impI, rule allI)
fix P::‹'s × ('a, 's) HML_formula ⇒ bool› and t::‹'s × ('a, 's) HML_formula›
obtain p φ where ‹t = (p, φ)› by force
assume ‹∀x. (∀y. (y, x) ∈ HML_wf_rel ⟶ P y) ⟶ P x›
hence ‹P (p, φ)›
apply (induct φ arbitrary: p)
apply (metis HML_formula.ctr_transfer(1) HML_formula.distinct(3) HML_formula.distinct(5) HML_formula.rel_distinct(2) HML_wf_relp.cases HML_wf_relp_HML_wf_rel_eq surj_pair)
apply (smt (verit) HML_formula.distinct(10) HML_formula.distinct(7) HML_formula.inject(1) HML_wf_rel_def UNIV_I case_prodE' image_eqI lts.HML_wf_rel.cases mem_Collect_eq split_conv)
apply (smt (verit, ccfv_threshold) HML_formula.distinct(11) HML_formula.distinct(7) HML_formula.inject(2) case_prodI2 case_prod_curry lts.HML_wf_rel.cases lts.HML_wf_rel_def)
apply (smt (verit, del_insts) HML_formula.distinct(3,5,9,11) HML_formula.inject(3) HML_wf_rel.cases case_prodD case_prodE' lts.HML_wf_rel_def mem_Collect_eq)
done
thus ‹P t› using ‹t = (p, φ)› by simp
qed
termination satisfies using HML_wf_rel_is_wf
by (standard, (simp add: HML_wf_rel.intros)+)
text ‹\newpage›
subsubsection ‹Modal Characterisation of Strong Bisimilarity›
definition HML_equivalent :: ‹'s ⇒ 's ⇒ bool›
where ‹HML_equivalent p q
≡ (∀ φ::('a, 's) HML_formula. (p ⊨ φ) ⟷ (q ⊨ φ))›
lemma distinguishing_formula:
assumes ‹¬ HML_equivalent p q›
shows ‹∃ φ. p ⊨ φ ∧ ¬ q ⊨ φ›
proof -
from assms obtain φ where ‹p ⊨ φ ∧ ¬ q ⊨ φ ∨ q ⊨ φ ∧ ¬ p ⊨ φ›
using HML_equivalent_def assms by blast
thus ?thesis proof (elim disjE, auto)
assume ‹q ⊨ φ› and ‹¬ p ⊨ φ›
from ‹q ⊨ φ› have ‹¬ q ⊨ HML_neg φ› by simp
moreover from ‹¬ p ⊨ φ› have ‹p ⊨ HML_neg φ› by simp
ultimately show ‹∃ φ. p ⊨ φ ∧ ¬ q ⊨ φ› by blast
qed
qed
lemma HML_equivalent_symm:
assumes ‹HML_equivalent p q›
shows ‹HML_equivalent q p›
using HML_equivalent_def assms by presburger
lemma strong_bisimilarity_implies_HML_equivalent:
assumes ‹p ↔ q› ‹p ⊨ φ›
shows ‹q ⊨ φ›
using assms
proof (induct φ arbitrary: p q)
case HML_true
then show ?case
by force
next
case (HML_conj X F)
then show ?case
by force
next
case (HML_neg φ)
then show ?case
using satisfies.simps(3) strongly_bisimilar_symm
by meson
next
case (HML_poss α φ)
then show ?case
using satisfies.simps(4) strongly_bisimilar_step(1)
by meson
qed
text ‹\newpage›
lemma HML_equivalence_is_SB:
shows ‹SB HML_equivalent›
proof -
{
fix p q p' α
assume ‹HML_equivalent p q› ‹p ⟼α p'›
assume ‹∀ q' ∈ Der(q, α). ¬ HML_equivalent p' q'›
hence "exists_φ⇘q'⇙": ‹∀q' ∈ Der(q, α). ∃φ. p' ⊨ φ ∧ ¬ q' ⊨ φ›
using distinguishing_formula by blast
let ?I = ‹Der(q, α)›
let ?F = ‹(λ q'. SOME φ. p' ⊨ φ ∧ ¬ q' ⊨ φ)›
let ?φ = ‹HML_conj ?I ?F›
from "exists_φ⇘q'⇙" have ‹p' ⊨ ?φ›
by (smt (z3) satisfies.simps(2) someI_ex)
hence ‹p ⊨ HML_poss α ?φ› using ‹p ⟼α p'› by auto
from "exists_φ⇘q'⇙" have ‹∀q' ∈ Der(q, α). ¬ q' ⊨ ?φ›
by (smt (z3) satisfies.simps(2) someI_ex)
hence ‹¬ q ⊨ HML_poss α ?φ› by simp
from ‹p ⊨ HML_poss α ?φ› ‹¬ q ⊨ HML_poss α ?φ› have False
using ‹HML_equivalent p q› HML_equivalent_def by blast
}
thus ‹SB HML_equivalent› unfolding SB_def
using HML_equivalent_symm by blast
qed
theorem modal_characterisation_of_strong_bisimilarity:
shows ‹p ↔ q ⟺ (∀ φ. p ⊨ φ ⟷ q ⊨ φ)›
proof
show ‹p ↔ q ⟹ ∀φ. (p ⊨ φ) = (q ⊨ φ)›
using strong_bisimilarity_implies_HML_equivalent
strongly_bisimilar_symm
by blast
next
show ‹∀φ. (p ⊨ φ) = (q ⊨ φ) ⟹ p ↔ q›
using HML_equivalence_is_SB HML_equivalent_def
strongly_bisimilar_def
by blast
qed
end
end