On the relationships between theories of time granularity and the monadic second-order theory of one successor

In this paper we explore the connections between the monadic second-order theory of one successor MSO[<] for short) and the theories of omega-layered structures for time granularity. We first prove that the decision problem for MSO[<] and that for a suitable first-order theory of the upward unbounded layered structure are inter-reducible. Then, we show that a similar result holds for suitable chain variants of the MSO theory of the totally unbounded layered structure (this allows us to solve a decision problem about theories of time granularity left open by Franceschet et al. [FRA 06])).