Резюме. In this talk we make an application of our separation theorem for discrete time Interval Temporal Logic (ITL) to the study of Interval-based Computation Tree Logic (ICTL*). We prove that the expressibility of the expanding modalities and, most importantly, propositional quantification, carry over from linear time ITL to the branching time system of ICTL*. The relevance of this follows from the fact that point-based propositionally quantified CTL* (QCTL*) is the established intermediate language for temporal logics of agency as propositional quantification enables expressing the existence of strategies with given temporal properties. By moving to ITL we move a step further, using the expressibility of propositional quantification in the logic, which is markedly more expressive than point-based CTL* and facilitates the compositionality of specifications.