spot
2.5.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 dpa, 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... | |
std::pair< region_t, strategy_t > | solve () const |
bool | solve_qp () const |
|
inline |
parity_game provides an interface to manipulate a deterministic parity automaton as a parity game, including methods to solve the game.
dpa | the underlying deterministic parity automaton |
owner | a vector of Booleans indicating the owner of each state, with the convention that true represents player 1 and false represents player 0. |
void spot::parity_game::print | ( | std::ostream & | os | ) |
Print the parity game in PGSolver's format.
std::pair<region_t, strategy_t> spot::parity_game::solve | ( | ) | 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}, }