---
res:
  bibo_abstract:
  - We consider concurrent two-player timed automaton games with omega-regular objectives
    specified as parity conditions. These games offer an appropriate model for the
    synthesis of real-time controllers. Earlier works on timed games focused on pure
    strategies for each player. We study, for the first time, the use of randomized
    strategies in such games. While pure (i.e., nonrandomized) strategies in timed
    games require infinite memory for winning even with respect to reachability objectives,
    we show that randomized strategies can win with finite memory with respect to
    all parity objectives. Also, the synthesized randomized real-time controllers
    are much simpler in structure than the corresponding pure controllers, and therefore
    easier to implement. For safety objectives we prove the existence of pure finite-memory
    winning strategies. Finally, while randomization helps in simplifying the strategies
    required for winning timed parity games, we prove that randomization does not
    help in winning at more states.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - 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: Vinayak
      foaf_name: Prabhu, Vinayak
      foaf_surname: Prabhu
  bibo_doi: 10.1007/978-3-540-78929-1_7
  bibo_volume: 4981
  dct_date: 2008^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0302-9743
  - http://id.crossref.org/issn/1611-3349
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_title: Trading infinite memory for uniform randomness in timed games@
...