Compositional Reasoning using Intervals and Time Reversal

We apply Interval Temporal Logic (ITL), an established temporal formalism for reasoning about time periods, to extending known facts by looking at them in reverse and then reducing reasoning about infinite time to finite time. Our presentation discusses various basic and interesting classes of compositional ITL formulas closed under conjunction and the temporal operator "always" as well as some properties then obtainable with the aid of time reversal. We are currently exploring the use of time reversal as part of a compositional analysis of some aspects of concurrent behaviour involving mutual exclusion. It also appears that time reversal can sometimes assist in reducing reasoning in ITL to conventional linear-time temporal logic.