Theory HM_Logic

(*<*)
theory HM_Logic
  imports 
    Strong_Bisimilarity
    "HOL-Library.Countable_Set_Type"
begin
(*>*)

section ‹Hennessy-Milner Logic›
text ‹\label{sec:HML}›

text ‹In their seminal paper @{cite hm85}, Matthew Hennessy and Robin Milner present a modal-logical characterisation of strong bisimilarity (although they do not call it that), by process properties: \enquote{two processes are equivalent if and only if they enjoy the same set of properties.} These properties are expressed as terms of a modal-logical language, consisting merely of (finite) conjunction, negation, and a family of modal possibility operators. This language is known today as Hennessy-Milner logic (HML), with formulas $\varphi$ defined by the following grammar (where $\alpha$ ranges over the set of actions $\Act$):
$$\varphi ::= t\!t \mid \varphi_1 \;\wedge\; \varphi_2 \mid \neg\varphi \mid \langle\alpha\rangle\varphi$$

The semantics (on LTS processes) is given as follows: all processes satisfy $t\!t$, $\varphi_1 \;\wedge\; \varphi_2$ is satisfied if both $\varphi_1$ and $\varphi_2$ are satisfied, $\neg\varphi$ is satisfied if $\varphi$ is not satisfied, and $\langle\alpha\rangle\varphi$ is satisfied by a process if it is possible to perform an $\alpha$-transition into a process that satisfies $\varphi$.

@{cite hm85} also contains the proof that this modal-logical characterisation of strong bisimilarity coincides with a characterisation that is effectively the same as the one we saw in \cref{sec:strong_bisimilarity} using strong bisimulations. Although they use different terminology, their result can be summarised as follows: for image-finite LTSs, two processes are strongly bisimilar iff they satisfy the same set of HML formulas. We call this the \emph{modal characterisation} of strong bisimilarity.

Let the \emph{cardinality of conjunction} be the maximally allowed cardinality of sets of (sub-)formulas conjoined within a formula (for a given variant of HML). For the simple variant above, conjunction has finite cardinality. By allowing for conjunction of arbitrary cardinality (infinitary HML), the modal characterisation of strong bisimilarity can be proved for arbitrary LTSs. This is done in \cref{chap:HML_infinitary}.

In this section, however, conjunction is constrained to be of countable cardinality, as this turned out to be significantly easier to deal with in the upcoming proofs. The modal characterisation of strong bisimilarity, then, works for LTSs that are image-countable, as we shall see below.

Formulas $\varphi$ are given by the following grammar, where $I$ ranges over all subsets of the natural numbers:
$$\varphi ::= \bigwedge_{i \in I} \varphi_i \mid \neg\varphi \mid \langle\alpha\rangle\varphi$$

The semantics of HML formulas on LTSs are as above, with the alteration that a process satisfies $\bigwedge_{i \in I} \varphi_i$ iff it satisfies $\varphi_i$ for all $i \in I$.

Additional logical constants can be added as \enquote{syntactic sugar}:
\begin{align*}
    t\!t &\equiv \textstyle\bigwedge_{i \in \emptyset} \varphi_i \\
    f\!\!f &\equiv \neg t\!t \\
    \bigvee_{i \in I} \varphi_i &\equiv \neg \bigwedge_{i \in I} \neg\varphi_i
\end{align*}›


subsection ‹Isabelle›

subsubsection ‹Syntax›

text ‹By definition of countability, all countable sets of formulas can be given by $\{\varphi_i\}_{i \in I} =: \Phi$ for some $I \subseteq \mathbb{N}$ (then $\bigwedge_{i \in I} \varphi_i$ shall correspond to $\bigwedge \Phi$). Therefore, the following data type (parameterised by the type of actions ‹'a›) formalises the definition of HML formulas above (‹cset› is the type constructor for countable sets; ‹acset› and ‹rcset› are the type morphisms between the types ‹set› and ‹cset›; more details below).

I abstained from assigning the constructors a more readable symbolic notation because of the ambiguities and name clashes that would ensue in upcoming sections. The symbolic notations after the constructors below are just code comments.
\pagebreak›

datatype ('a)HML_formula =
  HML_conj  ‹('a)HML_formula cset› ― ‹$\bigwedge \Phi$› 
| HML_neg   ‹('a)HML_formula› ― ‹$\neg\varphi$› 
| HML_poss  ‹'a› ‹('a)HML_formula› ― ‹$\langle\alpha\rangle\varphi$›

text ‹The following abbreviations introduce useful constants as syntactic sugar (where ‹cimage HML_neg Φ› corresponds to $\{ \neg\varphi \mid \varphi\in\Phi \}$).›

abbreviation HML_true :: ‹('a)HML_formula› ― ‹$t\!t$›
  where ‹HML_true ≡ HML_conj (acset ∅)›
abbreviation HML_false :: ‹('a)HML_formula› ― ‹$f\!\!f$›
  where ‹HML_false ≡ HML_neg HML_true›
abbreviation HML_disj :: ‹('a)HML_formula cset ⇒ ('a)HML_formula› ― ‹$\bigvee \Phi$›
  where ‹HML_disj Φ ≡ HML_neg (HML_conj (cimage HML_neg Φ))›


subsubsection ‹Aside: The Type of Countable Sets›

text ‹Since sets ‹set› and countable sets ‹cset› are different types in Isabelle, they have different membership relation terms. We introduce the following notation for membership of countable sets.›

notation cin (‹_ ∈⇩c _› [100, 100] 100)

text ‹The following propositions should clarify how the type constructor ‹cset› and its morphisms are used. Note how the first proposition requires the assumption ‹countable X›, whereas the second one does not. ›

proposition 
  fixes X::‹'x set›
  assumes ‹countable X›
  shows ‹x ∈ X  ⟺  x ∈⇩c acset X› 
  using assms by (simp add: cin.rep_eq)
proposition
  fixes X::‹'x cset›
  shows ‹x ∈⇩c X  ⟺  x ∈ rcset X› 
  by (simp add: cin.rep_eq)


subsubsection ‹Semantics›

text ‹The semantic satisfaction relation is formalised by the following function. Since the relation is not monotonic (due to negation terms), it cannot be directly defined in Isabelle as an inductive predicate, so we use the ‹function› command instead. This, then, requires us to prove that the function is well-defined (i.e.\@ the function definition completely and compatibly covers all constructors of our data type) and total (i.e.\@ it always terminates). It is easy to see that the former is the case for the function below.
\pagebreak›

context lts begin

function HML_sat :: ‹'s ⇒ ('a)HML_formula ⇒ bool›
  (‹_ ⊨ _› [50, 50] 50)
  where
    HML_sat_conj: ‹(p ⊨ HML_conj Φ) = (∀ φ. φ ∈⇩c Φ ⟶ p ⊨ φ)› 
  | HML_sat_neg:  ‹(p ⊨ HML_neg φ) = (¬ p ⊨ φ)› 
  | HML_sat_poss: ‹(p ⊨ HML_poss α φ) = (∃ p'. p ⟼α p' ∧ p' ⊨ φ)›
  using HML_formula.exhaust by (auto, blast)

text ‹In order to prove that the function always terminates, we need to show that each sequence of recursive invocations reaches a base case%
\footnote{For our satisfaction function, the recursive base case is, of course, the empty conjunction, since
$\forall\varphi.\; \varphi \in \emptyset \longrightarrow p \vDash \varphi$
is a tautology.}
after finitely many steps. We do this by proving that the relation between process-formula pairs given by the recursive definition of the function is (contained within) a well-founded relation.
A relation $R \subseteq X \times X$ is called well-founded if each non-empty subset $X' \subseteq X$ has a minimal element $m$ that is not \enquote{$R$-greater} than any element of $X'$, i.e.\@ $\forall x \in X'.\; (x,m) \notin R$.
A property of well-founded relations is that all descending chains $(x_0, x_1, x_2, \dots)$ (with $(x_i, x_{i+1}) \in R$) starting at any element $x_0 \in X$ are finite. This, then, implies that each sequence of recursive invocations terminates after finitely many steps.

These proofs were inspired by the Isabelle formalisations done in @{cite weber2021modal}.›

inductive_set HML_wf_rel :: ‹('s × ('a)HML_formula) rel› 
  where
    ‹φ ∈⇩c Φ ⟹ ((p, φ), (p, HML_conj Φ)) ∈ 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)HML_formula ⇒ bool› and t::‹'s × ('a)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 (smt (verit, ccfv_SIG) HML_formula.distinct(1) HML_formula.distinct(3) HML_formula.inject(1) HML_wf_rel_def case_prodE' cin.rep_eq HML_wf_rel.cases mem_Collect_eq split_conv)
    apply (metis HML_formula.distinct(1) HML_formula.distinct(5) HML_formula.inject(2) HML_wf_rel.cases surj_pair)
    apply (smt (verit, del_insts) HML_formula.distinct(3) HML_formula.distinct(5) HML_formula.inject(3) HML_wf_rel.cases case_prodD case_prodE' HML_wf_rel_def mem_Collect_eq)
    done
  thus ‹P t› using ‹t = (p, φ)› by simp
qed

termination✐‹tag (proof) visible› HML_sat using HML_wf_rel_is_wf 
  by (standard, (simp add: HML_wf_rel.intros)+)


text ‹The semantic clauses for our additional constants are now easily derivable.›

lemma HML_sat_true:
  shows ‹(p ⊨ HML_true) = True›
  using bot_cset.abs_eq by auto
lemma HML_sat_false:
  shows ‹(p ⊨ HML_false) = False›
  using HML_sat_true by auto
lemma HML_sat_disj:
  shows ‹(p ⊨ HML_disj Φ) = (∃ φ. φ ∈⇩c Φ ∧ p ⊨ φ)›
  by auto


subsubsection ‹Modal Characterisation of Strong Bisimilarity›

text ‹First, we introduce HML-equivalence as follows.›

definition HML_equivalent :: ‹'s ⇒ 's ⇒ bool›
  where ‹HML_equivalent p q ≡ (∀ φ. (p ⊨ φ) ⟷ (q ⊨ φ))›

text ‹Since formulas are closed under negation, the following lemma holds.›

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

text ‹HML-equivalence is clearly symmetrical.›

lemma HML_equivalent_symm:
  assumes ‹HML_equivalent p q›
  shows ‹HML_equivalent q p›
  using HML_equivalent_def assms by presburger

text ‹We can now formally prove the modal characterisation of strong bisimilarity, i.e.: two processes are HML-equivalent iff they are strongly bisimilar. The proof is borrowed from @{cite ‹theorem 5.1› reactivesystems}. 

I chose to include these proofs in the thesis document, because they translate quite beautifully, in my opinion, and are comparatively short.

We show the $\Longrightarrow$-case first, by induction over ‹φ›.›

lemma✐‹tag (proof) visible› strong_bisimilarity_implies_HM_equivalence:
  assumes ‹p ↔ q› ‹p ⊨ φ›
  shows ‹q ⊨ φ›
  using assms
proof (induct φ arbitrary: p q)
  case (HML_conj Φ)
  then show ?case 
    using HML_sat_conj by (meson cin.rep_eq)
next
  case (HML_neg φ)
  then show ?case
    using HML_sat_neg strongly_bisimilar_symm by meson
next
  case (HML_poss α φ)
  then show ?case
    using HML_sat_poss strongly_bisimilar_step(1) by meson
qed

text ‹\pagebreak
Before we can show the $\Longleftarrow$-case, we need to prove the following lemma: for some binary predicate $P$, if for every element $a$ of a set $A$, there exists an element $x$ such that $P(a,x)$ is true, then we can obtain a set $X$ that contains these $x$ (for all $a \in A$) and has the same cardinality as $A$. 

Since more than one $x$ might exist for each $a$ such that $P(a,x)$ is true, the set
$\{ x \mid a \in A \wedge P(a,x) \}$
might have greater cardinality than $A$. In order to obtain a set $X$ of same cardinality as A, we need to invoke the axiom of choice in our proof.›

lemma✐‹tag (proof) visible› obtaining_set:
  assumes 
    ‹∀ a ∈ A. ∃ x. P a x› 
    ‹countable A›
  obtains X where 
    ‹∀ a ∈ A. ∃ x ∈ X. P a x› 
    ‹∀ x ∈ X. ∃ a ∈ A. P a x› 
    ‹countable X›
proof
  ― ‹the ‹SOME› operator (Hilbert's selection operator $\varepsilon$) invokes the axiom of choice›
  define xm where ‹xm ≡ λ a. SOME x. P a x›
  define X where ‹X ≡ {xm a | a. a ∈ A}›

  show ‹∀a∈A. ∃x∈X. P a x›
    using X_def xm_def assms(1) by✐‹tag proof› (metis (mono_tags, lifting) mem_Collect_eq someI)
  show ‹∀x ∈ X. ∃a∈A. P a x›
    using X_def xm_def assms(1) by✐‹tag proof› (smt (verit, best) mem_Collect_eq someI_ex)
  show ‹countable X› 
    using X_def xm_def assms(2) by✐‹tag proof› (simp add: Setcompr_eq_image)
qed

text ‹We can now show, assuming image-countability of the given LTS, that HML-equivalence is a strong bisimulation. The proof utilises classical contradiction: 
if HML-equivalence were no strong bisimulation, there would be some processes $p$ and $q$ that are HML-equivalent, with $p \xrightarrow{\alpha} p'$ for some $p'$ (i.e.\@ $p' \in \text{Der}(p, \alpha)$), but for all $q' \in \text{Der}(q, \alpha)$, $p'$ and $q'$ are not HML-equivalent. 
Then, for each $q' \in \text{Der}(q, \alpha)$, there would be a distinguishing formula $\varphi_{q'}$ which $p'$ satisfies but $q'$ does not. 
Using our ‹obtaining_set› lemma, we can obtain the set 
$\Phi = \{ \varphi_{q'} \}_{q' \in \text{Der}(q, \alpha)}$, which is countable, since $\text{Der}(q, \alpha)$ is countable, by the image-countability assumption.
Since we allow for conjunction of countable cardinality, $\bigwedge \Phi$ is a valid formula. 
By construction, $p$ can make an $\alpha$-transition into a state that satisfies $\bigwedge \Phi$ 
(i.e.\@ $p \vDash \langle\alpha\rangle \bigwedge \Phi$), whereas q cannot 
(i.e.\@ $q \not\vDash \langle\alpha\rangle \bigwedge \Phi$).
This is a contradiction, since, by assumption, $p$ and $q$ are HML-equivalent. 
Therefore, HML-equivalence must be a strong bisimulation.
\pagebreak›

lemma✐‹tag (proof) visible› HML_equivalence_is_SB:
  assumes
    ‹image_countable›
  shows
    ‹SB HML_equivalent›
proof -
  {
    fix p q p' α
    assume ‹HML_equivalent p q› 
    assume ‹p ⟼α p'›
    assume ‹∀q' ∈ Der(q, α). ¬ HML_equivalent p' q'›
    
    hence "exists_φ⇘q'⇙": ‹∀q' ∈ Der(q, α). ∃φ. p' ⊨ φ ∧ ¬ q' ⊨ φ›
      using distinguishing_formula by blast

    from ‹image_countable› have ‹countable Der(q, α)› 
      using image_countable_def by simp

    from obtaining_set[
          where ?A = ‹Der(q, α)›
            and ?P = ‹λ q' φ. p' ⊨ φ ∧ ¬ q' ⊨ φ›, 
          OF "exists_φ⇘q'⇙" ‹countable Der(q, α)›]
    obtain Φ where *:
      ‹∀φ ∈ Φ. ∃q' ∈ Der(q, α). p' ⊨ φ ∧ ¬ q' ⊨ φ› 
      ‹∀q' ∈ Der(q, α). ∃φ ∈ Φ. p' ⊨ φ ∧ ¬ q' ⊨ φ› 
      ‹countable Φ›
      by (this, blast+)
  
    have ‹p ⊨ HML_poss α (HML_conj (acset Φ))›
      using ‹p ⟼α p'› *(1,3) HML_sat.simps(1,3)
        acset_inverse mem_Collect_eq cin.rep_eq
      by metis

    moreover have ‹¬ q ⊨ HML_poss α (HML_conj (acset Φ))›
      using *(2,3) cin.rep_eq 
      by fastforce

    ultimately have False 
      using ‹HML_equivalent p q› 
      unfolding HML_equivalent_def
      by meson
  }

  ― ‹We showed the case for ‹p ⟼α p'›, but not ‹q ⟼α q'›.›
  ― ‹Clearly, this case is covered by the symmetry of HML-equivalence.›
  from this show ‹SB HML_equivalent› unfolding SB_def 
    using HML_equivalent_symm by blast
qed

text ‹\pagebreak
We can now conclude the modal characterisation of strong bisimilarity.›
  
theorem✐‹tag (proof) visible› modal_characterisation_of_strong_bisimilarity: 
  assumes ‹image_countable›
  shows ‹(p ↔ q)  ⟺  (∀ φ. p ⊨ φ ⟷ q ⊨ φ)›
proof
  show ‹(p ↔ q) ⟹ ∀φ. (p ⊨ φ) = (q ⊨ φ)›
    using strong_bisimilarity_implies_HM_equivalence 
      strongly_bisimilar_symm 
    by blast
next
  show ‹∀φ. (p ⊨ φ) = (q ⊨ φ) ⟹ (p ↔ q)› 
    using HML_equivalence_is_SB[OF assms] 
      HML_equivalent_def strongly_bisimilar_def 
    by blast
qed

end ― ‹of context lts›
(*<*)
end ― ‹of theory›
(*>*)