2026-07-21T12:57:58Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2309 2024-03-06T10:33:16Z ddc:004 open_access

On Timed Alternating Simulation for Concurrent Timed Games Bozzelli, Laura Legay, Axel Pinchinat, Sophie Concurrent Timed Games Timed Alternating Simulation Timed Alternating Temporal Logics 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 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Laura Bozzelli and Axel Legay and Sophie Pinchinat 2009 Is Part Of LIPIcs, Volume 4, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2009) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2009.2309 urn:nbn:de:0030-drops-23092 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2309 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode