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

Details 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

2011-02-28

arxiv.org/abs/1102.5638v2

Computer Science

Logic in Computer Science

Major revision of the paper

Scientific paper

Timed temporal logics exhibit a bewildering diversity of operators and the resulting decidability and expressiveness properties also vary considerably. We study the expressive power of timed logics TPTL[U,S] and MTL[U,S] as well as of 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. As our first main result, we show that MTL[U,S] is strictly contained within the freeze logic TPTL[U,S] for both weakly and strictly monotonic timed words, thereby extending the result of Bouyer et al and completing the proof of the original conjecture of Alur and Henziger from 1990. We also relate the expressiveness of a recently proposed deterministic freeze logic TTL[X,Y] (with NP-complete satisfiability) to MTL. As our second main result, we show by an explicit reduction that TTL[X,Y] lies strictly within the unary, non-punctual logic MITL[F,P]. This shows that deterministic freezing with punctuality is expressible in the non-punctual MITL[F,P].

Affiliated with

Also associated with

No associations

Rating

On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-425208