Graded Computation Tree Logic with Binary Coding

Graded path quantifiers have been recently introduced and investigated as a useful framework for generalizing standard existential and universal path quantifiers in the branching-time temporal logic CTL (GCTL), in such a way that they can express statements about a minimal and conservative number of accessible paths. These quantifiers naturally extend to paths the concept of graded world modalities, which has been deeply investigated for the mu-Calculus (Gmu-Calculus) where it allows to express statements about a given number of immediately accessible worlds. As for the “non-graded” case, it has been shown that the satisfiability problem for GCTL and the Gmu-Calculus coincides and, in particular, it remains solvable in ExpTime. However, GCTL has been only investigated w.r.t. graded numbers coded in unary, while Gmu-Calculus uses for this a binary coding, and it was left open the problem to decide whether the same result may or may not hold for binary GCTL. In this paper, by exploiting an automata theoretic-approach, which involves a model of alternating automata with satellites, we answer positively to this question. We further investigate the succinctness of binary GCTL and show that it is at least exponentially more succinct than Gmu-Calculus. Finally, we discuss the extension of the exploited technique to the case of binary graded CTL* (GCTL*). In this case, the satisfiability problem becomes solvable in 3ExpTime.