Solving parity games by a reduction to SAT
From MaRDI portal
Publication:414902
DOI10.1016/j.jcss.2011.05.004zbMath1279.68211MaRDI 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
91A05: 2-person games
91A43: Games involving graphs
91A80: Applications of game theory
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
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, SAT Modulo Graphs: Acyclicity
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
