Decidable Theories of $\omega$-Layered Metric Temporal Structures
Angelo Montanari, Adriano Peron, Alberto Policriti

Abstract:
This paper focuses on decidability problems for metric and layered temporal 
logics which allow one to model time granularity in various contexts. The 
decidability of pure metric (non­granular) fragments and of metric temporal 
logics endowed with finitely many layers has been already proved by reduction 
to the decidability problem of the well­known theory S1S. In the present work, 
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 fine temporal layers. The proof for the first theory is obtained 
by reduction to the decidability problem of an extension of S1S which is 
proved to be the logical counterpart of the class of \omega­languages accepted 
by systolic tree automata. The proof for the second one is done through the 
reduction to the monadic second­order decidable theory of k successors SkS.