Compositional Reasoning using Intervals and Time Reversal

14^th December 2011, 11:00 ALT
Ben Moszkowski
Software Technology Research Laboratory
De Montfort University
Leicester
UK

Abstract

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 a basic and interesting class of compositional ITL formulas and some properties obtained from them with the aid of time reversal. We are currently exploring the use of these techniques as part 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.