Solving parity games by a reduction to SAT
From MaRDI portal
Publication:414902
DOI10.1016/j.jcss.2011.05.004zbMath1279.68211OpenAlexW2090204914MaRDI QIDQ414902
Martin Lange, Ilkka Niemelä, Misa Keinänen, Keijo Heljanko
Publication date: 11 May 2012
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jcss.2011.05.004
2-person games (91A05) Games involving graphs (91A43) Applications of game theory (91A80) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (4)
SAT Modulo Graphs: Acyclicity ⋮ Stable-unstable semantics: Beyond NP with normal logic programs ⋮ Solving parity games by a reduction to SAT ⋮ Solving Parity Games Using an Automata-Based Algorithm
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
- Solving parity games by a reduction to SAT
- Tableau-based model checking in the propositional mu-calculus
- Symbolic model checking: \(10^{20}\) states and beyond
- Fast and simple nested fixpoints
- The complexity of mean payoff games on graphs
- Extending and implementing the stable model semantics
- A subexponential randomized algorithm for the simple stochastic game problem
- A deterministic subexponential algorithm for solving parity games
- Notes on finite asynchronous automata
- Linear Encodings of Bounded LTL Model Checking
- Verification of Timed Automata via Satisfiability Checking
- On Nonterminating Stochastic Games
- Computer Aided Verification
- Bounded Model Checking for Weak Alternating Büchi Automata
- On model checking for the \(\mu\)-calculus and its fragments
- Bounded model checking using satisfiability solving
This page was built for publication: Solving parity games by a reduction to SAT
