Academic
Publications
On Timed Alternating Simulation for Concurrent Timed Games

On Timed Alternating Simulation for Concurrent Timed Games,10.4230/LIPIcs.FSTTCS.2009.2309,Laura Bozzelli,Axel Legay,Sophie Pinchinat

On Timed Alternating Simulation for Concurrent Timed Games   (Citations: 1)
BibTex | RIS | RefWorks Download
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 on strategies where the designated player 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 in EXPTIME.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Similarly, deciding timed alternating (bi)simulation for timed games, which can be used to model real-time controller synthesis problems, is also in EXPTIME [13]...
    • ...The logical characterization of timed bisimulation for a subclass of timed systems has been considered in [16], whereas the logical characterization of timed alternating simulation for timed games has been presented in [13] (this result also provides a logical characterization for simulation and bisimulation for timed automata)...
    • ...automata are a generalization of both timed automata and Segala’s probabilistic automata, our algorithm is inspired by [12,13] for timing aspects, and by [14,15] for probabilistic aspects...
    • ...The logical characterization that we present considers a logic in which the classical diamond operator is replaced with a diamond operator with a time constraint, as in [13], and which features probability thresholds, as in [18]...
    • ...Our approach is to extend the techniques of [12,13], which were applied to non-probabilistic timed automata/timed games, to the case 220 J. Sproston and A. Troina...
    • ...a finite set Times ((lA ,v A), (lB ,v B)) of time durations from [12,13]; it will suffice to consider only the time durations in this set in the subsequent algorithm...
    • ...Following [12,13], the distance d ∈ Times((lA ,v A), (lB ,v B)) between the midpoint 1 (τi + τi+1) and an integer c ∈ I can be used as a representative for all...
    • ...One-Step Goodness. We now define two notions of “goodness”, which we will use subsequently to refer to a single transition step from each of the PTA A and B. This notion will be presented in two versions: a concrete version, defined on the states of A and B, and a symbolic version, defined on RegionsA�B and using time durations taken from Times ( , ). Analogues of these notions, and their associated results, can be found in [12,13]...
    • ...Here we extend the logic of [18] with constraints on the duration of transitions, similarly to [16,13]...
    • ...However, inspired by [13], we note that a version of PTLogic restricted to non-negative rationals Q≥0 provides a logical characterization of timed bisimulation for those states of a PTA with rational values of clocks...
    • ...The proof of Theorem 5 follows that of direction (⇐) of Theorem 3, except that, as in [13], and without loss of generality, only transitions with durations taken from Times (s, s � ) are considered...

    Jeremy Sprostonet al. Simulation and Bisimulation for Probabilistic Timed Automata

Sort by: