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 betweenTG is EXPTIME-complete, and provide a logical characterization of thispreorder in terms of a meaningful fragment of a new logic, TAMTLSTAR.TAMTLSTAR is an action-based timed extension of standard alternating-timetemporal logic ATLSTAR, which allows to quantify on strategies where thedesignated player is not responsible for blocking time. While for full TAMTLSTAR, model-checking TG is undecidable, we show that for its fragment TAMTL, corresponding to the timed version of ATL, in EXPTIME