spot  2.5
Public Types | Public Member Functions | List of all members
spot::parity_game Class Reference
Collaboration diagram for spot::parity_game:

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_tout (unsigned src) const
 
internal::state_out< const twa_graph::graph_tout (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
 

Constructor & Destructor Documentation

◆ parity_game()

spot::parity_game::parity_game ( const twa_graph_ptr  dpa,
std::vector< bool >  owner 
)
inline

parity_game provides an interface to manipulate a deterministic parity automaton as a parity game, including methods to solve the game.

Parameters
dpathe underlying deterministic parity automaton
ownera vector of Booleans indicating the owner of each state, with the convention that true represents player 1 and false represents player 0.

Member Function Documentation

◆ print()

void spot::parity_game::print ( std::ostream &  os)

Print the parity game in PGSolver's format.

◆ solve()

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",
}

◆ solve_qp()

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},
}

The documentation for this class was generated from the following file:

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13