A Hierarchical Analysis of Propositional Temporal Logic based on Intervals

Speaker: Ben Moszkowski

31st October 2005 , 1pm , Devonshire G21/G22 Conference Room

Abstract

We present a hierarchical framework for analysing propositional linear-time temporal logic (PTL) to obtain standard results such as a small model property, decision procedures and axiomatic completeness. Both finite time and infinite time are considered. The treatment of PTL with both the operator Until and past time is readily reduced to that for a version of PTL without either one. Our method is based on a low-level normal form for PTL called a transition configuration. In addition, we employ reasoning about intervals of time. Besides being hierarchical and interval-based, the approach differs from other analyses of PTL which in general utilise sets of formulas and sequences of such sets. Models are instead described by means of time intervals represented as finite and countably infinite sequences of states. The analysis naturally relates larger intervals with smaller ones. The steps involved are expressed in a propositional version of Interval Temporal Logic (ITL) since it is better suited than PTL for sequentially combining and decomposing formulas. Consequently, we can articulate various issues in PTL model construction which are equally relevant within a more conventional analysis but normally only considered at the metalevel. We also briefly describe a prototype implementation of a decision procedure based on Binary Decision Diagrams. Beyond the specific issues involving PTL, the research can be viewed as a significant application of ITL and interval-based reasoning and also illustrates a general approach to formally reasoning about a number of issues involving discrete linear time. For example, it makes use of various techniques for performing sequential and parallel composition. The formal notational framework for a hierarchical reduction of infinite-time reasoning to simpler finite-time reasoning could also be used in model checking. The work includes some interesting representation theorems and exploits properties of fixpoints of a certain interval-oriented temporal operator. In addition, it has relevance to hardware description and verification since the property specification languages PSL/Sugar (just made IEEE standard 1850) and "temporal e" (part of IEEE candidate standard 1647) both contain temporal constructs concerning intervals of time.