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 μ-Calculus (Gμ-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 Gμ-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 Gμ-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 Gμ-Calculus.