Academic
Publications
On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing

On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing,10.1007/978-3-642-23217-6_5,Computing Research

On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing  
BibTex | RIS | RefWorks Download
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 Ehrenfeucht-Fraisse 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 non-punctuality), 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 2-way 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 non-punctual MITL[F,P].
Journal: Computing Research Repository - CORR , vol. abs/1102.5, 2011
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.