Suitable extensions of monadic second-order theories of k
successors have been proposed in the literature to specify in a
concise way reactive systems whose behaviour can be naturally
modeled with respect to a (possibly infinite) set of
differently-grained temporal domains. This is the case, for
instance, of the wide-ranging class of real-time reactive systems
whose components have dynamic behaviours regulated by very
different time constants, e.g., days, hours, and seconds. In this
paper, we focus on the theory of k-refinable downward
unbounded layered structures
MSO[<_{tot},(\downarrow_i)_{i=0}^{k-1}], that is, the theory of infinitely refinable structures consisting of a coarsest domain and an infinite number of finer and finer domains, whose satisfiability problem is nonelementarily decidable. We define a propositional temporal logic counterpart of
MSO[<_{tot},(\downarrow_i)_{i=0}^{k-1}], with set quantification restricted to infinite paths, called CTSL, which features an original mix of linear and branching temporal operators. We prove the expressive completeness of CTSL with respect to such a path fragment of
MSO[<_{tot}, (\downarrow_i)_{i=0}^{k-1}], and show that its satisfiability problem is 2EXPTIME-complete.
