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.
Type de document :
Article dans une revue
Acta Informatica, Springer Verlag, 2012, Acta Informatica, 49 (4), pp.31. 〈10.1007/s00236-012-0158-y〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01098747
Contributeur : Sophie Pinchinat <>
Soumis le : lundi 29 décembre 2014 - 10:21:23
Dernière modification le : mardi 16 janvier 2018 - 15:54:23

Identifiants

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〉

Partager

Métriques

Consultations de la notice

234