Skip to Main content Skip to Navigation
Journal articles

On timed alternating simulation for concurrent timed games

Laura Bozzelli 1 Axel Legay 2 Sophie Pinchinat 3
2 ESTASYS - Efficient STAtistical methods in SYstems of systems
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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 over strategies where the designated coalition of players 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 decidable and in EXPTIME.
Document type :
Journal articles
Complete list of metadata

https://hal.inria.fr/hal-01098747
Contributor : Sophie Pinchinat <>
Submitted on : Monday, December 29, 2014 - 10:21:23 AM
Last modification on : Friday, July 10, 2020 - 4:00:54 PM

Links full text

Identifiers

Citation

Laura Bozzelli, Axel Legay, Sophie Pinchinat. On timed alternating simulation for concurrent timed games. Acta Informatica, Springer Verlag, 2012, Acta Informatica, 49 (4), pp.31. ⟨10.1007/s00236-012-0158-y⟩. ⟨hal-01098747⟩

Share

Metrics

Record views

403