On Timed Alternating Simulation for Concurrent Timed Games

Laura Bozzelli, Axel Legay & Sophie Pinchinat
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...
This data center is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.
We found no citations for this text. For information on how to provide citation information, please see our documentation.