Ambre Peron

This paper focuses on decidability problems for metric and layered temporal logics. The considered logics - suitable to model time granularity in various contexts - allow one to build granular temporal models by referring to the natural scale in any component of the model and properly constraining the interactions between differently grained components. We prove the decidability of both the theory of metric temporal structures provided with an infinite number of arbitrarily coarse temporal layers and the theory of metric temporal structures provided with an infinite number of arbitrarily coarse temporal layers and the theory of metric temporal structures provided with an infinite number of arbitrarily fine temporal layers. The proof for the first theory is obtained by a reduction to the decidability problem of an extension of the standard monadic second-order theory of one successor MSO[

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