Abstract
We present a formalization of parity games (a two-player game on
directed graphs) and a proof of their positional determinacy in
Isabelle/HOL. This proof works for both finite and infinite games.
License
Topics
Session Parity_Game
- MoreCoinductiveList
- ParityGame
- Strategy
- AttractingStrategy
- Attractor
- WinningStrategy
- WellOrderedStrategy
- WinningRegion
- UniformStrategy
- AttractorStrategy
- PositionalDeterminacy
- AttractorInductive
- Graph_TheoryCompatibility