Abstract

Logic and computer science communities have traditionally followed a different approach to the problem of representing and reasoning about time and states. Research in logic resulted in a family of tense logics that take time as a primitive notion and definite states as sets of atomic propositions which are true at given instants, while research in computer science concentrated on the so-called temporal logics of programs that take state as a primitive notion, and define time as an attribute of states. In this paper, we provide a unifying framework within which the two approaches can be reconciled. Our main tools are metric and layered temporal logics originally proposed to model time granularity in various contexts. In such a framework, states and time-instants can be uniformly referred to as elements of a theory of ω-layered metric temporal structures. Furthermore, we show that the theory of timed state sequences, underlying real-time logics, is naturally recovered as an abstraction of such a theory