Linear temporal logic

InductiveFormulas of linear temporal logic#✓fully proved

For a type \(A\) of atoms, the formulas of linear temporal logic (LTL) over \(A\) are generated inductively: every atom \(a \in A\) is a formula, the truth constant \(\top\) is a formula, and if \(\varphi\) and \(\psi\) are formulas then so are the negation \(\neg\varphi\), the conjunction \(\varphi \wedge \psi\), the next formula \(\mathbf{X}\,\varphi\) and the until formula \(\varphi \mathbin{\mathbf{U}} \psi\).

inductive Formula (Atom : Type u) : Type u where
  | atom (a : Atom) : Formula Atom
  | top : Formula Atom
  | not (φ : Formula Atom) : Formula Atom
  | and (φ ψ : Formula Atom) : Formula Atom
  | next (φ : Formula Atom) : Formula Atom
  | until (φ ψ : Formula Atom) : Formula Atom
  deriving DecidableEq, Repr

Used by 58

Used byBüchi automata for the restricted safety fragment · The always automaton recognizes G φ · Propositional formulas are evaluated at the current letter · Propositional formulas as LTL formulas · Safety formulas as LTL formulas · Embedding of LTL formulas as CTL\(^{\ast}\) path formulas · The LTL embedding preserves semantics on every sequence · The LTL embedding preserves semantics at every position · The always operator of LTL · Idempotence of always · Always eventually means infinitely often · Satisfaction of an atom · Falsity in LTL · Falsity is never satisfied · The eventually operator of LTL · Eventually always means from some point on · Semantics of eventually · Bi-implication in LTL · Implication in LTL · Language of an LTL formula · Membership in the language of a formula · Next is self-dual · Disjunction in LTL · The release operator of LTL · Expansion law for release · Semantics of release · Satisfaction of LTL formulas on ω-words · Satisfaction at a position · Satisfaction of an atom at a position · Satisfaction on a suffix · Satisfaction at position zero · Relabelling the letters of an ω-word · Expansion law for until · Computable fairness-counter update · Generalized Büchi tableau for an LTL formula · Büchi automaton for an LTL formula · Büchi transition test via the computable counter update · Executable full-LTL model checker · Correctness of the executable LTL model checker · Counterexample product for an LTL formula · Every LTL formula has a finite-state Büchi automaton · Fairness of a tableau annotation sequence · Tableau fairness is generalized Büchi acceptance · Generalized LTL tableau language equals the formula language · Büchi automaton language equals the LTL formula language · LTL tableau accepts exactly the satisfying words · Büchi automaton accepts exactly the satisfying words · Counterexample words are runs violating the formula · Tableau acceptance via initial, local and fairness conditions · Satisfaction of an LTL formula by all initial runs · LTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso · Computable counter update equals generic degeneralization · Boolean test for an until fairness obligation · Number of until fairness obligations · Truth-annotation states of the LTL tableau · Local transition relation of the LTL tableau · Root truth bit of a tableau annotation

DefinitionFalsity in LTL#✓fully proved

The LTL formula \(\bot\) (falsity) is defined as \(\neg\top\), the negation of the truth constant \(\top\).

def bot : Formula Atom := .not .top

Uses 1 · Used by 1

Statement usesFormulas of linear temporal logic

Used byFalsity is never satisfied

DefinitionDisjunction in LTL#✓fully proved

For LTL formulas \(\varphi\) and \(\psi\), the disjunction \(\varphi \vee \psi\) is defined as \(\neg(\neg\varphi \wedge \neg\psi)\).

def or (φ ψ : Formula Atom) : Formula Atom := .not (.and (.not φ) (.not ψ))

Uses 1 · Used by 3

Statement usesFormulas of linear temporal logic

Used byBüchi automata for the restricted safety fragment · Safety formulas as LTL formulas · Implication in LTL

DefinitionImplication in LTL#✓fully proved

For LTL formulas \(\varphi\) and \(\psi\), the implication \(\varphi \to \psi\) is defined as the disjunction \(\neg\varphi \vee \psi\).

def imp (φ ψ : Formula Atom) : Formula Atom := or (.not φ) ψ

Uses 2 · Used by 1

Statement usesFormulas of linear temporal logic · Disjunction in LTL

Used byBi-implication in LTL

DefinitionBi-implication in LTL#✓fully proved

For LTL formulas \(\varphi\) and \(\psi\), the bi-implication \(\varphi \leftrightarrow \psi\) is defined as the conjunction \((\varphi \to \psi) \wedge (\psi \to \varphi)\) of the two implications.

def iff (φ ψ : Formula Atom) : Formula Atom := .and (imp φ ψ) (imp ψ φ)

Uses 2

Statement usesFormulas of linear temporal logic · Implication in LTL

DefinitionThe eventually operator of LTL#✓fully proved

For an LTL formula \(\varphi\), the formula \(\mathbf{F}\,\varphi\) ("eventually \(\varphi\)") is defined as the until formula \(\top \mathbin{\mathbf{U}} \varphi\).

On an ω-word, \(\mathbf{F}\,\varphi\) holds at a position exactly when \(\varphi\) holds at that position or at some later one.

def eventually (φ : Formula Atom) : Formula Atom := .until .top φ

Uses 1 · Used by 8

Statement usesFormulas of linear temporal logic

Used byThe infinitely-often automaton recognizes G F φ · The always automaton recognizes G φ · The eventually-always automaton recognizes F G φ · The always operator of LTL · Idempotence of always · Always eventually means infinitely often · Eventually always means from some point on · Semantics of eventually

DefinitionThe always operator of LTL#✓fully proved

For an LTL formula \(\varphi\), the formula \(\mathbf{G}\,\varphi\) ("always \(\varphi\)") is defined as \(\neg\,\mathbf{F}\,\neg\varphi\), the negation of "eventually \(\neg\varphi\)".

On an ω-word, \(\mathbf{G}\,\varphi\) holds at a position exactly when \(\varphi\) holds at that position and at every later one.

def always (φ : Formula Atom) : Formula Atom := .not (eventually (.not φ))

Uses 2 · Used by 7

Statement usesFormulas of linear temporal logic · The eventually operator of LTL

Used byThe infinitely-often automaton recognizes G F φ · The always automaton recognizes G φ · The eventually-always automaton recognizes F G φ · Safety formulas as LTL formulas · Idempotence of always · Always eventually means infinitely often · Eventually always means from some point on

DefinitionThe release operator of LTL#✓fully proved

For LTL formulas \(\varphi\) and \(\psi\), the release formula \(\varphi \mathbin{\mathbf{R}} \psi\) is defined as \(\neg(\neg\varphi \mathbin{\mathbf{U}} \neg\psi)\), the dual of until.

On an ω-word, \(\varphi \mathbin{\mathbf{R}} \psi\) holds at a position when, from that position on, \(\psi\) holds up to and including the first position where \(\varphi\) holds, or forever if there is no such position.

def release (φ ψ : Formula Atom) : Formula Atom := .not (.until (.not φ) (.not ψ))

Uses 1 · Used by 2

Statement usesFormulas of linear temporal logic

Used byExpansion law for release · Semantics of release

DefinitionSatisfaction of LTL formulas on ω-words#✓fully proved

Let \(v\) be a valuation that says which atoms are true at each letter, and for an ω-word \(w\) and a natural number \(k\) let \(w^{(k)}\) be the suffix \(i \mapsto w(k + i)\). Whether \(w\) satisfies an LTL formula \(\varphi\) under \(v\), written \(w \models \varphi\), is defined by recursion on \(\varphi\): an atom \(a\) holds when \(v\) makes \(a\) true at the first letter \(w(0)\); truth always holds; \(\neg \varphi\) holds when \(\varphi\) does not; \(\varphi \wedge \psi\) holds when both \(\varphi\) and \(\psi\) do; \(\mathsf{X}\, \varphi\) (next \(\varphi\)) holds when \(w^{(1)} \models \varphi\); and \(\varphi \mathbin{\mathsf{U}} \psi\) (\(\varphi\) until \(\psi\)) holds when there is a \(k\) with \(w^{(k)} \models \psi\) and \(w^{(j)} \models \varphi\) for all \(j < k\).

def Satisfies (valuation : Symbol → Atom → Prop) (w : ωSequence Symbol) :
    Formula Atom → Prop
  | .atom a => valuation (w 0) a
  | .top => True
  | .not φ => ¬ Satisfies valuation w φ
  | .and φ ψ => Satisfies valuation w φ ∧ Satisfies valuation w ψ
  | .next φ => Satisfies valuation w.tail φ
  | .until φ ψ =>
      ∃ k, Satisfies valuation (w.drop k) ψ ∧ ∀ j < k, Satisfies valuation (w.drop j) φ

Uses 1 · Used by 30

Statement usesFormulas of linear temporal logic

Used byBüchi automata for the restricted safety fragment · The infinitely-often automaton recognizes G F φ · The always automaton recognizes G φ · The eventually-always automaton recognizes F G φ · The propositional automaton recognizes φ · Propositional formulas are evaluated at the current letter · Propositional formulas are evaluated at the first letter · The LTL embedding preserves semantics on every sequence · Idempotence of always · Always eventually means infinitely often · Satisfaction of an atom · Falsity is never satisfied · Eventually always means from some point on · Semantics of eventually · Language of an LTL formula · Membership in the language of a formula · Next is self-dual · Expansion law for release · Semantics of release · Satisfaction at a position · Satisfaction on a suffix · Satisfaction at position zero · Relabelling the letters of an ω-word · Expansion law for until · LTL tableau accepts exactly the satisfying words · Büchi automaton accepts exactly the satisfying words · Counterexample words are runs violating the formula · Satisfaction of an LTL formula by all initial runs · LTL satisfaction iff the counterexample language is empty · Finite-model LTL satisfaction iff no counterexample lasso

DefinitionSatisfaction at a position#✓fully proved

Let \(v\) be a valuation of atoms on letters, \(w\) an ω-word, \(k\) a natural number and \(\varphi\) an LTL formula. Then \(\varphi\) holds at position \(k\) of \(w\) under \(v\) when the suffix of \(w\) starting at position \(k\), the ω-word \(i \mapsto w(k + i)\), satisfies \(\varphi\) under \(v\).

def SatisfiesAt (valuation : Symbol → Atom → Prop) (w : ωSequence Symbol) (k : ℕ)
    (φ : Formula Atom) : Prop :=
  Satisfies valuation (w.drop k) φ

Uses 2 · Used by 16

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words

Used byBüchi automata for the restricted safety fragment · The infinitely-often automaton recognizes G F φ · The always automaton recognizes G φ · The eventually-always automaton recognizes F G φ · Propositional formulas are evaluated at the current letter · The LTL embedding preserves semantics at every position · Idempotence of always · Always eventually means infinitely often · Eventually always means from some point on · Semantics of eventually · Semantics of release · Satisfaction of an atom at a position · Satisfaction on a suffix · Satisfaction at position zero · Expansion law for until · LTL tableau accepts exactly the satisfying words

DefinitionLanguage of an LTL formula#✓fully proved

Given a valuation \(v\) of atoms on letters, the ω-language of an LTL formula \(\varphi\) is the set of ω-words that satisfy \(\varphi\) under \(v\).

def language (valuation : Symbol → Atom → Prop) (φ : Formula Atom) : ωLanguage Symbol :=
  { w : ωSequence Symbol | Satisfies valuation w φ }

Uses 2 · Used by 10

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words

Used byBüchi automata for the restricted safety fragment · The infinitely-often automaton recognizes G F φ · The always automaton recognizes G φ · The eventually-always automaton recognizes F G φ · The propositional automaton recognizes φ · Membership in the language of a formula · Every LTL formula has a finite-state Büchi automaton · Generalized LTL tableau language equals the formula language · Büchi automaton language equals the LTL formula language · Büchi automaton accepts exactly the satisfying words

TheoremSatisfaction at position zero#✓fully proved

For every valuation of atoms on letters, ω-word \(w\) and LTL formula \(\varphi\), \(\varphi\) holds at position \(0\) of \(w\) if and only if \(w\) satisfies \(\varphi\).

@[simp]
theorem satisfiesAt_zero : SatisfiesAt valuation w 0 φ ↔ Satisfies valuation w φ

Uses 3

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words · Satisfaction at a position

TheoremSatisfaction on a suffix#✓fully proved

Let \(w\) be an ω-word and, for a natural number \(k\), let \(w^{(k)}\) be its suffix starting at position \(k\), the ω-word \(i \mapsto w(k + i)\). For every valuation of atoms on letters, every LTL formula \(\varphi\) and every natural number \(j\), \(\varphi\) holds at position \(j\) of \(w^{(k)}\) if and only if \(\varphi\) holds at position \(k + j\) of \(w\).

theorem satisfiesAt_drop {k j : ℕ} :
    SatisfiesAt valuation (w.drop k) j φ ↔ SatisfiesAt valuation w (k + j) φ

Uses 3 · Used by 4

Statement usesFormulas of linear temporal logic · Satisfaction at a position

Proof usesSatisfaction of LTL formulas on ω-words

Used byAlways eventually means infinitely often · Eventually always means from some point on · Expansion law for until · LTL tableau accepts exactly the satisfying words

TheoremSatisfaction of an atom#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and every atom \(a\), the word \(w\) satisfies the atomic formula \(a\) under \(v\) if and only if \(v\) makes \(a\) true at the first letter \(w_0\) of \(w\).

theorem atom_iff : Satisfies valuation w (.atom a) ↔ valuation (w 0) a

Uses 2

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words

TheoremFalsity is never satisfied#✓fully proved

For every valuation \(v\) of atoms on letters and every ω-word \(w\), the word \(w\) does not satisfy the LTL formula \(\bot\) (falsity) under \(v\).

theorem bot_iff : Satisfies valuation w (Formula.bot : Formula Atom) ↔ False

Uses 3

Statement usesFalsity in LTL · Satisfaction of LTL formulas on ω-words

Proof usesFormulas of linear temporal logic

TheoremSemantics of eventually#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and every LTL formula \(\varphi\), the word \(w\) satisfies \(\mathbf{F}\,\varphi\) (eventually \(\varphi\)) under \(v\) if and only if for some \(k \in \mathbb{N}\) the suffix of \(w\) starting at position \(k\) satisfies \(\varphi\) under \(v\).

theorem eventually_iff :
    Satisfies valuation w (Formula.eventually φ) ↔ ∃ k, SatisfiesAt valuation w k φ

Uses 4 · Used by 4

Statement usesFormulas of linear temporal logic · The eventually operator of LTL · Satisfaction of LTL formulas on ω-words · Satisfaction at a position

Used byThe always automaton recognizes G φ · Idempotence of always · Always eventually means infinitely often · Eventually always means from some point on

TheoremSemantics of release#✓fully proved

For a valuation of atoms on letters, an ω-word \(w\) and LTL formulas \(\varphi\) and \(\psi\), \(w\) satisfies \(\varphi \mathbin{\mathsf{R}} \psi\) (\(\varphi\) releases \(\psi\)) if and only if for every position \(k\), either \(\psi\) holds at position \(k\) of \(w\) or \(\varphi\) holds at some position \(j < k\) of \(w\).

theorem release_iff :
    Satisfies valuation w (Formula.release φ ψ) ↔
      ∀ k, SatisfiesAt valuation w k ψ ∨ ∃ j < k, SatisfiesAt valuation w j φ

Uses 4

Statement usesFormulas of linear temporal logic · The release operator of LTL · Satisfaction of LTL formulas on ω-words · Satisfaction at a position

TheoremNext is self-dual#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and every LTL formula \(\varphi\), the word \(w\) satisfies \(\neg\mathbf{X}\,\varphi\) under \(v\) if and only if it satisfies \(\mathbf{X}\,\neg\varphi\) under \(v\), where \(\mathbf{X}\) is the next operator.

theorem not_next :
    Satisfies valuation w (.not (.next φ)) ↔ Satisfies valuation w (.next (.not φ))

Uses 2

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words

TheoremExpansion law for until#✓fully proved

For every valuation of atoms on letters, ω-word \(w\) and LTL formulas \(\varphi\) and \(\psi\), \(w\) satisfies \(\varphi \mathbin{\mathsf{U}} \psi\) (\(\varphi\) until \(\psi\)) if and only if either \(w\) satisfies \(\psi\), or \(w\) satisfies \(\varphi\) and also satisfies \(\mathsf{X}(\varphi \mathbin{\mathsf{U}} \psi)\), that is, next (\(\varphi\) until \(\psi\)).

theorem until_expansion :
    Satisfies valuation w (.until φ ψ) ↔
      Satisfies valuation w ψ ∨
        (Satisfies valuation w φ ∧ Satisfies valuation w (.next (.until φ ψ)))

Uses 4 · Used by 2

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words

Proof usesSatisfaction at a position · Satisfaction on a suffix

Used byExpansion law for release · LTL tableau accepts exactly the satisfying words

TheoremExpansion law for release#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and all LTL formulas \(\varphi\) and \(\psi\), the word \(w\) satisfies \(\varphi \mathbin{\mathcal{R}} \psi\) (\(\varphi\) releases \(\psi\)) under \(v\) if and only if it satisfies \(\psi\) and it satisfies \(\varphi\) or \(\mathbf{X}(\varphi \mathbin{\mathcal{R}} \psi)\), all under \(v\), where \(\mathbf{X}\) is the next operator.

theorem release_expansion :
    Satisfies valuation w (Formula.release φ ψ) ↔
      Satisfies valuation w ψ ∧
        (Satisfies valuation w φ ∨ Satisfies valuation w (.next (Formula.release φ ψ)))

Uses 4

Statement usesFormulas of linear temporal logic · The release operator of LTL · Satisfaction of LTL formulas on ω-words

Proof usesExpansion law for until

TheoremIdempotence of always#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and every LTL formula \(\varphi\), the word \(w\) satisfies \(\mathbf{G}\,\mathbf{G}\,\varphi\) under \(v\) if and only if it satisfies \(\mathbf{G}\,\varphi\) under \(v\), where \(\mathbf{G}\) is the always operator.

theorem always_always :
    Satisfies valuation w (Formula.always (Formula.always φ)) ↔
      Satisfies valuation w (Formula.always φ)

Uses 6

Statement usesFormulas of linear temporal logic · The always operator of LTL · Satisfaction of LTL formulas on ω-words

Proof usesThe eventually operator of LTL · Semantics of eventually · Satisfaction at a position

TheoremAlways eventually means infinitely often#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and every LTL formula \(\varphi\), the word \(w\) satisfies \(\mathbf{G}\,\mathbf{F}\,\varphi\) (always eventually \(\varphi\)) under \(v\) if and only if there are infinitely many \(k \in \mathbb{N}\) such that the suffix of \(w\) starting at position \(k\) satisfies \(\varphi\) under \(v\).

theorem always_eventually_iff :
    Satisfies valuation w (Formula.always (Formula.eventually φ)) ↔
      ∃ᶠ k in atTop, SatisfiesAt valuation w k φ

Uses 7 · Used by 1

Statement usesFormulas of linear temporal logic · The always operator of LTL · The eventually operator of LTL · Satisfaction of LTL formulas on ω-words · Satisfaction at a position

Proof usesSemantics of eventually · Satisfaction on a suffix

Used byThe infinitely-often automaton recognizes G F φ

TheoremEventually always means from some point on#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and every LTL formula \(\varphi\), the word \(w\) satisfies \(\mathbf{F}\,\mathbf{G}\,\varphi\) (eventually always \(\varphi\)) under \(v\) if and only if there is \(n \in \mathbb{N}\) such that for every \(k \ge n\) the suffix of \(w\) starting at position \(k\) satisfies \(\varphi\) under \(v\).

theorem eventually_always_iff :
    Satisfies valuation w (Formula.eventually (Formula.always φ)) ↔
      ∀ᶠ k in atTop, SatisfiesAt valuation w k φ

Uses 7 · Used by 1

Statement usesFormulas of linear temporal logic · The always operator of LTL · The eventually operator of LTL · Satisfaction of LTL formulas on ω-words · Satisfaction at a position

Proof usesSemantics of eventually · Satisfaction on a suffix

Used byThe eventually-always automaton recognizes F G φ

TheoremSatisfaction of an atom at a position#✓fully proved

Let \(v\) be a valuation of atoms on letters, \(w\) an ω-word, \(a\) an atom and \(k\) a natural number. The atomic formula \(a\) holds at position \(k\) of \(w\) under \(v\) if and only if \(v\) makes \(a\) true at the letter \(w(k)\).

theorem satisfiesAt_atom {k : ℕ} : SatisfiesAt valuation w k (.atom a) ↔ valuation (w k) a

Uses 2 · Used by 1

Statement usesFormulas of linear temporal logic · Satisfaction at a position

Used byLTL tableau accepts exactly the satisfying words

TheoremRelabelling the letters of an ω-word#✓fully proved

Let \(v\) be a valuation of atoms on letters of an alphabet \(\Sigma\), let \(f \colon \Sigma' \to \Sigma\) be a map, and let \(w\) be an ω-word over \(\Sigma'\). For every LTL formula \(\varphi\), the relabelled word \(i \mapsto f(w(i))\) satisfies \(\varphi\) under \(v\) if and only if \(w\) satisfies \(\varphi\) under the valuation that makes an atom \(a\) true at a letter \(s\) of \(\Sigma'\) exactly when \(v\) makes \(a\) true at \(f(s)\).

theorem satisfies_map {Symbol' : Type*} (f : Symbol' → Symbol) :
    ∀ (φ : Formula Atom) (w : ωSequence Symbol'),
      Satisfies valuation (w.map f) φ ↔ Satisfies (fun s a => valuation (f s) a) w φ

Uses 2

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words

TheoremMembership in the language of a formula#✓fully proved

For every valuation \(v\) of atoms on letters, every ω-word \(w\) and every LTL formula \(\varphi\), the word \(w\) belongs to the ω-language of \(\varphi\) under \(v\) if and only if \(w\) satisfies \(\varphi\) under \(v\).

@[simp]
theorem mem_language : w ∈ language valuation φ ↔ Satisfies valuation w φ

Uses 3 · Used by 6

Statement usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words · Language of an LTL formula

Used byBüchi automata for the restricted safety fragment · The infinitely-often automaton recognizes G F φ · The always automaton recognizes G φ · The eventually-always automaton recognizes F G φ · The propositional automaton recognizes φ · Büchi automaton accepts exactly the satisfying words

26 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.