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.
@InProceedings{bozzelli_et_al:LIPIcs.FSTTCS.2009.2309, author = {Bozzelli, Laura and Legay, Axel and Pinchinat, Sophie}, title = {{On Timed Alternating Simulation for Concurrent Timed Games}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {85--96}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-13-2}, ISSN = {1868-8969}, year = {2009}, volume = {4}, editor = {Kannan, Ravi and Narayan Kumar, K.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2009.2309}, URN = {urn:nbn:de:0030-drops-23092}, doi = {10.4230/LIPIcs.FSTTCS.2009.2309}, annote = {Keywords: Concurrent Timed Games, Timed Alternating Simulation, Timed Alternating Temporal Logics} }
Feedback for Dagstuhl Publishing