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 [HM85], which includes a negation connective, and a variation without negation, for example as in [AI99]. 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
• L. Aceto, A. Ingólfsdóttir, Testing Hennessy-Milner Logic with Recursion

inductive Cslib.Logic.HML.Proposition (Label : Type u) : Type u

Propositions.

• true {Label : Type u} : Proposition Label

  Truth.

• and {Label : Type u} (φ₁ φ₂ : Proposition Label) : Proposition Label

  Conjunction.

• not {Label : Type u} (φ : Proposition Label) : Proposition Label

  Negation.

• diamond {Label : Type u} (μ : Label) (φ : Proposition Label) : Proposition Label

  Possibility (dynamic diamond modality).

@[instance_reducible]

instance Cslib.Logic.HML.instTopProposition {Label : Type u_1} : Top (Proposition Label)

Equations

• Cslib.Logic.HML.instTopProposition = { top := Cslib.Logic.HML.Proposition.true }

@[instance_reducible]

instance Cslib.Logic.HML.instHasAndProposition {Label : Type u_1} : HasAnd (Proposition Label)

Equations

• Cslib.Logic.HML.instHasAndProposition = { and := Cslib.Logic.HML.Proposition.and }

@[instance_reducible]

instance Cslib.Logic.HML.instHasNotProposition {Label : Type u_1} : HasNot (Proposition Label)

Equations

• Cslib.Logic.HML.instHasNotProposition = { not := Cslib.Logic.HML.Proposition.not }

@[instance_reducible]

instance Cslib.Logic.HML.instHasDynamicDiamondProposition {Label : Type u_1} : HasDynamicDiamond (Proposition Label) Label

Equations

• Cslib.Logic.HML.instHasDynamicDiamondProposition = { dynDiamond := Cslib.Logic.HML.Proposition.diamond }

@[match_pattern]

def Cslib.Logic.HML.Proposition.false {Label : Type u_1} : Proposition Label

Falsity, derived from negation and truth.

Equations

• Cslib.Logic.HML.Proposition.false = Cslib.Logic.HasNot.not ⊤

@[instance_reducible]

instance Cslib.Logic.HML.instBotProposition {Label : Type u_1} : Bot (Proposition Label)

Equations

• Cslib.Logic.HML.instBotProposition = { bot := Cslib.Logic.HML.Proposition.false }

@[match_pattern]

def Cslib.Logic.HML.Proposition.or {Label : Type u_1} (φ₁ φ₂ : Proposition Label) : Proposition Label

Disjunction, derived from negation and conjunction.

Equations

• φ₁.or φ₂ = Cslib.Logic.HasNot.not (Cslib.Logic.HasAnd.and (Cslib.Logic.HasNot.not φ₁) (Cslib.Logic.HasNot.not φ₂))

@[instance_reducible]

instance Cslib.Logic.HML.instHasOrProposition {Label : Type u_1} : HasOr (Proposition Label)

Equations

• Cslib.Logic.HML.instHasOrProposition = { or := Cslib.Logic.HML.Proposition.or }

@[match_pattern]

def Cslib.Logic.HML.Proposition.imp {Label : Type u_1} (φ₁ φ₂ : Proposition Label) : Proposition Label

Implication.

Equations

• φ₁.imp φ₂ = Cslib.Logic.HasOr.or (Cslib.Logic.HasNot.not φ₁) φ₂

@[instance_reducible]

instance Cslib.Logic.HML.instHasImpProposition {Label : Type u_1} : HasImp (Proposition Label)

Equations

• Cslib.Logic.HML.instHasImpProposition = { imp := Cslib.Logic.HML.Proposition.imp }

@[match_pattern]

def Cslib.Logic.HML.Proposition.iff {Label : Type u_1} (φ₁ φ₂ : Proposition Label) : Proposition Label

Bi-implication.

Equations

• φ₁.iff φ₂ = Cslib.Logic.HasAnd.and (Cslib.Logic.HasImp.imp φ₁ φ₂) (Cslib.Logic.HasImp.imp φ₂ φ₁)

@[instance_reducible]

instance Cslib.Logic.HML.instHasIffProposition {Label : Type u_1} : HasIff (Proposition Label)

Equations

• Cslib.Logic.HML.instHasIffProposition = { iff := Cslib.Logic.HML.Proposition.iff }

@[match_pattern]

def Cslib.Logic.HML.Proposition.box {Label : Type u_1} (μ : Label) (φ : Proposition Label) : Proposition Label

Necessity (dynamic box modality), derived from dynamic diamond and negation.

Equations

• Cslib.Logic.HML.Proposition.box μ φ = Cslib.Logic.HasNot.not (Cslib.Logic.HasDynamicDiamond.dynDiamond μ (Cslib.Logic.HasNot.not φ))

@[instance_reducible]

instance Cslib.Logic.HML.instHasDynamicBoxProposition {Label : Type u_1} : HasDynamicBox (Proposition Label) Label

Equations

• Cslib.Logic.HML.instHasDynamicBoxProposition = { dynBox := Cslib.Logic.HML.Proposition.box }

theorem Cslib.Logic.HML.Proposition.top_def {Label : Type u_1} : true = ⊤

theorem Cslib.Logic.HML.Proposition.bot_def {Label : Type u_1} : false = ⊥

theorem Cslib.Logic.HML.Proposition.and_def {Label : Type u_1} (φ₁ φ₂ : Proposition Label) : φ₁.and φ₂ = HasAnd.and φ₁ φ₂

theorem Cslib.Logic.HML.Proposition.not_def {Label : Type u_1} (φ : Proposition Label) : φ.not = HasNot.not φ

theorem Cslib.Logic.HML.Proposition.diamond_def {Label : Type u_1} (μ : Label) (φ : Proposition Label) : diamond μ φ = HasDynamicDiamond.dynDiamond μ φ

theorem Cslib.Logic.HML.Proposition.or_def {Label : Type u_1} (φ₁ φ₂ : Proposition Label) : φ₁.or φ₂ = HasOr.or φ₁ φ₂

theorem Cslib.Logic.HML.Proposition.imp_def {Label : Type u_1} (φ₁ φ₂ : Proposition Label) : φ₁.imp φ₂ = HasImp.imp φ₁ φ₂

theorem Cslib.Logic.HML.Proposition.iff_def {Label : Type u_1} (φ₁ φ₂ : Proposition Label) : φ₁.iff φ₂ = HasIff.iff φ₁ φ₂

theorem Cslib.Logic.HML.Proposition.box_def {Label : Type u_1} (μ : Label) (φ : Proposition Label) : box μ φ = HasDynamicBox.dynBox μ φ

def Cslib.Logic.HML.Proposition.finiteAnd {Label : Type u_1} (φs : List (Proposition Label)) : Proposition Label

Finite conjunction of propositions.

Equations

• Cslib.Logic.HML.Proposition.finiteAnd φs = List.foldr (fun (x1 x2 : Cslib.Logic.HML.Proposition Label) => Cslib.Logic.HasAnd.and x1 x2) ⊤ φs

def Cslib.Logic.HML.Proposition.finiteOr {Label : Type u_1} (φs : List (Proposition Label)) : Proposition Label

Finite disjunction of propositions.

Equations

• Cslib.Logic.HML.Proposition.finiteOr φs = List.foldr (fun (x1 x2 : Cslib.Logic.HML.Proposition Label) => Cslib.Logic.HasOr.or x1 x2) ⊥ φs

def Cslib.Logic.HML.Satisfies {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s : State) : Proposition Label → Prop

Satisfaction relation. Satisfies lts s φ means that, in the LTS lts, the state s satisfies the proposition φ.

Equations

• Cslib.Logic.HML.Satisfies lts s Cslib.Logic.HML.Proposition.true = True
• Cslib.Logic.HML.Satisfies lts s (φ₁.and φ₂) = (Cslib.Logic.HML.Satisfies lts s φ₁ ∧ Cslib.Logic.HML.Satisfies lts s φ₂)
• Cslib.Logic.HML.Satisfies lts s φ.not = ¬Cslib.Logic.HML.Satisfies lts s φ
• Cslib.Logic.HML.Satisfies lts s (Cslib.Logic.HML.Proposition.diamond μ φ) = ∃ (s' : State), lts.Tr s μ s' ∧ Cslib.Logic.HML.Satisfies lts s' φ

structure Cslib.Logic.HML.Judgement (State : Type u_1) (Label : Type u_2) : Type (max u_1 u_2)

Judgement, representing the conclusions one reaches in HML.

• lts : LTS State Label

  LTS.

• state : State

  The state satisfying the proposition φ.

• φ : Proposition Label

  The proposition satisfied by the state s.

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

Constructs a judgement.

Equations

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

def Cslib.Logic.HML.Satisfies.Bundled {State : Type u_1} {Label : Type u_2} (j : Judgement State Label) : Prop

Satisfaction for judgements. This just refers to the unbundled Satisfies.

Equations

• Cslib.Logic.HML.Satisfies.Bundled j = Cslib.Logic.HML.Satisfies j.lts j.state j.φ

@[instance_reducible]

instance Cslib.Logic.HML.instHasInferenceSystemJudgement {State : Type u_1} {Label : Type u_2} : HasInferenceSystem (Judgement State Label)

Equations

• Cslib.Logic.HML.instHasInferenceSystemJudgement = { derivation := Cslib.Logic.HML.Satisfies.Bundled }

theorem Cslib.Logic.HML.derivation_def {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φ : Proposition Label✝} : Satisfies lts s φ = ⇓{ lts := lts, state := s, φ := φ }

theorem Cslib.Logic.HML.Satisfies.not_iff_not {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φ : Proposition Label✝} : ⇓{ lts := lts, state := s, φ := HasNot.not φ } ↔ ¬⇓{ lts := lts, state := s, φ := φ }

theorem Cslib.Logic.HML.Satisfies.top {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} : ⇓{ lts := lts, state := s, φ := ⊤ }

theorem Cslib.Logic.HML.Satisfies.bot {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} : ¬⇓{ lts := lts, state := s, φ := ⊥ }

theorem Cslib.Logic.HML.Satisfies.and_iff_and {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φ₁ φ₂ : Proposition Label✝} : ⇓{ lts := lts, state := s, φ := HasAnd.and φ₁ φ₂ } ↔ ⇓{ lts := lts, state := s, φ := φ₁ } ∧ ⇓{ lts := lts, state := s, φ := φ₂ }

theorem Cslib.Logic.HML.Satisfies.or_iff_or {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φ₁ φ₂ : Proposition Label✝} : ⇓{ lts := lts, state := s, φ := HasOr.or φ₁ φ₂ } ↔ ⇓{ lts := lts, state := s, φ := φ₁ } ∨ ⇓{ lts := lts, state := s, φ := φ₂ }

theorem Cslib.Logic.HML.Satisfies.diamond_iff_exists {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {μ : Label✝} {φ : Proposition Label✝} : ⇓{ lts := lts, state := s, φ := HasDynamicDiamond.dynDiamond μ φ } ↔ ∃ (s' : State✝), lts.Tr s μ s' ∧ ⇓{ lts := lts, state := s', φ := φ }

theorem Cslib.Logic.HML.Satisfies.imp_iff_imp {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φ₁ φ₂ : Proposition Label✝} : ⇓{ lts := lts, state := s, φ := HasImp.imp φ₁ φ₂ } ↔ ⇓{ lts := lts, state := s, φ := φ₁ } → ⇓{ lts := lts, state := s, φ := φ₂ }

Characterisation of the → connective.

Implication is defined in terms of the more primitive connectives given in Proposition. This result proves that the definition is correct.

theorem Cslib.Logic.HML.Satisfies.iff_iff_iff {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φ₁ φ₂ : Proposition Label✝} : ⇓{ lts := lts, state := s, φ := HasIff.iff φ₁ φ₂ } ↔ (⇓{ lts := lts, state := s, φ := φ₁ } ↔ ⇓{ lts := lts, state := s, φ := φ₂ })

Characterisation of the ↔ connective.

Bi-implication is defined in terms of the more primitive connectives given in Proposition. This result proves that the definition is correct.

theorem Cslib.Logic.HML.Satisfies.box_iff_forall {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {μ : Label✝} {φ : Proposition Label✝} : ⇓{ lts := lts, state := s, φ := HasDynamicBox.dynBox μ φ } ↔ ∀ (s' : State✝), lts.Tr s μ s' → ⇓{ lts := lts, state := s', φ := φ }

theorem Cslib.Logic.HML.Satisfies.finiteAnd_iff_forall {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φs : List (Proposition Label✝)} : ⇓{ lts := lts, state := s, φ := Proposition.finiteAnd φs } ↔ ∀ φ ∈ φs, ⇓{ lts := lts, state := s, φ := φ }

A state satisfies a finite conjunction iff it satisfies all conjuncts.

theorem Cslib.Logic.HML.Satisfies.finiteOr_iff_exists {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φs : List (Proposition Label✝)} : ⇓{ lts := lts, state := s, φ := Proposition.finiteOr φs } ↔ ∃ φ ∈ φs, ⇓{ lts := lts, state := s, φ := φ }

A state satisfies a finite disjunction iff it satisfies some disjunct.

def Cslib.Logic.HML.Proposition.denotation {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : Proposition Label → Set State

Denotation of a proposition.

Equations

• Cslib.Logic.HML.Proposition.denotation lts Cslib.Logic.HML.Proposition.true = Set.univ
• Cslib.Logic.HML.Proposition.denotation lts (φ₁.and φ₂) = Cslib.Logic.HML.Proposition.denotation lts φ₁ ∩ Cslib.Logic.HML.Proposition.denotation lts φ₂
• Cslib.Logic.HML.Proposition.denotation lts φ.not = (Cslib.Logic.HML.Proposition.denotation lts φ)ᶜ
• Cslib.Logic.HML.Proposition.denotation lts (Cslib.Logic.HML.Proposition.diamond μ φ) = {s : State | ∃ (s' : State), lts.Tr s μ s' ∧ s' ∈ Cslib.Logic.HML.Proposition.denotation lts φ}

@[reducible, inline]

abbrev Cslib.Logic.HML.theory {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s : State) : Set (Proposition Label)

The theory of a state is the set of all propositions that it satisfies.

Equations

• Cslib.Logic.HML.theory lts s = {φ : Cslib.Logic.HML.Proposition Label | ⇓{ lts := lts, state := s, φ := φ }}

@[reducible, inline]

abbrev Cslib.Logic.HML.TheoryEq {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s1 s2 : State) : Prop

Two states are theory-equivalent (for a specific LTS) if they have the same theory.

Equations

• Cslib.Logic.HML.TheoryEq lts s1 s2 = (Cslib.Logic.HML.theory lts s1 = Cslib.Logic.HML.theory lts s2)

theorem Cslib.Logic.HML.mem_denotation_iff_satisfies {Label : Type u_1} {State✝ : Type u_2} {lts : LTS State✝ Label} {s : State✝} {φ : Proposition Label} : s ∈ Proposition.denotation lts φ ↔ ⇓{ lts := lts, state := s, φ := φ }

Characterisation theorem for the denotational semantics.

theorem Cslib.Logic.HML.mem_theory_iff_satisfies {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {φ : Proposition Label✝} : φ ∈ theory lts s ↔ ⇓{ lts := lts, state := s, φ := φ }

theorem Cslib.Logic.HML.not_denotation {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (φ : Proposition Label) : s ∉ Proposition.denotation lts (HasNot.not φ) ↔ s ∈ Proposition.denotation lts φ

A state is in the denotation of a proposition iff it is not in the denotation of the negation of the proposition.

theorem Cslib.Logic.HML.theoryEq_denotation_eq {State : Type u_1} {Label : Type u_2} {s1 s2 : State} {lts : LTS State Label} : TheoryEq lts s1 s2 ↔ ∀ (φ : Proposition Label), s1 ∈ Proposition.denotation lts φ ↔ s2 ∈ Proposition.denotation lts φ

Two states are theory-equivalent iff they are denotationally equivalent.

theorem Cslib.Logic.HML.not_theoryEq_satisfies {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s1 s2 : State✝} (h : ¬TheoryEq lts s1 s2) : ∃ (φ : Proposition Label✝), ⇓{ lts := lts, state := s1, φ := φ } ∧ ¬⇓{ lts := lts, state := s2, φ := φ }

If two states are not theory equivalent, there exists a distinguishing proposition.

theorem Cslib.Logic.HML.theoryEq_satisfies {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s1 s2 : State✝} {φ : Proposition Label✝} (h : TheoryEq lts s1 s2) (hs : ⇓{ lts := lts, state := s1, φ := φ }) : ⇓{ lts := lts, state := s2, φ := φ }

If two states are theory equivalent and the former satisfies a proposition, the latter does as well.

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

The list of propositions over finite μ-derivatives.

Equations

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

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

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

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

Theory equivalence is a bisimulation.

theorem Cslib.Logic.HML.bisimulation_satisfies {State✝ : Type u_1} {r : State✝ → State✝ → Prop} {Label : Type u_2} {lts : LTS State✝ Label} {s1 s2 : State✝} {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) (φ : Proposition Label) : ⇓{ lts := lts, state := s1, φ := φ } ↔ ⇓{ lts := lts, state := s2, φ := φ }

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

theorem Cslib.Logic.HML.bisimulation_theoryEq {State✝ : Type u_1} {r : State✝ → State✝ → Prop} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s1 s2 : State✝} {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) : TheoryEq lts s1 s2

theorem Cslib.Logic.HML.theoryEq_eq_bisimilarity {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} [image_finite : ∀ (s : State) (μ : Label), Finite ↑(lts.image s μ)] : TheoryEq lts = lts.HomBisimilarity

Theory equivalence and bisimilarity coincide for image-finite LTSs.