On timed alternating simulation for concurrent timed games
(2012) Acta Informatica —
Files
No attached file found for this publication.
Details
- Authors
- 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.
Citations
Bozzelli, L., Legay, A., & Pinchinat, S. (2012). On timed alternating simulation for concurrent timed games. Acta Informatica. https://doi.org/10.1007/s00236-012-0158-y