Citation
Krishnendu Chatterjee, Tom Henzinger, Vinayak Prabhu. "Trading Infinite Memory for Uniform Randomness in Timed Games". Technical report, EECS Department University of California, Berkeley, UCB/EECS-2008-4, January, 2008.

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.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-4.html

• HTML

  Krishnendu Chatterjee, Tom Henzinger, Vinayak Prabhu. <a
  href="http://chess.eecs.berkeley.edu/pubs/456.html"
  ><i>Trading Infinite Memory for Uniform Randomness
  in Timed Games</i></a>, Technical report,  EECS
  Department University of California, Berkeley,
  UCB/EECS-2008-4, January, 2008.

• Plain text

  Krishnendu Chatterjee, Tom Henzinger, Vinayak Prabhu.
  "Trading Infinite Memory for Uniform Randomness in
  Timed Games". Technical report,  EECS Department
  University of California, Berkeley, UCB/EECS-2008-4,
  January, 2008.

• BibTeX

  @techreport{ChatterjeeHenzingerPrabhu08_TradingInfiniteMemoryForUniformRandomnessInTimedGames,
      author = {Krishnendu Chatterjee and Tom Henzinger and
                Vinayak Prabhu},
      title = {Trading Infinite Memory for Uniform Randomness in
                Timed Games},
      institution = {EECS Department University of California, Berkeley},
      number = {UCB/EECS-2008-4},
      month = {January},
      year = {2008},
      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. },
      URL = {http://chess.eecs.berkeley.edu/pubs/456.html}
  }
  

Posted by Vinayak Prabhu on 23 Jun 2008.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.