locus: Blueprint

7.1. Hennessy–Milner logic over contexts🔗

Definition7.1.1
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 7.1.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsbridged

In a wide reactive system, formulas at an interface I are \varphi ::= \top \mid \neg\varphi \mid \varphi \wedge \varphi \mid \langle L, \lambda \rangle \varphi, for a context L : I \to J, a location \lambda (a set of roots of J) and \varphi at J. An agent satisfies \langle L, \lambda \rangle \varphi when a \xrightarrow{\pi \bullet L,\, \lambda} a' and a' \models \varphi for some support translation \pi of the label. Agents are logically equivalent, a \equiv_{\mathcal{L}} b, when they satisfy the same formulas.

Lean code for Definition7.1.1●3 definitions
  • inductive(4 constructors, 2 parameters)defined in Logic/HML.lean
    complete
    inductive Form.{u, v} (W : WRS) : W.Obj → Type (max u v)
    inductive Form.{u, v} (W : WRS) :
  W.Obj → Type (max u v)
    **A formula at the interface `I`**: `⊤`, negation, conjunction, and the
located modality `⟨L, λ⟩φ` for a context `L : I → J`, a location
`λ ⊆ width J` and a formula `φ` at `J`.

    Constructors

    tt.{u, v} {W : WRS} {I : W.Obj} : Form W I
    neg.{u, v} {W : WRS} {I : W.Obj} : Form W I → Form W I
    and.{u, v} {W : WRS} {I : W.Obj} :
  Form W I → Form W I → Form W I
    dia.{u, v} {W : WRS} {I J : W.Obj} (L : W.Hom I J)
  (loc : Fin (W.width J) → Prop) : Form W J → Form W I
  • defdefined in Logic/HML.lean
    complete
    def Sat.{u, v} {W : WRS} {I : W.Obj} : W.Hom W.origin I → Form W I → Prop
    def Sat.{u, v} {W : WRS} {I : W.Obj} :
  W.Hom W.origin I → Form W I → Prop
    **Satisfaction** `a ⊨ φ`.  `a ⊨ ⟨L, λ⟩φ` iff for some translation `π`,
`a —π•L▷_λ a'` and `a' ⊨ φ`.
  • defdefined in Logic/HML.lean
    complete
    def LEquiv.{u, v} {W : WRS} {I : W.Obj} (a b : W.Hom W.origin I) : Prop
    def LEquiv.{u, v} {W : WRS} {I : W.Obj}
  (a b : W.Hom W.origin I) : Prop
    **Logical equivalence**: the same formulas.
Definition7.1.2
uses 0
Used by 4
Reverse dependency previews
Preview
Theorem 7.1.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagsnew

A wide reactive system is image-finite (up to support equivalence) when for all a, L, \lambda there are finitely many agents c_1, \dots, c_n such that a \xrightarrow{L,\, \lambda} a' implies a' \bumpeq c_i for some i. It is strongly image-finite when the c_i can be taken among the successors themselves.

Lean code for Definition7.1.2●2 definitions
  • defdefined in Logic/HML.lean
    complete
    def ImageFinite.{u, v} (W : WRS) : Prop
    def ImageFinite.{u, v} (W : WRS) : Prop
    **Image-finiteness up to `≏`** (statement S1's conclusion): for each
agent, context and location, finitely many agents cover every successor
up to support equivalence.
  • defdefined in Logic/HML.lean
    complete
    def StrongImageFinite.{u, v} (W : WRS) : Prop
    def StrongImageFinite.{u, v} (W : WRS) : Prop
    **Strong image-finiteness**: the covering agents are themselves
successors.  The constructive apartness theorem asks for this form; it
follows from `ImageFinite` classically (`ImageFinite.strong`).
Theorem7.1.3
uses 1used by 1✓L∃∀N

Bisimilar agents satisfy the same formulas, in any wide reactive system:

a \sim b \;\Longrightarrow\; (a \models \varphi \iff b \models \varphi) .

Lean code for Theorem7.1.3●1 theorem
  • theoremdefined in Logic/HML.lean
    complete
    theorem sat_of_bisim.{u, v} {W : WRS} {I : W.Obj} (φ : Form W I)
  {a b : W.Hom W.origin I} : a ∼ b → (a ⊨ φ ↔ b ⊨ φ)
    theorem sat_of_bisim.{u, v} {W : WRS} {I : W.Obj}
  (φ : Form W I)
  {a b : W.Hom W.origin I} :
  a ∼ b → (a ⊨ φ ↔ b ⊨ φ)
    **Bisimilar agents are logically equivalent** (Hennessy–Milner,
soundness direction).  Constructive.
Theorem7.1.4
Statement uses 2
Statement dependency previews
Preview
Definition 7.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The Hennessy–Milner theorem, with contexts as labels. CLASSICAL. In an image-finite wide reactive system,

a \sim b \;\iff\; a \equiv_{\mathcal{L}} b .

Rests on NEW: ImageFinite.

Lean code for Theorem7.1.4●1 theorem
  • theoremdefined in Logic/HML.lean
    complete
    theorem bisim_iff_lequiv.{u, v} {W : WRS} (hfin : ImageFinite W) {I : W.Obj}
  {a b : W.Hom W.origin I} : a ∼ b ↔ a ≡ₗ b
    theorem bisim_iff_lequiv.{u, v} {W : WRS}
  (hfin : ImageFinite W) {I : W.Obj}
  {a b : W.Hom W.origin I} :
  a ∼ b ↔ a ≡ₗ b
    **The Hennessy–Milner theorem for wide bisimilarity** (statement S2):
in an image-finite wide reactive system, two agents are bisimilar iff
they satisfy the same formulas.  CLASSICAL (through `bisim_of_lequiv`).
Theorem7.1.5
uses 1used by 0✓L∃∀N

A BRS over pure hard bigraphs whose parametric rules \mathcal{R} all lie in one finite list is image-finite. CLASSICAL. For all a, L, \lambda,

\exists c_1, \dots, c_n.\;\; \forall a'.\;\; a \xrightarrow{L,\, \lambda} a' \;\Longrightarrow\; \exists i.\; a' \bumpeq c_i .

Rests on NEW: ImageFinite.

Lean code for Theorem7.1.5●1 theorem
  • theoremdefined in Logic/ImageFinite.lean
    complete
    theorem brs_imageFinite {Ctrl : Type} {S : Bigraph.Sig Ctrl}
  {rules : PRule S → Prop}
  (hR : ∃ rl, ∀ (ρ : PRule S), rules ρ → ρ ∈ rl) :
  ImageFinite (BRS rules)
    theorem brs_imageFinite {Ctrl : Type}
  {S : Bigraph.Sig Ctrl}
  {rules : PRule S → Prop}
  (hR :
    ∃ rl,
      ∀ (ρ : PRule S), rules ρ → ρ ∈ rl) :
  ImageFinite (BRS rules)
    **Statement S1** (CLASSICAL): a BRS over ´BIG_h with finitely many
parametric rules is image-finite up to support equivalence.
Theorem7.1.6
Statement uses 2
Statement dependency previews
Preview
Definition 7.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

The constructive form (after Geuvers and Jacobs 2021). Apartness a \mathrel{\#} b is the least symmetric relation holding whenever a has a transition under a translate of some L at \lambda to an a' apart from every result of b under a translate of L at \lambda; \mathrm{Pos}\,a\,\varphi and \mathrm{Neg}\,a\,\varphi say, by explicit evidence, that a verifies, respectively refutes, \varphi. In a strongly image-finite wide reactive system,

a \mathrel{\#} b \;\iff\; \exists \varphi.\;\; \mathrm{Pos}\,a\,\varphi \;\wedge\; \mathrm{Neg}\,b\,\varphi .

Rests on NEW: StrongImageFinite.

Lean code for Theorem7.1.6●4 declarations
  • inductive(2 constructors, Prop, 4 parameters)defined in Logic/HML.lean
    complete
    inductive Apart.{u, v} (W : WRS) {I : W.Obj} :
  W.Hom W.origin I → W.Hom W.origin I → Prop
    inductive Apart.{u, v} (W : WRS) {I : W.Obj} :
  W.Hom W.origin I →
    W.Hom W.origin I → Prop
    **Apartness** `a # b` (Geuvers–Jacobs): the least symmetric relation
such that `a # b` whenever `a` has a transition `a —π•L▷_λ a'` and
every transition `b —ρ•L▷_λ b'` lands apart from `a'`.

    Constructors

    step.{u, v} {W : WRS} {I J : W.Obj} {a b : W.Hom W.origin I}
  (L : W.Hom I J) (loc : Fin (W.width J) → Prop) (π : Perm)
  (a' : W.Hom W.origin J) (htr : a ─[W.tr π L, loc]→ a')
  (hall :
    ∀ (ρ : Perm) (b' : W.Hom W.origin J),
      b ─[W.tr ρ L, loc]→ b' → Apart W a' b') :
  Apart W a b
    symm.{u, v} {W : WRS} {I : W.Obj} {a b : W.Hom W.origin I} :
  Apart W a b → Apart W b a
  • abbrevdefined in Logic/HML.lean
    complete
    abbrev Pos.{u, v} {W : WRS} {I : W.Obj} (a : W.Hom W.origin I) (φ : Form W I) :
  Prop
    abbrev Pos.{u, v} {W : WRS} {I : W.Obj}
  (a : W.Hom W.origin I) (φ : Form W I) :
  Prop
    `a` verifies `φ`.
  • abbrevdefined in Logic/HML.lean
    complete
    abbrev Neg.{u, v} {W : WRS} {I : W.Obj} (a : W.Hom W.origin I) (φ : Form W I) :
  Prop
    abbrev Neg.{u, v} {W : WRS} {I : W.Obj}
  (a : W.Hom W.origin I) (φ : Form W I) :
  Prop
    `a` refutes `φ`.
  • theoremdefined in Logic/HML.lean
    complete
    theorem apart_iff_distinguish.{u, v} {W : WRS} (hfin : StrongImageFinite W)
  {I : W.Obj} {a b : W.Hom W.origin I} :
  Apart W a b ↔ ∃ φ, Pos a φ ∧ Bigraph.Logic.Neg b φ
    theorem apart_iff_distinguish.{u, v} {W : WRS}
  (hfin : StrongImageFinite W) {I : W.Obj}
  {a b : W.Hom W.origin I} :
  Apart W a b ↔
    ∃ φ, Pos a φ ∧ Bigraph.Logic.Neg b φ
    **The apartness form of the Hennessy–Milner theorem** (statement S2,
constructive): under strong image-finiteness, two agents are apart iff
some formula is verified by one and refuted by the other.
Theorem7.1.7
uses 0used by 0✓L∃∀N

Finitely many rules do not give finitely many labels. REFUTED, over the signature with one atomic control k of arity 0, is the statement that for every finite list of rules and every agent a there are labels M_1, \dots, M_n with

a \xrightarrow{L,\, \lambda} a' \;\Longrightarrow\; \exists j,\, \pi,\, \iota.\;\; L = \iota \circ (\pi \bullet M_j), \quad \iota \text{ an elementary iso} .

The countermodel is the rule k \mid \square_0 \to k, the agent k and the labels \square \mid k^{n+1}. The phenomenon is known (Di Gianantonio, Honsell and Lenisa, RPO, second-order contexts, and λ-calculus, 2009; Klin, Sassone and Sobociński, Labels from reductions, 2005).

Rests on NEW: Perm; not audited: BigH.tr, LFinCounter.C, LFinCounter.sig.

Lean code for Theorem7.1.7●2 declarations
  • defdefined in Logic/Mu.lean
    complete
    def LFinStatement {Ctrl : Type} (S : Bigraph.Sig Ctrl) : Prop
    def LFinStatement {Ctrl : Type}
  (S : Bigraph.Sig Ctrl) : Prop
    **L-fin** (REFUTED: `LFinCounter.lfin_refuted`; restated for parameter-free rules as `LFin0Statement`): for a BRS whose rules lie in a finite list, each agent
has a finite list of labels covering all its IPO labels, up to a
support translation and an elementary iso of the outer face.
  • theoremdefined in Logic/LFinCounter.lean
    complete
    theorem lfin_refuted : ¬LFinStatement LFinCounter.sig
    theorem lfin_refuted :
  ¬LFinStatement LFinCounter.sig
    **L-fin is REFUTED.**