Satisfiability of the modal μ-calculus

DefinitionSatisfiability of a closed modal μ-calculus formula#✓fully proved

A closed μ-calculus formula is satisfiable: some Kripke model has a world satisfying it under the empty environment.

def muSat (φ : Cslib.Modal.MuCalculus.MuFormula ℕ) : Prop :=
  ∃ (World : Type) (M : Cslib.Modal.KripkeModel World ℕ) (w : World),
    Cslib.Modal.MuCalculus.sat M (fun _ _ => False) φ w

inductive MuFormula (Atom : Type u) : Type u where
  | atom : Atom → MuFormula Atom
  | natom : Atom → MuFormula Atom
  | var : ℕ → MuFormula Atom
  | bot : MuFormula Atom
  | top : MuFormula Atom
  | and : MuFormula Atom → MuFormula Atom → MuFormula Atom
  | or : MuFormula Atom → MuFormula Atom → MuFormula Atom
  | box : MuFormula Atom → MuFormula Atom
  | dia : MuFormula Atom → MuFormula Atom
  | mu : MuFormula Atom → MuFormula Atom
  | nu : MuFormula Atom → MuFormula Atom

CSLibExt/Logics/Modal/MuCalculus.lean:55

structure KripkeModel (World : Type u) (Atom : Type v) where
  /-- There is at least one world. -/
  nonempty_world : Nonempty World
  /-- The accessibility relation. -/
  rel : World → World → Prop
  /-- The atoms true at each world. -/
  valuation : World → Atom → Prop

CSLibExt/Logics/Modal/Kripke.lean:83

def sat (env : ℕ → World → Prop) : MuFormula Atom → (World → Prop)
  | .atom a => fun w => M.valuation w a
  | .natom a => fun w => ¬ M.valuation w a
  | .var n => env n
  | .bot => fun _ => False
  | .top => fun _ => True
  | .and φ ψ => fun w => sat env φ w ∧ sat env ψ w
  | .or φ ψ => fun w => sat env φ w ∨ sat env ψ w
  | .box φ => fun w => ∀ v, M.rel w v → sat env φ v
  | .dia φ => fun w => ∃ v, M.rel w v ∧ sat env φ v
  | .mu φ => fun w => ∀ S : World → Prop,
      (∀ v, sat (extendEnv env S) φ v → S v) → S w
  ⋯

CSLibExt/Logics/Modal/MuCalculus.lean:124

Uses 3 · Used by 1

Statement usesKripke model · Formulas of the modal μ-calculus · Satisfaction in the modal μ-calculus

Used byModal μ-calculus satisfiability as a decision problem

DefinitionModal μ-calculus satisfiability as a decision problem#✓fully proved

Satisfiability of the modal μ-calculus as a decision problem over bitstrings: the input decodes to a formula token list, which decodes to a formula; the answer is whether that formula is closed and satisfiable.

noncomputable def muCalculusSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := List ℕ) x with
  | some toks =>
    match Cslib.Modal.MuCalculus.muDecodeList toks with
    | some φ =>
      if Cslib.Modal.MuCalculus.MuFormula.Closed φ ∧ muSat φ then true else false
    | none => false
  | none => false

abbrev DecisionProblem := List Bool → Bool

MathlibExt/Computability/Complexity.lean:170

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def muDecodeList (l : List ℕ) : Option (MuFormula ℕ) :=
  match muParseFuel (l.length + 1) l with
  | some (φ, []) => some φ
  | _ => none

CSLibExt/Logics/Modal/MuCalculusEncoding.lean:424

def Closed (φ : MuFormula Atom) : Prop := ClosedAt 0 φ

CSLibExt/Logics/Modal/MuCalculusEncoding.lean:68

def muSat (φ : Cslib.Modal.MuCalculus.MuFormula ℕ) : Prop :=
  ∃ (World : Type) (M : Cslib.Modal.KripkeModel World ℕ) (w : World),
    Cslib.Modal.MuCalculus.sat M (fun _ _ => False) φ w

WantedExt/Complexity/KeyTheorems/MuCalculusEXPTIMECompleteWanted.lean:55

Uses 13 · Used by 1

Statement usesFormulas of the modal μ-calculus · Closed modal μ-calculus formula · Decoding a modal μ-calculus token list to a formula · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Satisfiability of a closed modal μ-calculus formula · Decision problems

Used bySatisfiability of a modal μ-calculus formula is EXPTIME-complete

TheoremSatisfiability of a modal μ-calculus formula is EXPTIME-complete#●ready to prove

Sources: D. Kozen, "Results on the propositional μ-calculus", Theoretical Computer Science 27 (1983), 333-354; E. A. Emerson and C. S. Jutla, "Tree automata, μ-calculus and determinacy", FOCS 1991, 368-377.

public theorem_wanted mu_calculus_sat_exp_complete :
    muCalculusSatDec ∈ EXP ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ EXP → Cslib.CookLevin.PolyManyOneRed L muCalculusSatDec

noncomputable def muCalculusSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := List ℕ) x with
  | some toks =>
    match Cslib.Modal.MuCalculus.muDecodeList toks with
    | some φ =>
      if Cslib.Modal.MuCalculus.MuFormula.Closed φ ∧ muSat φ then true else false
    | none => false
  | none => false

WantedExt/Complexity/KeyTheorems/MuCalculusEXPTIMECompleteWanted.lean:63

def EXP : DecisionComplexityClass :=
  {L | ∃ d, langOf L ∈ Cslib.Turing.MultiTapeTM.DTIME (fun n => 2 ^ (n ^ d))}

CSLibExt/Computability/Complexity/Classes.lean:121

abbrev DecisionProblem := List Bool → Bool

MathlibExt/Computability/Complexity.lean:170

def PolyManyOneRed (L₁ L₂ : MetaMathlibExt.ComplexityTheory.DecisionProblem) : Prop :=
  ∃ reduce : List Bool → List Bool,
    MetaMathlibExt.ComplexityTheory.IsPolyTime reduce ∧ ∀ x, L₁ x = L₂ (reduce x)

CSLibExt/Computability/CookLevin.lean:396

Uses 5

Statement usesThe class EXP · Polynomial-time many-one reduction · Modal μ-calculus satisfiability as a decision problem · Complexity classes · Decision problems

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.