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 latter, which is used in many recent papers. Negation is recovered as usual, by having a false atomic proposition and a function that, given any proposition, returns its negated form (see Proposition.neg).

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]

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

Propositions.

• true {Label : Type u} : Proposition Label
• false {Label : Type u} : Proposition Label
• and {Label : Type u} (φ₁ φ₂ : Proposition Label) : Proposition Label
• or {Label : Type u} (φ₁ φ₂ : Proposition Label) : Proposition Label
• diamond {Label : Type u} (μ : Label) (φ : Proposition Label) : Proposition Label
• box {Label : Type u} (μ : Label) (φ : Proposition Label) : Proposition Label

def Cslib.Logic.HML.Proposition.neg {Label : Type u_1} (a : Proposition Label) : Proposition Label

Negation of a proposition.

Equations

• Cslib.Logic.HML.Proposition.true.neg = Cslib.Logic.HML.Proposition.false
• Cslib.Logic.HML.Proposition.false.neg = Cslib.Logic.HML.Proposition.true
• (a_2.and b).neg = a_2.neg.or b.neg
• (a_2.or b).neg = a_2.neg.and b.neg
• (Cslib.Logic.HML.Proposition.diamond μ a_2).neg = Cslib.Logic.HML.Proposition.box μ a_2.neg
• (Cslib.Logic.HML.Proposition.box μ a_2).neg = Cslib.Logic.HML.Proposition.diamond μ a_2.neg

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

Finite conjunction of propositions.

Equations

• Cslib.Logic.HML.Proposition.finiteAnd as = List.foldr Cslib.Logic.HML.Proposition.and Cslib.Logic.HML.Proposition.true as

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

Finite disjunction of propositions.

Equations

• Cslib.Logic.HML.Proposition.finiteOr as = List.foldr Cslib.Logic.HML.Proposition.or Cslib.Logic.HML.Proposition.false as

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

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

• true {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} : Satisfies lts s Proposition.true
• and {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {a b : Proposition Label} : Satisfies lts s a → Satisfies lts s b → Satisfies lts s (a.and b)
• or₁ {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {a b : Proposition Label} : Satisfies lts s a → Satisfies lts s (a.or b)
• or₂ {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {a b : Proposition Label} : Satisfies lts s b → Satisfies lts s (a.or b)
• diamond {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s s' : State} {μ : Label} {a : Proposition Label} (htr : lts.Tr s μ s') (hs : Satisfies lts s' a) : Satisfies lts s (Proposition.diamond μ a)
• box {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {μ : Label} {a : Proposition Label} (h : ∀ (s' : State), lts.Tr s μ s' → Satisfies lts s' a) : Satisfies lts s (Proposition.box μ a)

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

Denotation of a proposition.

Equations

• Cslib.Logic.HML.Proposition.true.denotation lts = Set.univ
• Cslib.Logic.HML.Proposition.false.denotation lts = ∅
• (a_2.and b).denotation lts = a_2.denotation lts ∩ b.denotation lts
• (a_2.or b).denotation lts = a_2.denotation lts ∪ b.denotation lts
• (Cslib.Logic.HML.Proposition.diamond μ a_2).denotation lts = {s : State | ∃ (s' : State), lts.Tr s μ s' ∧ s' ∈ a_2.denotation lts}
• (Cslib.Logic.HML.Proposition.box μ a_2).denotation lts = {s : State | ∀ (s' : State), lts.Tr s μ s' → s' ∈ a_2.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 satifies.

Equations

• Cslib.Logic.HML.theory lts s = {a : Cslib.Logic.HML.Proposition Label | Cslib.Logic.HML.Satisfies lts s a}

@[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.satisfies_mem_denotation {State : Type u_1} {Label : Type u_2} {s : State} {a : Proposition Label} {lts : LTS State Label} : Satisfies lts s a ↔ s ∈ a.denotation lts

Characterisation theorem for the denotational semantics.

@[simp]

theorem Cslib.Logic.HML.neg_satisfies {State : Type u_1} {Label : Type u_2} {s : State} {a : Proposition Label} {lts : LTS State Label} : ¬Satisfies lts s a.neg ↔ Satisfies lts s a

A state satisfies a proposition iff it does not satisfy the negation of the proposition.

theorem Cslib.Logic.HML.neg_denotation {State : Type u_1} {Label : Type u_2} {s : State} {lts : LTS State Label} (a : Proposition Label) : s ∉ a.neg.denotation lts ↔ s ∈ a.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.satisfies_finiteAnd {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {as : List (Proposition Label)} : Satisfies lts s (Proposition.finiteAnd as) ↔ ∀ a ∈ as, Satisfies lts s a

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

theorem Cslib.Logic.HML.satisfies_finiteOr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {as : List (Proposition Label)} : Satisfies lts s (Proposition.finiteOr as) ↔ ∃ a ∈ as, Satisfies lts s a

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

theorem Cslib.Logic.HML.satisfies_theory {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} {s : State✝} {a : Proposition Label✝} (h : Satisfies lts s a) : a ∈ theory lts s

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 ↔ ∀ (a : Proposition Label), s1 ∈ a.denotation lts ↔ s2 ∈ a.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) : ∃ (a : Proposition Label✝), Satisfies lts s1 a ∧ ¬Satisfies lts s2 a

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} {s1 s2 : State} {a : Proposition Label} {lts : LTS State Label} (h : TheoryEq lts s1 s2) (hs : Satisfies lts s1 a) : Satisfies lts s2 a

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 μ)), Satisfies lts s1' (stateMap s2')) : Satisfies lts s1 (Proposition.diamond μ (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.IsBisimulation (TheoryEq lts)

Theory equivalence is a bisimulation.

theorem Cslib.Logic.HML.bisimulation_satisfies {State : Type u_1} {Label : Type u_2} {r : State → State → Prop} {s1 s2 : State} {lts : LTS State Label} {hrb : lts.IsBisimulation r} (hr : r s1 s2) (a : Proposition Label) (hs : Satisfies lts s1 a) : Satisfies lts s2 a

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

theorem Cslib.Logic.HML.bisimulation_TheoryEq {State : Type u_1} {Label : Type u_2} {r : State → State → Prop} {s1 s2 : State} {lts : LTS State Label} {hrb : lts.IsBisimulation 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 = Bisimilarity lts

Theory equivalence and bisimilarity coincide for image-finite LTSs.