CTL\(^\ast\) with graded path modalities (Q1784942)

The paper studies Graded CTL*, an extension of the well-known branching-time temporal logic CTL* with path quantifiers that can express the existence of $k$ different paths satisfying some linear-time temporal formula, for an arbitrary $k$. This logic truly extends CTL* as it does not preserve bisimulations anymore, hence, it is more expressive. \par The main focus of the paper is a worst-case complexity analysis of the standard decision problems of model checking and satisfiability checking for this logic. Decidability is easily obtained by noticing that -- despite a general lack of invariance under bisimulations -- the logic cannot distinguish a graph model from its tree unfolding. This forms the basis of a translation into MSO interpreted over trees which yields decidability. It does not give optimal complexity bounds, though. These are obtained using the well-established automata-theoretic approach to temporal logics. The paper introduces a specialisation of alternating tree automata whose features tightly correspond to those present in the logic. It then establishes decidability of emptiness in exponential time which, for example, yields decidability of satisfiability in doubly exponential time. \par The paper is generally well written and easy to follow. The concluding section contains some interesting remarks on open problems in this area, most notably regarding the succinctness of Graded CTL* in comparison to other logics of equal expressive power.