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
(5)
Expressive Power
Logic In Computer Science
Temporal Logic
Timed Automata
Partial Order
Subscribe
Academic
Publications
On Expressive Powers of Timed Logics: Comparing Boundedness, Nonpunctuality and Deterministic Freezing
On Expressive Powers of Timed Logics: Comparing Boundedness, Nonpunctuality and Deterministic Freezing,10.1007/9783642232176_5,Computing Research
Edit
On Expressive Powers of Timed Logics: Comparing Boundedness, Nonpunctuality and Deterministic Freezing
BibTex

RIS

RefWorks
Download
Paritosh K. Pandya
,
Simoni S. Shah
Timed temporal logics exhibit a bewildering diversity of operators and the resulting decidability and expressiveness properties also vary considerably. We study the expressive powers of timed logics TPTL[U,S] and MTL[U,S] as well as their several fragments. Extending the LTL EF games of Etessami and Wilke, we define MTL EhrenfeuchtFraisse games on a pair of timed words. Using the associated EF theorem we show that, expressively, the timed logics BoundedMTL[U,S], MTL[F,P] and MITL[U,S] (respectively incorporating the restrictions of boundedness, unary modalities and nonpunctuality), are all pairwise incomparable. Going to more expressive logics, we show that MTL[U,S] is expressively incomparable with the unary freeze logic TPTL[F,P] extending the result of Bouyer et al. Finally, we consider the deterministic freeze logic TTL[X,Y], which is expressively equivalent to partially ordered 2way deterministic
timed automata
(po2DTA). As our second main result, we show by explicit reductions that TTL[X,Y] lies strictly between the unary, nonpunctual logic MITL[F,P] and its bounded fragment BoundedMITL[F,P]. This shows that deterministic punctuality is expressible by the nonpunctual MITL[F,P].
Journal:
Computing Research Repository  CORR
, vol. abs/1102.5, 2011
DOI:
10.1007/9783642232176_5
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.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.informatik.unitrier.de
)
(
arxiv.org
)
(
adsabs.harvard.edu
)
More »
References
(16)
Marking the chops: an unambiguous temporal logic
(
Citations: 10
)
Kamal Lodaya
,
Paritosh K. Pandya
,
Simoni S. Shah
Conference:
IFIP International Conference on Theoretical Computer Science  IFIP TCS
, pp. 461476, 2008
Weak Alternating Timed Automata
(
Citations: 4
)
Pawel Parys
,
Igor Walukiewicz
Conference:
International Colloquium on Automata, Languages and Programming  ICALP
, pp. 273284, 2009
Realtime Logics: Complexity and Expressiveness
(
Citations: 260
)
Rajeev Alur
,
Thomas A. Henzinger
Conference:
Logic in Computer Science  LICS
, pp. 390401, 1990
Back to the Future: Towards a Theory of Timed Regular Languages
(
Citations: 50
)
Rajeev Alur
,
Thomas A. Henzinger
Conference:
IEEE Symposium on Foundations of Computer Science  FOCS
, pp. 177186, 1992
A Really Temporal Logic
(
Citations: 336
)
Rajeev Alur
,
Thomas A. Henzinger
Conference:
IEEE Symposium on Foundations of Computer Science  FOCS
, pp. 164169, 1994