Solving parity games by a reduction to SAT

DOI10.1016/J.JCSS.2011.05.004MaRDI QIDQ414902zbMATH OpenOpenAlexFDO

Authors Keijo Heljanko, Misa Keinänen, Martin Lange, Ilkka Niemelä

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

zbMATH Keywords

propositional satisfiabilityparity gamesdifference logic

Mathematics Subject Classification ID

Applications of game theory (91A80) 2-person games (91A05) Specification and verification (program logics, model checking, etc.) (68Q60) Games involving graphs (91A43) Logic in computer science (03B70)

Recommendations

• Solving parity games in practice
• Parity game reductions
• Solving parity games using an automata-based algorithm
• Solving parity games: explicit vs symbolic
• A CSP-Based Approach for Solving Parity Game
• Solving counter parity games
• Algorithms for solving parity games
• Solving parity games on integer vectors
• Solving parity games in big steps
• Solving Parity Games in Big Steps

Cites work

• scientific article; zbMATH DE number 1670778 (Why is no real title available?)
• scientific article; zbMATH DE number 3566230 (Why is no real title available?)
• scientific article; zbMATH DE number 1962853 (Why is no real title available?)
• scientific article; zbMATH DE number 1500523 (Why is no real title available?)
• scientific article; zbMATH DE number 1773090 (Why is no real title available?)
• A deterministic subexponential algorithm for solving parity games
• A subexponential randomized algorithm for the simple stochastic game problem
• Bounded Model Checking for Weak Alternating Büchi Automata
• Bounded model checking for all regular properties
• Bounded model checking using satisfiability solving
• Computer Aided Verification
• Deciding the winner in parity games is in \(\mathrm{UP}\cap\mathrm{co-UP}\)
• Extending and implementing the stable model semantics
• Fast and simple nested fixpoints
• Linear Encodings of Bounded LTL Model Checking
• Notes on finite asynchronous automata
• On Nonterminating Stochastic Games
• On model checking for the \(\mu\)-calculus and its fragments
• Solving parity games by a reduction to SAT
• Symbolic model checking: \(10^{20}\) states and beyond
• Tableau-based model checking in the propositional mu-calculus
• The complexity of mean payoff games on graphs
• Verification of timed automata via satisfiability checking

Cited in

(12)

• Solving parity games by a reduction to SAT
• Stable-unstable semantics: Beyond NP with normal logic programs
• SAT modulo graphs: acyclicity
• Partial-order reduction for parity games with an application on parameterised Boolean equation systems
• Parity game reductions
• Solving parity games using an automata-based algorithm
• Parity to safety in polynomial time for pushdown and collapsible pushdown systems
• From Parity and Payoff Games to Linear Programming
• Winning Regions of Pushdown Parity Games: A Saturation Method
• Improving parity game solvers with justifications
• scientific article; zbMATH DE number 5914170 (Why is no real title available?)
• A CSP-Based Approach for Solving Parity Game

Describes a project that uses

Uses Software

• Chaff

This page was built for publication: Solving parity games by a reduction to SAT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q414902)