Dense Time Reasoning via Mosaics

In this paper we consider the problem of temporal reasoning over a real numbers model of time. After a quick survey of related logics such as those based on intervals, or metric information or rational numbers, we concentrate on using the Until and Since temporal connectives introduced in. We will call this logic RTL. Although RTL has been axiomatized and is known to be decidable it has only recently been established that a PSPACE decision procedure exists. Thus, it is just as easy to reason over real-numbers time as over the traditional natural numbers model of time. The body of the paper outlines the basics of the novel temporal "mosaic" method used to show this complexity.