Model Graphs (Section 7.1)

Definition of Model Graphs

def PDL.Modelgraphs.Q {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) : Program → ↥W → ↥W → Prop

Definition 6.3: Given relations for all atomic programs over model graph states (i.e. sets of formulas), define relations for all PDL programs inductively as usual, but using membership to interpret the test operator.

Equations

• PDL.Modelgraphs.Q R (PDL.Program.atom_prog c) = R c
• PDL.Modelgraphs.Q R (PDL.Program.test τ) = fun (v w : ↥W) => v = w ∧ τ ∈ ↑v
• PDL.Modelgraphs.Q R (α.union β) = fun (v w : ↥W) => PDL.Modelgraphs.Q R α v w ∨ PDL.Modelgraphs.Q R β v w
• PDL.Modelgraphs.Q R (α.sequence β) = Relation.Comp (PDL.Modelgraphs.Q R α) (PDL.Modelgraphs.Q R β)
• PDL.Modelgraphs.Q R α.star = Relation.ReflTransGen (PDL.Modelgraphs.Q R α)

def PDL.ModelGraph (W : Finset (Finset Formula)) : Type

Definition 6.4. A model graph is a Kripke model over sets of formulas as states fulfilling the conditions (a) to (b). See also [MB1988] Def 19 on page 31 where (a)-(b) are named (i)-(iv). Note: In MB item (b) aka (ii) only has →. We use ↔ similar to [BRV2001] Def 4.18 and 4.84. Note: In item (c) a is atomic, but in item (d) α is any program.

Equations

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

Truth Lemma

theorem PDL.get_eq_getzip {α : Type u_1} {l : List α} {α✝ : Type u_2} {x : α✝} {δ : List α✝} {X Y : α} {i : Fin (l ++ [Y]).length} {h : ↑i < ((x, X) :: δ.zip (l ++ [Y])).length} : (X :: (l ++ [Y])).get i.castSucc = ((x, X) :: δ.zip (l ++ [Y]))[↑i].2

theorem PDL.loadClaimHelper {Worlds : Finset (Finset Formula)} {MG : ModelGraph Worlds} {X Y : ↥Worlds} {δ : List Program} {φ : Formula} {l : List ↥Worlds} (length_def : l.length + 1 = δ.length) (δφ_in_X : Formula.boxes δ φ ∈ ↑X) (lchain : List.IsChain (pairRel ↑MG) ((Program.test ⊤ :: δ).zip (X :: l ++ [Y]))) (IHδ : ∀ d ∈ δ, ∀ (X' Y' : ↥Worlds) (φ' : Formula), Formula.box d φ' ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y') (i : Fin (X :: l ++ [Y]).length) : Formula.boxes (List.drop (↑i) δ) φ ∈ ↑((X :: l ++ [Y]).get i)

theorem PDL.Q_then_relate {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (α : Program) (X Y : ↥Worlds) : Modelgraphs.Q (↑MG).Rel α X Y → relate (↑MG) α X Y

C3 in notes. Originally MB Lemma 9, page 32, stronger version for induction loading. Now also using Q relation to overwrite tests.

theorem PDL.loadedTruthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (X : ↥Worlds) (P : Formula) : (P ∈ ↑X → evaluate (↑MG) X P) ∧ (P.neg ∈ ↑X → ¬evaluate (↑MG) X P)

C1 and C2 in notes

theorem PDL.loadedTruthLemmaProg {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (α : Program) (X : ↥Worlds) (φ : Formula) : Formula.box α φ ∈ ↑X → ∀ (Y : ↥Worlds), relate (↑MG) α X Y → φ ∈ ↑Y

C4 in notes

theorem PDL.truthLemma {Worlds : Finset (Finset Formula)} (MG : ModelGraph Worlds) (X : ↥Worlds) (P : Formula) : P ∈ ↑X → evaluate (↑MG) X P

Additional Q relations for the completeness proof

def PDL.Qtests {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (F : List Formula) : ↥W → ↥W → Prop

Q_F - for a list F of tests (instead of a set in the notes).

Equations

• PDL.Qtests R F x✝¹ x✝ = ((x✝¹ == x✝) = true ∧ ∀ τ ∈ F, PDL.Modelgraphs.Q R (PDL.Program.test τ) x✝¹ x✝)

def PDL.Qsteps {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) : List Program → ↥W → ↥W → Prop

Q_δ for a list δ of programs.

Equations

• PDL.Qsteps R [] x✝¹ x✝ = ((x✝¹ == x✝) = true)
• PDL.Qsteps R (α :: δ) x✝¹ x✝ = Relation.Comp (PDL.Modelgraphs.Q R α) (PDL.Qsteps R δ) x✝¹ x✝

@[simp]

theorem PDL.Qsteps_single {a✝ : Finset (Finset Formula)} {R : ℕ → ↥a✝ → ↥a✝ → Prop} {α : Program} {v w : ↥a✝} : Qsteps R [α] v w ↔ Modelgraphs.Q R α v w

theorem PDL.Qsteps_append {a✝ : Finset (Finset Formula)} {R : ℕ → ↥a✝ → ↥a✝ → Prop} {δ1 δ2 : List Program} {v w : ↥a✝} : Qsteps R (δ1 ++ δ2) v w ↔ ∃ (u : ↥a✝), Qsteps R δ1 v u ∧ Qsteps R δ2 u w

def PDL.Qcombo {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (F : List Formula) (δ : List Program) : ↥W → ↥W → Prop

Q_Fδ for a list of tests F and a list or programs δ.

Equations

• PDL.Qcombo R F δ = Relation.Comp (PDL.Qtests R F) (PDL.Qsteps R δ)

theorem PDL.cpHelpA {W : Finset (Finset Formula)} (R : ℕ → ↥W → ↥W → Prop) (α : Program) (Fδ : List Formula × List Program) : Fδ ∈ Dset α → ∀ (v w : ↥W), Qcombo R Fδ.1 Fδ.2 v w → Modelgraphs.Q R α v w

Q_Fδ v w implies Q v w.