Documentation

LeanPool.LeanModelChecking.LTLNNF

Negation normal form for Linear Temporal Logic #

We define negation normal form (NNF) formulas, their language, and a translation LTL.toNNF from LTL formulas to equivalent NNF formulas. The main result LTL.exists_equiv_nnf shows every LTL formula has an equivalent NNF formula.

source
inductive LeanModelChecking.NNF (AP : Type) :
Type

Linear temporal logic formulas in negation normal form over atomic propositions AP: negation is pushed to the atoms (atom/not_atom), and the temporal operators are next, until, and the dual release.

Instances For
    source
    def LeanModelChecking.instDecidableEqNNF.decEq {AP✝ : Type} [DecidableEq AP✝] (x✝ x✝¹ : NNF AP✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance LeanModelChecking.instDecidableEqNNF {AP✝ : Type} [DecidableEq AP✝] :
      DecidableEq (NNF AP✝)
      Equations
      source
      def LeanModelChecking.NNF.language {AP : Type} (f : NNF AP) (w : ℕ → Letter AP) :
      Prop

      The language of an NNF formula: the predicate on infinite words w that holds exactly when w satisfies f at position 0.

      Equations
      Instances For
        source
        theorem LeanModelChecking.not_exists_until_iff_forall {P Q : ℕ → Prop} :
        (¬∃ (i : ℕ), Q i ∧ ∀ (k : ℕ), k < i → P k) ↔ ∀ (i : ℕ), ¬Q i ∨ ∃ (k : ℕ), k < i ∧ ¬P k
        source
        def LeanModelChecking.LTL.toNNFCore {AP : Type} :
        Bool → LTL AP → NNF AP

        Translate an LTL formula to an NNF formula, optionally negated: the Boolean flag, when true, requests the NNF of the negation of the formula, allowing negation to be pushed down to the atoms recursively.

        Equations
        Instances For
          source
          def LeanModelChecking.LTL.toNNF {AP : Type} (f : LTL AP) :
          NNF AP

          The NNF formula equivalent to the LTL formula f.

          Equations
          Instances For
            source
            def LeanModelChecking.LTL.toNNFNeg {AP : Type} (f : LTL AP) :
            NNF AP

            The NNF formula equivalent to the negation of the LTL formula f.

            Equations
            Instances For
              source
              theorem LeanModelChecking.LTL.toNNFCore_sound {AP : Type} (f : LTL AP) :
              (∀ (w : ℕ → Letter AP), f.language w ↔ f.toNNF.language w) ∧ ∀ (w : ℕ → Letter AP), ¬f.language w ↔ f.toNNFNeg.language w
              source
              theorem LeanModelChecking.LTL.exists_equiv_nnf {AP : Type} (ψ : LTL AP) :
              ∃ (nnf : NNF AP), ψ.language = nnf.language