Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(3)
Model Checking
Timing Game
Alternating Time Temporal Logic
Subscribe
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
Edit
On Timed Alternating Simulation for Concurrent Timed Games
(
Citations: 1
)
BibTex

RIS

RefWorks
Download
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 EXPTIMEcomplete, and provide a logical characterization of this preorder in terms of a meaningful fragment of a new logic, TAMTL∗. TAMTL∗ is an actionbased timed extension of standard alternatingtime
temporal logic
ATL∗, which allows to quantify on strategies where the designated player is not responsible for blocking time. While for full TAMTL∗, modelchecking TG is undecidable, we show that for its fragment TAMTL, corresponding to the timed version of ATL, the problem is instead in EXPTIME.
Conference:
Foundations of Software Technology and Theoretical Computer Science  FSTTCS
, pp. 8596, 2009
DOI:
10.4230/LIPIcs.FSTTCS.2009.2309
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.
(
drops.dagstuhl.de
)
(
www.informatik.unitrier.de
)
(
dx.doi.org
)
Citation Context
(1)
...Similarly, deciding timed alternating (bi)simulation for timed games, which can be used to model realtime 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 nonprobabilistic 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...
...OneStep 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 nonnegative 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 Sproston
,
et al.
Simulation and Bisimulation for Probabilistic Timed Automata
References
(18)
A Complete Axiomatization of Timed Bisimulation for a Class of Timed Regular Behaviours
(
Citations: 16
)
Luca Aceto
,
Alan Jeffrey
Journal:
Theoretical Computer Science  TCS
, vol. 152, no. 2, pp. 251268, 1995
Modelchecking in dense realtime
(
Citations: 499
)
Rajeev Alur
,
Costas Courcoubetis
,
David L. Dill
Journal:
Information and Computation/information and Control  IANDC
, vol. 104, no. 1, pp. 234, 1993
The Theory of Timed Automata
(
Citations: 1367
)
Rajeev Alur
Conference:
Research and Education in Concurrent Systems  REX
, pp. 4573, 1991
Alternatingtime temporal logic
(
Citations: 496
)
Rajeev Alur
,
Thomas A. Henzinger
,
Orna Kupferman
Journal:
Journal of The ACM  JACM
, vol. 49, no. 5, pp. 672713, 2002
Alternating Refinement Relations
(
Citations: 130
)
Rajeev Alur
,
Thomas A. Henzinger
,
Orna Kupferman
,
Moshe Y. Vardi
Conference:
International Conference on Concurrency Theory  CONCUR
, pp. 163178, 1998
Sort by:
Citations
(1)
Simulation and Bisimulation for Probabilistic Timed Automata
(
Citations: 1
)
Jeremy Sproston
,
Angelo Troina
Conference:
Formal Modeling and Analysis of Timed Systems  FORMATS
, pp. 213227, 2010