On Relaxing Metric Information in Linear Temporal Logic

Details On Relaxing Metric Information in Linear Temporal Logic On Relaxing Metric Information in Linear Temporal Logic

2009-06-25

arxiv.org/abs/0906.4711v4

Computer Science

Logic in Computer Science

Minor changes

Scientific paper

Metric LTL formulas rely on the next operator to encode time distances, whereas qualitative LTL formulas use only the until operator. This paper shows how to transform any metric LTL formula M into a qualitative formula Q, such that Q is satisfiable if and only if M is satisfiable over words with variability bounded with respect to the largest distances used in M (i.e., occurrences of next), but the size of Q is independent of such distances. Besides the theoretical interest, this result can help simplify the verification of systems with time-granularity heterogeneity, where large distances are required to express the coarse-grain dynamics in terms of fine-grain time units.

Affiliated with

Also associated with

No associations

Rating

On Relaxing Metric Information in Linear Temporal Logic 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 Relaxing Metric Information in Linear Temporal Logic, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On Relaxing Metric Information in Linear Temporal Logic will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-537549