Turning Temporal Logic on its Head with Time Reversal

Title: Turning Temporal Logic on its Head with Time Reversal
Speaker: Dr. Ben Moszkowski (Software Technology Research Laboratory De Montfort University Leicester, England)
Time: 3:00pm,Monday,Oct.25
Venue: Lecture Room, Level 3 Building #5, Institute of Software, CAS

Abstract:For several decades the widely held conventional wisdom has been that point-based linear-time temporal logic is much superior to Interval Temporal Logic (ITL) for reasoning about safety and liveness properties of concurrent systems, especially when tool support is required. This perception has partially stemmed from ITL’s computational intractability.

We offer evidence suggesting that the prevailing viewpoint should be reexamined. Our presentation applies time reversal to Peterson’s classic mutual exclusion algorithm to illustrate how correctness properties in ITL can be more natural and at a higher level than in point-based temporal logic.

For computational purposes such as in decision procedures and model checking, the ITL formulas discussed are systematically transformable into related lower-level point-based ones. Hence point-based temporal logic primarily serves as a subordinate formalism.