---
OA_type: closed access
_id: '4437'
abstract:
- lang: eng
  text: 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.
acknowledgement: This research was supported in part by the Swiss National Science
  Foundation.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Nir
  full_name: Piterman, Nir
  last_name: Piterman
citation:
  ama: 'Henzinger TA, Piterman N. Solving games without determinization. In: <i>Proceedings
    of the 20th International Conference on Computer Science Logic</i>. Vol 4207.
    Springer; 2006:395-410. doi:<a href="https://doi.org/10.1007/11874683_26">10.1007/11874683_26</a>'
  apa: 'Henzinger, T. A., &#38; Piterman, N. (2006). Solving games without determinization.
    In <i>Proceedings of the 20th international conference on Computer Science Logic</i>
    (Vol. 4207, pp. 395–410). Szeged, Hungary: Springer. <a href="https://doi.org/10.1007/11874683_26">https://doi.org/10.1007/11874683_26</a>'
  chicago: Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization.”
    In <i>Proceedings of the 20th International Conference on Computer Science Logic</i>,
    4207:395–410. Springer, 2006. <a href="https://doi.org/10.1007/11874683_26">https://doi.org/10.1007/11874683_26</a>.
  ieee: T. A. Henzinger and N. Piterman, “Solving games without determinization,”
    in <i>Proceedings of the 20th international conference on Computer Science Logic</i>,
    Szeged, Hungary, 2006, vol. 4207, pp. 395–410.
  ista: 'Henzinger TA, Piterman N. 2006. Solving games without determinization. Proceedings
    of the 20th international conference on Computer Science Logic. CSL: Computer
    Science Logic, LNCS, vol. 4207, 395–410.'
  mla: Henzinger, Thomas A., and Nir Piterman. “Solving Games without Determinization.”
    <i>Proceedings of the 20th International Conference on Computer Science Logic</i>,
    vol. 4207, Springer, 2006, pp. 395–410, doi:<a href="https://doi.org/10.1007/11874683_26">10.1007/11874683_26</a>.
  short: T.A. Henzinger, N. Piterman, in:, Proceedings of the 20th International Conference
    on Computer Science Logic, Springer, 2006, pp. 395–410.
conference:
  end_date: 2006-09-29
  location: Szeged, Hungary
  name: 'CSL: Computer Science Logic'
  start_date: 2006-09-25
date_created: 2018-12-11T12:08:51Z
date_published: 2006-09-20T00:00:00Z
date_updated: 2026-08-21T11:30:47Z
day: '20'
doi: 10.1007/11874683_26
extern: '1'
fulldoi: https://doi.org/10.1007/11874683_26
intvolume: '      4207'
language:
- iso: eng
month: '09'
oa_version: None
page: 395 - 410
publication: Proceedings of the 20th international conference on Computer Science
  Logic
publication_identifier:
  eisbn:
  - '9783540454595'
  eissn:
  - 1611-3349
  isbn:
  - '9783540454588'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
publist_id: '295'
status: public
title: Solving games without determinization
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4207
year: '2006'
...