Citation
Thomas A. Brihaye, Tom Henzinger, Vinayak Prabhu, Jean-Francois Raskin. "Minimum-Time Reachability in Timed Games". Technical report, University of California, Berkeley, UCB/EECS-2007-47, April, 2007.

Abstract
We consider the minimum-time reachability problem in concurrent two-player timed automaton game structures. We show how to compute the minimum time needed by a player to reach a target location against all possible choices of the opponent. We do not put any syntactic restriction on the game structure, nor do we require any player to guarantee time divergence. We only require players to use receptive strategies which do not block time. The minimal time is computed in part using a fixpoint expression, which we show can be evaluated on equivalence classes of a non-trivial extension of the clock-region equivalence relation for timed automata.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-47.html. (See also http://chess.eecs.berkeley.edu/pubs/313)

• HTML

  Thomas A.  Brihaye, Tom Henzinger, Vinayak Prabhu,
  Jean-Francois Raskin. <a
  href="http://chess.eecs.berkeley.edu/pubs/313.html"
  ><i>Minimum-Time Reachability in Timed
  Games</i></a>, Technical report,  University of
  California, Berkeley, UCB/EECS-2007-47, April, 2007.

• Plain text

  Thomas A.  Brihaye, Tom Henzinger, Vinayak Prabhu,
  Jean-Francois Raskin. "Minimum-Time Reachability in
  Timed Games". Technical report,  University of
  California, Berkeley, UCB/EECS-2007-47, April, 2007.

• BibTeX

  @techreport{BrihayeHenzingerPrabhuRaskin07_MinimumTimeReachabilityInTimedGames,
      author = {Thomas A.  Brihaye and Tom Henzinger and Vinayak
                Prabhu and Jean-Francois Raskin},
      title = {Minimum-Time Reachability in Timed Games},
      institution = {University of California, Berkeley},
      number = {UCB/EECS-2007-47},
      month = {April},
      year = {2007},
      abstract = {We consider the minimum-time reachability problem
                in concurrent two-player timed automaton game
                structures. We show how to compute the minimum
                time needed by a player to reach a target location
                against all possible choices of the opponent. We
                do not put any syntactic restriction on the game
                structure, nor do we require any player to
                guarantee time divergence. We only require players
                to use receptive strategies which do not block
                time. The minimal time is computed in part using a
                fixpoint expression, which we show can be
                evaluated on equivalence classes of a non-trivial
                extension of the clock-region equivalence relation
                for timed automata.},
      URL = {http://chess.eecs.berkeley.edu/pubs/313.html}
  }
  

Posted by Christopher Brooks on 7 Jun 2007.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.