Modal μ-calculus

InductiveFormulas of the modal μ-calculus#✓fully proved

The formulas over a type of atoms are built from atoms \(a\), negated atoms \(\neg a\), variables \(X_n\) for \(n \in \mathbb{N}\) (de Bruijn indices for the fixed-point binders), \(\bot\) and \(\top\) by conjunction \(\varphi \wedge \psi\), disjunction \(\varphi \vee \psi\), the modalities \(\Box\varphi\) and \(\Diamond\varphi\), and the fixed-point binders \(\mu\varphi\) and \(\nu\varphi\).

There is no negation of arbitrary formulas. Negated atoms are present so that the meta-level negation, which swaps each connective with its dual, is an involution.

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

Used by 101

Used byThe μ-calculus formula \(\mathsf{AG}\,p\) · \(\mathsf{AG}\) is universal reachability · Closed modal μ-calculus formula · μ-calculus formula closed at a given binding depth · Depth of a modal μ-calculus formula · Depth of a μ-calculus formula is at most its number code · The μ-calculus formula \(\mathsf{EF}\,p\) · \(\mathsf{EF}\) is reachability · Cantor-pairing number code of a μ-calculus formula · Injectivity of the μ-calculus number code · Decoding a μ-calculus number code to a formula · Fuelled decoding of a μ-calculus number code · Fuelled decoding inverts the μ-calculus number code · Decoding a modal μ-calculus token list to a formula · Token-list decoding inverts modal μ-calculus token encoding · Decoding inverts the μ-calculus number code · Park induction · The least fixed point is contained in its unfolding · The formula \(\mu X.\, \mu Y.\, X\) is false everywhere · The fixed-point operator of a formula · Fuelled parser for modal μ-calculus token lists · Fuelled parsing inverts modal μ-calculus token encoding · The least fixed point is a pre-fixed point · Polynomial-size token-list encoding of μ-calculus formulas · Negation of μ-calculus formulas · Meta-level negation is an involution · Coinduction for the greatest fixed point · The greatest fixed point is a pre-fixed point · The formula \(\nu X.\, \nu Y.\, X\) is true everywhere · The greatest fixed point is a post-fixed point · Satisfaction in the modal μ-calculus · Denotation of a closed μ-calculus formula is environment-independent · Satisfaction is monotone in the environment · Monotonicity in the bound variable · The μ formula denotes the least fixed point · The μ unfolding · Duality · The ν formula denotes the greatest fixed point · The ν unfolding · Canonical next move induced by a bespoke strategy · Verifier's positional strategies make a game move at Verifier positions that have one · The canonical move follows the bespoke strategy at Verifier positions with a move · Segments of canonical plays through fragment positions are bespoke plays · Step map of the regression play · The regression play is a play · Starting position of the regression play · Second position of the regression play · Third position of the regression play · Closed formulas · Formulas closed at depth \(d\) · A least fixpoint over a vacuous greatest fixpoint · \(\mu X.\, \nu Y.\, X\) is false in the one-world model · Moves from a diamond position · Moves of the totalized fragment game · Moves of the totalized fragment game, by cases · Projection of game positions onto the fragment arena · Projection of an embedded position · Owners in the totalized fragment game · Owner of an embedded position in the totalized fragment game · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Game position of a fragment position · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Fragment parity game · Wins is the winning region of the fragment game · Position of the μ-calculus model-checking game · The losing state is absorbing · Closedness is monotone in the depth · Moves of the μ-calculus model-checking game · Fragment moves decrease the formula size · No infinite play from a fragment position · Inversion for disjunction moves · Owner of a game position · Fragment moves between embedded positions are game moves · Moves to the losing state come from terminal losing positions · Moves to the winning state come from terminal winning positions · Priority of a game position · Closed formulas are environment-independent · Satisfaction depends only on the environment below the closure depth · Size of a μ-calculus formula · Winner at a terminal position · Embedding of the fixpoint-free fragment into the μ-calculus · The fixpoint-free embedding is injective · Partial inverse of the fixpoint-free embedding · The partial inverse recovers fixpoint-free formulas · The embedding inverts the partial inverse · Game-vs-satisfaction, converse direction · The absorbing win state · Backward-induction winning equals satisfaction on the fixpoint-free fragment · Backward-induction winning equals game winning on the fixpoint-free fragment · Game-vs-satisfaction, strategy direction · Wins-guided move · The Wins-guided move at a diamond · The Wins-guided move is legal · The Wins-guided move at a disjunction · Wins-guided strategy · Wins-guided strategy wins every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction) · Modal μ-calculus satisfiability as a decision problem · Satisfiability of a closed modal μ-calculus formula

DefinitionNegation of μ-calculus formulas#✓fully proved

The meta-level negation \(\neg\varphi\) of a μ-calculus formula \(\varphi\) swaps each connective with its dual. It is defined by recursion: an atom \(p\) becomes the negated atom \(\overline{p}\) and \(\overline{p}\) becomes \(p\), each variable \(x_n\) stays \(x_n\), \(\neg\bot = \top\), \(\neg\top = \bot\), \(\neg(\varphi \wedge \psi) = \neg\varphi \vee \neg\psi\), \(\neg(\varphi \vee \psi) = \neg\varphi \wedge \neg\psi\), \(\neg\Box\varphi = \Diamond\neg\varphi\), \(\neg\Diamond\varphi = \Box\neg\varphi\), \(\neg\mu\varphi = \nu\neg\varphi\) and \(\neg\nu\varphi = \mu\neg\varphi\).

def neg : MuFormula Atom → MuFormula Atom
  | .atom a => .natom a
  | .natom a => .atom a
  | .var n => .var n
  | .bot => .top
  | .top => .bot
  | .and φ ψ => .or (neg φ) (neg ψ)
  | .or φ ψ => .and (neg φ) (neg ψ)
  | .box φ => .dia (neg φ)
  | .dia φ => .box (neg φ)
  | .mu φ => .nu (neg φ)
  | .nu φ => .mu (neg φ)

Uses 1 · Used by 2

Statement usesFormulas of the modal μ-calculus

Used byMeta-level negation is an involution · Duality

TheoremMeta-level negation is an involution#✓fully proved

Write \(\neg\varphi\) for the meta-level negation of a μ-calculus formula \(\varphi\), which swaps each connective with its dual. For every μ-calculus formula \(\varphi\), negating twice gives back \(\varphi\): \(\neg\neg\varphi = \varphi\).

theorem neg_neg : ∀ (φ : MuFormula Atom), (neg (neg φ)) = φ

Uses 2

Statement usesFormulas of the modal μ-calculus · Negation of μ-calculus formulas

DefinitionExtending an environment under a binder#✓fully proved

An environment \(\rho\) assigns to each variable index \(n \in \mathbb{N}\) a predicate \(\rho(n)\) on worlds. Its extension by a predicate \(S\) on worlds is the environment that assigns \(S\) to index \(0\) and \(\rho(n)\) to index \(n + 1\).

With de Bruijn indices, variable \(1\) inside a binder thus refers to the enclosing binder.

def extendEnv {World : Type*} (env : ℕ → World → Prop) (S : World → Prop) :
    ℕ → World → Prop
  | 0 => S
  | n + 1 => env n

Used by 22

Used by\(\mathsf{AG}\) is universal reachability · \(\mathsf{EF}\) is reachability · Complementing an extended environment · Park induction · The least fixed point is contained in its unfolding · The formula \(\mu X.\, \mu Y.\, X\) is false everywhere · The fixed-point operator of a formula · The least fixed point is a pre-fixed point · Coinduction for the greatest fixed point · The greatest fixed point is a pre-fixed point · The formula \(\nu X.\, \nu Y.\, X\) is true everywhere · The greatest fixed point is a post-fixed point · Satisfaction in the modal μ-calculus · Denotation of a closed μ-calculus formula is environment-independent · Satisfaction is monotone in the environment · Monotonicity in the bound variable · The μ unfolding · Duality · The ν formula denotes the greatest fixed point · The ν unfolding · \(\mu X.\, \nu Y.\, X\) is false in the one-world model · Satisfaction depends only on the environment below the closure depth

DefinitionSatisfaction in the modal μ-calculus#✓fully proved

Let \(M\) be a Kripke model with accessibility relation \(R\) and valuation \(V\), and let \(\rho\) be an environment assigning a set of worlds to each variable index \(n \in \mathbb{N}\). For a set of worlds \(S\), write \(\rho[0 \mapsto S]\) for the environment sending index \(0\) to \(S\) and index \(n + 1\) to \(\rho(n)\). The set \([\![\varphi]\!]_\rho\) of worlds satisfying a formula \(\varphi\) in \(M\) under \(\rho\) is defined by recursion on \(\varphi\): an atom \(a\) holds at \(w\) when \(V\) makes \(a\) true at \(w\), and the negated atom of \(a\) when \(V\) does not; the variable with index \(n\) denotes \(\rho(n)\); \(\bot\) holds nowhere and \(\top\) everywhere; conjunction and disjunction denote intersection and union; \(\Box\varphi\) holds at \(w\) when \(\varphi\) holds at every \(v\) with \(w \mathrel{R} v\), and \(\Diamond\varphi\) when \(\varphi\) holds at some such \(v\); \(\mu\varphi\) holds at \(w\) when \(w \in S\) for every set of worlds \(S\) with \([\![\varphi]\!]_{\rho[0 \mapsto S]} \subseteq S\); and \(\nu\varphi\) holds at \(w\) when \(w \in S\) for some set of worlds \(S\) with \(S \subseteq [\![\varphi]\!]_{\rho[0 \mapsto S]}\).

So \(\mu\varphi\) is the least pre-fixed point of \(S \mapsto [\![\varphi]\!]_{\rho[0 \mapsto S]}\), stated directly as an infimum over pre-fixed points, and \(\nu\varphi\) is the greatest post-fixed point, stated as a supremum over post-fixed points.

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
  | .nu φ => fun w => ∃ S : World → Prop,
      (∀ v, S v → sat (extendEnv env S) φ v) ∧ S w

Uses 3 · Used by 24

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder

Used by\(\mathsf{AG}\) is universal reachability · \(\mathsf{EF}\) is reachability · Park induction · The least fixed point is contained in its unfolding · The formula \(\mu X.\, \mu Y.\, X\) is false everywhere · The fixed-point operator of a formula · The least fixed point is a pre-fixed point · Coinduction for the greatest fixed point · The greatest fixed point is a pre-fixed point · The formula \(\nu X.\, \nu Y.\, X\) is true everywhere · The greatest fixed point is a post-fixed point · Denotation of a closed μ-calculus formula is environment-independent · Satisfaction is monotone in the environment · Monotonicity in the bound variable · The μ formula denotes the least fixed point · The μ unfolding · Duality · The ν formula denotes the greatest fixed point · The ν unfolding · \(\mu X.\, \nu Y.\, X\) is false in the one-world model · Closed formulas are environment-independent · Satisfaction depends only on the environment below the closure depth · Backward-induction winning equals satisfaction on the fixpoint-free fragment · Satisfiability of a closed modal μ-calculus formula

TheoremSatisfaction is monotone in the environment#✓fully proved

Let \(M\) be a Kripke model and let \(\rho\) and \(\rho'\) be environments (each assigns a set of worlds of \(M\) to every variable \(n\)) with \(\rho(n) \subseteq \rho'(n)\) for every \(n\). Then every μ-calculus formula \(\varphi\) holds under \(\rho'\) at every world of \(M\) where it holds under \(\rho\): enlarging every variable's denotation can only enlarge a formula's denotation.

theorem sat_mono_env : ∀ (φ : MuFormula Atom) {env env' : ℕ → World → Prop},
    (∀ n, env n ≤ env' n) → sat M env φ ≤ sat M env' φ

Uses 4 · Used by 1

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

Proof usesExtending an environment under a binder

Used byMonotonicity in the bound variable

TheoremMonotonicity in the bound variable#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment assigning a set of worlds to each variable index \(n \in \mathbb{N}\), and \(\varphi\) a μ-calculus formula. For a set of worlds \(S\), write \(\rho[0 \mapsto S]\) for the environment sending index \(0\) to \(S\) and index \(n + 1\) to \(\rho(n)\). If \(S_1 \subseteq S_2\) are sets of worlds, then every world that satisfies \(\varphi\) in \(M\) under \(\rho[0 \mapsto S_1]\) also satisfies \(\varphi\) in \(M\) under \(\rho[0 \mapsto S_2]\).

theorem sat_mono_extend {env : ℕ → World → Prop} {S₁ S₂ : World → Prop} (h : S₁ ≤ S₂)
    (φ : MuFormula Atom) :
    sat M (extendEnv env S₁) φ ≤ sat M (extendEnv env S₂) φ

Uses 5 · Used by 5

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Proof usesSatisfaction is monotone in the environment

Used byThe least fixed point is contained in its unfolding · The fixed-point operator of a formula · The least fixed point is a pre-fixed point · The greatest fixed point is a pre-fixed point · The greatest fixed point is a post-fixed point

TheoremThe least fixed point is a pre-fixed point#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment and \(\varphi\) a μ-calculus formula. Write \(\llbracket\psi\rrbracket_\sigma\) for the set of worlds of \(M\) at which \(\psi\) holds under the environment \(\sigma\), and \(\rho[S]\) for the extension of \(\rho\) under a binder by a set of worlds \(S\) (variable \(0\) denotes \(S\) and variable \(n + 1\) denotes \(\rho(n)\)). For \(T = \llbracket\mu\varphi\rrbracket_\rho\), where \(\mu\varphi\) binds variable \(0\) of \(\varphi\), we have \(\llbracket\varphi\rrbracket_{\rho[T]} \subseteq T\).

theorem mu_pre_fixed (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M (extendEnv env (sat M env (.mu φ))) φ ≤ sat M env (.mu φ)

Uses 5 · Used by 3

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Proof usesMonotonicity in the bound variable

Used byThe least fixed point is contained in its unfolding · The μ formula denotes the least fixed point · The μ unfolding

TheoremThe least fixed point is contained in its unfolding#✓fully proved

For every Kripke model \(M\), environment \(\rho\) and μ-calculus formula \(\varphi\), every world satisfying \(\mu\varphi\) in \(\rho\) also satisfies \(\varphi\) in the extension of \(\rho\) by the set of worlds satisfying \(\mu\varphi\) in \(\rho\).

theorem mu_le_fixed (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M env (.mu φ) ≤ sat M (extendEnv env (sat M env (.mu φ))) φ

Uses 6 · Used by 1

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Proof usesThe least fixed point is a pre-fixed point · Monotonicity in the bound variable

Used byThe μ unfolding

TheoremThe μ unfolding#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment assigning a set of worlds to each variable index \(n \in \mathbb{N}\), and \(\varphi\) a μ-calculus formula. Let \(A\) be the set of worlds satisfying \(\mu\varphi\) in \(M\) under \(\rho\). Then \(A\) is exactly the set of worlds satisfying \(\varphi\) in \(M\) under the environment that sends index \(0\) to \(A\) and index \(n + 1\) to \(\rho(n)\).

theorem sat_mu_unfold (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M env (.mu φ) = sat M (extendEnv env (sat M env (.mu φ))) φ

Uses 6 · Used by 2

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Proof usesThe least fixed point is contained in its unfolding · The least fixed point is a pre-fixed point

Used by\(\mathsf{EF}\) is reachability · Duality

TheoremThe greatest fixed point is a post-fixed point#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment and \(\varphi\) a μ-calculus formula. Write \(\llbracket\psi\rrbracket_\sigma\) for the set of worlds of \(M\) at which \(\psi\) holds under the environment \(\sigma\), and \(\rho[S]\) for the extension of \(\rho\) under a binder by a set of worlds \(S\) (variable \(0\) denotes \(S\) and variable \(n + 1\) denotes \(\rho(n)\)). For \(T = \llbracket\nu\varphi\rrbracket_\rho\), where \(\nu\varphi\) binds variable \(0\) of \(\varphi\), we have \(T \subseteq \llbracket\varphi\rrbracket_{\rho[T]}\).

theorem nu_post_fixed (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M env (.nu φ) ≤ sat M (extendEnv env (sat M env (.nu φ))) φ

Uses 5 · Used by 2

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Proof usesMonotonicity in the bound variable

Used byThe greatest fixed point is a pre-fixed point · The ν unfolding

TheoremThe greatest fixed point is a pre-fixed point#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment and \(\varphi\) a μ-calculus formula. Write \(\llbracket\psi\rrbracket_\sigma\) for the set of worlds of \(M\) at which \(\psi\) holds under the environment \(\sigma\), and \(\rho[S]\) for the extension of \(\rho\) under a binder by a set of worlds \(S\) (variable \(0\) denotes \(S\) and variable \(n + 1\) denotes \(\rho(n)\)). For \(T = \llbracket\nu\varphi\rrbracket_\rho\), where \(\nu\varphi\) binds variable \(0\) of \(\varphi\), we have \(\llbracket\varphi\rrbracket_{\rho[T]} \subseteq T\).

theorem nu_le_post_fixed (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M (extendEnv env (sat M env (.nu φ))) φ ≤ sat M env (.nu φ)

Uses 6 · Used by 1

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Proof usesThe greatest fixed point is a post-fixed point · Monotonicity in the bound variable

Used byThe ν unfolding

TheoremThe ν unfolding#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment assigning a set of worlds to each variable index \(n \in \mathbb{N}\), and \(\varphi\) a μ-calculus formula. Let \(A\) be the set of worlds satisfying \(\nu\varphi\) in \(M\) under \(\rho\). Then \(A\) is exactly the set of worlds satisfying \(\varphi\) in \(M\) under the environment that sends index \(0\) to \(A\) and index \(n + 1\) to \(\rho(n)\).

theorem sat_nu_unfold (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M env (.nu φ) = sat M (extendEnv env (sat M env (.nu φ))) φ

Uses 6 · Used by 2

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Proof usesThe greatest fixed point is a pre-fixed point · The greatest fixed point is a post-fixed point

Used by\(\mathsf{AG}\) is universal reachability · Duality

TheoremPark induction#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment, \(\varphi\) a μ-calculus formula and \(P\) a predicate on worlds. If every world satisfying \(\varphi\) in the extension of \(\rho\) by \(P\) satisfies \(P\), then every world satisfying \(\mu\varphi\) in \(\rho\) satisfies \(P\).

theorem mu_induction {env : ℕ → World → Prop} {φ : MuFormula Atom} {P : World → Prop}
    (hP : sat M (extendEnv env P) φ ≤ P) : sat M env (.mu φ) ≤ P

Uses 4 · Used by 3

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Used by\(\mathsf{EF}\) is reachability · The formula \(\mu X.\, \mu Y.\, X\) is false everywhere · Duality

TheoremCoinduction for the greatest fixed point#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment, \(\varphi\) a μ-calculus formula and \(P\) a set of worlds of \(M\). Write \(\llbracket\psi\rrbracket_\sigma\) for the set of worlds at which \(\psi\) holds under the environment \(\sigma\), and \(\rho[P]\) for the extension of \(\rho\) under a binder by \(P\) (variable \(0\) denotes \(P\) and variable \(n + 1\) denotes \(\rho(n)\)). If \(P \subseteq \llbracket\varphi\rrbracket_{\rho[P]}\), then \(P \subseteq \llbracket\nu\varphi\rrbracket_\rho\), where \(\nu\varphi\) binds variable \(0\) of \(\varphi\): every post-fixed point is below the greatest fixed point.

theorem nu_coinduction {env : ℕ → World → Prop} {φ : MuFormula Atom} {P : World → Prop}
    (hP : P ≤ sat M (extendEnv env P) φ) : P ≤ sat M env (.nu φ)

Uses 4 · Used by 3

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus

Used by\(\mathsf{AG}\) is universal reachability · The formula \(\nu X.\, \nu Y.\, X\) is true everywhere · Duality

DefinitionThe fixed-point operator of a formula#✓fully proved

Given a Kripke model \(M\), an environment \(\rho\) (a set of worlds \(\rho(n)\) for each variable \(n\)) and a μ-calculus formula \(\varphi\), this is the monotone map on sets of worlds of \(M\) sending \(S\) to the set of worlds at which \(\varphi\) holds under \(\rho[S]\), the extension of \(\rho\) under a binder by \(S\) (variable \(0\) denotes \(S\) and variable \(n + 1\) denotes \(\rho(n)\)).

def muOp (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    (World → Prop) →o (World → Prop) :=
  ⟨fun S => sat M (extendEnv env S) φ, fun _ _ hle => sat_mono_extend M hle φ⟩

Uses 5 · Used by 3

Statement usesKripke model · Formulas of the modal μ-calculus · Extending an environment under a binder · Satisfaction in the modal μ-calculus · Monotonicity in the bound variable

Used byDenotation of a closed μ-calculus formula is environment-independent · The μ formula denotes the least fixed point · The ν formula denotes the greatest fixed point

TheoremThe μ formula denotes the least fixed point#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment assigning a set of worlds to each variable index \(n \in \mathbb{N}\), and \(\varphi\) a μ-calculus formula. For a set of worlds \(S\), write \(\rho[0 \mapsto S]\) for the environment sending index \(0\) to \(S\) and index \(n + 1\) to \(\rho(n)\). Then the set of worlds satisfying \(\mu\varphi\) in \(M\) under \(\rho\) is the least fixed point of the monotone operator on sets of worlds that sends \(S\) to the set of worlds satisfying \(\varphi\) in \(M\) under \(\rho[0 \mapsto S]\).

theorem sat_mu_eq_lfp (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M env (.mu φ) = (muOp M env φ).lfp

Uses 5 · Used by 1

Statement usesKripke model · Formulas of the modal μ-calculus · The fixed-point operator of a formula · Satisfaction in the modal μ-calculus

Proof usesThe least fixed point is a pre-fixed point

Used byDenotation of a closed μ-calculus formula is environment-independent

TheoremThe ν formula denotes the greatest fixed point#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment assigning a set of worlds to each variable index \(n \in \mathbb{N}\), and \(\varphi\) a μ-calculus formula. For a set of worlds \(S\), write \(\rho[0 \mapsto S]\) for the environment sending index \(0\) to \(S\) and index \(n + 1\) to \(\rho(n)\). Then the set of worlds satisfying \(\nu\varphi\) in \(M\) under \(\rho\) is the greatest fixed point of the monotone operator on sets of worlds that sends \(S\) to the set of worlds satisfying \(\varphi\) in \(M\) under \(\rho[0 \mapsto S]\).

theorem sat_nu_eq_gfp (env : ℕ → World → Prop) (φ : MuFormula Atom) :
    sat M env (.nu φ) = (muOp M env φ).gfp

Uses 5 · Used by 1

Statement usesKripke model · Formulas of the modal μ-calculus · The fixed-point operator of a formula · Satisfaction in the modal μ-calculus

Proof usesExtending an environment under a binder

Used byDenotation of a closed μ-calculus formula is environment-independent

TheoremComplementing an extended environment#✓fully proved

For every environment \(\rho\) (assigning to each variable index \(n\) a predicate \(\rho(n)\) on worlds) and every predicate \(S\) on worlds, complementing every predicate of the extension of \(\rho\) by \(S\) gives the extension of the complemented environment \(n \mapsto \neg\rho(n)\) by the predicate \(w \mapsto \neg S(w)\).

theorem extendEnv_compl (env : ℕ → World → Prop) (S : World → Prop) :
    (fun n => fun w => ¬ extendEnv env S n w) =
      extendEnv (fun n => fun w => ¬ env n w) (fun w => ¬ S w)

Uses 1 · Used by 1

Statement usesExtending an environment under a binder

Used byDuality

TheoremDouble complement of a predicate#✓fully proved

For every predicate \(S\) on worlds, the predicate \(w \mapsto \neg\neg S(w)\) equals \(S\).

theorem compl_compl (S : World → Prop) :
    (fun w => ¬ ¬ S w) = S

Used by 1

Used byDuality

TheoremDuality#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment assigning a set of worlds to each variable index \(n \in \mathbb{N}\), and \(\varphi\) a μ-calculus formula. Let \(\neg\varphi\) be the dual formula of \(\varphi\), obtained by swapping atoms with negated atoms, \(\bot\) with \(\top\), \(\wedge\) with \(\vee\), \(\Box\) with \(\Diamond\) and \(\mu\) with \(\nu\), and keeping variables. Write \(\overline{\rho}\) for the environment sending each index \(n\) to the complement of \(\rho(n)\). Then for every world \(w\), \(w\) satisfies \(\neg\varphi\) in \(M\) under \(\overline{\rho}\) if and only if \(w\) does not satisfy \(\varphi\) in \(M\) under \(\rho\).

theorem sat_neg : ∀ (φ : MuFormula Atom) (env : ℕ → World → Prop) (w : World),
    sat M (fun n => fun w => ¬ env n w) (MuFormula.neg φ) w ↔ ¬ sat M env φ w

Uses 11

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

Proof usesDouble complement of a predicate · Extending an environment under a binder · Complementing an extended environment · Park induction · Coinduction for the greatest fixed point · The μ unfolding · The ν unfolding

DefinitionThe μ-calculus formula \(\mathsf{EF}\,p\)#✓fully proved

For an atom \(p\), \(\mathsf{EF}\,p\) is the least fixed point formula \(\mu X.\,(p \vee \Diamond X)\). It expresses that some state reachable from the current one satisfies \(p\).

def EF (p : Atom) : MuFormula Atom := .mu (.or (.atom p) (.dia (.var 0)))

Uses 1 · Used by 1

Statement usesFormulas of the modal μ-calculus

Used by\(\mathsf{EF}\) is reachability

DefinitionThe μ-calculus formula \(\mathsf{AG}\,p\)#✓fully proved

For an atom \(p\), \(\mathsf{AG}\,p\) is the greatest fixed point formula \(\nu X.\,(p \wedge \Box X)\). It expresses that every state reachable from the current one satisfies \(p\).

def AG (p : Atom) : MuFormula Atom := .nu (.and (.atom p) (.box (.var 0)))

Uses 1 · Used by 1

Statement usesFormulas of the modal μ-calculus

Used by\(\mathsf{AG}\) is universal reachability

Theorem\(\mathsf{EF}\) is reachability#✓fully proved

For every Kripke model \(M\), every environment \(\rho\) (an assignment of a predicate on worlds to each variable index), every atom \(p\) and every world \(w\), the μ-calculus formula \(\mathsf{EF}\,p\) holds at \(w\) in \(\rho\) if and only if \(p\) is true at some world reachable from \(w\) in zero or more steps of the accessibility relation of \(M\).

theorem EF_iff_reachable (env : ℕ → World → Prop) (p : Atom) (w : World) :
    sat M env (EF p) w ↔
      ∃ v, Relation.ReflTransGen M.rel w v ∧ M.valuation v p

Uses 7

Statement usesKripke model · The μ-calculus formula \(\mathsf{EF}\,p\) · Satisfaction in the modal μ-calculus

Proof usesFormulas of the modal μ-calculus · Extending an environment under a binder · Park induction · The μ unfolding

Theorem\(\mathsf{AG}\) is universal reachability#✓fully proved

For every Kripke model \(M\), every environment \(\rho\) (an assignment of a predicate on worlds to each variable index), every atom \(p\) and every world \(w\), the μ-calculus formula \(\mathsf{AG}\,p\) holds at \(w\) in \(\rho\) if and only if \(p\) is true at every world reachable from \(w\) in zero or more steps of the accessibility relation of \(M\).

theorem AG_iff_forall_reachable (env : ℕ → World → Prop) (p : Atom) (w : World) :
    sat M env (AG p) w ↔
      ∀ v, Relation.ReflTransGen M.rel w v → M.valuation v p

Uses 7

Statement usesKripke model · The μ-calculus formula \(\mathsf{AG}\,p\) · Satisfaction in the modal μ-calculus

Proof usesFormulas of the modal μ-calculus · Extending an environment under a binder · Coinduction for the greatest fixed point · The ν unfolding

TheoremThe formula \(\mu X.\, \mu Y.\, X\) is false everywhere#✓fully proved

For every Kripke model \(M\) and every environment \(\rho\), the formula \(\mu X.\, \mu Y.\, X\) holds at no world of \(M\) under \(\rho\). In de Bruijn form this formula is \(\mu\, \mu\, x_1\): inside the inner binder, variable \(1\) refers to the outer binder, not to the inner one.

theorem mu_mu_var_one_eq_bot (env : ℕ → World → Prop) :
    sat M env (.mu (.mu (.var 1))) = fun _ => False

Uses 5

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

Proof usesExtending an environment under a binder · Park induction

TheoremThe formula \(\nu X.\, \nu Y.\, X\) is true everywhere#✓fully proved

For every Kripke model \(M\) and every environment \(\rho\), the formula \(\nu X.\, \nu Y.\, X\) holds at every world of \(M\) under \(\rho\). In de Bruijn form this formula is \(\nu\, \nu\, x_1\): inside the inner binder, variable \(1\) refers to the outer binder. This is the dual of the fact that \(\mu X.\, \mu Y.\, X\) is false everywhere.

theorem nu_nu_var_one_eq_top (env : ℕ → World → Prop) :
    sat M env (.nu (.nu (.var 1))) = fun _ => True

Uses 5

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

Proof usesExtending an environment under a binder · Coinduction for the greatest fixed point

Definitionμ-calculus formula closed at a given binding depth#✓fully proved

A formula is closed at depth d when every free de Bruijn variable is < d: only μ / ν increase the depth; □ / ◇ do not bind variables and preserve it.

def ClosedAt : ℕ → MuFormula Atom → Prop
  | _, .atom _ => True
  | _, .natom _ => True
  | d, .var n => n < d
  | _, .bot => True
  | _, .top => True
  | d, .and φ ψ => ClosedAt d φ ∧ ClosedAt d ψ
  | d, .or φ ψ => ClosedAt d φ ∧ ClosedAt d ψ
  | d, .box φ => ClosedAt d φ
  | d, .dia φ => ClosedAt d φ
  | d, .mu φ => ClosedAt (d + 1) φ
  | d, .nu φ => ClosedAt (d + 1) φ

Uses 1 · Used by 2

Statement usesFormulas of the modal μ-calculus

Used byClosed modal μ-calculus formula · Denotation of a closed μ-calculus formula is environment-independent

DefinitionClosed modal μ-calculus formula#✓fully proved

A formula is closed when it is closed at depth 0: every variable is bound.

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

Uses 2 · Used by 1

Statement usesFormulas of the modal μ-calculus · μ-calculus formula closed at a given binding depth

Used byModal μ-calculus satisfiability as a decision problem

DefinitionDepth of a modal μ-calculus formula#✓fully proved

The depth of a formula: the length of its longest root-to-leaf path, counting each connective once.

def depth : MuFormula Atom → ℕ
  | .atom _ => 0
  | .natom _ => 0
  | .var _ => 0
  | .bot => 0
  | .top => 0
  | .and φ ψ => 1 + max (depth φ) (depth ψ)
  | .or φ ψ => 1 + max (depth φ) (depth ψ)
  | .box φ => 1 + depth φ
  | .dia φ => 1 + depth φ
  | .mu φ => 1 + depth φ
  | .nu φ => 1 + depth φ

Uses 1 · Used by 2

Statement usesFormulas of the modal μ-calculus

Used byDepth of a μ-calculus formula is at most its number code · Fuelled decoding inverts the μ-calculus number code

TheoremDenotation of a closed μ-calculus formula is environment-independent#✓fully proved

A closed formula does not depend on the environment: environments agreeing below the depth give the same denotation.

theorem sat_closed_env :
    ∀ (φ : MuFormula Atom) (d : ℕ) {env env' : ℕ → World → Prop},
    MuFormula.ClosedAt d φ → (∀ n, n < d → env n = env' n) →
    sat M env φ = sat M env' φ

Uses 8

Statement usesKripke model · Formulas of the modal μ-calculus · μ-calculus formula closed at a given binding depth · Satisfaction in the modal μ-calculus

Proof usesExtending an environment under a binder · The fixed-point operator of a formula · The μ formula denotes the least fixed point · The ν formula denotes the greatest fixed point

DefinitionCantor-pairing number code of a μ-calculus formula#✓fully proved

An injective encoding of μ-calculus formulas over ℕ atoms as natural numbers, via the Cantor pairing function Nat.pair. This is a Nat code only, not a complexity input encoding: repeated pairing squares the code at every unary connective, so the binary length of the code of box^d (atom 0) doubles at each box and is exponential in d. Complexity statements use muTokens / muDecodeList instead.

def muCode : MuFormula ℕ → ℕ
  | .atom a => Nat.pair 0 a
  | .natom a => Nat.pair 1 a
  | .var n => Nat.pair 2 n
  | .bot => Nat.pair 3 0
  | .top => Nat.pair 4 0
  | .and φ ψ => Nat.pair 5 (Nat.pair (muCode φ) (muCode ψ))
  | .or φ ψ => Nat.pair 6 (Nat.pair (muCode φ) (muCode ψ))
  | .box φ => Nat.pair 7 (muCode φ)
  | .dia φ => Nat.pair 8 (muCode φ)
  | .mu φ => Nat.pair 9 (muCode φ)
  | .nu φ => Nat.pair 10 (muCode φ)

Uses 1 · Used by 4

Statement usesFormulas of the modal μ-calculus

Used byDepth of a μ-calculus formula is at most its number code · Injectivity of the μ-calculus number code · Fuelled decoding inverts the μ-calculus number code · Decoding inverts the μ-calculus number code

DefinitionFuelled decoding of a μ-calculus number code#✓fully proved

Fuelled decoding of a muCode number back to a formula. The fuel bounds the recursion depth; muDecode supplies fuel c + 1, which exceeds every formula's depth (see depth_le_code).

Cslib.Modal.MuCalculus.muDecodeFuel · 26 lines

def muDecodeFuel : ℕ → ℕ → Option (MuFormula ℕ)
  | 0, _ => none
  | fuel + 1, c =>
    match Nat.unpair c with
    | (0, a) => some (.atom a)
    | (1, a) => some (.natom a)
    | (2, n) => some (.var n)
    | (3, _) => some .bot
    | (4, _) => some .top
    | (5, r) =>
      match Nat.unpair r with
      | (c₁, c₂) =>
        match muDecodeFuel fuel c₁, muDecodeFuel fuel c₂ with
        | some f₁, some f₂ => some (.and f₁ f₂)
        | _, _ => none
    | (6, r) =>
      match Nat.unpair r with
      | (c₁, c₂) =>
        match muDecodeFuel fuel c₁, muDecodeFuel fuel c₂ with
        | some f₁, some f₂ => some (.or f₁ f₂)
        | _, _ => none
    | (7, c₁) => .box <$> muDecodeFuel fuel c₁
    | (8, c₁) => .dia <$> muDecodeFuel fuel c₁
    | (9, c₁) => .mu <$> muDecodeFuel fuel c₁
    | (10, c₁) => .nu <$> muDecodeFuel fuel c₁
    | (_, _) => none

Uses 1 · Used by 2

Statement usesFormulas of the modal μ-calculus

Used byDecoding a μ-calculus number code to a formula · Fuelled decoding inverts the μ-calculus number code

DefinitionDecoding a μ-calculus number code to a formula#✓fully proved

Decode a muCode number back to the formula it encodes.

def muDecode (c : ℕ) : Option (MuFormula ℕ) := muDecodeFuel (c + 1) c

Uses 2 · Used by 2

Statement usesFormulas of the modal μ-calculus · Fuelled decoding of a μ-calculus number code

Used byInjectivity of the μ-calculus number code · Decoding inverts the μ-calculus number code

TheoremDepth of a μ-calculus formula is at most its number code#✓fully proved

A formula's depth is at most its code: pairing dominates each component (Nat.add_le_pair).

theorem depth_le_code : ∀ φ : MuFormula ℕ, MuFormula.depth φ ≤ muCode φ

Uses 3 · Used by 1

Statement usesFormulas of the modal μ-calculus · Depth of a modal μ-calculus formula · Cantor-pairing number code of a μ-calculus formula

Used byDecoding inverts the μ-calculus number code

TheoremFuelled decoding inverts the μ-calculus number code#✓fully proved

Decoding inverts encoding, with enough fuel: a formula's own code carries more fuel than its depth needs.

theorem muDecodeFuel_muCode : ∀ (φ : MuFormula ℕ) (fuel : ℕ),
    MuFormula.depth φ ≤ fuel → muDecodeFuel (fuel + 1) (muCode φ) = some φ

Uses 4 · Used by 1

Statement usesFormulas of the modal μ-calculus · Depth of a modal μ-calculus formula · Cantor-pairing number code of a μ-calculus formula · Fuelled decoding of a μ-calculus number code

Used byDecoding inverts the μ-calculus number code

TheoremDecoding inverts the μ-calculus number code#✓fully proved

Decoding inverts encoding.

theorem muDecode_muCode (φ : MuFormula ℕ) : muDecode (muCode φ) = some φ

Uses 5 · Used by 1

Statement usesFormulas of the modal μ-calculus · Cantor-pairing number code of a μ-calculus formula · Decoding a μ-calculus number code to a formula

Proof usesDepth of a μ-calculus formula is at most its number code · Fuelled decoding inverts the μ-calculus number code

Used byInjectivity of the μ-calculus number code

DefinitionPolynomial-size token-list encoding of μ-calculus formulas#✓fully proved

A polynomial-size token-list encoding of μ-calculus formulas over ℕ atoms, used for the complexity statements in WantedExt. Each connective contributes one tag token (Nat.pair of a small tag with 0), and each atom or variable contributes one token Nat.pair tag value, whose binary size is O(log value). The canonical bitstring encoding of a List ℕ delimits each token, so the bitstring for a formula has length linear in the number of connectives plus the total binary size of its atoms: box^d (atom 0) is encoded by exactly d + 1 tokens, unlike its Cantor-paired muCode, whose binary length is exponential in d.

def muTokens : MuFormula ℕ → List ℕ
  | .atom a => [Nat.pair 0 a]
  | .natom a => [Nat.pair 1 a]
  | .var n => [Nat.pair 2 n]
  | .bot => [Nat.pair 3 0]
  | .top => [Nat.pair 4 0]
  | .and φ ψ => Nat.pair 5 0 :: muTokens φ ++ muTokens ψ
  | .or φ ψ => Nat.pair 6 0 :: muTokens φ ++ muTokens ψ
  | .box φ => Nat.pair 7 0 :: muTokens φ
  | .dia φ => Nat.pair 8 0 :: muTokens φ
  | .mu φ => Nat.pair 9 0 :: muTokens φ
  | .nu φ => Nat.pair 10 0 :: muTokens φ

Uses 1 · Used by 2

Statement usesFormulas of the modal μ-calculus

Used byToken-list decoding inverts modal μ-calculus token encoding · Fuelled parsing inverts modal μ-calculus token encoding

DefinitionFuelled parser for modal μ-calculus token lists#✓fully proved

Fuelled parsing of a muTokens token list back to a formula, returning the formula and the unconsumed suffix. The fuel bounds the recursion depth; muDecodeList supplies fuel l.length + 1.

Cslib.Modal.MuCalculus.muParseFuel · 43 lines

def muParseFuel : ℕ → List ℕ → Option (MuFormula ℕ × List ℕ)
  | 0, _ => none
  | fuel + 1, xs =>
    match xs with
    | [] => none
    | c :: rest =>
      match Nat.unpair c with
      | (0, a) => some (.atom a, rest)
      | (1, a) => some (.natom a, rest)
      | (2, n) => some (.var n, rest)
      | (3, _) => some (.bot, rest)
      | (4, _) => some (.top, rest)
      | (5, _) =>
        match muParseFuel fuel rest with
        | some (φ, rest₁) =>
          match muParseFuel fuel rest₁ with
          | some (ψ, rest₂) => some (.and φ ψ, rest₂)
          | none => none
        | none => none
      | (6, _) =>
        match muParseFuel fuel rest with
        | some (φ, rest₁) =>
          match muParseFuel fuel rest₁ with
          | some (ψ, rest₂) => some (.or φ ψ, rest₂)
          | none => none
        | none => none
      | (7, _) =>
        match muParseFuel fuel rest with
        | some (φ, rest₁) => some (.box φ, rest₁)
        | none => none
      | (8, _) =>
        match muParseFuel fuel rest with
        | some (φ, rest₁) => some (.dia φ, rest₁)
        | none => none
      | (9, _) =>
        match muParseFuel fuel rest with
        | some (φ, rest₁) => some (.mu φ, rest₁)
        | none => none
      | (10, _) =>
        match muParseFuel fuel rest with
        | some (φ, rest₁) => some (.nu φ, rest₁)
        | none => none
      | (_, _) => none

Uses 1 · Used by 3

Statement usesFormulas of the modal μ-calculus

Used byDecoding a modal μ-calculus token list to a formula · Token-list decoding inverts modal μ-calculus token encoding · Fuelled parsing inverts modal μ-calculus token encoding

DefinitionDecoding a modal μ-calculus token list to a formula#✓fully proved

Decode a muTokens token list back to the formula it encodes, rejecting trailing tokens.

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

Uses 2 · Used by 2

Statement usesFormulas of the modal μ-calculus · Fuelled parser for modal μ-calculus token lists

Used byToken-list decoding inverts modal μ-calculus token encoding · Modal μ-calculus satisfiability as a decision problem

TheoremFuelled parsing inverts modal μ-calculus token encoding#✓fully proved

Parsing inverts token encoding, with enough fuel.

theorem muParseFuel_muTokens : ∀ (φ : MuFormula ℕ) (rest : List ℕ) (fuel : ℕ),
    (muTokens φ).length ≤ fuel →
    muParseFuel (fuel + 1) (muTokens φ ++ rest) = some (φ, rest)

Uses 3 · Used by 1

Statement usesFormulas of the modal μ-calculus · Fuelled parser for modal μ-calculus token lists · Polynomial-size token-list encoding of μ-calculus formulas

Used byToken-list decoding inverts modal μ-calculus token encoding

TheoremToken-list decoding inverts modal μ-calculus token encoding#✓fully proved

Decoding inverts token encoding.

theorem muDecodeList_muTokens (φ : MuFormula ℕ) :
    muDecodeList (muTokens φ) = some φ

Uses 5

Statement usesFormulas of the modal μ-calculus · Decoding a modal μ-calculus token list to a formula · Polynomial-size token-list encoding of μ-calculus formulas

Proof usesFuelled parser for modal μ-calculus token lists · Fuelled parsing inverts modal μ-calculus token encoding

TheoremInjectivity of the μ-calculus number code#✓fully proved

The encoding is injective.

theorem muCode_injective : Function.Injective muCode

Uses 4

Statement usesFormulas of the modal μ-calculus · Cantor-pairing number code of a μ-calculus formula

Proof usesDecoding a μ-calculus number code to a formula · Decoding inverts the μ-calculus number code

43 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.