Satisfiability and model checking for the linear-time μ-calculus

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

A closed linear μ-calculus formula is satisfiable: some word and position satisfy it under the empty environment.

def linearMuSat (φ : Cslib.Modal.LinearMuCalculus.LinearMuFormula ℕ) : Prop :=
  ∃ (val : ℕ → ℕ → Prop) (n : ℕ),
    Cslib.Modal.LinearMuCalculus.sat val (fun _ _ => False) φ n

Uses 2 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Satisfaction of linear μ-calculus formulas

Used byLinear μ-calculus satisfiability as a decision problem

DefinitionValidity of a closed linear μ-calculus formula#✓fully proved

A closed linear μ-calculus formula is valid: every word and position satisfy it under the empty environment.

def linearMuValid (φ : Cslib.Modal.LinearMuCalculus.LinearMuFormula ℕ) : Prop :=
  ∀ (val : ℕ → ℕ → Prop) (n : ℕ),
    Cslib.Modal.LinearMuCalculus.sat val (fun _ _ => False) φ n

Uses 2 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Satisfaction of linear μ-calculus formulas

Used byLinear μ-calculus validity as a decision problem

DefinitionLinear μ-calculus model checking on a finite Kripke structure#✓fully proved

Model checking a linear μ-calculus formula against a finite Kripke structure: every infinite path π from start following edges satisfies φ at position 0, where the path turns the structure's valuation worldVal into a word valuation.

def linearMuModelCheck (edges : List (ℕ × ℕ)) (worldVal : ℕ → ℕ → Prop)
    (start : ℕ) (φ : Cslib.Modal.LinearMuCalculus.LinearMuFormula ℕ) : Prop :=
  ∀ π : ℕ → ℕ, π 0 = start ∧ (∀ t, (π t, π (t + 1)) ∈ edges) →
    Cslib.Modal.LinearMuCalculus.sat (fun t a => worldVal (π t) a)
      (fun _ _ => False) φ 0

Uses 2 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Satisfaction of linear μ-calculus formulas

Used byLinear μ-calculus model checking as a decision problem

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

Satisfiability of the linear μ-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 linearMuSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := List ℕ) x with
  | some toks =>
    match Cslib.Modal.LinearMuCalculus.linearMuDecodeList toks with
    | some φ =>
      if Cslib.Modal.LinearMuCalculus.LinearMuFormula.Closed φ ∧ linearMuSat φ
      then true else false
    | none => false
  | none => false

Uses 13 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Closed linear μ-calculus formula · Decoding a linear μ-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 linear μ-calculus formula · Decision problems

Used byThe model checking, satisfiability and validity problems of the linear modal μ-calculus are PSPACE-complete

DefinitionLinear μ-calculus validity as a decision problem#✓fully proved

Validity of the linear μ-calculus as a decision problem over bitstrings.

noncomputable def linearMuValidDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode (α := List ℕ) x with
  | some toks =>
    match Cslib.Modal.LinearMuCalculus.linearMuDecodeList toks with
    | some φ =>
      if Cslib.Modal.LinearMuCalculus.LinearMuFormula.Closed φ ∧ linearMuValid φ
      then true else false
    | none => false
  | none => false

Uses 13 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Closed linear μ-calculus formula · Decoding a linear μ-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 · Validity of a closed linear μ-calculus formula · Decision problems

Used byThe model checking, satisfiability and validity problems of the linear modal μ-calculus are PSPACE-complete

DefinitionLinear μ-calculus model checking as a decision problem#✓fully proved

Model checking of the linear μ-calculus as a decision problem over bitstrings: the input decodes to (n, edges, worldVals, start, tokens), where worldVals lists, per world, the atoms true at that world; the answer is whether the decoded formula is closed, the structure is well-formed and total (every world has a successor world, so the path quantification is not vacuous at deadlocks), and every path from start satisfies the formula.

noncomputable def linearMuModelCheckDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List (ℕ × ℕ) × List (List ℕ) × ℕ × List ℕ) x with
  | some (n, edges, worldVals, start, toks) =>
    match Cslib.Modal.LinearMuCalculus.linearMuDecodeList toks with
    | some φ =>
      if Cslib.Modal.LinearMuCalculus.LinearMuFormula.Closed φ ∧ start < n ∧
          (∀ e ∈ edges, e.1 < n ∧ e.2 < n) ∧
          (∀ w, w < n → ∃ v, v < n ∧ (w, v) ∈ edges) ∧
          linearMuModelCheck edges (fun w a => a ∈ worldVals.getD w []) start φ
      then true else false
    | none => false
  | none => false

Uses 13 · Used by 1

Statement usesFormulas of the linear-time μ-calculus · Closed linear μ-calculus formula · Decoding a linear μ-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 · Linear μ-calculus model checking on a finite Kripke structure · Decision problems

Used byThe model checking, satisfiability and validity problems of the linear modal μ-calculus are PSPACE-complete

TheoremThe model checking, satisfiability and validity problems of the linear modal μ-calculus are PSPACE-complete#●ready to prove

The model checking, satisfiability and validity problems of the linear modal μ-calculus are PSPACE-complete, like for linear temporal logic. Source: M. Y. Vardi, "A temporal fixpoint calculus", POPL 1988, 250-259; cf. A. P. Sistla and E. M. Clarke, "The complexity of propositional linear temporal logics", JACM 32 (1985), 733-749.

public theorem_wanted linear_mu_calculus_pspace_complete :
    (linearMuSatDec ∈ PSPACE ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ PSPACE → Cslib.CookLevin.PolyManyOneRed L linearMuSatDec) ∧
    (linearMuValidDec ∈ PSPACE ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ PSPACE → Cslib.CookLevin.PolyManyOneRed L linearMuValidDec) ∧
    (linearMuModelCheckDec ∈ PSPACE ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ PSPACE → Cslib.CookLevin.PolyManyOneRed L linearMuModelCheckDec)

Uses 7

Statement usesPolynomial space for decision problems · Polynomial-time many-one reduction · Linear μ-calculus model checking as a decision problem · Linear μ-calculus satisfiability as a decision problem · Linear μ-calculus validity as a decision problem · Complexity classes · Decision problems

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.