Hennessy-Milner Logic (HML)

Hennessy-Milner Logic (HML) is a logic for reasoning about the behaviour of nondeterministic and concurrent systems.

Implementation notes

There are two main versions of HML. The original [Hennessy1985], which includes a negation connective, and a variation without negation, for example as in [Aceto1999]. We follow the former and focus on a minimal set of connectives, recovering the others as derived constructs.

Main definitions

• Proposition: the language of propositions.
• Satisfies lts s a: in the LTS lts, the state s satisfies the proposition a.
• denotation a: the denotation of a proposition a, defined as the set of states that satisfy a.
• theory lts s: the set of all propositions satisfied by state s in the LTS lts.

Main statements

• satisfies_mem_denotation: the denotational semantics of HML is correct, in the sense that it coincides with the notion of satisfiability.
• not_theoryEq_satisfies: if two states have different theories, then there exists a distinguishing proposition that one state satisfies and the other does not.
• theoryEq_eq_bisimilarity: two states have the same theory iff they are bisimilar (see Bisimilarity).

References

• [M. Hennessy, R. Milner, Algebraic Laws for Nondeterminism and Concurrency][Hennessy1985]
• [L. Aceto, A. Ingólfsdóttir, Testing Hennessy-Milner Logic with Recursion][Aceto1999]

@[reducible, inline]

abbrev Cslib.Logic.Modal.HML.Proposition (Label : Type u_1) (Atom : Type u_2) : Type (max (max u_2 u_1) 0)

Propositions.

Equations

• Cslib.Logic.Modal.HML.Proposition Label Atom = Cslib.Logic.Modal.Proposition (PFunctor.mkUnary Label) Atom

structure Cslib.Logic.Modal.HML.Model (State : Type u_1) (Label : Type u_2) (Atom : Sort u_3) : Sort (max (max (u_1 + 1) (u_2 + 1)) u_3)

An HML model consists of an LTS and a valuation for its states.

• lts : LTS State Label

  The labelled transition system.

• v : State → Atom → Prop

  Valuation of atoms at states.

def Cslib.Logic.Modal.HML.Model.toModal {State : Type u_1} {Label : Type u_2} {Atom : Type u_3} (m : Model State Label Atom) : Modal.Model State (PFunctor.mkUnary Label) Atom

Converts an HML into a unary modal model.

Equations

• m.toModal = { toFrame := m.lts.toFrame, v := m.v }

@[simp]

theorem Cslib.Logic.Modal.HML.Model.toModal_toFrame {State : Type u_1} {Label : Type u_2} {Atom : Type u_3} (m : Model State Label Atom) : m.toModal.toFrame = m.lts.toFrame

def Cslib.Logic.Modal.HML.«termHML[_,_⊨_]» : Lean.ParserDescr

Shortcut for Modal[HML.Model.toModal m,s ⊨ φ].

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.Logic.Modal.Satisfies.hml_atom_iff {State : Type u_3} {Label : Type u_2} {Atom : Type u_1} {m : HML.Model State Label Atom} {s : State} {p : Atom} : ⇓{ m := m.toModal, w := s, φ := Proposition.atom p } ↔ m.v s p

theorem Cslib.Logic.Modal.Satisfies.hml_dynDiamond_iff_exists {State : Type u_3} {Label : Type u_1} {Atom : Type u_2} {m : HML.Model State Label Atom} {s : State} {μ : (PFunctor.mkUnary Label).A} {φ : Proposition (PFunctor.mkUnary Label) Atom} : ⇓{ m := m.toModal, w := s, φ := HasDynamicDiamond.dynDiamond μ φ } ↔ ∃ (s' : State), m.lts.Tr s μ s' ∧ ⇓{ m := m.toModal, w := s', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.hml_dynBox_iff_forall {State : Type u_3} {Label : Type u_1} {Atom : Type u_2} {m : HML.Model State Label Atom} {s : State} {μ : (PFunctor.mkUnary Label).A} {φ : Proposition (PFunctor.mkUnary Label) Atom} : ⇓{ m := m.toModal, w := s, φ := HasDynamicBox.dynBox μ φ } ↔ ∀ (s' : State), m.lts.Tr s μ s' → ⇓{ m := m.toModal, w := s', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.hml_dynDiamond_intro {State : Type u_3} {Label : Type u_2} {Atom : Type u_1} {m : HML.Model State Label Atom} {s : State} {μ : Label} {s' : State} {φ : Proposition (PFunctor.mkUnary Label) Atom} (htr : m.lts.Tr s μ s') (h : ⇓{ m := m.toModal, w := s', φ := φ }) : ⇓{ m := m.toModal, w := s, φ := HasDynamicDiamond.dynDiamond μ φ }

theorem Cslib.Logic.Modal.Satisfies.hml_dynBox_elim {State : Type u_3} {Label : Type u_1} {Atom : Type u_2} {m : HML.Model State Label Atom} {s : State} {μ : (PFunctor.mkUnary Label).A} {φ : Proposition (PFunctor.mkUnary Label) Atom} {s' : State} (hbox : ⇓{ m := m.toModal, w := s, φ := HasDynamicBox.dynBox μ φ }) (htr : m.lts.Tr s μ s') : ⇓{ m := m.toModal, w := s', φ := φ }

noncomputable def Cslib.Logic.Modal.propositions {State : Type u_1} {Label : Type u_2} {Atom : Type u_3} {s : State} {μ : Label} {m : HML.Model State Label Atom} (stateMap : ↑(m.lts.image s μ) → HML.Proposition Label Atom) [finImage : Fintype ↑(m.lts.image s μ)] : List (HML.Proposition Label Atom)

The list of propositions over finite μ-derivatives.

Equations

• Cslib.Logic.Modal.propositions stateMap = List.map stateMap Fintype.elems.toList

theorem Cslib.Logic.Modal.propositions_complete {State : Type u_1} {Label : Type u_2} {Atom : Type u_3} {s : State} {μ : Label} {m : HML.Model State Label Atom} (stateMap : ↑(m.lts.image s μ) → HML.Proposition Label Atom) [finImage : Fintype ↑(m.lts.image s μ)] (s' : ↑(m.lts.image s μ)) : stateMap s' ∈ propositions stateMap

theorem Cslib.Logic.Modal.propositions_satisfies_conjunction {State : Type u_1} {Label : Type u_2} {Atom : Type u_3} {s : State} {μ : Label} {m : HML.Model State Label Atom} (stateMap : ↑(m.lts.image s μ) → HML.Proposition Label Atom) [finImage : Fintype ↑(m.lts.image s μ)] {s1 s1' : State} (htr : m.lts.Tr s1 μ s1') (hdist_spec : ∀ (s2' : ↑(m.lts.image s μ)), ⇓{ m := m.toModal, w := s1', φ := stateMap s2' }) : ⇓{ m := m.toModal, w := s1, φ := HasDynamicDiamond.dynDiamond μ (finiteAnd (propositions stateMap)) }

theorem Cslib.Logic.Modal.theoryEq_isBisimulation {State : Type u_1} {Label : Type u_2} {Atom : Type u_3} {m : HML.Model State Label Atom} [image_finite : ∀ (s : State) (μ : Label), Finite ↑(m.lts.image s μ)] : m.lts.IsHomBisimulation (TheoryEq m.toModal)

Theory equivalence is a bisimulation.

theorem Cslib.Logic.Modal.bisimulation_satisfies {State : Type u_2} {Label : Type u_1} {Atom : Type u_3} {m : HML.Model State Label Atom} {r : State → State → Prop} {s1 s2 : State} {hrb : m.lts.IsHomBisimulation r} (hv : ∀ {s1 s2 : State}, r s1 s2 → ∀ (p : Atom), m.v s1 p ↔ m.v s2 p) (hr : r s1 s2) (φ : HML.Proposition Label Atom) : ⇓{ m := m.toModal, w := s1, φ := φ } ↔ ⇓{ m := m.toModal, w := s2, φ := φ }

If two states are in a bisimulation, one satisfies a proposition iff the other does.

theorem Cslib.Logic.Modal.bisimulation_theoryEq {State : Type u_2} {Label : Type u_1} {Atom : Type u_3} {m : HML.Model State Label Atom} {r : State → State → Prop} {s1 s2 : State} {hrb : m.lts.IsHomBisimulation r} (hv : ∀ {s1 s2 : State}, r s1 s2 → ∀ (p : Atom), m.v s1 p ↔ m.v s2 p) (hr : r s1 s2) : TheoryEq m.toModal s1 s2

theorem Cslib.Logic.Modal.theoryEq_eq_bisimilarity {State : Type u_1} {Label : Type u_2} {Atom : Type u_3} {m : HML.Model State Label Atom} [image_finite : ∀ (s : State) (μ : Label), Finite ↑(m.lts.image s μ)] (hv : ∀ {s1 s2 : State}, m.lts.HomBisimilarity s1 s2 → ∀ (p : Atom), m.v s1 p ↔ m.v s2 p := by grind) : TheoryEq m.toModal = m.lts.HomBisimilarity

Theory equivalence and bisimilarity coincide for image-finite LTSs.