Model-checking game for the modal μ-calculus

AbbreviationPosition of the μ-calculus model-checking game#✓fully proved

A position of the μ-calculus model-checking game: the formula, the world, and the stack of enclosing fixpoint binders, innermost first.

abbrev GamePosition (Atom World : Type u) :=
  MuFormula Atom × World × List (MuFormula Atom)

Uses 1 · Used by 53

Statement usesFormulas of the modal μ-calculus

Used byCanonical next move induced by a bespoke strategy · 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 · Regression cycle, first step · Regression cycle, second step · Regression cycle, third step · The regression play · The regression play stays on the cycle · The regression play is a play · The regression play returns to its start every three steps · The regression play has period three · Starting position of the regression play · Second position of the regression play · Third position of the regression play · Verifier loses the infinite play of \(\mu X.\, \nu Y.\, X\) · Moves from a diamond position · Projection of game positions onto the fragment arena · Segment of a fragment play as game positions · Splitting off the head of a segment · Segments are nonempty · Last position of a segment · 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 · Moves of the μ-calculus model-checking game · Fragment moves decrease the formula size · Finite plays are nonempty · No infinite play from a fragment position · Positions with no moves · Inversion for disjunction moves · Owner of a game position · Parity winning condition · Finite plays consistent with a strategy · Last position of a play · Prepending to a nonempty play keeps the last position · Priority of a game position · Verifier strategy · Winning strategy from a position · Winning strategies stay winning along consistent moves · Winner at a terminal position · Verifier has a winning strategy · Game-vs-satisfaction, converse direction · 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)

AbbreviationPlayer of the μ-calculus model-checking game#✓fully proved

The player to move: true is Verifier, false is Refuter.

abbrev Player := Bool

Used by 18

Used byCanonical next move induced by a bespoke strategy · The canonical move follows the bespoke strategy at Verifier positions with a move · Segments of canonical plays through fragment positions are bespoke plays · Owners in the totalized fragment game · Owner of an embedded position in the totalized fragment game · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · Finite plays are nonempty · Owner of a game position · Finite plays consistent with a strategy · Verifier strategy · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction · The Wins-guided move is legal · Wins-guided strategy · Wins-guided strategy wins finite plays (auxiliary induction)

InductiveMoves of the μ-calculus model-checking game#✓fully proved

Fix a Kripke model \(M\) with accessibility relation \(R\). A game position \((\varphi, w, s)\) consists of a μ-calculus formula \(\varphi\) (with de Bruijn variables), a world \(w\) and a stack \(s\) of fixpoint binders, innermost first. The moves are exactly the following. From \((\varphi \wedge \psi, w, s)\) and from \((\varphi \vee \psi, w, s)\) to \((\varphi, w, s)\) and to \((\psi, w, s)\). From \((\Box \varphi, w, s)\) and from \((\Diamond \varphi, w, s)\) to \((\varphi, v, s)\) for every world \(v\) with \(w R v\). From \((\mu \varphi, w, s)\) to \((\varphi, w, s')\), where \(s'\) is \(s\) with \(\mu \varphi\) pushed on top, and likewise from \((\nu \varphi, w, s)\) to \((\varphi, w, s'')\), where \(s''\) is \(s\) with \(\nu \varphi\) pushed on top. From \((x_n, w, s)\), where \(x_n\) is the variable with de Bruijn index \(n\) and \(n\) is less than the length of \(s\), to \((s_n, w, t)\), where \(s_n\) is the entry of \(s\) at index \(n\) (counting from \(0\)) and \(t\) is \(s\) with its first \(n + 1\) entries removed.

Cslib.Modal.MuCalculus.Game.Move · 29 lines

inductive Move (M : KripkeModel World Atom) :
    GamePosition Atom World → GamePosition Atom World → Prop
  /-- Refuter chooses a conjunct. -/
  | andLeft {φ ψ : MuFormula Atom} {w : World} {st : List (MuFormula Atom)} :
      Move M ⟨.and φ ψ, w, st⟩ ⟨φ, w, st⟩
  /-- Refuter chooses a conjunct. -/
  | andRight {φ ψ : MuFormula Atom} {w : World} {st : List (MuFormula Atom)} :
      Move M ⟨.and φ ψ, w, st⟩ ⟨ψ, w, st⟩
  /-- Verifier chooses a disjunct. -/
  | orLeft {φ ψ : MuFormula Atom} {w : World} {st : List (MuFormula Atom)} :
      Move M ⟨.or φ ψ, w, st⟩ ⟨φ, w, st⟩
  /-- Verifier chooses a disjunct. -/
  | orRight {φ ψ : MuFormula Atom} {w : World} {st : List (MuFormula Atom)} :
      Move M ⟨.or φ ψ, w, st⟩ ⟨ψ, w, st⟩
  /-- Refuter chooses a successor. -/
  | box {φ : MuFormula Atom} {w v : World} {st : List (MuFormula Atom)}
      (h : M.rel w v) : Move M ⟨.box φ, w, st⟩ ⟨φ, v, st⟩
  /-- Verifier chooses a successor. -/
  | dia {φ : MuFormula Atom} {w v : World} {st : List (MuFormula Atom)}
      (h : M.rel w v) : Move M ⟨.dia φ, w, st⟩ ⟨φ, v, st⟩
  /-- Unfold a least fixed point, pushing its binder on the stack. -/
  | mu {φ : MuFormula Atom} {w : World} {st : List (MuFormula Atom)} :
      Move M ⟨.mu φ, w, st⟩ ⟨φ, w, .mu φ :: st⟩
  /-- Unfold a greatest fixed point, pushing its binder on the stack. -/
  | nu {φ : MuFormula Atom} {w : World} {st : List (MuFormula Atom)} :
      Move M ⟨.nu φ, w, st⟩ ⟨φ, w, .nu φ :: st⟩
  /-- Jump back to the binder a variable refers to, restoring that binder's stack. -/
  | var {n : ℕ} {w : World} {st : List (MuFormula Atom)} (h : n < st.length) :
      Move M ⟨.var n, w, st⟩ ⟨st.getD n .bot, w, st.drop (n + 1)⟩

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 3 · Used by 32

Statement usesKripke model · Position of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byCanonical 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 · The regression play is a play · Moves from a diamond position · Moves of the totalized fragment game · Moves of the totalized fragment game, by cases · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Fragment parity game · The losing state is absorbing · Fragment moves decrease the formula size · Finite plays are nonempty · No infinite play from a fragment position · Positions with no moves · Inversion for disjunction moves · Finite plays consistent with a strategy · 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 · Verifier strategy · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · The absorbing win state · Game-vs-satisfaction, strategy direction · The Wins-guided move is legal · Wins-guided strategy · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionOwner of a game position#✓fully proved

The owner of a game position \((\varphi, w, s)\) is Verifier when \(\varphi\) is a disjunction, a diamond formula or a greatest fixed point, and Refuter for every other formula.

def Owner : GamePosition Atom World → Player
  | ⟨.or _ _, _, _⟩ | ⟨.dia _, _, _⟩ | ⟨.nu _, _, _⟩ => true
  | _ => false

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 3 · Used by 17

Statement usesPosition of the μ-calculus model-checking game · Player of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byCanonical next move induced by a bespoke strategy · The canonical move follows the bespoke strategy at Verifier positions with a move · Segments of canonical plays through fragment positions are bespoke plays · Owners in the totalized fragment game · Owner of an embedded position in the totalized fragment game · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · Finite plays are nonempty · Finite plays consistent with a strategy · Verifier strategy · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction · The Wins-guided move is legal · Wins-guided strategy · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionPriority of a game position#✓fully proved

Only fixpoint-binder positions carry a priority. For a formula \(\varphi\), a world \(w\) and a binder stack \(s\) of length \(k\), the position \((\mu X.\,\varphi, w, s)\), whose formula is the least fixpoint with body \(\varphi\), has priority \(2k+1\), the position \((\nu X.\,\varphi, w, s)\), whose formula is the greatest fixpoint with body \(\varphi\), has priority \(2k+2\), and every other position has no priority. Priorities strictly increase with nesting depth, so the outermost binder regenerated infinitely often has the least priority.

This is the nesting-depth refinement of the alternation-depth priority assignment: same-type nesting counts toward the depth, which only refines the order (outer still strictly below inner) and keeps parity tied to the binder kind. Fixed priorities (\(\mu \mapsto 1\), \(\nu \mapsto 2\)) under the greatest-recurring-priority rule would let an inner vacuous \(\nu\) dominate an outer \(\mu\): in \(\mu X.\,\nu Y.\,X\), whose denotation is empty, Verifier would win the only play.

def prio : GamePosition Atom World → Option ℕ
  | ⟨.mu _, _, st⟩ => some (2 * st.length + 1)
  | ⟨.nu _, _, st⟩ => some (2 * st.length + 2)
  | _ => none

Sources

• E. A. Emerson and C. S. Jutla, "Tree automata, μ-calculus and determinacy", Proceedings of FOCS 1991, 368-377; C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6; J. A. Bradfield, "The modal μ-calculus alternation hierarchy is strict", Theoretical Computer Science 195 (1998), 133-153 (alternation depth).

Uses 2 · Used by 5

Statement usesPosition of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byPriority of the outer binder in the regression play · Priority of the inner binder in the regression play · Verifier loses the infinite play of \(\mu X.\, \nu Y.\, X\) · Parity winning condition · Winning strategies stay winning along consistent moves

DefinitionPositions with no moves#✓fully proved

In a Kripke model \(M\), a game position \(p\) has no moves when there is no position \(q\) such that going from \(p\) to \(q\) is a move of the model-checking game in \(M\).

def NoMoves (M : KripkeModel World Atom) (p : GamePosition Atom World) : Prop :=
  ∀ q, ¬ Move M p q

Uses 3 · Used by 19

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game

Used byVerifier's positional strategies make a game move at Verifier positions that have one · Moves of the totalized fragment game · Moves of the totalized fragment game, by cases · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Fragment parity game · The losing state is absorbing · 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 · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · The absorbing win state · Game-vs-satisfaction, strategy direction · Wins-guided strategy wins every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionWinner at a terminal position#✓fully proved

Let \(M\) be a Kripke model and \(\mathit{env}\) an environment assigning a predicate on worlds to every index. At a game position \((\varphi, w, st)\), where \(st\) is the stack of enclosing fixpoint binders and \(|st|\) its length, Verifier wins exactly when \(\varphi\) is an atom \(a\) true at \(w\), a negated atom \(\neg a\) with \(a\) false at \(w\), \(\top\), a box \(\Box\psi\), or a variable with de Bruijn index \(n \ge |st|\) such that \(\mathit{env}(n - |st|)\) holds at \(w\). At every other position (a variable with index \(n < |st|\), \(\bot\), a diamond, a conjunction, a disjunction or a fixpoint) Refuter wins.

The condition is consulted only at positions with no moves: a box with no successors leaves Refuter stuck and a diamond with no successors leaves Verifier stuck, while a bound variable, a conjunction, a disjunction and a fixpoint always have a move. The environment index is shifted by \(|st|\) because each binder on the stack shifts de Bruijn indices by one.

def TerminalWin (M : KripkeModel World Atom) (env : ℕ → World → Prop) :
    GamePosition Atom World → Prop
  | ⟨.atom a, w, _⟩ => M.valuation w a
  | ⟨.natom a, w, _⟩ => ¬ M.valuation w a
  | ⟨.var n, w, st⟩ => if n < st.length then False else env (n - st.length) w
  | ⟨.top, _, _⟩ => True
  | ⟨.bot, _, _⟩ => False
  | ⟨.box _, _, _⟩ => True
  | ⟨.dia _, _, _⟩ => False
  | _ => False

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 3 · Used by 21

Statement usesKripke model · Position of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byCanonical 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 · Moves of the totalized fragment game · Moves of the totalized fragment game, by cases · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Fragment parity game · The losing state is absorbing · 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 · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · The absorbing win state · Game-vs-satisfaction, strategy direction · Wins-guided strategy wins every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionParity winning condition#✓fully proved

For an infinite sequence of game positions \(p_0, p_1, \dots\), Verifier wins by the parity condition when there is an even priority \(e\) such that infinitely many positions \(p_n\) have priority \(e\), and every priority \(e' < e\) is the priority of only finitely many positions \(p_n\). Equivalently, some priority occurs infinitely often and the least such priority is even; in particular, if no priority occurs infinitely often, Verifier does not win. Only fixpoint-binder positions carry a priority, so the other positions do not affect the outcome.

The least-priority convention is what makes outer binders dominate: an outer binder has a smaller priority than any binder nested inside it.

def ParityWin (play : ℕ → GamePosition Atom World) : Prop :=
  ∃ e, Even e ∧ (∀ N, ∃ n, N ≤ n ∧ prio (play n) = some e) ∧
    ∀ e', e' < e → ∃ N, ∀ n, N ≤ n → prio (play n) ≠ some e'

Sources

• E. A. Emerson and C. S. Jutla, "Tree automata, μ-calculus and determinacy", Proceedings of FOCS 1991, 368-377.

Uses 2 · Used by 6

Statement usesPosition of the μ-calculus model-checking game · Priority of a game position

Used byVerifier loses the infinite play of \(\mu X.\, \nu Y.\, X\) · Winning Verifier strategies transfer to the fragment game · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction

StructureVerifier strategy#✓fully proved

A Verifier strategy for the model-checking game on a Kripke model \(M\) is a map \(\sigma\) from game positions to game positions such that, at every Verifier-owned position \(p\) from which some move exists, there is a move from \(p\) to \(\sigma(p)\).

The move-respecting condition is what makes Verifier's winning meaningful: without it, a strategy could "win" by choosing a non-move at a Verifier position, leaving no legal play at all.

structure Strategy (M : KripkeModel World Atom) where
  /-- The chosen successor at a Verifier-owned position. -/
  choose : GamePosition Atom World → GamePosition Atom World
  /-- The chosen successor is a legal move whenever one exists. -/
  choose_move : ∀ p, Owner p = true → (∃ q, Move M p q) → Move M p (choose p)

Uses 5 · Used by 15

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game

Used byCanonical next move induced by a bespoke strategy · The canonical move follows the bespoke strategy at Verifier positions with a move · Segments of canonical plays through fragment positions are bespoke plays · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · Wins is the winning region of the fragment game · Finite plays are nonempty · Finite plays consistent with a strategy · Winning strategy from a position · Winning strategies stay winning along consistent moves · Verifier has a winning strategy · Game-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction · Wins-guided strategy · Wins-guided strategy wins finite plays (auxiliary induction)

InductiveFinite plays consistent with a strategy#✓fully proved

Fix a Kripke model \(M\) and a Verifier strategy \(\sigma\). The finite plays from a position \(p\) that follow \(\sigma\) are the lists of positions defined inductively: the one-element list \([p]\) is such a play; and if the game has a move from \(p\) to \(q\), where \(q\) is the position chosen by \(\sigma\) at \(p\) whenever Verifier owns \(p\), then \(p\) followed by any such play from \(q\) is such a play from \(p\).

A play need not end at a position with no moves: every finite prefix counts.

inductive PlayFrom (M : KripkeModel World Atom) (σ : Strategy M) :
    GamePosition Atom World → List (GamePosition Atom World) → Prop
  /-- The trivial play. -/
  | single {p : GamePosition Atom World} : PlayFrom M σ p [p]
  /-- A move followed by a play from the successor. -/
  | cons {p q : GamePosition Atom World} {ps : List (GamePosition Atom World)}
      (h : Move M p q) (hσ : Owner p = true → q = σ.choose p) (hps : PlayFrom M σ q ps) :
      PlayFrom M σ p (p :: ps)

Uses 6 · Used by 9

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game · Verifier strategy

Used bySegments of canonical plays through fragment positions are bespoke plays · Winning Verifier strategies transfer to the fragment game · Finite plays are nonempty · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction · Wins-guided strategy wins every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionLast position of a play#✓fully proved

The last position of a finite list of game positions is its final entry when the list is nonempty; the empty list has no last position.

def playLast (ps : List (GamePosition Atom World)) : Option (GamePosition Atom World) :=
  ps.getLast?

Uses 1 · Used by 9

Statement usesPosition of the μ-calculus model-checking game

Used byLast position of a segment · Winning Verifier strategies transfer to the fragment game · Prepending to a nonempty play keeps the last position · Winning strategy from a position · Winning strategies stay winning along consistent moves · Game-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction · Wins-guided strategy wins every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionWinning strategy from a position#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment assigning a predicate on worlds to every index, \(\sigma\) a Verifier strategy for the model-checking game on \(M\) and \(p\) a game position. A play is consistent with \(\sigma\) when each step is a move and, at every Verifier-owned position, goes to the position chosen by \(\sigma\). The strategy \(\sigma\) wins from \(p\) in \(\mathit{env}\) when every finite play from \(p\) consistent with \(\sigma\) whose last position has no moves ends in a position that is a terminal win for Verifier in \(\mathit{env}\), and every infinite play from \(p\) consistent with \(\sigma\) satisfies the parity condition.

def StrategyWins (M : KripkeModel World Atom) (env : ℕ → World → Prop)
    (σ : Strategy M) (p : GamePosition Atom World) : Prop :=
  (∀ ps : List (GamePosition Atom World), PlayFrom M σ p ps →
    (∃ q, playLast ps = some q ∧ NoMoves M q) →
      ∃ q, playLast ps = some q ∧ TerminalWin M env q) ∧
  (∀ play : ℕ → GamePosition Atom World, play 0 = p →
    (∀ n, Move M (play n) (play (n + 1)) ∧
      (Owner (play n) = true → play (n + 1) = σ.choose (play n))) →
      ParityWin play)

Uses 11 · Used by 6

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Positions with no moves · Owner of a game position · Parity winning condition · Finite plays consistent with a strategy · Player of the μ-calculus model-checking game · Verifier strategy · Winner at a terminal position · Last position of a play

Used byWinning Verifier strategies transfer to the fragment game · Wins is the winning region of the fragment game · Winning strategies stay winning along consistent moves · Verifier has a winning strategy · Game-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction

DefinitionVerifier has a winning strategy#✓fully proved

For a Kripke model \(M\), an environment \(\mathit{env}\) and a game position \(p\), Verifier wins from \(p\) when some Verifier strategy \(\sigma\) in the model-checking game on \(M\) wins from \(p\) in environment \(\mathit{env}\): every complete finite \(\sigma\)-consistent play from \(p\) ends at a terminal winning position, and every infinite \(\sigma\)-consistent play from \(p\) satisfies the parity condition.

def VerifierWins (M : KripkeModel World Atom) (env : ℕ → World → Prop)
    (p : GamePosition Atom World) : Prop :=
  ∃ σ : Strategy M, StrategyWins M env σ p

Uses 4 · Used by 4

Statement usesKripke model · Position of the μ-calculus model-checking game · Verifier strategy · Winning strategy from a position

Used byWins is the winning region of the fragment game · Game-vs-satisfaction, converse direction · Backward-induction winning equals game winning on the fixpoint-free fragment · Game-vs-satisfaction, strategy direction

97 fully proved

Closed formulas and the regression for nesting-depth priorities

DefinitionFormulas closed at depth \(d\)#✓fully proved

Closedness of a μ-calculus formula \(\varphi\) (with de Bruijn variables) at a depth \(d \in \mathbb{N}\) is defined by recursion on \(\varphi\): atoms, negated atoms, \(\bot\) and \(\top\) are closed at every depth; the variable with index \(n\) is closed at depth \(d\) exactly when \(n < d\); \(\varphi \wedge \psi\) and \(\varphi \vee \psi\) are closed at depth \(d\) when both \(\varphi\) and \(\psi\) are; \(\Box\varphi\) and \(\Diamond\varphi\) are closed at depth \(d\) when \(\varphi\) is; and \(\mu\varphi\) and \(\nu\varphi\) are closed at depth \(d\) when \(\varphi\) is closed at depth \(d + 1\). Thus every free variable of \(\varphi\) refers to one of \(d\) enclosing binders.

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

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6 (de Bruijn variables).

Uses 1 · Used by 3

Statement usesFormulas of the modal μ-calculus

Used byClosed formulas · Closedness is monotone in the depth · Satisfaction depends only on the environment below the closure depth

DefinitionClosed formulas#✓fully proved

A μ-calculus formula \(\varphi\) is closed when it is closed at depth \(0\), that is, when it has no free variables.

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

Uses 2 · Used by 1

Statement usesFormulas closed at depth \(d\) · Formulas of the modal μ-calculus

Used byClosed formulas are environment-independent

TheoremClosedness is monotone in the depth#✓fully proved

Let \(\varphi\) be a μ-calculus formula and let \(d \le d'\) be natural numbers. If \(\varphi\) is closed at depth \(d\) (every free variable of \(\varphi\) is less than \(d\)), then \(\varphi\) is closed at depth \(d'\): more enclosing binders can only bind more variables.

theorem ClosedAt.mono {φ : MuFormula Atom} {d d' : ℕ} (h : d ≤ d')
    (hc : ClosedAt φ d) : ClosedAt φ d'

Uses 2

Statement usesFormulas closed at depth \(d\) · Formulas of the modal μ-calculus

TheoremSatisfaction depends only on the environment below the closure depth#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a μ-calculus formula and \(d\) a natural number such that \(\varphi\) is closed at depth \(d\): every occurrence of a variable with de Bruijn index \(n\) lying under \(k\) fixpoint binders of \(\varphi\) satisfies \(n < d + k\). If two environments \(\mathit{env}\) and \(\mathit{env}'\), each assigning a predicate on worlds to every index, agree at every index \(n < d\), then for every world \(w\), \(\varphi\) is satisfied at \(w\) in \(M\) under \(\mathit{env}\) if and only if it is satisfied at \(w\) in \(M\) under \(\mathit{env}'\).

In particular, satisfaction of a closed formula is independent of the environment.

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

Sources

• D. Kozen, Results on the propositional μ-calculus, Theoretical Computer Science 27 (1983), 333-354.

Uses 5 · Used by 1

Statement usesKripke model · Formulas closed at depth \(d\) · Formulas of the modal μ-calculus · Satisfaction in the modal μ-calculus

Proof usesExtending an environment under a binder

Used byClosed formulas are environment-independent

TheoremClosed formulas are environment-independent#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a closed μ-calculus formula, that is, one with no free variables. For any two environments \(\mathrm{env}\) and \(\mathrm{env}'\), each assigning a set of worlds to every variable index, and every world \(w\), \(\varphi\) is satisfied at \(w\) in \(M\) under \(\mathrm{env}\) if and only if it is satisfied at \(w\) in \(M\) under \(\mathrm{env}'\).

theorem sat_closed (M : KripkeModel World Atom) {φ : MuFormula Atom}
    (hφ : Closed φ) (env env' : ℕ → World → Prop) (w : World) :
    sat M env φ w ↔ sat M env' φ w

Uses 5

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

Proof usesSatisfaction depends only on the environment below the closure depth

DefinitionThe one-world reflexive Kripke model#✓fully proved

The Kripke model with a single world, which is related to itself, and a single atom, which is false at that world.

def counterexampleModel : KripkeModel Unit Unit where
  nonempty_world := ⟨Unit.unit⟩
  rel := fun _ _ => True
  valuation := fun _ _ => False

Uses 1 · Used by 2

Statement usesKripke model

Used byThe regression play is a play · \(\mu X.\, \nu Y.\, X\) is false in the one-world model

DefinitionA least fixpoint over a vacuous greatest fixpoint#✓fully proved

The μ-calculus formula \(\mu X.\, \nu Y.\, X\) over a one-element type of atoms: a least fixpoint whose body is a greatest fixpoint whose body is the variable \(X\) bound by the outer least fixpoint, so the variable \(Y\) bound by the inner greatest fixpoint never occurs.

Its denotation is empty: the outer functional is the identity, and the least fixed point of the identity on predicates is the empty predicate.

def counterexampleFormula : MuFormula Unit := .mu (.nu (.var 1))

Uses 1 · Used by 1

Statement usesFormulas of the modal μ-calculus

Used by\(\mu X.\, \nu Y.\, X\) is false in the one-world model

DefinitionStarting position of the regression play#✓fully proved

The game position consisting of the formula \(\mu X.\,\nu Y.\,X\), the unique world of the one-world model, and the empty binder stack.

def cePos0 : GamePosition Unit Unit :=
  ⟨.mu (.nu (.var 1)), Unit.unit, []⟩

Uses 2 · Used by 8

Statement usesPosition of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byRegression cycle, first step · Regression cycle, third step · The regression play · The regression play stays on the cycle · The regression play is a play · The regression play returns to its start every three steps · Priority of the outer binder in the regression play · Verifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

DefinitionSecond position of the regression play#✓fully proved

The game position consisting of the formula \(\nu Y.\,X\), the unique world of the one-world model, and the binder stack \([\mu X.\,\nu Y.\,X]\). Here \(X\) is the de Bruijn variable \(1\), which refers to the binder \(\mu X\) on the stack.

def cePos1 : GamePosition Unit Unit :=
  ⟨.nu (.var 1), Unit.unit, [.mu (.nu (.var 1))]⟩

Uses 2 · Used by 6

Statement usesPosition of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byRegression cycle, first step · Regression cycle, second step · The regression play stays on the cycle · The regression play is a play · Priority of the inner binder in the regression play · Verifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

DefinitionThird position of the regression play#✓fully proved

The game position consisting of the variable \(X\), the unique world of the one-world model, and the binder stack \([\nu Y.\,X,\ \mu X.\,\nu Y.\,X]\), listed innermost first. Here \(X\) is the de Bruijn variable \(1\), which refers to the outer binder \(\mu X\).

def cePos2 : GamePosition Unit Unit :=
  ⟨.var 1, Unit.unit, [.nu (.var 1), .mu (.nu (.var 1))]⟩

Uses 2 · Used by 5

Statement usesPosition of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byRegression cycle, second step · Regression cycle, third step · The regression play stays on the cycle · The regression play is a play · Verifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

DefinitionStep map of the regression play#✓fully proved

Let \(\Phi = \mu X.\, \nu Y.\, X\) be the regression formula over the one-element type of atoms, and write game positions over the one-element type of worlds as (formula, world, stack of enclosing binders, innermost first). For every world \(w\), the step map sends \((\Phi, w, [\,])\) to \((\nu Y.\, X, w, [\Phi])\), sends \((\nu Y.\, X, w, [\Phi])\) to \((X, w, [\nu Y.\, X, \Phi])\), and sends \((X, w, [\nu Y.\, X, \Phi])\) to \((\Phi, w, [\,])\), where \(X\) is the variable bound by the outer \(\mu\); every other game position is sent to itself.

def ceNext : GamePosition Unit Unit → GamePosition Unit Unit
  | ⟨.mu (.nu (.var 1)), w, []⟩ => ⟨.nu (.var 1), w, [.mu (.nu (.var 1))]⟩
  | ⟨.nu (.var 1), w, [.mu (.nu (.var 1))]⟩ =>
      ⟨.var 1, w, [.nu (.var 1), .mu (.nu (.var 1))]⟩
  | ⟨.var 1, w, [.nu (.var 1), .mu (.nu (.var 1))]⟩ =>
      ⟨.mu (.nu (.var 1)), w, []⟩
  | p => p

Uses 2 · Used by 7

Statement usesPosition of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byRegression cycle, first step · Regression cycle, second step · Regression cycle, third step · The regression play · The regression play stays on the cycle · The regression play is a play · The regression play has period three

DefinitionThe regression play#✓fully proved

Write \(\ast\) for the unique world, and consider the game positions (formula, world, binder stack listed innermost first) \(P_0 = (\mu X.\,\nu Y.\,X,\ \ast,\ [\,])\), \(P_1 = (\nu Y.\,X,\ \ast,\ [\mu X.\,\nu Y.\,X])\) and \(P_2 = (X,\ \ast,\ [\nu Y.\,X,\ \mu X.\,\nu Y.\,X])\). Let \(s\) be the step map sending \(P_0\) to \(P_1\), \(P_1\) to \(P_2\) and \(P_2\) to \(P_0\), and fixing every other position. The regression play is the sequence of positions \(p_0 = P_0\), \(p_{n+1} = s(p_n)\), which cycles through \(P_0, P_1, P_2\).

These are the successive positions of the model-checking game for \(\mu X.\,\nu Y.\,X\) on the one-world model.

def cePlay : ℕ → GamePosition Unit Unit
  | 0 => cePos0
  | n + 1 => ceNext (cePlay n)

Uses 3 · Used by 5

Statement usesPosition of the μ-calculus model-checking game · Step map of the regression play · Starting position of the regression play

Used byThe regression play stays on the cycle · The regression play is a play · The regression play returns to its start every three steps · The regression play has period three · Verifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

TheoremRegression cycle, first step#✓fully proved

Let \(\Phi = \mu X.\, \nu Y.\, X\) be the regression formula, \(\ast\) the unique world, and write game positions as (formula, world, stack of enclosing binders, innermost first). The step map of the regression play sends the first cycle position \((\Phi, \ast, [\,])\) to the second cycle position \((\nu Y.\, X, \ast, [\Phi])\).

theorem ceNext_cePos0 : ceNext cePos0 = cePos1

Uses 4 · Used by 1

Statement usesPosition of the μ-calculus model-checking game · Step map of the regression play · Starting position of the regression play · Second position of the regression play

Used byThe regression play stays on the cycle

TheoremRegression cycle, second step#✓fully proved

Let \(\Phi = \mu X.\, \nu Y.\, X\) be the regression formula, \(\ast\) the unique world, and write game positions as (formula, world, stack of enclosing binders, innermost first). The step map of the regression play sends the second cycle position \((\nu Y.\, X, \ast, [\Phi])\) to the third cycle position \((X, \ast, [\nu Y.\, X, \Phi])\), where \(X\) is the variable bound by the outer \(\mu\).

theorem ceNext_cePos1 : ceNext cePos1 = cePos2

Uses 4 · Used by 1

Statement usesPosition of the μ-calculus model-checking game · Step map of the regression play · Second position of the regression play · Third position of the regression play

Used byThe regression play stays on the cycle

TheoremRegression cycle, third step#✓fully proved

Let \(\Phi = \mu X.\, \nu Y.\, X\) be the regression formula, \(\ast\) the unique world, and write game positions as (formula, world, stack of enclosing binders, innermost first). The step map of the regression play sends the third cycle position \((X, \ast, [\nu Y.\, X, \Phi])\), where \(X\) is the variable bound by the outer \(\mu\), back to the first cycle position \((\Phi, \ast, [\,])\).

theorem ceNext_cePos2 : ceNext cePos2 = cePos0

Uses 4 · Used by 1

Statement usesPosition of the μ-calculus model-checking game · Step map of the regression play · Starting position of the regression play · Third position of the regression play

Used byThe regression play stays on the cycle

TheoremThe regression play stays on the cycle#✓fully proved

For every \(n \in \mathbb{N}\), the position at step \(n\) of the regression play is the first, the second or the third cycle position.

theorem cePlay_mem (n : ℕ) :
    cePlay n = cePos0 ∨ cePlay n = cePos1 ∨ cePlay n = cePos2

Uses 9 · Used by 2

Statement usesPosition of the μ-calculus model-checking game · The regression play · Starting position of the regression play · Second position of the regression play · Third position of the regression play

Proof usesStep map of the regression play · Regression cycle, first step · Regression cycle, second step · Regression cycle, third step

Used byThe regression play is a play · Verifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

TheoremThe regression play has period three#✓fully proved

Number the positions of the regression play from \(0\). For every natural number \(n\), its position number \(n + 3\) equals its position number \(n\).

theorem cePlay_period (n : ℕ) : cePlay (n + 3) = cePlay n

Uses 3 · Used by 1

Statement usesPosition of the μ-calculus model-checking game · The regression play

Proof usesStep map of the regression play

Used byThe regression play returns to its start every three steps

TheoremThe regression play returns to its start every three steps#✓fully proved

Number the positions of the regression play of \(\mu X.\,\nu Y.\,X\) from \(0\). For every natural number \(k\), its position number \(3k\) is its starting position: the formula \(\mu X.\,\nu Y.\,X\) at the unique world, with the empty binder stack.

theorem cePlay_mul_three (k : ℕ) : cePlay (3 * k) = cePos0

Uses 4 · Used by 1

Statement usesPosition of the μ-calculus model-checking game · The regression play · Starting position of the regression play

Proof usesThe regression play has period three

Used byVerifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

TheoremThe regression play is a play#✓fully proved

For every \(n \in \mathbb{N}\), in the model-checking game on the one-world regression model there is a move from the position at step \(n\) of the regression play to the position at step \(n + 1\).

theorem cePlay_moves (n : ℕ) :
    Move counterexampleModel (cePlay n) (cePlay (n + 1))

Uses 11

Statement usesMoves of the μ-calculus model-checking game · The regression play · The one-world reflexive Kripke model

Proof usesKripke model · Position of the μ-calculus model-checking game · Step map of the regression play · The regression play stays on the cycle · Starting position of the regression play · Second position of the regression play · Third position of the regression play · Formulas of the modal μ-calculus

TheoremPriority of the outer binder in the regression play#✓fully proved

The starting position of the regression play, consisting of the formula \(\mu X.\,\nu Y.\,X\), the unique world and the empty binder stack, has priority \(1\): a \(\mu\)-binder position with \(k\) binders on the stack has priority \(2k + 1\), and here \(k = 0\).

Under fixed priorities (\(\mu \mapsto 1\), \(\nu \mapsto 2\)) the greatest priority recurring on this play would be \(2\) (even, Verifier wins); with priorities increasing with nesting depth (the inner \(\nu\) here has priority \(4\)) and the least-priority rule, the least binder priority recurring on this play is \(1\) (odd, Refuter wins).

theorem ce_prio0 : prio (cePos0 : GamePosition Unit Unit) = some 1

Uses 2 · Used by 1

Statement usesStarting position of the regression play · Priority of a game position

Used byVerifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

TheoremPriority of the inner binder in the regression play#✓fully proved

The second position of the regression play, consisting of the formula \(\nu Y.\,X\), the unique world and the binder stack \([\mu X.\,\nu Y.\,X]\), has priority \(4\): a \(\nu\)-binder position with \(k\) binders on the stack has priority \(2k + 2\), and here \(k = 1\).

theorem ce_prio1 : prio (cePos1 : GamePosition Unit Unit) = some 4

Uses 2 · Used by 1

Statement usesSecond position of the regression play · Priority of a game position

Used byVerifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)

TheoremVerifier loses the infinite play of \(\mu X.\, \nu Y.\, X\)#✓fully proved

Consider the infinite sequence of positions of the model-checking game for \(\mu X.\, \nu Y.\, X\) (with one-element types of worlds and atoms) that starts at this formula with empty binder stack and repeats three steps: unfold \(\mu X\), unfold \(\nu Y\), and follow the variable \(X\) back to the formula with empty stack. This play does not satisfy the parity condition: it is not the case that the least binder priority occurring infinitely often is even.

theorem counterexample_parityWin_false : ¬ ParityWin cePlay

Uses 11

Statement usesParity winning condition · The regression play

Proof usesPosition of the μ-calculus model-checking game · The regression play stays on the cycle · The regression play returns to its start every three steps · Starting position of the regression play · Second position of the regression play · Third position of the regression play · Priority of the outer binder in the regression play · Priority of the inner binder in the regression play · Priority of a game position

Theorem\(\mu X.\, \nu Y.\, X\) is false in the one-world model#✓fully proved

In the Kripke model with a single world, which is related to itself, and a single atom, which is false there, under the environment that assigns the empty set to every variable, the formula \(\mu X.\, \nu Y.\, X\) is not satisfied at the unique world.

This agrees with the model-checking game, where Verifier loses the play of this formula.

theorem counterexample_sat_false :
    ¬ sat counterexampleModel (fun _ => fun _ => False)
      counterexampleFormula Unit.unit

Uses 6

Statement usesA least fixpoint over a vacuous greatest fixpoint · The one-world reflexive Kripke model · Satisfaction in the modal μ-calculus

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

The fixpoint-free fragment

InductiveFixpoint-free formulas#✓fully proved

The fixpoint-free formulas over a type of atoms are built from atoms \(p\), negated atoms \(\neg p\), \(\bot\) and \(\top\) by conjunction \(\varphi \land \psi\), disjunction \(\varphi \lor \psi\), necessity \(\Box\varphi\) and possibility \(\Diamond\varphi\).

These are the formulas of basic modal logic in negation normal form: the μ-calculus formulas with no fixpoint operators and no variables.

Cslib.Modal.MuCalculus.Game.FixFreeFormula · 17 lines

inductive FixFreeFormula (Atom : Type u) : Type u where
  /-- An atom. -/
  | atom : Atom → FixFreeFormula Atom
  /-- A negated atom. -/
  | natom : Atom → FixFreeFormula Atom
  /-- Falsity. -/
  | bot : FixFreeFormula Atom
  /-- Truth. -/
  | top : FixFreeFormula Atom
  /-- Conjunction. -/
  | and : FixFreeFormula Atom → FixFreeFormula Atom → FixFreeFormula Atom
  /-- Disjunction. -/
  | or : FixFreeFormula Atom → FixFreeFormula Atom → FixFreeFormula Atom
  /-- Necessity. -/
  | box : FixFreeFormula Atom → FixFreeFormula Atom
  /-- Possibility. -/
  | dia : FixFreeFormula Atom → FixFreeFormula Atom

Used by 45

Used byCanonical 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 · 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 · Positions of the totalized fragment game · Terminal losing positions are not won by the even player · Priorities in the totalized fragment game · 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 · The losing state is absorbing · The lose play · The lose play stays at the losing state · The lose play starts at its fragment position · Fragment moves decrease the formula size · No infinite play from a fragment 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 · 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 region of the fixpoint-free fragment · 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 every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionEmbedding of the fixpoint-free fragment into the μ-calculus#✓fully proved

The map from fixpoint-free formulas to μ-calculus formulas defined by recursion: atoms, negated atoms, \(\bot\) and \(\top\) go to the same atom, negated atom, \(\bot\) and \(\top\), and \(\varphi \wedge \psi\), \(\varphi \vee \psi\), \(\Box \varphi\) and \(\Diamond \varphi\) go to the conjunction, disjunction, box and diamond of the images of \(\varphi\) and \(\psi\).

def toMu : FixFreeFormula Atom → MuFormula Atom
  | .atom a => .atom a
  | .natom a => .natom a
  | .bot => .bot
  | .top => .top
  | .and φ ψ => .and (toMu φ) (toMu ψ)
  | .or φ ψ => .or (toMu φ) (toMu ψ)
  | .box φ => .box (toMu φ)
  | .dia φ => .dia (toMu φ)

Uses 2 · Used by 36

Statement usesFixpoint-free formulas · Formulas of the modal μ-calculus

Used byCanonical 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 · Moves of the totalized fragment game · Moves of the totalized fragment game, by cases · 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 · The losing state is absorbing · Fragment moves decrease the formula size · No infinite play from a fragment 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 · The fixpoint-free embedding is injective · 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 every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

DefinitionBackward-induction winning region of the fixpoint-free fragment#✓fully proved

Let \(M\) be a Kripke model with accessibility relation \(R\). For a fixpoint-free formula \(\varphi\) and a world \(w\), "\(\varphi\) is winning at \(w\)" is defined by recursion on \(\varphi\): an atom \(a\) is winning at \(w\) iff \(a\) is true at \(w\) in \(M\); a negated atom \(\lnot a\) iff \(a\) is not true at \(w\); \(\bot\) is never winning and \(\top\) is always winning; \(\varphi \land \psi\) is winning at \(w\) iff both \(\varphi\) and \(\psi\) are; \(\varphi \lor \psi\) iff \(\varphi\) or \(\psi\) is; \(\Box \varphi\) iff \(\varphi\) is winning at every \(v\) with \(w \mathrel{R} v\); and \(\Diamond \varphi\) iff \(\varphi\) is winning at some \(v\) with \(w \mathrel{R} v\).

Verifier has a winning strategy in the model-checking game from the position \((\varphi, w, [])\) with empty stack exactly when \(\varphi\) is winning at \(w\).

def Wins (M : KripkeModel World Atom) : FixFreeFormula Atom → World → Prop
  | .atom a, w => M.valuation w a
  | .natom a, w => ¬ M.valuation w a
  | .bot, _ => False
  | .top, _ => True
  | .and φ ψ, w => Wins M φ w ∧ Wins M ψ w
  | .or φ ψ, w => Wins M φ w ∨ Wins M ψ w
  | .box φ, w => ∀ v, M.rel w v → Wins M φ v
  | .dia φ, w => ∃ v, M.rel w v ∧ Wins M φ v

Uses 2 · Used by 12

Statement usesKripke model · Fixpoint-free formulas

Used byThe fragment game's winning region is contained in Wins · Wins is the winning region of the fragment game · Game-vs-satisfaction, converse direction · 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 every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

TheoremBackward-induction winning equals satisfaction on the fixpoint-free fragment#✓fully proved

For every Kripke model \(M\), environment \(\mathit{env}\), fixpoint-free formula \(\varphi\) and world \(w\), \(w\) lies in the backward-induction winning region of \(\varphi\) if and only if \(w\) satisfies the μ-calculus embedding of \(\varphi\) in \(M\) under \(\mathit{env}\).

theorem wins_iff_sat (M : KripkeModel World Atom) (env : ℕ → World → Prop)
    (φ : FixFreeFormula Atom) (w : World) :
    Wins M φ w ↔ sat M env (FixFreeFormula.toMu φ) w

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 6

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Backward-induction winning region of the fixpoint-free fragment · Satisfaction in the modal μ-calculus

Proof usesFormulas of the modal μ-calculus

The Wins-guided strategy

DefinitionSize of a μ-calculus formula#✓fully proved

The size \(|\varphi|\) of a μ-calculus formula \(\varphi\) is the number of nodes of its syntax tree: an atom, a negated atom, a variable, \(\bot\) and \(\top\) have size \(1\); \(|\varphi \wedge \psi| = |\varphi \vee \psi| = |\varphi| + |\psi| + 1\); and \(|\Box\varphi| = |\Diamond\varphi| = |\mu\varphi| = |\nu\varphi| = |\varphi| + 1\).

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

Uses 1 · Used by 5

Statement usesFormulas of the modal μ-calculus

Used byThe canonical move follows the bespoke strategy at Verifier positions with a move · Positional strategy induced by a bespoke strategy · Fragment parity game · Fragment moves decrease the formula size · No infinite play from a fragment position

DefinitionPartial inverse of the fixpoint-free embedding#✓fully proved

The partial map from μ-calculus formulas to fixpoint-free formulas defined by recursion: an atom, a negated atom, \(\bot\) and \(\top\) are sent to the same formula; a conjunction or disjunction is sent to the conjunction or disjunction of the values at its two parts, and \(\Box\psi\), \(\Diamond\psi\) to the box or diamond of the value at \(\psi\), whenever those values are defined; the map is undefined at variables and at least and greatest fixpoints, and at every formula with a part where it is undefined.

It inverts the embedding of fixpoint-free formulas into μ-calculus formulas on its image.

def toMuInv : MuFormula Atom → Option (FixFreeFormula Atom)
  | .atom a => some (.atom a)
  | .natom a => some (.natom a)
  | .bot => some .bot
  | .top => some .top
  | .and φ ψ => (toMuInv φ).bind fun φ' => (toMuInv ψ).map (FixFreeFormula.and φ')
  | .or φ ψ => (toMuInv φ).bind fun φ' => (toMuInv ψ).map (FixFreeFormula.or φ')
  | .box φ => (toMuInv φ).map FixFreeFormula.box
  | .dia φ => (toMuInv φ).map FixFreeFormula.dia
  | _ => none

Uses 2 · Used by 9

Statement usesFixpoint-free formulas · Formulas of the modal μ-calculus

Used byProjection of game positions onto the fragment arena · Projection of an embedded position · The fixpoint-free embedding is injective · The partial inverse recovers fixpoint-free formulas · The embedding inverts the partial inverse · Wins-guided move · The Wins-guided move at a diamond · The Wins-guided move is legal · The Wins-guided move at a disjunction

TheoremThe partial inverse recovers fixpoint-free formulas#✓fully proved

For every fixpoint-free formula \(\varphi\), the partial inverse of the embedding of fixpoint-free formulas into μ-calculus formulas is defined at the image of \(\varphi\) under the embedding, with value \(\varphi\).

theorem toMuInv_toMu (φ : FixFreeFormula Atom) :
    toMuInv (FixFreeFormula.toMu φ) = some φ

Uses 4 · Used by 4

Statement usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Partial inverse of the fixpoint-free embedding

Proof usesFormulas of the modal μ-calculus

Used byProjection of an embedded position · The fixpoint-free embedding is injective · The Wins-guided move at a diamond · The Wins-guided move at a disjunction

TheoremThe embedding inverts the partial inverse#✓fully proved

For every μ-calculus formula \(\psi\) and every fixpoint-free formula \(\varphi\): if the partial inverse of the embedding of fixpoint-free formulas into μ-calculus formulas is defined at \(\psi\) with value \(\varphi\), then the embedding sends \(\varphi\) to \(\psi\).

theorem toMu_toMuInv {φ : FixFreeFormula Atom} {ψ : MuFormula Atom}
    (h : toMuInv ψ = some φ) : FixFreeFormula.toMu φ = ψ

Uses 4 · Used by 1

Statement usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Partial inverse of the fixpoint-free embedding · Formulas of the modal μ-calculus

Used byThe Wins-guided move is legal

TheoremThe fixpoint-free embedding is injective#✓fully proved

The embedding of fixpoint-free formulas into μ-calculus formulas is injective: distinct fixpoint-free formulas have distinct images.

This is what lets the canonical fragment game recover a fragment formula from an embedded game position.

theorem FixFreeFormula.toMu_injective :
    Function.Injective (FixFreeFormula.toMu (Atom := Atom))

Uses 5 · Used by 1

Statement usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Formulas of the modal μ-calculus

Proof usesPartial inverse of the fixpoint-free embedding · The partial inverse recovers fixpoint-free formulas

Used byThe fragment game's winning region is contained in Wins

DefinitionWins-guided move#✓fully proved

Let \(M\) be a Kripke model, and identify each fixpoint-free formula with its embedding into the μ-calculus. For a μ-calculus formula \(\psi\), a world \(w\) and a stack \(s\) of fixpoint binders, the Wins-guided move at the game position \((\psi, w, s)\) is the following position. If \(s\) is empty and \(\psi\) is a fixpoint-free disjunction \(\psi_1 \lor \psi_2\), it is \((\psi_1, w, [])\) when \(\psi_1\) is winning at \(w\) (in the backward-induction winning region of the fixpoint-free fragment) and \((\psi_2, w, [])\) otherwise. If \(s\) is empty and \(\psi\) is a fixpoint-free formula \(\Diamond \psi_1\), it is \((\psi_1, v, [])\) for a chosen successor \(v\) of \(w\) at which \(\psi_1\) is winning, if one exists; otherwise \((\psi_1, v, [])\) for a chosen successor \(v\) of \(w\), if one exists; otherwise \((\psi, w, [])\). In every other case: at a disjunction \(\varphi_1 \lor \varphi_2\) it is \((\varphi_1, w, s)\); at \(\Diamond \varphi_1\) it is \((\varphi_1, v, s)\) for a chosen successor \(v\) of \(w\) if one exists, and \((\psi, w, s)\) otherwise; at \(\nu \varphi_1\) it is \((\varphi_1, w, s')\), where \(s'\) is \(s\) with \(\nu \varphi_1\) pushed on top; and at every remaining formula (the positions owned by Refuter) it is \((\psi, w, s)\).

Only the left disjunct is tested: if a fixpoint-free disjunction is winning at \(w\) and its left disjunct is not, then its right disjunct is.

Cslib.Modal.MuCalculus.Game.winsMove · 29 lines

noncomputable def winsMove (M : KripkeModel World Atom) (ψ : MuFormula Atom) (w : World)
    (st : List (MuFormula Atom)) : GamePosition Atom World :=
  match ψ, st with
  | .or φ₁ φ₂, [] =>
      match toMuInv (.or φ₁ φ₂) with
      | some (.or ψ₁ ψ₂) =>
          if _ : Wins M ψ₁ w then
            (⟨FixFreeFormula.toMu ψ₁, w, []⟩ : GamePosition Atom World)
          else (⟨FixFreeFormula.toMu ψ₂, w, []⟩ : GamePosition Atom World)
      | _ => (⟨φ₁, w, []⟩ : GamePosition Atom World)
  | .dia φ₁, [] =>
      match toMuInv (.dia φ₁) with
      | some (.dia ψ₁) =>
          if h : ∃ v, M.rel w v ∧ Wins M ψ₁ v then
            (⟨FixFreeFormula.toMu ψ₁, Classical.choose h, []⟩ : GamePosition Atom World)
          else if hsucc : ∃ v, M.rel w v then
            (⟨φ₁, Classical.choose hsucc, []⟩ : GamePosition Atom World)
          else (⟨.dia φ₁, w, []⟩ : GamePosition Atom World)
      | _ =>
          if h : ∃ v, M.rel w v then
            (⟨φ₁, Classical.choose h, []⟩ : GamePosition Atom World)
          else (⟨.dia φ₁, w, []⟩ : GamePosition Atom World)
  | .or φ₁ _, st => (⟨φ₁, w, st⟩ : GamePosition Atom World)
  | .dia φ₁, st =>
      if h : ∃ v, M.rel w v then
        (⟨φ₁, Classical.choose h, st⟩ : GamePosition Atom World)
      else (⟨.dia φ₁, w, st⟩ : GamePosition Atom World)
  | .nu φ₁, st => (⟨φ₁, w, .nu φ₁ :: st⟩ : GamePosition Atom World)
  | _, _ => (⟨ψ, w, st⟩ : GamePosition Atom World)

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 7 · Used by 5

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Position of the μ-calculus model-checking game · Backward-induction winning region of the fixpoint-free fragment · Partial inverse of the fixpoint-free embedding · Formulas of the modal μ-calculus

Used byThe 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 finite plays (auxiliary induction)

TheoremThe Wins-guided move at a disjunction#✓fully proved

Let \(M\) be a Kripke model, \(\varphi_1\) and \(\varphi_2\) fixpoint-free formulas and \(w\) a world in the backward-induction winning region of \(\varphi_1 \vee \varphi_2\). Then for some \(i \in \{1, 2\}\), \(w\) lies in the backward-induction winning region of \(\varphi_i\) and the Wins-guided move at the position made of the embedding of \(\varphi_1 \vee \varphi_2\), the world \(w\) and the empty binder stack is the position made of the embedding of \(\varphi_i\), the world \(w\) and the empty stack.

theorem winsMove_or {M : KripkeModel World Atom} {φ₁ φ₂ : FixFreeFormula Atom} {w : World}
    (hW : Wins M (.or φ₁ φ₂) w) :
    (winsMove M (FixFreeFormula.toMu (.or φ₁ φ₂)) w [] =
        ⟨FixFreeFormula.toMu φ₁, w, []⟩ ∧ Wins M φ₁ w) ∨
    (winsMove M (FixFreeFormula.toMu (.or φ₁ φ₂)) w [] =
        ⟨FixFreeFormula.toMu φ₂, w, []⟩ ∧ Wins M φ₂ w)

Uses 9 · Used by 1

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Position of the μ-calculus model-checking game · Backward-induction winning region of the fixpoint-free fragment · Wins-guided move · Formulas of the modal μ-calculus

Proof usesPartial inverse of the fixpoint-free embedding · The partial inverse recovers fixpoint-free formulas

Used byWins-guided strategy wins finite plays (auxiliary induction)

TheoremThe Wins-guided move at a diamond#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a fixpoint-free formula and \(w\) a world in the backward-induction winning region of \(\Diamond \varphi\). Then there is a successor \(v\) of \(w\) in \(M\) lying in the backward-induction winning region of \(\varphi\) such that the Wins-guided move at the position made of the embedding of \(\Diamond \varphi\), the world \(w\) and the empty binder stack is the position made of the embedding of \(\varphi\), the world \(v\) and the empty stack.

theorem winsMove_dia {M : KripkeModel World Atom} {φ₁ : FixFreeFormula Atom} {w : World}
    (hW : Wins M (.dia φ₁) w) :
    ∃ v, winsMove M (FixFreeFormula.toMu (.dia φ₁)) w [] =
        ⟨FixFreeFormula.toMu φ₁, v, []⟩ ∧ M.rel w v ∧ Wins M φ₁ v

Uses 9 · Used by 1

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Position of the μ-calculus model-checking game · Backward-induction winning region of the fixpoint-free fragment · Wins-guided move · Formulas of the modal μ-calculus

Proof usesPartial inverse of the fixpoint-free embedding · The partial inverse recovers fixpoint-free formulas

Used byWins-guided strategy wins finite plays (auxiliary induction)

TheoremThe Wins-guided move is legal#✓fully proved

For a Kripke model \(M\) and a game position \(p\) owned by Verifier from which some move exists, the Wins-guided move at \(p\) is a legal move of the model-checking game on \(M\) from \(p\).

theorem winsMove_isMove (M : KripkeModel World Atom) (p : GamePosition Atom World)
    (hOwn : Owner p = true) (hExists : ∃ q, Move M p q) :
    Move M p (winsMove M p.1 p.2.1 p.2.2)

Uses 12 · Used by 1

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game · Wins-guided move · Formulas of the modal μ-calculus

Proof usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Backward-induction winning region of the fixpoint-free fragment · Partial inverse of the fixpoint-free embedding · The embedding inverts the partial inverse

Used byWins-guided strategy

DefinitionWins-guided strategy#✓fully proved

For a Kripke model \(M\), the Wins-guided strategy is the Verifier strategy of the model-checking game on \(M\) that chooses, at each game position \((\psi, w, s)\), the Wins-guided move at \((\psi, w, s)\). At every Verifier-owned position that has a move, this choice is a legal move.

noncomputable def winsStrategy (M : KripkeModel World Atom) : Strategy M where
  choose p := winsMove M p.1 p.2.1 p.2.2
  choose_move p hOwn hExists := winsMove_isMove M p hOwn hExists

Uses 9 · Used by 3

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game · Verifier strategy · Wins-guided move · The Wins-guided move is legal · Formulas of the modal μ-calculus

Used byGame-vs-satisfaction, strategy direction · Wins-guided strategy wins every complete finite play · Wins-guided strategy wins finite plays (auxiliary induction)

Play lemmas

TheoremFinite plays are nonempty#✓fully proved

Let \(M\) be a Kripke model, \(\sigma\) a Verifier strategy and \(p\) a game position. Every finite play from \(p\) consistent with \(\sigma\) is a nonempty list of positions.

theorem PlayFrom.ne_nil {M : KripkeModel World Atom} {σ : Strategy M}
    {p : GamePosition Atom World} {ps : List (GamePosition Atom World)}
    (h : PlayFrom M σ p ps) : ps ≠ []

Uses 7 · Used by 2

Statement usesKripke model · Position of the μ-calculus model-checking game · Finite plays consistent with a strategy · Verifier strategy

Proof usesMoves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game

Used byWinning strategies stay winning along consistent moves · Wins-guided strategy wins finite plays (auxiliary induction)

TheoremPrepending to a nonempty play keeps the last position#✓fully proved

For a game position \(p\) and a nonempty list \(ps\) of game positions, the list obtained by prepending \(p\) to \(ps\) has the same last position as \(ps\).

theorem playLast_cons {p : GamePosition Atom World} {ps : List (GamePosition Atom World)}
    (hne : ps ≠ []) : playLast (p :: ps) = playLast ps

Uses 2 · Used by 3

Statement usesPosition of the μ-calculus model-checking game · Last position of a play

Used byLast position of a segment · Winning strategies stay winning along consistent moves · Wins-guided strategy wins finite plays (auxiliary induction)

TheoremFragment moves decrease the formula size#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a fixpoint-free formula and \(w\) a world. Every move of the model-checking game in \(M\) from the position \((\varphi, w, [\,])\), with \(\varphi\) embedded in the μ-calculus and the empty stack, leads to a position \((\varphi', w', [\,])\) for some fixpoint-free formula \(\varphi'\) and world \(w'\), and the size of \(\varphi'\) is strictly smaller than the size of \(\varphi\) (sizes of the embedded μ-calculus formulas).

theorem move_of_toMu {M : KripkeModel World Atom} {φ : FixFreeFormula Atom} {w : World}
    {q : GamePosition Atom World} (h : Move M ⟨FixFreeFormula.toMu φ, w, []⟩ q) :
    ∃ φ' : FixFreeFormula Atom, ∃ w' : World, q = ⟨FixFreeFormula.toMu φ', w', []⟩ ∧
      MuFormula.size (FixFreeFormula.toMu φ') < MuFormula.size (FixFreeFormula.toMu φ)

Uses 7 · Used by 4

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Size of a μ-calculus formula · Formulas of the modal μ-calculus

Used byThe canonical move follows the bespoke strategy at Verifier positions with a move · Positional strategy induced by a bespoke strategy · Fragment parity game · No infinite play from a fragment position

TheoremNo infinite play from a fragment position#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a fixpoint-free formula and \(w\) a world. There is no sequence of game positions \(p_0, p_1, p_2, \dots\) with \(p_0 = (\varphi, w, [\,])\) (the embedded formula with the empty stack) such that each step from \(p_n\) to \(p_{n+1}\) is a move of the model-checking game in \(M\). The reason is that every move strictly decreases the formula size.

theorem no_infinite_play_of_fixFree {M : KripkeModel World Atom} {φ : FixFreeFormula Atom}
    {w : World} {play : ℕ → GamePosition Atom World}
    (h0 : play 0 = ⟨FixFreeFormula.toMu φ, w, []⟩)
    (hsteps : ∀ n, Move M (play n) (play (n + 1))) : False

Uses 8 · Used by 2

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Proof usesSize of a μ-calculus formula · Fragment moves decrease the formula size

Used byWinning Verifier strategies transfer to the fragment game · Game-vs-satisfaction, strategy direction

TheoremWinning strategies stay winning along consistent moves#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment and \(\sigma\) a Verifier strategy for the model-checking game on \(M\). If \(\sigma\) wins from a position \(p\) in \(\mathit{env}\), and \(q\) is a position reachable from \(p\) by one move that is the position chosen by \(\sigma\) at \(p\) whenever Verifier owns \(p\), then \(\sigma\) also wins from \(q\) in \(\mathit{env}\).

theorem strategyWins_of_move {M : KripkeModel World Atom} {env : ℕ → World → Prop}
    {σ : Strategy M} {p q : GamePosition Atom World} (hW : StrategyWins M env σ p)
    (hmove : Move M p q) (hσ : Owner p = true → q = σ.choose p) :
    StrategyWins M env σ q

Uses 15 · Used by 1

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game · Verifier strategy · Winning strategy from a position

Proof usesPositions with no moves · Parity winning condition · Finite plays consistent with a strategy · Finite plays are nonempty · Winner at a terminal position · Last position of a play · Prepending to a nonempty play keeps the last position · Priority of a game position

Used byGame-vs-satisfaction, converse direction

TheoremWins-guided strategy wins finite plays (auxiliary induction)#✓fully proved

The Wins-guided strategy wins every complete finite play from a winning fragment position.

theorem winsStrategy_wins_finite_aux (M : KripkeModel World Atom)
    {env : ℕ → World → Prop} {p : GamePosition Atom World}
    {ps : List (GamePosition Atom World)}
    (hplay : PlayFrom M (winsStrategy M) p ps) :
    (∀ (φ : FixFreeFormula Atom) (w : World), p = ⟨FixFreeFormula.toMu φ, w, []⟩ →
      Wins M φ w → (∃ q, playLast ps = some q ∧ NoMoves M q) →
        ∃ q, playLast ps = some q ∧ TerminalWin M env q)

Uses 20 · Used by 1

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Position of the μ-calculus model-checking game · Positions with no moves · Finite plays consistent with a strategy · Winner at a terminal position · Backward-induction winning region of the fixpoint-free fragment · Last position of a play · Wins-guided strategy · Formulas of the modal μ-calculus

Proof usesMoves of the μ-calculus model-checking game · Owner of a game position · Finite plays are nonempty · Player of the μ-calculus model-checking game · Verifier strategy · Prepending to a nonempty play keeps the last position · Wins-guided move · The Wins-guided move at a diamond · The Wins-guided move at a disjunction

Used byWins-guided strategy wins every complete finite play

TheoremWins-guided strategy wins every complete finite play#✓fully proved

The Wins-guided strategy wins every complete finite play from a winning fragment position.

theorem winsStrategy_wins_finite (M : KripkeModel World Atom)
    {env : ℕ → World → Prop} :
    ∀ (φ : FixFreeFormula Atom) (w : World), Wins M φ w →
      ∀ ps : List (GamePosition Atom World),
        PlayFrom M (winsStrategy M) ⟨FixFreeFormula.toMu φ, w, []⟩ ps →
          (∃ q, playLast ps = some q ∧ NoMoves M q) →
            ∃ q, playLast ps = some q ∧ TerminalWin M env q

Uses 12 · Used by 1

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Position of the μ-calculus model-checking game · Positions with no moves · Finite plays consistent with a strategy · Winner at a terminal position · Backward-induction winning region of the fixpoint-free fragment · Last position of a play · Wins-guided strategy · Formulas of the modal μ-calculus

Proof usesWins-guided strategy wins finite plays (auxiliary induction)

Used byGame-vs-satisfaction, strategy direction

TheoremGame-vs-satisfaction, strategy direction#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment assigning a set of worlds to each variable index, \(\varphi\) a fixpoint-free formula and \(w\) a world in the backward-induction winning region of \(\varphi\). Then Verifier has a winning strategy, in environment \(\mathit{env}\), in the model-checking game on \(M\) from the position made of the μ-calculus embedding of \(\varphi\), the world \(w\) and the empty binder stack.

theorem wins_implies_verifierWins (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) (φ : FixFreeFormula Atom)
    (w : World) (hW : Wins M φ w) :
    VerifierWins M env ⟨FixFreeFormula.toMu φ, w, []⟩

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 20 · Used by 2

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Verifier has a winning strategy · Backward-induction winning region of the fixpoint-free fragment · Formulas of the modal μ-calculus

Proof usesPosition of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Positions with no moves · Owner of a game position · Parity winning condition · Finite plays consistent with a strategy · Player of the μ-calculus model-checking game · Verifier strategy · Winning strategy from a position · Winner at a terminal position · No infinite play from a fragment position · Last position of a play · Wins-guided strategy · Wins-guided strategy wins every complete finite play

Used byWins is the winning region of the fragment game · Backward-induction winning equals game winning on the fixpoint-free fragment

TheoremInversion for disjunction moves#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) and \(\psi\) μ-calculus formulas, \(w\) a world and \(s\) a stack of fixpoint binders. If going from the game position \((\varphi \vee \psi, w, s)\) to a position \(q\) is a move of the model-checking game in \(M\), then \(q\) is \((\varphi, w, s)\) or \((\psi, w, s)\): the world and the stack are unchanged.

theorem Move.or_cases {M : KripkeModel World Atom} {φ ψ : MuFormula Atom} {w : World}
    {st : List (MuFormula Atom)} {q : GamePosition Atom World}
    (h : Move M ⟨.or φ ψ, w, st⟩ q) : q = ⟨φ, w, st⟩ ∨ q = ⟨ψ, w, st⟩

Uses 4 · Used by 2

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byThe fragment game's winning region is contained in Wins · Game-vs-satisfaction, converse direction

TheoremMoves from a diamond position#✓fully proved

In the model-checking game on a Kripke model \(M\), every move from the position with formula \(\Diamond\varphi\), world \(w\) and binder stack \(s\) goes to the position with formula \(\varphi\), world \(v\) and the same stack \(s\), for some world \(v\) accessible from \(w\) in \(M\).

theorem Move.dia_cases {M : KripkeModel World Atom} {φ : MuFormula Atom} {w : World}
    {st : List (MuFormula Atom)} {q : GamePosition Atom World}
    (h : Move M ⟨.dia φ, w, st⟩ q) :
    ∃ v, M.rel w v ∧ q = ⟨φ, v, st⟩

Uses 4 · Used by 2

Statement usesKripke model · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used byThe fragment game's winning region is contained in Wins · Game-vs-satisfaction, converse direction

TheoremGame-vs-satisfaction, converse direction#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment assigning a set of worlds to each variable index, \(\varphi\) a fixpoint-free formula and \(w\) a world. If Verifier has a winning strategy, in environment \(\mathit{env}\), in the model-checking game on \(M\) from the position made of the μ-calculus embedding of \(\varphi\), the world \(w\) and the empty binder stack, then \(w\) lies in the backward-induction winning region of \(\varphi\).

theorem verifierWins_implies_wins (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) (φ : FixFreeFormula Atom)
    (w : World) (hW : VerifierWins M env ⟨FixFreeFormula.toMu φ, w, []⟩) :
    Wins M φ w

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 20 · Used by 1

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Verifier has a winning strategy · Backward-induction winning region of the fixpoint-free fragment · Formulas of the modal μ-calculus

Proof usesPosition of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Moves from a diamond position · Inversion for disjunction moves · Positions with no moves · Owner of a game position · Parity winning condition · Finite plays consistent with a strategy · Player of the μ-calculus model-checking game · Verifier strategy · Winning strategy from a position · Winner at a terminal position · Last position of a play · Winning strategies stay winning along consistent moves

Used byBackward-induction winning equals game winning on the fixpoint-free fragment

TheoremBackward-induction winning equals game winning on the fixpoint-free fragment#✓fully proved

For every Kripke model \(M\), environment \(\mathit{env}\), fixpoint-free formula \(\varphi\) and world \(w\), \(w\) lies in the backward-induction winning region of \(\varphi\) if and only if Verifier has a winning strategy, in environment \(\mathit{env}\), in the model-checking game on \(M\) from the position made of the μ-calculus embedding of \(\varphi\), the world \(w\) and the empty binder stack.

theorem wins_iff_verifierWins (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) (φ : FixFreeFormula Atom) (w : World) :
    Wins M φ w ↔ VerifierWins M env ⟨FixFreeFormula.toMu φ, w, []⟩

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 8

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Verifier has a winning strategy · Backward-induction winning region of the fixpoint-free fragment · Formulas of the modal μ-calculus

Proof usesGame-vs-satisfaction, converse direction · Game-vs-satisfaction, strategy direction

The fragment game as a canonical parity game

InductivePositions of the totalized fragment game#✓fully proved

A position of the totalized fragment game, over a type of atoms and a type of worlds, is either an embedded position \((\varphi, w)\) of a fixpoint-free formula \(\varphi\) and a world \(w\), standing for the model-checking game position \((\varphi, w, [])\) with \(\varphi\) embedded as a μ-calculus formula and the empty fixpoint stack, or one of two absorbing states: the winning state, where Verifier has won, and the losing state, where Refuter has won.

Since the arena contains no fixpoint positions and every move between embedded positions strictly decreases the formula, priority \(0\) on embedded positions is sound. An embedded position with no moves leads to the winning state if it is a terminal win for Verifier and to the losing state otherwise, and both absorbing states loop to themselves, so the game has no dead ends and is a parity game.

inductive FragPos (Atom World : Type u) where
  /-- An embedded fragment position `(φ, w)`, standing for `⟨toMu φ, w, []⟩`. -/
  | pos : FixFreeFormula Atom → World → FragPos Atom World
  /-- Absorbing Verifier-wins state. -/
  | win : FragPos Atom World
  /-- Absorbing Refuter-wins state. -/
  | lose : FragPos Atom World

Uses 1 · Used by 34

Statement usesFixpoint-free formulas

Used byCanonical 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 · 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 · Plays of the totalized fragment game stay at the losing state · Plays of the totalized fragment game stay at the winning state · Terminal losing positions are not won by the even player · Priorities in the totalized fragment game · Segment of a fragment play as game positions · Splitting off the head of a segment · Segments are nonempty · Last position of a segment · 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 · The losing state is absorbing · The lose play · The lose play stays at the losing state · The lose play starts at its fragment 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 · The absorbing win state · Sequences that stay at the win state are won by the even player · Sequences that stay at the lose state are won by the odd player

DefinitionProjection of game positions onto the fragment arena#✓fully proved

A game position with empty binder stack whose formula is the μ-calculus reading of a fixpoint-free formula \(\varphi\), at world \(w\), is sent to the embedded position \((\varphi, w)\). Every other game position (one whose formula contains a fixpoint operator or a variable, or one with a nonempty stack) is sent to the losing state.

The losing state is a default that is never reached on plays that stay in the arena, since every move from an embedded position lands on an embedded position.

def fragOfGamePos : GamePosition Atom World → FragPos Atom World
  | ⟨ψ, w, []⟩ =>
      match toMuInv ψ with
      | some φ => .pos φ w
      | none => .lose
  | ⟨_, _, _ :: _⟩ => .lose

Sources

• C. Stirling, Modal and Temporal Properties of Processes, Springer 2001, Chapter 6.

Uses 5 · Used by 4

Statement usesFixpoint-free formulas · Positions of the totalized fragment game · Position of the μ-calculus model-checking game · Partial inverse of the fixpoint-free embedding · Formulas of the modal μ-calculus

Used byCanonical next move induced by a bespoke strategy · The canonical move follows the bespoke strategy at Verifier positions with a move · Projection of an embedded position · Positional strategy induced by a bespoke strategy

TheoremProjection of an embedded position#✓fully proved

For every fixpoint-free formula \(\varphi\) and world \(w\), projecting the game position with formula \(\varphi\) (read as a μ-calculus formula), world \(w\) and empty binder stack onto the fragment arena gives the embedded position \((\varphi, w)\).

theorem fragOfGamePos_toMu (φ : FixFreeFormula Atom) (w : World) :
    fragOfGamePos (⟨FixFreeFormula.toMu φ, w, []⟩ : GamePosition Atom World) =
      FragPos.pos φ w

Uses 7 · Used by 1

Statement usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Projection of game positions onto the fragment arena · Formulas of the modal μ-calculus

Proof usesPartial inverse of the fixpoint-free embedding · The partial inverse recovers fixpoint-free formulas

Used byThe canonical move follows the bespoke strategy at Verifier positions with a move

InductiveMoves of the totalized fragment game#✓fully proved

Let \(M\) be a Kripke model and \(e\) an environment, and read each fixpoint-free formula \(\varphi\) as a μ-calculus formula. The totalized fragment game of \(M\) and \(e\) has these moves: from an embedded position \((\varphi, w)\) to \((\varphi', w')\) whenever the model-checking game of \(M\) has a move from \((\varphi, w)\) to \((\varphi', w')\) with empty binder stacks; from \((\varphi, w)\) to the winning state when the game position \((\varphi, w)\) with empty stack has no moves and is won by Verifier in environment \(e\); from \((\varphi, w)\) to the losing state when that game position has no moves and is not won by Verifier; and from each of the winning and losing states to itself.

Cslib.Modal.MuCalculus.Game.FragMove · 21 lines

inductive FragMove (M : KripkeModel World Atom) (env : ℕ → World → Prop) :
    FragPos Atom World → FragPos Atom World → Prop
  /-- A game move between embedded fragment positions. -/
  | pos_move {φ φ' : FixFreeFormula Atom} {w w' : World}
      (h : Move M ⟨FixFreeFormula.toMu φ, w, []⟩
        ⟨FixFreeFormula.toMu φ', w', []⟩) :
      FragMove M env (.pos φ w) (.pos φ' w')
  /-- A terminal winning position moves to the absorbing win state. -/
  | toWin {φ : FixFreeFormula Atom} {w : World}
      (hNo : NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩)
      (hWin : TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩) :
      FragMove M env (.pos φ w) .win
  /-- A terminal losing position moves to the absorbing lose state. -/
  | toLose {φ : FixFreeFormula Atom} {w : World}
      (hNo : NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩)
      (hLose : ¬ TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩) :
      FragMove M env (.pos φ w) .lose
  /-- The win state loops. -/
  | win_self : FragMove M env .win .win
  /-- The lose state loops. -/
  | lose_self : FragMove M env .lose .lose

Uses 8 · Used by 15

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Moves of the μ-calculus model-checking game · Positions with no moves · Winner at a terminal position · Formulas of the modal μ-calculus

Used byVerifier's positional strategies make a game move at Verifier positions that have one · Segments of canonical plays through fragment positions are bespoke plays · Moves of the totalized fragment game, by cases · Plays of the totalized fragment game stay at the losing state · Plays of the totalized fragment game stay at the winning state · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Fragment parity game · The losing state is absorbing · 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 · The absorbing win state

DefinitionOwners in the totalized fragment game#✓fully proved

In the totalized fragment game, an embedded position \((\varphi, w)\) of a fixpoint-free formula \(\varphi\) at a world \(w\) is owned by the even player if Verifier owns the model-checking game position \((\varphi, w, [])\) (with \(\varphi\) embedded as a μ-calculus formula and the empty fixpoint stack), and by the odd player otherwise, that is, when Refuter owns it. The absorbing winning and losing states are both owned by the even player.

Verifier plays the even player; the moves at the absorbing states are forced, so their owner does not matter.

def fragOwner : FragPos Atom World → Cslib.Games.Player
  | .pos φ w =>
      if Owner ⟨FixFreeFormula.toMu φ, w, []⟩ = true then
        Cslib.Games.Player.even
      else Cslib.Games.Player.odd
  | .win => Cslib.Games.Player.even
  | .lose => Cslib.Games.Player.even

Uses 7 · Used by 4

Statement usesPlayers of a parity game · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Owner of a game position · Player of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used bySegments of canonical plays through fragment positions are bespoke plays · Owner of an embedded position in the totalized fragment game · Positional strategy induced by a bespoke strategy · Fragment parity game

DefinitionPriorities in the totalized fragment game#✓fully proved

In the totalized fragment game, every embedded position \((\varphi, w)\) of a fixpoint-free formula \(\varphi\) at a world \(w\) has priority \(0\), the absorbing winning state has priority \(0\), and the absorbing losing state has priority \(1\).

So an infinite play that eventually stays at the winning state is won by the even player, and one that eventually stays at the losing state by the odd player. Priority \(0\) on embedded positions is sound because the arena contains no fixpoint positions and every move between embedded positions strictly decreases the formula, so no infinite play visits only embedded positions.

def fragPriority : FragPos Atom World → ℕ
  | .pos _ _ => 0
  | .win => 0
  | .lose => 1

Uses 2 · Used by 3

Statement usesFixpoint-free formulas · Positions of the totalized fragment game

Used byFragment parity game · Sequences that stay at the win state are won by the even player · Sequences that stay at the lose state are won by the odd player

DefinitionFragment parity game#✓fully proved

Let \(M\) be a Kripke model and \(\rho\) an environment, and write \((\varphi, w, [])\) for the game position with formula \(\varphi\), world \(w\) and empty binder stack. The fragment game of \(M\) and \(\rho\) is the parity game on the totalized fragment positions defined as follows. An embedded position \((\varphi, w)\) moves to \((\varphi', w')\) when \((\varphi, w, [])\) has a move to \((\varphi', w', [])\) in the model-checking game on \(M\); if \((\varphi, w, [])\) has no moves, \((\varphi, w)\) moves to the winning state when \((\varphi, w, [])\) is a terminal win in \(\rho\) and to the losing state otherwise; the winning and losing states move only to themselves. The even player owns both absorbing states and the embedded positions \((\varphi, w)\) such that Verifier owns \((\varphi, w, [])\); the odd player owns the other embedded positions. Embedded positions and the winning state have priority \(0\); the losing state has priority \(1\).

Cslib.Modal.MuCalculus.Game.fragmentGame · 22 lines

noncomputable def fragmentGame (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) : Cslib.Games.ParityGame (FragPos Atom World) where
  owner := fragOwner
  Move := FragMove M env
  priority := fragPriority
  serial := by
    intro v
    cases v with
    | win => exact ⟨.win, FragMove.win_self⟩
    | lose => exact ⟨.lose, FragMove.lose_self⟩
    | pos φ w =>
        by_cases hExists : ∃ φ' w', Move M
            ⟨FixFreeFormula.toMu φ, w, []⟩ ⟨FixFreeFormula.toMu φ', w', []⟩
        · obtain ⟨φ', w', hq⟩ := hExists
          exact ⟨.pos φ' w', FragMove.pos_move hq⟩
        · have hNo : NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩ := by
            intro q hq
            obtain ⟨φ', w', hq', -⟩ := move_of_toMu hq
            exact hExists ⟨φ', w', by rwa [hq'] at hq⟩
          by_cases hWin : TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩
          · exact ⟨.win, FragMove.toWin hNo hWin⟩
          · exact ⟨.lose, FragMove.toLose hNo hWin⟩

Uses 16 · Used by 11

Statement usesParity game · Players of a parity game · Kripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the totalized fragment game · Positions of the totalized fragment game · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Size of a μ-calculus formula · Positions with no moves · Winner at a terminal position · Owners in the totalized fragment game · Priorities in the totalized fragment game · Fragment moves decrease the formula size · Formulas of the modal μ-calculus

Used byVerifier's positional strategies make a game move at Verifier positions that have one · Segments of canonical plays through fragment positions are bespoke plays · Plays of the totalized fragment game stay at the losing state · Plays of the totalized fragment game stay at the winning state · Terminal losing positions are not won by the even player · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Wins is the winning region of the fragment game · Sequences that stay at the win state are won by the even player · Sequences that stay at the lose state are won by the odd player

TheoremThe absorbing win state#✓fully proved

In the totalized fragment game on a Kripke model \(M\) with environment \(\mathit{env}\), every move from the absorbing Verifier-wins state \(\mathrm{win}\) leads back to it: if \(\mathrm{win}\) moves to \(v\), then \(v = \mathrm{win}\).

theorem FragMove.win_eq {M : KripkeModel World Atom} {env : ℕ → World → Prop}
    {v : FragPos Atom World} (h : FragMove M env .win v) : v = .win

Uses 9 · Used by 1

Statement usesKripke model · Moves of the totalized fragment game · Positions of the totalized fragment game

Proof usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the μ-calculus model-checking game · Positions with no moves · Winner at a terminal position · Formulas of the modal μ-calculus

Used byPlays of the totalized fragment game stay at the winning state

TheoremThe losing state is absorbing#✓fully proved

In the fragment game of a Kripke model \(M\) and an environment \(\rho\), every move from the losing state goes to the losing state.

theorem FragMove.lose_eq {M : KripkeModel World Atom} {env : ℕ → World → Prop}
    {v : FragPos Atom World} (h : FragMove M env .lose v) : v = .lose

Uses 9 · Used by 1

Statement usesKripke model · Moves of the totalized fragment game · Positions of the totalized fragment game

Proof usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the μ-calculus model-checking game · Positions with no moves · Winner at a terminal position · Formulas of the modal μ-calculus

Used byPlays of the totalized fragment game stay at the losing state

TheoremFragment moves between embedded positions are game moves#✓fully proved

Let \(M\) be a Kripke model, \(\mathrm{env}\) an environment, \(\varphi, \varphi'\) fixpoint-free formulas and \(w, w'\) worlds. If the totalized fragment game has a move from the embedded position \((\varphi, w)\) to the embedded position \((\varphi', w')\), then the model-checking game has a move from \((\varphi, w, [])\) to \((\varphi', w', [])\), where the fixpoint-free formulas are viewed as μ-calculus formulas and \([]\) is the empty binder stack.

theorem FragMove.pos_move_iff {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {φ φ' : FixFreeFormula Atom} {w w' : World}
    (h : FragMove M env (.pos φ w) (.pos φ' w')) :
    Move M ⟨FixFreeFormula.toMu φ, w, []⟩
      ⟨FixFreeFormula.toMu φ', w', []⟩

Uses 9 · Used by 2

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the totalized fragment game · Positions of the totalized fragment game · Moves of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Proof usesPositions with no moves · Winner at a terminal position

Used bySegments of canonical plays through fragment positions are bespoke plays · Winning Verifier strategies transfer to the fragment game

TheoremMoves to the winning state come from terminal winning positions#✓fully proved

Let \(M\) be a Kripke model, \(\mathrm{env}\) an environment, \(\varphi\) a fixpoint-free formula and \(w\) a world. If the totalized fragment game has a move from the embedded position \((\varphi, w)\) to the absorbing winning state, then the game position \((\varphi, w, [])\), with \(\varphi\) viewed as a μ-calculus formula and an empty binder stack, has no moves, and Verifier wins there as a terminal position in the environment \(\mathrm{env}\).

theorem FragMove.pos_toWin {M : KripkeModel World Atom} {env : ℕ → World → Prop}
    {φ : FixFreeFormula Atom} {w : World}
    (h : FragMove M env (.pos φ w) .win) :
    NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩ ∧
      TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩

Uses 9

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the totalized fragment game · Positions of the totalized fragment game · Positions with no moves · Winner at a terminal position · Formulas of the modal μ-calculus

Proof usesMoves of the μ-calculus model-checking game

TheoremMoves to the losing state come from terminal losing positions#✓fully proved

Let \(M\) be a Kripke model, \(\mathrm{env}\) an environment, \(\varphi\) a fixpoint-free formula and \(w\) a world. If the totalized fragment game has a move from the embedded position \((\varphi, w)\) to the absorbing losing state, then the game position \((\varphi, w, [])\), with \(\varphi\) viewed as a μ-calculus formula and an empty binder stack, has no moves, and Verifier does not win there as a terminal position in the environment \(\mathrm{env}\).

theorem FragMove.pos_toLose {M : KripkeModel World Atom} {env : ℕ → World → Prop}
    {φ : FixFreeFormula Atom} {w : World}
    (h : FragMove M env (.pos φ w) .lose) :
    NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩ ∧
      ¬ TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩

Uses 9 · Used by 1

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the totalized fragment game · Positions of the totalized fragment game · Positions with no moves · Winner at a terminal position · Formulas of the modal μ-calculus

Proof usesMoves of the μ-calculus model-checking game

Used byWinning Verifier strategies transfer to the fragment game

TheoremOwner of an embedded position in the totalized fragment game#✓fully proved

For every fixpoint-free formula \(\varphi\) and world \(w\), the even player owns the embedded position \((\varphi, w)\) of the totalized fragment game if and only if Verifier owns the model-checking game position \((\varphi, w, [])\), with \(\varphi\) embedded as a μ-calculus formula and the empty fixpoint stack.

theorem fragOwner_pos_eq_even {φ : FixFreeFormula Atom} {w : World} :
    fragOwner (FragPos.pos φ w : FragPos Atom World) = Cslib.Games.Player.even ↔
      Owner ⟨FixFreeFormula.toMu φ, w, []⟩ = true

Uses 8 · Used by 2

Statement usesPlayers of a parity game · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Owner of a game position · Player of the μ-calculus model-checking game · Owners in the totalized fragment game · Formulas of the modal μ-calculus

Used bySegments of canonical plays through fragment positions are bespoke plays · Positional strategy induced by a bespoke strategy

DefinitionCanonical next move induced by a bespoke strategy#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment and \(\sigma\) a Verifier strategy for the model-checking game on \(M\). Write \(\langle \psi, v \rangle\) for the game position with the embedding of a fixpoint-free formula \(\psi\), the world \(v\) and the empty binder stack. The canonical next move is the map on positions of the fragment arena defined as follows. The absorbing states \(\mathrm{win}\) and \(\mathrm{lose}\) are sent to themselves. A fragment position \((\varphi, w)\) such that \(\langle \varphi, w \rangle\) has a move to some \(\langle \varphi', w' \rangle\) is sent, if Verifier owns \(\langle \varphi, w \rangle\), to the projection into the fragment arena of the position that \(\sigma\) chooses there (an embedded position \(\langle \varphi', w' \rangle\) projects to \((\varphi', w')\), every other game position to \(\mathrm{lose}\)), and otherwise to a fragment position \((\varphi', w')\) chosen, by the axiom of choice, among those with a move from \(\langle \varphi, w \rangle\) to \(\langle \varphi', w' \rangle\). A fragment position \((\varphi, w)\) with no such move is sent to \(\mathrm{win}\) if \(\langle \varphi, w \rangle\) satisfies the terminal winning condition for Verifier in environment \(\mathit{env}\), and to \(\mathrm{lose}\) otherwise.

noncomputable def canonicalNext (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) (σ : Strategy M) : FragPos Atom World → FragPos Atom World
  | .win => .win
  | .lose => .lose
  | .pos φ w =>
      if hExists : ∃ φ' w', Move M ⟨FixFreeFormula.toMu φ, w, []⟩
          ⟨FixFreeFormula.toMu φ', w', []⟩ then
        if Owner ⟨FixFreeFormula.toMu φ, w, []⟩ = true then
          fragOfGamePos (σ.choose ⟨FixFreeFormula.toMu φ, w, []⟩)
        else
          .pos (Classical.choose hExists)
            (Classical.choose (Classical.choose_spec hExists))
      else if TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩ then .win else .lose

Uses 12 · Used by 3

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game · Verifier strategy · Winner at a terminal position · Projection of game positions onto the fragment arena · Formulas of the modal μ-calculus

Used byThe canonical move follows the bespoke strategy at Verifier positions with a move · Segments of canonical plays through fragment positions are bespoke plays · Positional strategy induced by a bespoke strategy

TheoremThe canonical move follows the bespoke strategy at Verifier positions with a move#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment and \(\sigma\) a Verifier strategy for the model-checking game on \(M\). Write \(\langle \psi, v \rangle\) for the game position with the embedding of a fixpoint-free formula \(\psi\), the world \(v\) and the empty binder stack. Let \(\varphi\) be a fixpoint-free formula and \(w\) a world such that Verifier owns \(\langle \varphi, w \rangle\) and \(\langle \varphi, w \rangle\) has a move to some \(\langle \varphi'', w'' \rangle\). Then there are a fixpoint-free formula \(\varphi'\) and a world \(w'\) such that the canonical next move induced by \(\sigma\) (in environment \(\mathit{env}\)) sends the fragment position \((\varphi, w)\) to the fragment position \((\varphi', w')\), and \(\sigma\) chooses \(\langle \varphi', w' \rangle\) at \(\langle \varphi, w \rangle\).

theorem canonicalNext_pos_of_owner {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {σ : Strategy M} {φ : FixFreeFormula Atom}
    {w : World}
    (hOwn : Owner ⟨FixFreeFormula.toMu φ, w, []⟩ = true)
    (hExists : ∃ φ' w', Move M ⟨FixFreeFormula.toMu φ, w, []⟩
      ⟨FixFreeFormula.toMu φ', w', []⟩) :
    ∃ φ' w', canonicalNext M env σ (.pos φ w) = .pos φ' w' ∧
      σ.choose ⟨FixFreeFormula.toMu φ, w, []⟩ = ⟨FixFreeFormula.toMu φ', w', []⟩

Uses 16 · Used by 2

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game · Verifier strategy · Canonical next move induced by a bespoke strategy · Formulas of the modal μ-calculus

Proof usesSize of a μ-calculus formula · Winner at a terminal position · Projection of game positions onto the fragment arena · Projection of an embedded position · Fragment moves decrease the formula size

Used bySegments of canonical plays through fragment positions are bespoke plays · Positional strategy induced by a bespoke strategy

DefinitionPositional strategy induced by a bespoke strategy#✓fully proved

The canonical positional strategy induced by a bespoke strategy.

Cslib.Modal.MuCalculus.Game.fragStrategy · 60 lines

noncomputable def fragStrategy (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) (σ : Strategy M) :
    (fragmentGame M env).PositionalStrategy Cslib.Games.Player.even where
  next := canonicalNext M env σ
  legal := by
    intro v hv
    cases v with
    | win =>
        show FragMove M env .win (canonicalNext M env σ .win)
        rw [show canonicalNext M env σ (FragPos.win : FragPos Atom World) = .win from rfl]
        exact FragMove.win_self
    | lose =>
        show FragMove M env .lose (canonicalNext M env σ .lose)
        rw [show canonicalNext M env σ (FragPos.lose : FragPos Atom World) = .lose from rfl]
        exact FragMove.lose_self
    | pos φ w =>
        have hOwn : Owner ⟨FixFreeFormula.toMu φ, w, []⟩ = true :=
          (fragOwner_pos_eq_even).mp hv
        show FragMove M env (.pos φ w) (canonicalNext M env σ (.pos φ w))
        by_cases hExists : ∃ φ' w', Move M ⟨FixFreeFormula.toMu φ, w, []⟩
            ⟨FixFreeFormula.toMu φ', w', []⟩
        · obtain ⟨φ', w', hNext, heq⟩ := canonicalNext_pos_of_owner hOwn hExists
          obtain ⟨φ₀, w₀, h₀⟩ := hExists
          have hChoose : Move M ⟨FixFreeFormula.toMu φ, w, []⟩
              ⟨FixFreeFormula.toMu φ', w', []⟩ := by
            rw [← heq]
            exact σ.choose_move _ hOwn ⟨⟨FixFreeFormula.toMu φ₀, w₀, []⟩, h₀⟩
          rw [hNext]
          exact FragMove.pos_move hChoose
        · have hNo : NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩ := by
            intro q hq
            obtain ⟨φ', w', hq', -⟩ := move_of_toMu hq
            exact hExists ⟨φ', w', by rwa [hq'] at hq⟩
          by_cases hWin : TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩
          · have hNext : canonicalNext M env σ (.pos φ w) = FragPos.win := by
              classical
              show (if h : ∃ φ' w', Move M ⟨FixFreeFormula.toMu φ, w, []⟩
                  ⟨FixFreeFormula.toMu φ', w', []⟩ then
                (if Owner ⟨FixFreeFormula.toMu φ, w, []⟩ = true then
                  fragOfGamePos (σ.choose ⟨FixFreeFormula.toMu φ, w, []⟩)
                else .pos (Classical.choose h)
                  (Classical.choose (Classical.choose_spec h)))
                else if TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩ then
                  FragPos.win else FragPos.lose) = FragPos.win
              rw [dite_eq_right hExists, ite_eq_left hWin]
            rw [hNext]
            exact FragMove.toWin hNo hWin
          · have hNext : canonicalNext M env σ (.pos φ w) = FragPos.lose := by
              classical
              show (if h : ∃ φ' w', Move M ⟨FixFreeFormula.toMu φ, w, []⟩
                  ⟨FixFreeFormula.toMu φ', w', []⟩ then
                (if Owner ⟨FixFreeFormula.toMu φ, w, []⟩ = true then
                  fragOfGamePos (σ.choose ⟨FixFreeFormula.toMu φ, w, []⟩)
                else .pos (Classical.choose h)
                  (Classical.choose (Classical.choose_spec h)))
                else if TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩ then
                  FragPos.win else FragPos.lose) = FragPos.lose
              rw [dite_eq_right hExists, ite_eq_right hWin]
            rw [hNext]
            exact FragMove.toLose hNo hWin

Uses 24 · Used by 3

Statement usesParity game · Positional strategy in a parity game · Players of a parity game · Kripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the totalized fragment game · Positions of the totalized fragment game · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Size of a μ-calculus formula · Positions with no moves · Owner of a game position · Player of the μ-calculus model-checking game · Verifier strategy · Winner at a terminal position · Canonical next move induced by a bespoke strategy · The canonical move follows the bespoke strategy at Verifier positions with a move · Projection of game positions onto the fragment arena · Owners in the totalized fragment game · Owner of an embedded position in the totalized fragment game · Fragment parity game · Fragment moves decrease the formula size · Formulas of the modal μ-calculus

Used bySegments of canonical plays through fragment positions are bespoke plays · Winning Verifier strategies transfer to the fragment game · Wins is the winning region of the fragment game

DefinitionGame position of a fragment position#✓fully proved

Given a default game position \(p_0\), an embedded fragment position \((\varphi, w)\) is sent to the game position with formula \(\varphi\), world \(w\) and empty binder stack, and the absorbing winning and losing states are both sent to \(p_0\).

The default is never used on plays that stay among embedded positions.

def fragToPos (p0 : GamePosition Atom World) : FragPos Atom World → GamePosition Atom World
  | .pos φ w => ⟨FixFreeFormula.toMu φ, w, []⟩
  | _ => p0

Uses 5 · Used by 6

Statement usesFixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Position of the μ-calculus model-checking game · Formulas of the modal μ-calculus

Used bySegments of canonical plays through fragment positions are bespoke plays · Segment of a fragment play as game positions · Splitting off the head of a segment · Segments are nonempty · Last position of a segment · Winning Verifier strategies transfer to the fragment game

DefinitionSegment of a fragment play as game positions#✓fully proved

Let \(p_0\) be a game position and let \(\pi = \pi_0 \pi_1 \pi_2 \dots\) be an infinite sequence of positions of the totalized fragment game. For natural numbers \(s\) and \(k\), the segment of \(\pi\) from \(s\) of length \(k + 1\) is the list of game positions obtained from \(\pi_s, \pi_{s+1}, \dots, \pi_{s+k}\), in this order, by sending each embedded position \((\varphi, w)\) to the game position with formula \(\varphi\), world \(w\) and empty binder stack, and each of the absorbing winning and losing states to \(p_0\).

def fragSegment (p0 : GamePosition Atom World) (π : ωSequence (FragPos Atom World))
    (start : ℕ) : ℕ → List (GamePosition Atom World)
  | 0 => [fragToPos p0 (π start)]
  | k + 1 => fragToPos p0 (π start) :: fragSegment p0 π (start + 1) k

Uses 3 · Used by 5

Statement usesPositions of the totalized fragment game · Position of the μ-calculus model-checking game · Game position of a fragment position

Used bySegments of canonical plays through fragment positions are bespoke plays · Splitting off the head of a segment · Segments are nonempty · Last position of a segment · Winning Verifier strategies transfer to the fragment game

TheoremSplitting off the head of a segment#✓fully proved

Let \(p_0\) be a model-checking game position and \(\pi\) an infinite sequence of positions of the totalized fragment game. For each \(i\), let \(\hat\pi_i\) be \(p_0\) if \(\pi_i\) is an absorbing state; if \(\pi_i\) is the embedded position \((\varphi, w)\) of a fixpoint-free formula \(\varphi\) and a world \(w\), let \(\hat\pi_i\) be the game position \((\varphi, w, [])\), with \(\varphi\) embedded as a μ-calculus formula and the empty fixpoint stack. For all natural numbers \(s\) and \(k\), the segment \([\hat\pi_s, \dots, \hat\pi_{s+k+1}]\) of \(\pi\) is the list with head \(\hat\pi_s\) followed by the segment \([\hat\pi_{s+1}, \dots, \hat\pi_{s+k+1}]\).

theorem fragSegment_cons (p0 : GamePosition Atom World)
    (π : ωSequence (FragPos Atom World)) (start k : ℕ) :
    fragSegment p0 π start (k + 1) =
      fragToPos p0 (π start) :: fragSegment p0 π (start + 1) k

Uses 4 · Used by 2

Statement usesPositions of the totalized fragment game · Position of the μ-calculus model-checking game · Segment of a fragment play as game positions · Game position of a fragment position

Used bySegments of canonical plays through fragment positions are bespoke plays · Last position of a segment

TheoremSegments of canonical plays through fragment positions are bespoke plays#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment and \(\sigma\) a Verifier strategy for the model-checking game on \(M\). Write \(\langle \psi, v \rangle\) for the game position with the embedding of a fixpoint-free formula \(\psi\), the world \(v\) and the empty binder stack. Let \(\pi\) be a play of the fragment game of \(M\) and \(\mathit{env}\) that conforms to the canonical positional strategy induced by \(\sigma\), and let \(s, k \in \mathbb{N}\). Suppose every \(\pi_i\) with \(s \le i \le s + k\) is a fragment position \((\varphi_i, w_i)\), not \(\mathrm{win}\) or \(\mathrm{lose}\). Then the list \(\langle \varphi_s, w_s \rangle, \langle \varphi_{s+1}, w_{s+1} \rangle, \dots, \langle \varphi_{s+k}, w_{s+k} \rangle\) is a finite play from \(\langle \varphi_s, w_s \rangle\) consistent with \(\sigma\): each position has a game move to the next, and at Verifier-owned positions the next position is the one \(\sigma\) chooses.

theorem canonical_playFrom_segment {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {σ : Strategy M} {π : ωSequence (FragPos Atom World)}
    (p0 : GamePosition Atom World) (start k : ℕ)
    (φ : FixFreeFormula Atom) (w : World)
    (hplay : (fragmentGame M env).IsPlay π)
    (hconf : Cslib.Games.ParityGame.Conforms (fragStrategy M env σ) π)
    (hstart : π start = .pos φ w)
    (hpos : ∀ i, start ≤ i → i ≤ start + k → ∃ φ' w', π i = .pos φ' w') :
    PlayFrom M σ ⟨FixFreeFormula.toMu φ, w, []⟩ (fragSegment p0 π start k)

Uses 27 · Used by 1

Statement usesPlays conforming to a strategy · Plays of a parity game · Players of a parity game · Kripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Position of the μ-calculus model-checking game · Finite plays consistent with a strategy · Verifier strategy · Segment of a fragment play as game positions · Positional strategy induced by a bespoke strategy · Fragment parity game · Formulas of the modal μ-calculus

Proof usesParity game · Positional strategy in a parity game · Moves of the totalized fragment game · Fragment moves between embedded positions are game moves · Moves of the μ-calculus model-checking game · Owner of a game position · Player of the μ-calculus model-checking game · Canonical next move induced by a bespoke strategy · The canonical move follows the bespoke strategy at Verifier positions with a move · Owners in the totalized fragment game · Owner of an embedded position in the totalized fragment game · Splitting off the head of a segment · Game position of a fragment position

Used byWinning Verifier strategies transfer to the fragment game

TheoremPlays of the totalized fragment game stay at the winning state#✓fully proved

Let \(M\) be a Kripke model and \(\mathit{env}\) an environment assigning a set of worlds to each free-variable index. If \(\pi\) is a play of the totalized fragment game of \(M\) and \(\mathit{env}\) and \(\pi_k\) is the absorbing winning state, then \(\pi_n\) is the winning state for every \(n \ge k\).

theorem fragPlay_eq_win_of_le {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {π : ωSequence (FragPos Atom World)} {k n : ℕ}
    (hplay : (fragmentGame M env).IsPlay π) (hk : π k = .win) (hn : k ≤ n) :
    π n = .win

Uses 6 · Used by 1

Statement usesPlays of a parity game · Kripke model · Positions of the totalized fragment game · Fragment parity game

Proof usesMoves of the totalized fragment game · The absorbing win state

Used byWinning Verifier strategies transfer to the fragment game

TheoremPlays of the totalized fragment game stay at the losing state#✓fully proved

Let \(M\) be a Kripke model and \(\mathit{env}\) an environment assigning a set of worlds to each free-variable index. If \(\pi\) is a play of the totalized fragment game of \(M\) and \(\mathit{env}\) and \(\pi_k\) is the absorbing losing state, then \(\pi_n\) is the losing state for every \(n \ge k\).

theorem fragPlay_eq_lose_of_le {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {π : ωSequence (FragPos Atom World)} {k n : ℕ}
    (hplay : (fragmentGame M env).IsPlay π) (hk : π k = .lose) (hn : k ≤ n) :
    π n = .lose

Uses 6

Statement usesPlays of a parity game · Kripke model · Positions of the totalized fragment game · Fragment parity game

Proof usesMoves of the totalized fragment game · The losing state is absorbing

TheoremSequences that stay at the win state are won by the even player#✓fully proved

Let \(M\) be a Kripke model and \(\mathit{env}\) an environment for free variables. If an infinite sequence \(\pi_0 \pi_1 \pi_2 \dots\) of positions of the totalized fragment game of \(M\) and \(\mathit{env}\) has a \(k_0\) such that \(\pi_n\) is the absorbing winning state for all \(n \ge k_0\), then \(\pi\) is won by the even player in that game.

theorem wonBy_even_of_eventually_win {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {π : ωSequence (FragPos Atom World)} {k0 : ℕ}
    (hwin : ∀ n, k0 ≤ n → π n = .win) :
    (fragmentGame M env).WonBy Cslib.Games.Player.even π

Uses 7 · Used by 1

Statement usesWinner of a play in a parity game · Players of a parity game · Kripke model · Positions of the totalized fragment game · Fragment parity game

Proof usesPriorities in the totalized fragment game · Largest infinitely occurring value

Used byWinning Verifier strategies transfer to the fragment game

TheoremSequences that stay at the lose state are won by the odd player#✓fully proved

Let \(M\) be a Kripke model and \(\mathit{env}\) an environment for free variables. If an infinite sequence \(\pi_0 \pi_1 \pi_2 \dots\) of positions of the totalized fragment game of \(M\) and \(\mathit{env}\) has a \(k_0\) such that \(\pi_n\) is the absorbing losing state for all \(n \ge k_0\), then \(\pi\) is won by the odd player in that game.

theorem wonBy_odd_of_eventually_lose {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {π : ωSequence (FragPos Atom World)} {k0 : ℕ}
    (hlose : ∀ n, k0 ≤ n → π n = .lose) :
    (fragmentGame M env).WonBy Cslib.Games.Player.odd π

Uses 7 · Used by 1

Statement usesWinner of a play in a parity game · Players of a parity game · Kripke model · Positions of the totalized fragment game · Fragment parity game

Proof usesPriorities in the totalized fragment game · Largest infinitely occurring value

Used byTerminal losing positions are not won by the even player

TheoremSegments are nonempty#✓fully proved

Let \(p_0\) be a model-checking game position and \(\pi\) an infinite sequence of positions of the totalized fragment game. For all natural numbers \(s\) and \(k\), the segment of \(\pi\) from index \(s\) to index \(s + k\), read as a list of model-checking game positions with \(p_0\) standing for the absorbing states, is not the empty list.

theorem fragSegment_ne_nil (p0 : GamePosition Atom World)
    (π : ωSequence (FragPos Atom World)) (start k : ℕ) :
    fragSegment p0 π start k ≠ []

Uses 4 · Used by 1

Statement usesPositions of the totalized fragment game · Position of the μ-calculus model-checking game · Segment of a fragment play as game positions

Proof usesGame position of a fragment position

Used byLast position of a segment

TheoremLast position of a segment#✓fully proved

Let \(p_0\) be a model-checking game position and \(\pi\) an infinite sequence of positions of the totalized fragment game. For each \(i\), let \(\hat\pi_i\) be \(p_0\) if \(\pi_i\) is an absorbing state; if \(\pi_i\) is the embedded position \((\varphi, w)\) of a fixpoint-free formula \(\varphi\) and a world \(w\), let \(\hat\pi_i\) be the game position \((\varphi, w, [])\), with \(\varphi\) embedded as a μ-calculus formula and the empty fixpoint stack. For all natural numbers \(s\) and \(k\), the segment \([\hat\pi_s, \dots, \hat\pi_{s+k}]\) has a last position, and it is \(\hat\pi_{s+k}\).

theorem fragSegment_playLast (p0 : GamePosition Atom World)
    (π : ωSequence (FragPos Atom World)) (start k : ℕ) :
    playLast (fragSegment p0 π start k) = some (fragToPos p0 (π (start + k)))

Uses 8 · Used by 1

Statement usesPositions of the totalized fragment game · Position of the μ-calculus model-checking game · Segment of a fragment play as game positions · Game position of a fragment position · Last position of a play

Proof usesSplitting off the head of a segment · Segments are nonempty · Prepending to a nonempty play keeps the last position

Used byWinning Verifier strategies transfer to the fragment game

TheoremWinning Verifier strategies transfer to the fragment game#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment, \(\sigma\) a Verifier strategy of the model-checking game on \(M\), \(\varphi\) a fixpoint-free formula and \(w\) a world. If \(\sigma\) wins in environment \(\rho\) from the game position with formula \(\varphi\), world \(w\) and empty binder stack, then the positional strategy of the even player induced by \(\sigma\) wins from the embedded position \((\varphi, w)\) in the fragment game of \(M\) and \(\rho\).

Every play conforming to the induced strategy reaches the absorbing winning state: it cannot reach the losing state, by the finite-play clause for \(\sigma\) applied to the segment before the first losing state, and it cannot stay among embedded positions forever, since fragment moves strictly decrease the formula.

theorem fragment_bespoke_to_canonical {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {σ : Strategy M} {φ : FixFreeFormula Atom}
    {w : World}
    (hσ : StrategyWins M env σ ⟨FixFreeFormula.toMu φ, w, []⟩) :
    (fragmentGame M env).WinsFrom (fragStrategy M env σ)
      (.pos φ w)

Uses 33 · Used by 1

Statement usesWinning strategy from a position · Players of a parity game · Kripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Verifier strategy · Winning strategy from a position · Positional strategy induced by a bespoke strategy · Fragment parity game · Formulas of the modal μ-calculus

Proof usesPlays conforming to a strategy · Plays of a parity game · Winner of a play in a parity game · Moves of the totalized fragment game · Fragment moves between embedded positions are game moves · Moves to the losing state come from terminal losing positions · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Positions with no moves · Owner of a game position · Parity winning condition · Finite plays consistent with a strategy · Player of the μ-calculus model-checking game · Winner at a terminal position · Segments of canonical plays through fragment positions are bespoke plays · Plays of the totalized fragment game stay at the winning state · Segment of a fragment play as game positions · Last position of a segment · Game position of a fragment position · No infinite play from a fragment position · Last position of a play · Sequences that stay at the win state are won by the even player

Used byWins is the winning region of the fragment game

TheoremMoves of the totalized fragment game, by cases#✓fully proved

Let \(M\) be a Kripke model and \(e\) an environment, and read each fixpoint-free formula \(\varphi\) as a μ-calculus formula. Every move from \(a\) to \(b\) in the totalized fragment game of \(M\) and \(e\) is of one of five kinds: \(a\) and \(b\) are embedded positions \((\varphi, w)\) and \((\varphi', w')\) and the model-checking game of \(M\) has a move from \((\varphi, w)\) to \((\varphi', w')\) with empty binder stacks; or \(a = (\varphi, w)\), \(b\) is the winning state, and the game position \((\varphi, w)\) with empty stack has no moves and is won by Verifier in environment \(e\); or \(a = (\varphi, w)\), \(b\) is the losing state, and that game position has no moves and is not won by Verifier; or \(a\) and \(b\) are both the winning state; or \(a\) and \(b\) are both the losing state.

theorem fragMove_cases {M : KripkeModel World Atom} {env : ℕ → World → Prop}
    {a b : FragPos Atom World} (h : FragMove M env a b) :
    (∃ φ w φ' w', a = .pos φ w ∧ b = .pos φ' w' ∧
      Move M ⟨FixFreeFormula.toMu φ, w, []⟩
        ⟨FixFreeFormula.toMu φ', w', []⟩) ∨
    (∃ φ w, a = .pos φ w ∧ b = .win ∧
      NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩ ∧
      TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩) ∨
    (∃ φ w, a = .pos φ w ∧ b = .lose ∧
      NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩ ∧
      ¬ TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩) ∨
    (a = .win ∧ b = .win) ∨ (a = .lose ∧ b = .lose)

Uses 9 · Used by 2

Statement usesKripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Moves of the totalized fragment game · Positions of the totalized fragment game · Moves of the μ-calculus model-checking game · Positions with no moves · Winner at a terminal position · Formulas of the modal μ-calculus

Used byVerifier's positional strategies make a game move at Verifier positions that have one · Terminal losing positions are not won by the even player

TheoremVerifier's positional strategies make a game move at Verifier positions that have one#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment, and \(\sigma\) any positional strategy of the even player (Verifier) in the fragment game of \(M\) and \(\mathit{env}\). Write \(\langle \psi, v \rangle\) for the game position with the embedding of a fixpoint-free formula \(\psi\), the world \(v\) and the empty binder stack. Let \(\varphi\) be a fixpoint-free formula and \(w\) a world such that the even player owns the fragment position \((\varphi, w)\) and, in the model-checking game on \(M\), \(\langle \varphi, w \rangle\) has a move to some \(\langle \varphi'', w'' \rangle\). Then \(\sigma\) sends \((\varphi, w)\) to a fragment position \((\varphi', w')\) such that \(\langle \varphi, w \rangle\) has a move to \(\langle \varphi', w' \rangle\); in particular \(\sigma\) does not move to the absorbing state \(\mathrm{win}\) or \(\mathrm{lose}\).

theorem canonical_next_pos {M : KripkeModel World Atom} {env : ℕ → World → Prop}
    {σ : (fragmentGame M env).PositionalStrategy Cslib.Games.Player.even}
    {φ : FixFreeFormula Atom} {w : World}
    (hown : (fragmentGame M env).owner (.pos φ w) = Cslib.Games.Player.even)
    (hExists : ∃ φ' w', Move M ⟨FixFreeFormula.toMu φ, w, []⟩
      ⟨FixFreeFormula.toMu φ', w', []⟩) :
    ∃ φ' w', σ.next (.pos φ w) = .pos φ' w' ∧
      Move M ⟨FixFreeFormula.toMu φ, w, []⟩
        ⟨FixFreeFormula.toMu φ', w', []⟩

Uses 14 · Used by 1

Statement usesParity game · Positional strategy in a parity game · Players of a parity game · Kripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Moves of the μ-calculus model-checking game · Fragment parity game · Formulas of the modal μ-calculus

Proof usesMoves of the totalized fragment game · Positions with no moves · Winner at a terminal position · Moves of the totalized fragment game, by cases

Used byThe fragment game's winning region is contained in Wins

DefinitionThe lose play#✓fully proved

For a fixpoint-free formula \(\varphi\) and a world \(w\), the lose play is the infinite sequence of positions of the fragment arena that is at the position \((\varphi, w)\) at time \(0\) and at the absorbing losing state at every later time. It is used for terminal losing positions \((\varphi, w)\).

def losePlay (φ : FixFreeFormula Atom) (w : World) :
    ωSequence (FragPos Atom World) :=
  ⟨fun n => if n = 0 then FragPos.pos φ w else FragPos.lose⟩

Uses 2 · Used by 3

Statement usesFixpoint-free formulas · Positions of the totalized fragment game

Used byTerminal losing positions are not won by the even player · The lose play stays at the losing state · The lose play starts at its fragment position

TheoremThe lose play starts at its fragment position#✓fully proved

For a fixpoint-free formula \(\varphi\) and a world \(w\), the lose play from \((\varphi, w)\) is at the fragment-arena position \((\varphi, w)\) at time \(0\).

theorem losePlay_zero (φ : FixFreeFormula Atom) (w : World) :
    losePlay φ w 0 = .pos φ w

Uses 3 · Used by 1

Statement usesFixpoint-free formulas · Positions of the totalized fragment game · The lose play

Used byTerminal losing positions are not won by the even player

TheoremThe lose play stays at the losing state#✓fully proved

For every fixpoint-free formula \(\varphi\), world \(w\) and natural number \(n\), the lose play from \((\varphi, w)\) is at the losing state at time \(n + 1\).

theorem losePlay_succ (φ : FixFreeFormula Atom) (w : World) (n : ℕ) :
    losePlay φ w (n + 1) = .lose

Uses 3 · Used by 1

Statement usesFixpoint-free formulas · Positions of the totalized fragment game · The lose play

Used byTerminal losing positions are not won by the even player

TheoremTerminal losing positions are not won by the even player#✓fully proved

Let \(M\) be a Kripke model, \(\mathit{env}\) an environment assigning a set of worlds to each free-variable index, \(\varphi\) a fixpoint-free formula and \(w\) a world. If the model-checking game position \((\varphi, w, [])\), with \(\varphi\) embedded as a μ-calculus formula and the empty fixpoint stack, has no moves in \(M\) and is not a terminal win for Verifier in \(M\) under \(\mathit{env}\), then the embedded position \((\varphi, w)\) of the totalized fragment game of \(M\) and \(\mathit{env}\) is not in the winning region of the even player.

The play that moves from \((\varphi, w)\) to the losing state and stays there conforms to every strategy of the even player and is won by the odd player.

theorem fragPos_not_mem_winningRegion_of_terminal_lose {M : KripkeModel World Atom}
    {env : ℕ → World → Prop} {φ : FixFreeFormula Atom} {w : World}
    (hNo : NoMoves M ⟨FixFreeFormula.toMu φ, w, []⟩)
    (hLose : ¬ TerminalWin M env ⟨FixFreeFormula.toMu φ, w, []⟩) :
    (.pos φ w : FragPos Atom World) ∉
      (fragmentGame M env).WinningRegion Cslib.Games.Player.even

Uses 25 · Used by 1

Statement usesWinning region of a parity game · Players of a parity game · Kripke model · Fixpoint-free formulas · Embedding of the fixpoint-free fragment into the μ-calculus · Positions of the totalized fragment game · Positions with no moves · Winner at a terminal position · Fragment parity game · Formulas of the modal μ-calculus

Proof usesParity game · Plays conforming to a strategy · Plays of a parity game · Positional strategy in a parity game · Winning strategy from a position · Winner of a play in a parity game · No play is won by both players · Opponent · Moves of the totalized fragment game · Moves of the μ-calculus model-checking game · Moves of the totalized fragment game, by cases · The lose play · The lose play stays at the losing state · The lose play starts at its fragment position · Sequences that stay at the lose state are won by the odd player

Used byThe fragment game's winning region is contained in Wins

TheoremThe fragment game's winning region is contained in Wins#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment, \(\varphi\) a fixpoint-free formula and \(w\) a world. If the embedded position \((\varphi, w)\) lies in the winning region of the even player in the fragment game of \(M\) and \(\rho\), then the backward-induction winning condition \(\mathrm{Wins}_M(\varphi, w)\) holds.

The proof is by induction on \(\varphi\), using that the winning region is closed under the opponent's moves and under the moves of a winning strategy, so no strategy composition is needed.

theorem fragment_canonical_to_wins (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) (φ : FixFreeFormula Atom) (w : World)
    (h : (.pos φ w : FragPos Atom World) ∈
      (fragmentGame M env).WinningRegion Cslib.Games.Player.even) :
    Wins M φ w

Uses 24 · Used by 1

Statement usesWinning region of a parity game · Players of a parity game · Kripke model · Fixpoint-free formulas · Positions of the totalized fragment game · Backward-induction winning region of the fixpoint-free fragment · Fragment parity game

Proof usesParity game · Positional strategy in a parity game · Winning strategy from a position · Opponent moves stay in the winning region · A winning strategy's move stays in the winning region · Embedding of the fixpoint-free fragment into the μ-calculus · The fixpoint-free embedding is injective · Moves of the totalized fragment game · Position of the μ-calculus model-checking game · Moves of the μ-calculus model-checking game · Moves from a diamond position · Inversion for disjunction moves · Positions with no moves · Winner at a terminal position · Verifier's positional strategies make a game move at Verifier positions that have one · Terminal losing positions are not won by the even player · Formulas of the modal μ-calculus

Used byWins is the winning region of the fragment game

TheoremWins is the winning region of the fragment game#✓fully proved

Let \(M\) be a Kripke model, \(\rho\) an environment, \(\varphi\) a fixpoint-free formula and \(w\) a world. Then the backward-induction winning condition \(\mathrm{Wins}_M(\varphi, w)\) holds if and only if the embedded position \((\varphi, w)\) lies in the winning region of the even player in the fragment game of \(M\) and \(\rho\).

theorem fragmentWins_iff_winningRegion (M : KripkeModel World Atom)
    (env : ℕ → World → Prop) (φ : FixFreeFormula Atom) (w : World) :
    Wins M φ w ↔ (.pos φ w : FragPos Atom World) ∈
      (fragmentGame M env).WinningRegion Cslib.Games.Player.even

Uses 18

Statement usesWinning region of a parity game · Players of a parity game · Kripke model · Fixpoint-free formulas · Positions of the totalized fragment game · Backward-induction winning region of the fixpoint-free fragment · Fragment parity game

Proof usesPositional strategy in a parity game · Winning strategy from a position · Embedding of the fixpoint-free fragment into the μ-calculus · Verifier strategy · Winning strategy from a position · Verifier has a winning strategy · Positional strategy induced by a bespoke strategy · Winning Verifier strategies transfer to the fragment game · The fragment game's winning region is contained in Wins · Game-vs-satisfaction, strategy direction · Formulas of the modal μ-calculus

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.