Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

Minimum-Time Reachability in Timed Games

Thomas Brihaye, Thomas A. Henzinger, Vinayak Prabhu and Jean-Francois Raskin

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2007-47
April 24, 2007

http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-47.pdf

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.


BibTeX citation:

@techreport{Brihaye:EECS-2007-47,
    Author = {Brihaye, Thomas and Henzinger, Thomas A. and Prabhu, Vinayak and Raskin, Jean-Francois},
    Title = {Minimum-Time Reachability in Timed Games},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2007},
    Month = {Apr},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-47.html},
    Number = {UCB/EECS-2007-47},
    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.}
}

EndNote citation:

%0 Report
%A Brihaye, Thomas
%A Henzinger, Thomas A.
%A Prabhu, Vinayak
%A Raskin, Jean-Francois
%T Minimum-Time Reachability in Timed Games
%I EECS Department, University of California, Berkeley
%D 2007
%8 April 24
%@ UCB/EECS-2007-47
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2007/EECS-2007-47.html
%F Brihaye:EECS-2007-47