spot
2.6.1
|
Public Types | |
typedef std::unordered_set< unsigned > | region_t |
typedef std::unordered_map< unsigned, unsigned > | strategy_t |
Public Member Functions | |
parity_game (const twa_graph_ptr &arena, const std::vector< bool > &owner) | |
unsigned | num_states () const |
unsigned | get_init_state_number () const |
internal::state_out< const twa_graph::graph_t > | out (unsigned src) const |
internal::state_out< const twa_graph::graph_t > | out (unsigned src) |
bool | owner (unsigned src) const |
unsigned | max_parity () const |
void | print (std::ostream &os) |
Print the parity game in PGSolver's format. More... | |
void | solve (region_t(&w)[2], strategy_t(&s)[2]) const |
bool | solve_qp () const |
spot::parity_game::parity_game | ( | const twa_graph_ptr & | arena, |
const std::vector< bool > & | owner | ||
) |
parity_game provides an interface to manipulate a colorized parity automaton as a parity game, including methods to solve the game. The input automaton (arena) should be colorized and have a max-odd parity acceptance condition.
arena | the underlying parity automaton |
owner | a vector of Booleans indicating the owner of each state: true stands for Player 1, false stands for Player 0. |
void spot::parity_game::print | ( | std::ostream & | os | ) |
Print the parity game in PGSolver's format.
void spot::parity_game::solve | ( | region_t(&) | w[2], |
strategy_t(&) | s[2] | ||
) | const |
Compute the winning strategy and winning region of this game for player 1 using Zielonka's recursive algorithm.
@article{ zielonka.98.tcs title = "Infinite games on finitely coloured graphs with applications to automata on infinite trees", journal = "Theoretical Computer Science", volume = "200", number = "1", pages = "135 - 183", year = "1998", author = "Wieslaw Zielonka", }
bool spot::parity_game::solve_qp | ( | ) | const |
Whether player 1 has a winning strategy from the initial state. Implements Calude et al.'s quasipolynomial time algorithm.
@inproceedings{calude.17.stoc, author = {Calude, Cristian S. and Jain, Sanjay and Khoussainov, Bakhadyr and Li, Wei and Stephan, Frank}, title = {Deciding Parity Games in Quasipolynomial Time}, booktitle = {Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing}, series = {STOC 2017}, year = {2017}, isbn = {978-1-4503-4528-6}, location = {Montreal, Canada}, pages = {252--263}, numpages = {12}, url = {http://doi.acm.org/10.1145/3055399.3055409}, doi = {10.1145/3055399.3055409}, acmid = {3055409}, publisher = {ACM}, address = {New York, NY, USA}, keywords = {Muller Games, Parity Games, Quasipolynomial Time Algorithm}, }