---
res:
  bibo_abstract:
  - The synthesis of reactive systems requires the solution of two-player games on
    graphs with ω-regular objectives. When the objective is specified by a linear
    temporal logic formula or nondeterministic Büchi automaton, then previous algorithms
    for solving the game require the construction of an equivalent deterministic automaton.
    However, determinization for automata on infinite words is extremely complicated,
    and current implementations fail to produce deterministic automata even for relatively
    small inputs. We show how to construct, from a given nondeterministic Büchi automaton,
    an equivalent nondeterministic parity automaton that is good for solving games
    with objective . The main insight is that a nondeterministic automaton is good
    for solving games if it fairly simulates the equivalent deterministic automaton.
    In this way, we omit the determinization step in game solving and reactive synthesis.
    The fact that our automata are nondeterministic makes them surprisingly simple,
    amenable to symbolic implementation, and allows an incremental search for winning
    strategies.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Henzinger, Thomas A
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Nir
      foaf_name: Piterman, Nir
      foaf_surname: Piterman
  bibo_doi: 10.1007/11874683_26
  bibo_volume: 4207
  dct_date: 2006^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0302-9743
  - http://id.crossref.org/issn/1611-3349
  - http://id.crossref.org/issn/9783540454588
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Solving games without determinization@
...