Citation
Tom Henzinger, Vinayak Prabhu. "Timed alternating-time temporal logic". Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006, Paris, France, LCNS 4202, Asarin, Eugene; Bouyer, Patricia (eds.), 1-17, September, 2006.

Abstract
We add freeze quantifiers to the game logic ATL in order to specify real-time objectives for games played on timed structures. We define the semantics of the resulting logic TATL by restricting the players to physically meaningful strategies, which do not prevent time from diverging. We show that TATL can be model checked over timed automaton games. We also specify timed optimization problems for physically meaningful strategies, and we show that for timed automaton games, the optimal answers can be approximated to within any degree of precision.

Electronic downloads

• http://mtc.epfl.ch/~tah/Publications/timed_alternating-time_temporal_logic.html
• http://dx.doi.org/10.1007/11867340_1

• HTML

  Tom Henzinger, Vinayak Prabhu. <a
  href="http://chess.eecs.berkeley.edu/pubs/249.html"
  >Timed alternating-time temporal logic</a>, Formal
  Modeling and Analysis of Timed Systems, 4th International
  Conference, FORMATS 2006, Paris, France, LCNS 4202, Asarin,
  Eugene; Bouyer, Patricia (eds.), 1-17, September, 2006.

• Plain text

  Tom Henzinger, Vinayak Prabhu. "Timed alternating-time
  temporal logic". Formal Modeling and Analysis of Timed
  Systems, 4th International Conference, FORMATS 2006, Paris,
  France, LCNS 4202, Asarin, Eugene; Bouyer, Patricia (eds.),
  1-17, September, 2006.

• BibTeX

  @inproceedings{HenzingerPrabhu06_TimedAlternatingtimeTemporalLogic,
      author = {Tom Henzinger and Vinayak Prabhu},
      title = {Timed alternating-time temporal logic},
      booktitle = {Formal Modeling and Analysis of Timed Systems, 4th
                International Conference, FORMATS 2006, Paris,
                France, LCNS 4202},
      editor = {Asarin, Eugene; Bouyer, Patricia},
      pages = {1-17},
      month = {September},
      year = {2006},
      abstract = {We add freeze quantifiers to the game logic ATL in
                order to specify real-time objectives for games
                played on timed structures. We define the
                semantics of the resulting logic TATL by
                restricting the players to physically meaningful
                strategies, which do not prevent time from
                diverging. We show that TATL can be model checked
                over timed automaton games. We also specify timed
                optimization problems for physically meaningful
                strategies, and we show that for timed automaton
                games, the optimal answers can be approximated to
                within any degree of precision. },
      URL = {http://chess.eecs.berkeley.edu/pubs/249.html}
  }
  

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