7.2. Certified model checking of closed systems🔗

Definition7.2.1

uses 0

Used by 5

Reverse dependency previews

Preview

Theorem 7.2.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Tagsfrom source

A closed system is a ground agent with a finite rule list \mathcal{R}; no context is applied. Its formulas are \varphi ::= p \mid \neg p \mid \varphi \wedge \varphi \mid \varphi \vee \varphi \mid \Diamond\varphi \mid \Box\varphi \mid X \mid \mu.\varphi \mid \nu.\varphi, the modalities ranging over reactions \longrightarrow_{\mathcal{R}} and the atoms p invariant under support equivalence. When each rule carries a tag, silent or a visible action, strong and weak bisimilarity, a \sim b and a \approx b, of two closed systems are defined on tagged reactions in the usual way (Milner, Communication and Concurrency, 1989). These are bisimilarities over rule tags, not the library's bisimilarity over contexts, and no theorem relates the two (see the section Congruence). Below, \llbracket s \rrbracket is the bigraph of a well-formed ground agent s given as finite data, and G1 is the guard that every root of every redex has a node child.

Lean code for Definition7.2.1●4 definitions

inductive(9 constructors)defined in Logic/Closed.lean

complete

inductive CForm : Type

inductive CForm : Type

**Closed-system formulas** (positive normal form, de Bruijn variables;
atoms index a table).

Constructors

atom (i : Nat) : CForm

natom (i : Nat) : CForm

and (φ ψ : CForm) : CForm

or (φ ψ : CForm) : CForm

dia (φ : CForm) : CForm

box (φ : CForm) : CForm

var (k : Nat) : CForm

mu (φ : CForm) : CForm

nu (φ : CForm) : CForm

defdefined in Logic/Closed.lean

complete

def CSat {Ctrl : Type} [DecidableEq Ctrl] (S : Bigraph.Sig Ctrl)
  (rules : List (BigraphSim.RuleD Ctrl)) (atoms : List (AtomD S))
  {J : Face} :
  (Nat → BigH S Face.origin J → Prop) →
    BigH S Face.origin J → CForm → Prop

def CSat {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl)
  (rules : List (BigraphSim.RuleD Ctrl))
  (atoms : List (AtomD S)) {J : Face} :
  (Nat → BigH S Face.origin J → Prop) →
    BigH S Face.origin J → CForm → Prop

**The library meaning** of a closed-system formula.

defdefined in Logic/CertBisim.lean

complete

def TBisim {α : Type} [DecidableEq α] {Ctrl₁ Ctrl₂ : Type}
  [DecidableEq Ctrl₁] [DecidableEq Ctrl₂] (S₁ : Bigraph.Sig Ctrl₁)
  (trs₁ : TRules α Ctrl₁) (S₂ : Bigraph.Sig Ctrl₂)
  (trs₂ : TRules α Ctrl₂) {J₁ J₂ : Face} (a : BigH S₁ Face.origin J₁)
  (b : BigH S₂ Face.origin J₂) : Prop

def TBisim {α : Type} [DecidableEq α]
  {Ctrl₁ Ctrl₂ : Type} [DecidableEq Ctrl₁]
  [DecidableEq Ctrl₂]
  (S₁ : Bigraph.Sig Ctrl₁)
  (trs₁ : TRules α Ctrl₁)
  (S₂ : Bigraph.Sig Ctrl₂)
  (trs₂ : TRules α Ctrl₂) {J₁ J₂ : Face}
  (a : BigH S₁ Face.origin J₁)
  (b : BigH S₂ Face.origin J₂) : Prop

Strong bisimilarity `a ∼ b`.

defdefined in Logic/CertBisim.lean

complete

def WBisim {α : Type} [DecidableEq α] {Ctrl₁ Ctrl₂ : Type}
  [DecidableEq Ctrl₁] [DecidableEq Ctrl₂] (S₁ : Bigraph.Sig Ctrl₁)
  (trs₁ : TRules α Ctrl₁) (S₂ : Bigraph.Sig Ctrl₂)
  (trs₂ : TRules α Ctrl₂) {J₁ J₂ : Face} (a : BigH S₁ Face.origin J₁)
  (b : BigH S₂ Face.origin J₂) : Prop

def WBisim {α : Type} [DecidableEq α]
  {Ctrl₁ Ctrl₂ : Type} [DecidableEq Ctrl₁]
  [DecidableEq Ctrl₂]
  (S₁ : Bigraph.Sig Ctrl₁)
  (trs₁ : TRules α Ctrl₁)
  (S₂ : Bigraph.Sig Ctrl₂)
  (trs₂ : TRules α Ctrl₂) {J₁ J₂ : Face}
  (a : BigH S₁ Face.origin J₁)
  (b : BigH S₂ Face.origin J₂) : Prop

Weak bisimilarity `a ≈ b`.

Theorem7.2.2

uses 1

Used by 3

Reverse dependency previews

Preview

Theorem 7.2.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Matcher completeness: the simulator's matcher finds every reaction of the library, up to support equivalence. For rules \mathcal{R} satisfying G1 and \mathrm{step}_{\mathcal{R}}(s) the matcher's list of successors,

\llbracket s \rrbracket \longrightarrow_{\mathcal{R}} a' \;\Longrightarrow\; \exists x \in \mathrm{step}_{\mathcal{R}}(s).\;\; a' \bumpeq \llbracket x \rrbracket .

For the simulator's earlier matcher, kept frozen, completeness is REFUTED, and already for a rule that satisfies G1: a rule that discards a parameter lying beside a node under a redex root has a library reaction that no offered successor matches. The matcher and its soundness are in the simulator chapter.

Rests on NEW: BigraphSim.BD.Fits, BigraphSim.BD.outFace, BigraphSim.Item, BigraphSim.Match.embeds, BigraphSim.Occ, BigraphSim.Par, COccCounter.agentA, COccCounter.dropR and 1 more; not audited: BigraphSim.Test.T, BigraphSim.Test.sig, COccV1.

Lean code for Theorem7.2.2●2 theorems

theoremdefined in Logic/COccG1.lean

complete

theorem cocc_G1 {Ctrl : Type} [DecidableEq Ctrl] (S : Bigraph.Sig Ctrl) :
  COccG1 S

theorem cocc_G1 {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) : COccG1 S

**Matcher completeness under G1** (C-occ″).

theoremdefined in Logic/COcc.lean

complete

theorem cocc_refuted :
  ¬COccV1 BigraphSim.Test.sig [COccCounter.dropR] COccCounter.agentA
      COccCounter.agentA_check ⋯ ⋯

theorem cocc_refuted :
  ¬COccV1 BigraphSim.Test.sig
      [COccCounter.dropR]
      COccCounter.agentA
      COccCounter.agentA_check ⋯ ⋯

**C-occ, unrestricted, is REFUTED**: `agentA` reacts in the library to
an agent that is support equivalent to no successor the matcher
offers.

Theorem7.2.3

uses 1used by 1✓L∃∀N

A certificate c lists states s_0, \dots, s_n, a successor table, and one renumbering witness per matcher step; its check runs the matcher once per state and searches nothing. A passing certificate has a table that is sound and complete for the matcher's steps up to renumbering, and then, for rules satisfying G1, every listed state and every formula \varphi,

\mathrm{check}(c, \varphi, i) = \mathrm{true} \;\iff\; \llbracket s_i \rrbracket \models \varphi .

Rests on NEW: AtomD, BigraphSim.BD.outFace, BigraphSim.Item, BigraphSim.Occ, BigraphSim.Par, RuleG.g1; not audited: RenTo, succIdx.

Lean code for Theorem7.2.3●3 declarations

defdefined in Logic/M1Prime.lean

complete

def certCheck {Ctrl : Type} [DecidableEq Ctrl] (S : Bigraph.Sig Ctrl)
  (rules : List (BigraphSim.RuleD Ctrl)) (c : Cert Ctrl) : Bool

def certCheck {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl)
  (rules : List (BigraphSim.RuleD Ctrl))
  (c : Cert Ctrl) : Bool

**The certificate check.** One `Match.step` per listed state; no search.

theoremdefined in Logic/M1PrimeCert.lean

complete

theorem certCheck_sound {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) : CertCheckStatement S

theorem certCheck_sound {Ctrl : Type}
  [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) :
  CertCheckStatement S

**The certificate check is sound** (PROVED; `CertCheckStatement`).

theoremdefined in Logic/M1PrimeProof.lean

complete

theorem m1Prime {Ctrl : Type} [DecidableEq Ctrl] (S : Bigraph.Sig Ctrl) :
  M1PrimeStatement S

theorem m1Prime {Ctrl : Type} [DecidableEq Ctrl]
  (S : Bigraph.Sig Ctrl) :
  M1PrimeStatement S

**M1′ is correct** (PROVED; `M1PrimeStatement`).

Theorem7.2.4

uses 1used by 0✓L∃∀N

Dining philosophers (three philosophers, three forks, a held fork nested in its philosopher), from the initial agent a_0. Write \mathit{safe} = \nu X.\, \mathit{noNeighboursEat} \wedge \Box X, \mathit{dead} = \mu X.\, \Box\bot \vee \Diamond X and \mathit{eat}_i = \nu Y.\, (\mu X.\, \mathit{eating}_i \vee \Diamond X) \wedge \Box Y (bound variables are named here for reading only). For the naive, the repaired and the fair protocol respectively,

a_0 \models \mathit{safe},\;\; a_0 \models \mathit{dead},\;\; a_0 \not\models \mathit{eat}_0; \qquad a_0 \models \mathit{safe},\;\; a_0 \not\models \mathit{dead},\;\; a_0 \models \mathit{eat}_0; \qquad a_0 \models \mathit{safe},\;\; a_0 \not\models \mathit{dead},\;\; a_0 \models \mathit{eat}_0 \wedge \mathit{eat}_1 \wedge \mathit{eat}_2 .

The fair protocol nevertheless has a livelock, an infinite run on which nobody eats, proved from a lasso witness:

a_0 \models \nu X.\, (\neg\mathit{eating}_0 \wedge \neg\mathit{eating}_1 \wedge \neg\mathit{eating}_2) \wedge \Diamond X .

Rests on UNBRIDGED: Dining.Fair.canEat, Dining.Fair.fair, Dining.agent0, Dining.naive, Dining.repaired; NEW: AtomD, BigraphSim.BD.outFace, BigraphSim.Item, BigraphSim.Par, Perm; not audited: Dining.Ctl, Dining.atoms, Dining.canEat0, Dining.deadlockReach, Dining.safety, Dining.sig, M1PrimeDiningLivelock.livelockF.

Lean code for Theorem7.2.4●4 theorems

theoremdefined in Logic/Examples/M1Prime/Dining.lean

complete

theorem naive_verdicts :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.naive | Dining.atoms | fun x x_1 => False]
      Dining.safety ∧
    ⟦Dining.agent0⟧ ⊨ᶜ[Dining.naive | Dining.atoms | fun x x_1 => False]
        Dining.deadlockReach ∧
      ¬⟦Dining.agent0⟧ ⊨ᶜ[Dining.naive | Dining.atoms | fun x x_1 =>
          False] Dining.canEat0

theorem naive_verdicts :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.naive |
      Dining.atoms | fun x x_1 => False]
      Dining.safety ∧
    ⟦Dining.agent0⟧ ⊨ᶜ[Dining.naive |
        Dining.atoms | fun x x_1 => False]
        Dining.deadlockReach ∧
      ¬⟦Dining.agent0⟧ ⊨ᶜ[Dining.naive |
          Dining.atoms | fun x x_1 =>
          False] Dining.canEat0

**Naive: safe, deadlock reachable, philosopher 0 not guaranteed to eat.**

theoremdefined in Logic/Examples/M1Prime/Dining.lean

complete

theorem repaired_verdicts :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.repaired | Dining.atoms | fun x x_1 =>
      False] Dining.safety ∧
    ¬⟦Dining.agent0⟧ ⊨ᶜ[Dining.repaired | Dining.atoms | fun x x_1 =>
          False] Dining.deadlockReach ∧
      ⟦Dining.agent0⟧ ⊨ᶜ[Dining.repaired | Dining.atoms | fun x x_1 =>
        False] Dining.canEat0

theorem repaired_verdicts :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.repaired |
      Dining.atoms | fun x x_1 => False]
      Dining.safety ∧
    ¬⟦Dining.agent0⟧ ⊨ᶜ[Dining.repaired |
          Dining.atoms | fun x x_1 =>
          False] Dining.deadlockReach ∧
      ⟦Dining.agent0⟧ ⊨ᶜ[Dining.repaired |
        Dining.atoms | fun x x_1 => False]
        Dining.canEat0

**Repaired: safe, no deadlock reachable, philosopher 0 can always eventually eat.**

theoremdefined in Logic/Examples/M1Prime/DiningFair.lean

complete

theorem fair_verdicts :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair | Dining.atoms | fun x x_1 =>
      False] Dining.safety ∧
    ¬⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair | Dining.atoms | fun x x_1 =>
          False] Dining.deadlockReach ∧
      ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair | Dining.atoms | fun x x_1 =>
          False] Dining.Fair.canEat 0 ∧
        ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair | Dining.atoms |
            fun x x_1 => False] Dining.Fair.canEat 1 ∧
          ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair | Dining.atoms |
            fun x x_1 => False] Dining.Fair.canEat 2

theorem fair_verdicts :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair |
      Dining.atoms | fun x x_1 => False]
      Dining.safety ∧
    ¬⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair |
          Dining.atoms | fun x x_1 =>
          False] Dining.deadlockReach ∧
      ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair |
          Dining.atoms | fun x x_1 =>
          False] Dining.Fair.canEat 0 ∧
        ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair |
            Dining.atoms | fun x x_1 =>
            False] Dining.Fair.canEat 1 ∧
          ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair |
            Dining.atoms | fun x x_1 =>
            False] Dining.Fair.canEat 2

**Fair: safe, no deadlock reachable, and every philosopher can always
still eat.**

theoremdefined in Logic/Examples/M1Prime/DiningLivelock.lean

complete

theorem livelock :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair | Dining.atoms | fun x x_1 =>
    False] M1PrimeDiningLivelock.livelockF

theorem livelock :
  ⟦Dining.agent0⟧ ⊨ᶜ[Dining.Fair.fair |
    Dining.atoms | fun x x_1 => False]
    M1PrimeDiningLivelock.livelockF

**The fair protocol livelocks**: from `agent0` there is an infinite run
on which nobody ever eats (the library meaning).