
A Hierarchical Analysis of Propositional Temporal Logic based on IntervalsBen Moszkowski Software Technology Research Laboratory De Montfort University 4pm Tuesday 13th September 2005 Room 2511, JCMB, King's Buildings We present a hierarchical framework for analysing propositional lineartime 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 lowlevel normal form for PTL called a transition configuration. In addition, we employ reasoning about intervals of time. Besides being hierarchical and intervalbased, 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. Document Actions 
