Document Open Access Logo

On Timed Alternating Simulation for Concurrent Timed Games

Authors Laura Bozzelli, Axel Legay, Sophie Pinchinat

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2009.2309.pdf
  • Filesize: 155 kB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • Concurrent Timed Games
  • Timed Alternating Simulation
  • Timed Alternating Temporal Logics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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 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.

Cite As Get BibTex

Laura Bozzelli, Axel Legay, and Sophie Pinchinat. On Timed Alternating Simulation for Concurrent Timed Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 85-96, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009) https://doi.org/10.4230/LIPIcs.FSTTCS.2009.2309

Author Details

Laura Bozzelli
Axel Legay
Sophie Pinchinat
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact