Branching-time logics with path relativisation

• We relativise path quantifier in branching-time logics using ω-languages.
• The extended logics are based on CTL, CTL+, CTL⁎, and ΔPDL.
• We study expressivity and complexity of satisfiability and model checking.
• Path relativisation captures abstractions and refinements of large systems.
• Logics with non-regular relativisations may be useful for software synthesis.

We define extensions of the full branching-time temporal logic CTL⁎ in which the path quantifiers are relativised by formal languages of infinite words, and consider its natural fragments obtained by extending the logics CTL and CTL+ in the same way. This yields a small and two-dimensional hierarchy of temporal logics parametrised by the class of languages used for the path restriction on one hand, and the use of temporal operators on the other. We motivate the study of such logics through two application scenarios: in abstraction and refinement they offer more precise means for the exclusion of spurious traces; and they may be useful in software synthesis where decidable logics without the finite model property are required. We study the relative expressive power of these logics as well as the complexities of their satisfiability and model-checking problems.