On Timed Alternating Simulation for Concurrent Timed Games

We address the problem of alternating simulation refinement for concurrent timed games (TG). We show that checking timed alternating simulation between TG is EXPTIME-complete, and provide a logical characterization of this preorder in terms of a meaningful fragment of a new logic, TAMTL∗. TAMTL∗ is an action-based timed extension of standard alternating-time temporal logic ATL∗, which allows to quantify on strategies where the designated player is not responsible for blocking time. While for full TAMTL∗, model-checking TG is undecidable, we show that for its fragment TAMTL, corresponding to the timed version of ATL, the problem is instead in EXPTIME.

• Type: Conference
• Year: 2009
• Where: FSTTCS
• Authors: Laura Bozzelli, Axel Legay, Sophie Pinchinat
• Keywords: Action-based Timed Extension, Alternating-time Temporal Logic, Concurrent Timed Games, FSTTCS 2009, Theoretical Computer Science