Propositional dynamic logic (PDL)

StructurePDL model#✓fully proved

A model of propositional dynamic logic with set of worlds \(W\) consists of a binary accessibility relation \(R_a\) on \(W\) for each atomic action label \(a\), and a valuation that says which atoms are true at each world.

structure Model (World : Type u) (Atom : Type v) (Label : Type w) where
  /-- One accessibility relation per atomic program label. -/
  rel : Label → World → World → Prop
  /-- The atoms true at each world. -/
  valuation : World → Atom → Prop

Used by 29

Used byHoare rule for nondeterministic choice · Hoare rule of consequence · Partial-correctness Hoare triple for PDL programs · Hoare triples with formula assertions as box validity · Partial correctness as inclusion in the relational core · Hoare triples as KAT absorption equations · Hoare triples as KAT test inequalities · PDL induction restricted to reachable states · Hoare rule for sequential composition · Hoare invariant rule for iteration · Hoare rule for formula tests · Test absorption lifts through iteration · Loop exit absorption from a guarded-body absorption equation · Hoare invariant rule for guarded while loops · While-loop rule with initialization and exit implication · Semantic completeness of the while-loop invariant rule · Relation denoted by a PDL program · Satisfaction of PDL formulas · Box of a choice · Box of a sequential composition · Unfolding the box of an iteration · Box of a test · The toggle model · Relational interpretation preserves executions · Relational interpretation of a PDL program · Choice is interpreted by relational union · Sequencing is interpreted by relational composition · Iteration is interpreted by reflexive-transitive closure · Tests are interpreted by PDL satisfaction

InductivePDL formulas#✓fully proved

The formulas of propositional dynamic logic over a type of atoms and a type of atomic action labels are the atoms \(p\), falsity \(\bot\), implications \(\varphi \to \psi\) of formulas, and boxes \([\alpha]\varphi\) of a program \(\alpha\) and a formula \(\varphi\). Formulas and programs are defined by simultaneous induction.

inductive Formula (Atom : Type v) (Label : Type w) where
  | atom (a : Atom) : Formula Atom Label
  | bot : Formula Atom Label
  | imp (φ ψ : Formula Atom Label) : Formula Atom Label
  | box (α : Program Atom Label) (φ : Formula Atom Label) : Formula Atom Label

Used by 17

Used byHoare triples with formula assertions as box validity · PDL induction restricted to reachable states · Hoare rule for formula tests · Loop exit absorption from a guarded-body absorption equation · Guarded while loop in PDL · Hoare invariant rule for guarded while loops · While-loop rule with initialization and exit implication · Semantic completeness of the while-loop invariant rule · Possibility in PDL · Relation denoted by a PDL program · Satisfaction of PDL formulas · Box of a choice · Box of a sequential composition · Unfolding the box of an iteration · Box of a test · Failure of \((a;a)\,p\) in the toggle model · Tests are interpreted by PDL satisfaction

InductivePDL programs#✓fully proved

The programs of propositional dynamic logic over a type of atoms and a type of atomic action labels are the atomic actions \(a\), sequential compositions \(\alpha ; \beta\), nondeterministic choices \(\alpha \cup \beta\), iterations \(\alpha^*\), and tests \(\varphi?\) of a formula \(\varphi\). Programs and formulas are defined by simultaneous induction.

inductive Program (Atom : Type v) (Label : Type w) where
  | atomic (a : Label) : Program Atom Label
  | seq (α β : Program Atom Label) : Program Atom Label
  | choice (α β : Program Atom Label) : Program Atom Label
  | star (α : Program Atom Label) : Program Atom Label
  | test (φ : Formula Atom Label) : Program Atom Label

Used by 31

Used byHoare rule for nondeterministic choice · Hoare rule of consequence · Partial-correctness Hoare triple for PDL programs · Hoare triples with formula assertions as box validity · Partial correctness as inclusion in the relational core · Hoare triples as KAT absorption equations · Hoare triples as KAT test inequalities · PDL induction restricted to reachable states · Hoare rule for sequential composition · Hoare invariant rule for iteration · Hoare rule for formula tests · Test absorption lifts through iteration · Loop exit absorption from a guarded-body absorption equation · Guarded while loop in PDL · Hoare invariant rule for guarded while loops · While-loop rule with initialization and exit implication · Semantic completeness of the while-loop invariant rule · Possibility in PDL · Relation denoted by a PDL program · Satisfaction of PDL formulas · Box of a choice · Box of a sequential composition · Unfolding the box of an iteration · Box of a test · Failure of \((a;a)\,p\) in the toggle model · Relational interpretation preserves executions · Relational interpretation of a PDL program · Choice is interpreted by relational union · Sequencing is interpreted by relational composition · Iteration is interpreted by reflexive-transitive closure · Tests are interpreted by PDL satisfaction

DefinitionPossibility in PDL#✓fully proved

For a program \(\alpha\) and a formula \(\varphi\), the formula \(\langle\alpha\rangle\varphi\) is defined as \([\alpha](\varphi \to \bot) \to \bot\), that is, as \(\neg[\alpha]\neg\varphi\): possibility is the dual of necessity.

def Formula.dia {Atom Label : Type*} (α : Program Atom Label) (φ : Formula Atom Label) :
    Formula Atom Label :=
  .imp (.box α (.imp φ .bot)) .bot

Uses 2

Statement usesPDL formulas · PDL programs

DefinitionRelation denoted by a PDL program#✓fully proved

In a model \(M\), each program \(\alpha\) denotes a binary relation \(R_\alpha\) on worlds: an atomic action \(a\) denotes its accessibility relation \(R_a\); \((w, v) \in R_{\alpha;\beta}\) iff \((w, u) \in R_\alpha\) and \((u, v) \in R_\beta\) for some world \(u\); \(R_{\alpha \cup \beta} = R_\alpha \cup R_\beta\); \(R_{\alpha^*}\) is the reflexive-transitive closure of \(R_\alpha\); and \((w, v) \in R_{\varphi?}\) iff \(w = v\) and \(\varphi\) holds at \(w\) in \(M\).

def ProgRel {World Atom Label : Type*} (M : Model World Atom Label) :
    Program Atom Label → World → World → Prop
  | .atomic a, w, v => M.rel a w v
  | .seq α β, w, v => ∃ u, ProgRel M α w u ∧ ProgRel M β u v
  | .choice α β, w, v => ProgRel M α w v ∨ ProgRel M β w v
  | .star α, w, v => Relation.ReflTransGen (ProgRel M α) w v
  | .test φ, w, v => w = v ∧ Sat M φ w

Uses 3 · Used by 18

Statement usesPDL formulas · PDL model · PDL programs

Used byHoare rule for nondeterministic choice · Hoare rule of consequence · Partial-correctness Hoare triple for PDL programs · Hoare triples with formula assertions as box validity · Partial correctness as inclusion in the relational core · PDL induction restricted to reachable states · Hoare rule for sequential composition · Hoare invariant rule for iteration · Hoare rule for formula tests · Hoare invariant rule for guarded while loops · Semantic completeness of the while-loop invariant rule · Box of a choice · Box of a sequential composition · Unfolding the box of an iteration · Box of a test · Failure of \((a;a)\,p\) in the toggle model · Relational interpretation preserves executions · Relational interpretation of a PDL program

DefinitionSatisfaction of PDL formulas#✓fully proved

Truth of a formula at a world \(w\) of a model \(M\) is defined by recursion: an atom \(p\) holds at \(w\) iff the valuation of \(M\) makes \(p\) true at \(w\); \(\bot\) holds nowhere; \(\varphi \to \psi\) holds at \(w\) iff \(\psi\) holds at \(w\) whenever \(\varphi\) does; and \([\alpha]\varphi\) holds at \(w\) iff \(\varphi\) holds at every world \(v\) with \((w, v) \in R_\alpha\), where \(R_\alpha\) is the relation denoted by \(\alpha\) in \(M\).

def Sat {World Atom Label : Type*} (M : Model World Atom Label) :
    Formula Atom Label → World → Prop
  | .atom a, w => M.valuation w a
  | .bot, _ => False
  | .imp φ ψ, w => Sat M φ w → Sat M ψ w
  | .box α φ, w => ∀ v, ProgRel M α w v → Sat M φ v

Uses 3 · Used by 13

Statement usesPDL formulas · PDL model · PDL programs

Used byHoare triples with formula assertions as box validity · PDL induction restricted to reachable states · Hoare rule for formula tests · Loop exit absorption from a guarded-body absorption equation · Hoare invariant rule for guarded while loops · While-loop rule with initialization and exit implication · Semantic completeness of the while-loop invariant rule · Box of a choice · Box of a sequential composition · Unfolding the box of an iteration · Box of a test · Failure of \((a;a)\,p\) in the toggle model · Tests are interpreted by PDL satisfaction

TheoremBox of a sequential composition#✓fully proved

For every model \(M\), world \(w\), programs \(\alpha\) and \(\beta\), and formula \(\varphi\), the formula \([\alpha;\beta]\varphi\) holds at \(w\) if and only if \([\alpha][\beta]\varphi\) holds at \(w\).

theorem sat_box_seq :
    Sat M (.box (.seq α β) φ) w ↔ Sat M (.box α (.box β φ)) w

Uses 5

Statement usesPDL formulas · PDL model · PDL programs · Satisfaction of PDL formulas

Proof usesRelation denoted by a PDL program

TheoremBox of a choice#✓fully proved

For every model \(M\), world \(w\), programs \(\alpha\) and \(\beta\), and formula \(\varphi\), the formula \([\alpha \cup \beta]\varphi\) holds at \(w\) if and only if both \([\alpha]\varphi\) and \([\beta]\varphi\) hold at \(w\).

theorem sat_box_choice :
    Sat M (.box (.choice α β) φ) w ↔
      Sat M (.box α φ) w ∧ Sat M (.box β φ) w

Uses 5

Statement usesPDL formulas · PDL model · PDL programs · Satisfaction of PDL formulas

Proof usesRelation denoted by a PDL program

TheoremUnfolding the box of an iteration#✓fully proved

For every model \(M\), world \(w\), program \(\alpha\) and formula \(\varphi\), the formula \([\alpha^*]\varphi\) holds at \(w\) if and only if \(\varphi\) holds at \(w\) and \([\alpha][\alpha^*]\varphi\) holds at \(w\).

theorem sat_box_star_unfold :
    Sat M (.box (.star α) φ) w ↔
      Sat M φ w ∧ Sat M (.box α (.box (.star α) φ)) w

Uses 5

Statement usesPDL formulas · PDL model · PDL programs · Satisfaction of PDL formulas

Proof usesRelation denoted by a PDL program

TheoremBox of a test#✓fully proved

For every model \(M\), world \(w\) and formulas \(\psi\) and \(\varphi\), the formula \([\psi?]\varphi\) holds at \(w\) if and only if \(\varphi\) holds at \(w\) whenever \(\psi\) holds at \(w\).

theorem sat_box_test :
    Sat M (.box (.test ψ) φ) w ↔ (Sat M ψ w → Sat M φ w)

Uses 5

Statement usesPDL formulas · PDL model · PDL programs · Satisfaction of PDL formulas

Proof usesRelation denoted by a PDL program

DefinitionThe toggle model#✓fully proved

The PDL model whose worlds are the two Booleans \(\mathsf{true}\) and \(\mathsf{false}\), with a single atomic action \(a\) and a single atom \(p\): the action \(a\) relates each world \(s\) exactly to its negation \(\lnot s\), and \(p\) holds exactly at \(\mathsf{true}\).

def toggleModel : Model Bool Unit Unit where
  rel := fun _ s t => t = !s
  valuation := fun s _ => s = true

Uses 1 · Used by 1

Statement usesPDL model

Used byFailure of \((a;a)\,p\) in the toggle model

TheoremFailure of \((a;a)\,p\) in the toggle model#✓fully proved

In the toggle model, with atomic action \(a\) and atom \(p\), the formula \([a;a]\,p\) is not satisfied at the world \(\mathsf{false}\).

Performing \(a\) twice leads from \(\mathsf{false}\) back to \(\mathsf{false}\), where \(p\) is false.

theorem toggle_not_box_seq_atom :
    ¬ Sat toggleModel
      (.box (.seq (.atomic ()) (.atomic ())) (.atom ())) false

Uses 5

Statement usesPDL formulas · PDL programs · Satisfaction of PDL formulas · The toggle model

Proof usesRelation denoted by a PDL program

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.