A propositional dense time logic

This paper extends propositional linear time temporal logic (PTL) to propositional dense time logic (PDTL). While a PTL model is a single sequence of states, a PDTL model, called an omega-tree, consists of a nested sequence of states. Two new operators, called within and everywhere are introduced to access nested sequences. Besides its application in describing activities for Artificial Intelligence, PDTL can be used to represent more naturally procedural abstractions in control flow. PDTL is shown to be decidable by a tableau based method, and a complete axiomatization is given.PDTL's omega tree models allow a dense mix of events. By imposing a stability condition on the propositions we get a subset of the omega tree models called ordinal trees which are free of dense mix. This logic called Propositional Ordinal Tree Logic (POTL) is also shown to be decidable in exponential time. Ordinal tree models though based on dense points, represent interval based information which maybe refined to any finite level. Hence POTL is a good bridge between point based and interval based temporal logics.Ordinal trees can be easily embedded as a temporal data structure in a conventional logic programming language and thus provide a framework for temporal logic programming.