Büchi automata for a fragment of linear temporal logic

InductivePropositional formulas#✓fully proved

The propositional formulas over a set of atoms are generated by the atoms, the constant truth \(\top\), negation \(\neg\varphi\) and conjunction \(\varphi \wedge \psi\).

inductive PropFormula (Atom : Type*) where
  /-- An atom, true at a letter containing it. -/
  | atom (a : Atom) : PropFormula Atom
  /-- Truth. -/
  | top : PropFormula Atom
  /-- Negation. -/
  | not (φ : PropFormula Atom) : PropFormula Atom
  /-- Conjunction. -/
  | and (φ ψ : PropFormula Atom) : PropFormula Atom

Used by 13

Used byOne-state Büchi automaton for always φ · Evaluating a propositional formula at a letter · Bü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 for a propositional formula · The restricted safety fragment of LTL · Propositional formulas are evaluated at the current letter · Propositional formulas are evaluated at the first letter · Propositional formulas as LTL formulas · Safety formulas as LTL formulas

DefinitionEvaluating a propositional formula at a letter#✓fully proved

A letter is a set \(s\) of atoms (the atoms true at it). A propositional formula is evaluated at \(s\) by recursion: an atom \(a\) is true iff \(a \in s\), truth \(\top\) is true, \(\neg\varphi\) is true iff \(\varphi\) is not, and \(\varphi \wedge \psi\) is true iff both \(\varphi\) and \(\psi\) are true.

def eval : PropFormula Atom → Set Atom → Prop
  | .atom a, s => a ∈ s
  | .top, _ => True
  | .not φ, s => ¬ eval φ s
  | .and φ ψ, s => eval φ s ∧ eval ψ s

Uses 1 · Used by 8

Statement usesPropositional formulas

Used byOne-state Büchi automaton for always φ · 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 for a propositional formula · Propositional formulas are evaluated at the current letter · Propositional formulas are evaluated at the first letter

DefinitionPropositional formulas as LTL formulas#✓fully proved

The translation of propositional formulas into LTL formulas is defined by recursion: an atom \(a\) goes to the LTL atom \(a\), truth goes to the LTL truth constant \(\top\), \(\neg\varphi\) goes to the LTL negation of the translation of \(\varphi\), and \(\varphi \wedge \psi\) goes to the LTL conjunction of the translations of \(\varphi\) and \(\psi\).

def toLTL : PropFormula Atom → Formula Atom
  | .atom a => .atom a
  | .top => .top
  | .not φ => .not (toLTL φ)
  | .and φ ψ => .and (toLTL φ) (toLTL ψ)

Uses 2 · Used by 7

Statement usesFormulas of linear temporal logic · Propositional formulas

Used byThe 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 · Safety formulas as LTL formulas

TheoremPropositional formulas are evaluated at the first letter#✓fully proved

Let \(\varphi\) be a propositional formula and let \(w = w_0 w_1 w_2 \dots\) be an ω-word whose letters are sets of atoms. Under the valuation in which an atom holds at a letter exactly when it belongs to that letter, \(w\) satisfies the LTL translation of \(\varphi\) if and only if \(\varphi\) evaluates to true on the first letter \(w_0\).

theorem satisfies_toLTL (φ : PropFormula Atom) (w : ωSequence (Set Atom)) :
    Word.Satisfies (fun s a => a ∈ s) w φ.toLTL ↔ φ.eval (w 0)

Uses 4 · Used by 2

Statement usesPropositional formulas · Evaluating a propositional formula at a letter · Propositional formulas as LTL formulas · Satisfaction of LTL formulas on ω-words

Used byThe propositional automaton recognizes φ · Propositional formulas are evaluated at the current letter

TheoremPropositional formulas are evaluated at the current letter#✓fully proved

Let \(\varphi\) be a propositional formula, let \(w = w_0 w_1 w_2 \dots\) be an ω-word whose letters are sets of atoms, and let \(k \in \mathbb{N}\). Under the valuation in which an atom holds at a letter exactly when it belongs to that letter, the LTL translation of \(\varphi\) holds at position \(k\) of \(w\) if and only if \(\varphi\) evaluates to true on the letter \(w_k\).

theorem satisfiesAt_toLTL (φ : PropFormula Atom) (w : ωSequence (Set Atom)) (k : ℕ) :
    Word.SatisfiesAt (fun s a => a ∈ s) w k φ.toLTL ↔ φ.eval (w k)

Uses 7 · Used by 3

Statement usesPropositional formulas · Evaluating a propositional formula at a letter · Propositional formulas as LTL formulas · Satisfaction at a position

Proof usesFormulas of linear temporal logic · Satisfaction of LTL formulas on ω-words · Propositional formulas are evaluated at the first letter

Used byThe infinitely-often automaton recognizes G F φ · The always automaton recognizes G φ · The eventually-always automaton recognizes F G φ

16 fully proved

The always automaton

DefinitionOne-state Büchi automaton for always φ#✓fully proved

The one-state Büchi automaton for G φ with φ propositional: it stays forever, requiring every letter to satisfy φ.

def alwaysNa (φ : PropFormula Atom) : Buchi Unit (Set Atom) where
  Tr _ s _ := φ.eval s
  start := {()}
  accept := {()}

Uses 2 · Used by 2

Statement usesPropositional formulas · Evaluating a propositional formula at a letter

Used byBüchi automata for the restricted safety fragment · The always automaton recognizes G φ

TheoremThe always automaton recognizes G φ#✓fully proved

For a propositional formula \(\varphi\), the one-state Büchi automaton for \(\mathbf{G}\,\varphi\) accepts exactly the infinite words of letters (sets of atoms) that satisfy the LTL formula \(\mathbf{G}\,\varphi\), where an atom \(a\) holds at a letter \(s\) iff \(a \in s\).

theorem language_alwaysNa (φ : PropFormula Atom) :
    language (alwaysNa φ) =
      Word.language (fun s a => a ∈ s) (Formula.always φ.toLTL)

Uses 13 · Used by 1

Statement usesThe always operator of LTL · Propositional formulas · Propositional formulas as LTL formulas · Language of an LTL formula · One-state Büchi automaton for always φ

Proof usesFormulas of linear temporal logic · The eventually operator of LTL · Evaluating a propositional formula at a letter · Satisfaction of LTL formulas on ω-words · Semantics of eventually · Satisfaction at a position · Membership in the language of a formula · Propositional formulas are evaluated at the current letter

Used byBüchi automata for the restricted safety fragment

The G F / F G automata

TheoremThe infinitely-often automaton recognizes G F φ#✓fully proved

Let \(\varphi\) be a propositional formula and \(p\) the set of letters (sets of atoms) at which \(\varphi\) evaluates to true. The two-state Büchi automaton for “infinitely often \(p\)” accepts exactly the infinite words that satisfy the LTL formula \(\mathbf{G}\,\mathbf{F}\,\varphi\), where an atom \(a\) holds at a letter \(s\) iff \(a \in s\). Equivalently, a word is accepted iff \(\varphi\) holds at infinitely many positions.

theorem language_always_eventually (φ : PropFormula Atom) :
    language (infinitelyOftenNa {s | φ.eval s}) =
      Word.language (fun s a => a ∈ s) (Formula.always (Formula.eventually φ.toLTL))

Uses 13

Statement usesThe always operator of LTL · The eventually operator of LTL · Propositional formulas · Evaluating a propositional formula at a letter · Propositional formulas as LTL formulas · Language of an LTL formula · Two-state Büchi automaton for “infinitely often”

Proof usesSatisfaction of LTL formulas on ω-words · Always eventually means infinitely often · Satisfaction at a position · Membership in the language of a formula · Propositional formulas are evaluated at the current letter · Infinitely often

TheoremThe eventually-always automaton recognizes F G φ#✓fully proved

Let \(\varphi\) be a propositional formula and \(p\) the set of letters (sets of atoms) at which \(\varphi\) evaluates to true. The two-state Büchi automaton for “eventually always \(p\)” accepts exactly the infinite words that satisfy the LTL formula \(\mathbf{F}\,\mathbf{G}\,\varphi\), where an atom \(a\) holds at a letter \(s\) iff \(a \in s\). Equivalently, a word is accepted iff \(\varphi\) holds at all but finitely many positions.

theorem language_eventually_always (φ : PropFormula Atom) :
    language (eventuallyAlwaysNa {s | φ.eval s}) =
      Word.language (fun s a => a ∈ s)
        (Formula.eventually (Formula.always φ.toLTL))

Uses 13

Statement usesThe always operator of LTL · The eventually operator of LTL · Propositional formulas · Evaluating a propositional formula at a letter · Propositional formulas as LTL formulas · Language of an LTL formula · Two-state Büchi automaton for “eventually always”

Proof usesSatisfaction of LTL formulas on ω-words · Eventually always means from some point on · Satisfaction at a position · Membership in the language of a formula · Propositional formulas are evaluated at the current letter · Eventually always

The propositional automaton

DefinitionBüchi automaton for a propositional formula#✓fully proved

For a propositional formula \(\varphi\), this Büchi automaton over letters that are sets of atoms has a start state \(u\) and two verdict states \(t\) and \(f\), of which only \(t\) is accepting. From \(u\), on a letter \(s\) it moves to \(t\) if \(\varphi\) evaluates to true at \(s\) and to \(f\) otherwise; from \(t\) and from \(f\) it stays in the same state on every letter. So it records the verdict of \(\varphi\) on the first letter.

def propNa (φ : PropFormula Atom) : Buchi (Option Bool) (Set Atom) where
  Tr p x q :=
    (∃ b, p = none ∧ q = some b ∧ ((b = true ∧ φ.eval x) ∨ (b = false ∧ ¬ φ.eval x))) ∨
      (∃ b, p = some b ∧ q = some b)
  start := {none}
  accept := {some true}

Uses 2 · Used by 2

Statement usesPropositional formulas · Evaluating a propositional formula at a letter

Used byBüchi automata for the restricted safety fragment · The propositional automaton recognizes φ

TheoremThe propositional automaton recognizes φ#✓fully proved

For a propositional formula \(\varphi\), the three-state Büchi automaton for \(\varphi\) accepts exactly the infinite words of letters (sets of atoms) that satisfy \(\varphi\) read as an LTL formula, where an atom \(a\) holds at a letter \(s\) iff \(a \in s\).

theorem language_propNa (φ : PropFormula Atom) :
    language (propNa φ) =
      Word.language (fun s a => a ∈ s) φ.toLTL

Uses 8 · Used by 1

Statement usesPropositional formulas · Propositional formulas as LTL formulas · Language of an LTL formula · Büchi automaton for a propositional formula

Proof usesEvaluating a propositional formula at a letter · Satisfaction of LTL formulas on ω-words · Membership in the language of a formula · Propositional formulas are evaluated at the first letter

Used byBüchi automata for the restricted safety fragment

The shift automaton

DefinitionThe shift of a Büchi automaton#✓fully proved

Let \(A\) be a Büchi automaton over the alphabet of sets of atoms. Its shift is the Büchi automaton whose states are the states of \(A\) together with one new state \(\bot\), whose only start state is \(\bot\), and whose accepting states are the accepting states of \(A\). Its transitions are exactly the following: on every letter, from \(\bot\) to each start state of \(A\); and on a letter \(x\), from a state \(q\) of \(A\) to a state \(q'\) of \(A\) whenever \(A\) has a transition from \(q\) to \(q'\) on \(x\).

The shift accepts a word exactly when \(A\) accepts the word with its first letter removed.

def shiftBuchi (a : Buchi State (Set Atom)) : Buchi (Option State) (Set Atom) where
  Tr p x q :=
    (∃ s, p = none ∧ q = some s ∧ s ∈ a.start) ∨
      (∃ s s', p = some s ∧ q = some s' ∧ a.Tr s x s')
  start := {none}
  accept := some '' a.accept

Used by 2

Used byBüchi automata for the restricted safety fragment · The shift automaton reads the tail

TheoremThe shift automaton reads the tail#✓fully proved

For a Büchi automaton \(A\) over letters that are sets of atoms, the shift automaton of \(A\) accepts an infinite word \(x_0 x_1 x_2 \ldots\) iff \(A\) accepts its tail \(x_1 x_2 x_3 \ldots\).

theorem language_shiftBuchi (a : Buchi State (Set Atom)) :
    language (shiftBuchi a) = {xs : ωSequence (Set Atom) | xs.tail ∈ language a}

Uses 1 · Used by 1

Statement usesThe shift of a Büchi automaton

Used byBüchi automata for the restricted safety fragment

The safety fragment

InductiveThe restricted safety fragment of LTL#✓fully proved

The safety formulas over a type of atoms are generated by the following rules: every propositional formula \(\varphi\) is a safety formula; if \(\psi\) and \(\rho\) are safety formulas, then so are \(\psi \wedge \rho\), \(\psi \vee \rho\) and \(X\,\psi\) (next \(\psi\)); and for every propositional formula \(\varphi\), \(G\,\varphi\) (always \(\varphi\)) is a safety formula.

The operator \(G\) is applied only to propositional formulas: for atoms \(p\) and \(q\), the formula \(G(p \vee X\,q)\) is not in this fragment, since \(G\) does not distribute over \(\vee\).

inductive Safety (Atom : Type*) where
  /-- A propositional formula, checked on the first letter. -/
  | prop (φ : PropFormula Atom) : Safety Atom
  /-- Conjunction. -/
  | and (ψ ρ : Safety Atom) : Safety Atom
  /-- Disjunction. -/
  | or (ψ ρ : Safety Atom) : Safety Atom
  /-- Next. -/
  | next (ψ : Safety Atom) : Safety Atom
  /-- `always` of a propositional formula. -/
  | alwaysProp (φ : PropFormula Atom) : Safety Atom

Uses 1 · Used by 2

Statement usesPropositional formulas

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

DefinitionSafety formulas as LTL formulas#✓fully proved

The translation \(t\) of safety formulas into LTL formulas is defined by recursion: \(t(\varphi)\) is the LTL translation of \(\varphi\) for a propositional formula \(\varphi\); \(t(\psi \wedge \rho) = t(\psi) \wedge t(\rho)\); \(t(\psi \vee \rho) = \neg(\neg t(\psi) \wedge \neg t(\rho))\), the derived LTL disjunction; \(t(X\,\psi) = X\,t(\psi)\), where \(X\) is next; and \(t(G\,\varphi) = G\,t(\varphi)\) for a propositional formula \(\varphi\), where \(G\) is the derived LTL operator always.

def toLTL : Safety Atom → Formula Atom
  | .prop φ => φ.toLTL
  | .and ψ ρ => .and ψ.toLTL ρ.toLTL
  | .or ψ ρ => Formula.or ψ.toLTL ρ.toLTL
  | .next ψ => .next ψ.toLTL
  | .alwaysProp φ => Formula.always φ.toLTL

Uses 6 · Used by 1

Statement usesFormulas of linear temporal logic · The always operator of LTL · Disjunction in LTL · Propositional formulas · Propositional formulas as LTL formulas · The restricted safety fragment of LTL

Used byBüchi automata for the restricted safety fragment

TheoremBüchi automata for the restricted safety fragment#✓fully proved

Take as letters the sets of atoms, an atom \(a\) holding at a letter \(s\) iff \(a \in s\). For every formula \(\psi\) of the restricted safety fragment there is a nondeterministic Büchi automaton with finitely many states whose ω-language is exactly the set of infinite words satisfying \(\psi\), read as an LTL formula.

The finite state set is what makes the automaton a certificate of ω-regularity: every ω-language is accepted by some Büchi automaton with infinitely many states. The fragment applies the always operator \(\mathbf{G}\) only to propositional formulas, so for example \(\mathbf{G}(p \vee \mathbf{X}\,q)\), for atoms \(p\) and \(q\) and the next operator \(\mathbf{X}\), is not covered.

theorem exists_buchi_of_safety (ψ : Safety Atom) :
    ∃ (S : Type) (_ : Finite S) (a : Buchi S (Set Atom)),
      language a = Word.language (fun s a => a ∈ s) ψ.toLTL

Uses 15

Statement usesThe restricted safety fragment of LTL · Safety formulas as LTL formulas · Language of an LTL formula

Proof usesFormulas of linear temporal logic · Disjunction in LTL · Propositional formulas · Satisfaction of LTL formulas on ω-words · Satisfaction at a position · Membership in the language of a formula · One-state Büchi automaton for always φ · The always automaton recognizes G φ · The propositional automaton recognizes φ · The shift automaton reads the tail · Büchi automaton for a propositional formula · The shift of a Büchi automaton

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.