Graded CTL* over finite paths

               Aniello Murano, Sasha Rubin, Loredana Sorrentino

                     Università degli Studi di Napoli Federico II



       Abstract. In this paper we introduce Graded Computation Tree Logic
       over finite paths (GCTL∗f , for short), a variant of Computation Tree
       Logic CTL∗ , in which path quantifiers are interpreted over finite paths
       and can count the number of such paths. State formulas of GCTL∗f are
       interpreted over Kripke structures with a designated set of states, which
       we call "check points". These special states serve to delineate the end
       points of the finite executions. The syntax of GCTL∗f has path quantifiers
       of the form E≥g ψ which express that there are at least g many distinct
       finite paths that a) end in a check point, and b) satisfy ψ. After defining
       and justifying the logic GCTL∗f , we solve its model checking problem
       and establish that its computational complexity is PSPACE-complete.


1    Introduction
Temporal logics are a special kind of modal logics in which the truth values of the
assertions vary with time [24]. Introduced in the seventies, these logics provide a
very useful framework for checking the reliability of reactive systems, i.e., systems
that continuously interact with the external environment. In formal verification
[7,8,21,25] to check whether a system meets a desired behaviour, we check, by
means of a suitable algorithm, whether a mathematical model of the system
satisfies a formal specification of the required behaviour, the latter usually given
in terms of a temporal-logic formula.
    Depending on the view of the underlying nature of the time, we distinguish
between two types of temporal logics. In linear-time temporal logics (such as
LTL [24]) each moment in time follows a unique possible future. On the other
hand, in branching-time temporal logics (such as CTL [7] and CTL? [13]) each
moment in time can be split into various possible futures. In order to express
properties along one or all the possible futures, branching logics make use of
existential and universal path quantifiers.
    Driven by the need to capture some specific system requirements, several
variants and extensions of classic temporal logics have been considered over the
years. One direction concerns the use of graded path modalities in branching-time
temporal logics [3,18,26,14,6,1,17,20,2,22]. These modalities allow us to express
properties such as "there exists at least n possible paths that satisfy a formula" or
"all but n paths satisfy a formula". In [5], the authors introduce the extension of
CTL with graded modalities, namely GCTL. They prove that, although GCTL
is more expressive than CTL, the satisfiability problem for GCTL remains
solvable in ExpTime, even in the case the graded numbers are coded in binary.
In [16] the authors consider the model-checking problem using formulas expressed
in GCTL and investigate its complexity: given a GCTL formula ϕ and a system
model represented by a Kripke structure K, the model-checking problem can be
solved in time (|K| · |ϕ|), that is the same running time required for CTL. In
[2], the logic GCTL? was investigated. First, it was proved that it is equivalent,
over trees, to Monadic Path Logic. Then, the authors turn to the satisfiability
problem and show that it is 2ExpTime-complete. Finally, they show that the
complexity of the model checking problem is PSpace-complete. So, for both
decision problems we have the same complexity as for CTL? , although GCTL?
is strictly more expressive.
     Another meaningful direction concerning variations of classic temporal logics
concerns the interpretation of formulas over finite paths [10,9,19,11,12]. The
motivation for this is that many areas of Artificial Intelligence and Computer
Science involve finite executions. A seminal work in this setting is [10], where
the LTL logic framework was revisited under this assumption. In [10] it was
proved that the resulting logic, namely LTLf , has the expressive power of
First Order Logic. Also, it was proved that satisfiability and model-checking are
PSpace-complete, thus not harder than LTL. Branching-time temporal logics
interpreted over finite paths were also introduced and studied in the literature
[27,13]. Very recently, this was also investigated for logics of strategic reasoning [4].
     Although the interpretation of graded formulas over finite computations seems
natural and useful in practice, surprisingly this specific combination has never
been addressed in the literature. In formal verification, such a formalism could be
useful to accelerate the process of finding bad computations (similarly to what was
done in [15,16] for infinite computations) or to check an unambiguous satisfaction
of a property (similarly to what was done in [1] for infinite computations).
     Our Contribution. In this paper we introduce a variant of Computation
Tree Logic (CTL∗ ), namely GCTL∗f , in which path quantifiers E ≥g are graded
and interpreted over finite paths. The difference with CTL? is that we restrict the
evaluation of formulas to finite paths and, that it makes use of a grade g (a natural
number or infinity) that is coupled with the path quantifiers E and A in order
to count paths. GCTL∗f formulas are interpreted over Kripke structures that
are additionally annotated by marked states which we call check points. As the
name advocates, these states represent moments along a system computation that
should be inspected (by the formula). We address the computational complexity
of the model-checking problem for GCTL∗f . The complexity is PSpace-hard, a
fact that already holds for the fragment of formulas in which g = 1 [4]. On the
other hand, we provide a matching upper-bound using a mix of automata-theory
and nondeterministic algorithms.

Outline This paper is structured in the following way. In Section 2 we present
some basic known concepts about automata and directed graphs that we use
to solve our problem. In Section 3 we introduce and discuss the syntax and
semantics of GCTL∗f . In Section 4 we provide a PSpace algorithm for the model
checking problem of GCTL∗f . Finally, in Section 5 we give some possible future
directions.
2    Preliminaries
In this section, we provide basic concepts about graphs and automata that we
will use. As these are common definitions, an expert reader can skip this part.

Directed Graphs A graph G is pair (V, E) where V is a finite set of vertices
(also, called states nodes or points) and E ⊆ V × V is a set of edges (also, called
arcs or lines). A path in G, of length m, is a sequence of m vertices v0 , ..., vm−1
such that, for each i = 1, ..., m − 1 we have that (vi−1 , vi ) ∈ E. Given two vertices
va and vb , we also say that vb is reachable from va if there exists a path of length
at least 1 that starts with va and ends with vb . A path is called simple if no
vertex appears more than once.

Nondeterministic Finite Word Automaton. A Nondeterministic Finite
Word Automaton (NFW, for short) is a tuple A = (AP, N, I, δ, F) where
 – AP is a finite non-empty set of atomic propositions;
 – N is a finite non-empty set of states;
 – I ⊆ N is a non-empty set of initial states;
 – δ : N × 2AP → 2N is a transition function;
 – F ⊆ N is a set of final states.
     Intuitively, δ(s, σ) is the set of states that A can move into when it is in the
state s and reads a subset of atoms σ ∈ 2AP . The automaton A is deterministic
(DFW, for short) if |I| = 1 and |δ(s, σ)| = 1 for each state s and input σ ∈ 2AP .
     A run r of A on a word w = σ0 , σ1 , ..., σm−1 ∈ (2AP )∗ is a sequence
s0 , s1 , ..., sm of m + 1 states (i.e., elements of N ) such that s0 ∈ I and si+1 =
δ(si , σi ) for 0 ≤ i < m. A run r is accepting if sm ∈ F. A word w is accepted by
A if A has an accepting run on w. The language of A is the set of words accepted
by A.
     The size of an NFW A, denoted |A|, is the cardinality of N.


3    Graded Computation Tree Logic over finite paths
In this section, we introduce Graded Computation Tree Logic over finite paths
(GCTL∗f , for short), a variant of CTL∗ in which the path quantifiers are graded
and interpreted over finite paths. In particular, the syntax of GCTL∗f is an
adaptation of branching-time logic with the following main features. On the one
hand it restricts GCTL? [5] by considering finite paths that end in check points,
and on the other hand it extends CTL? [13] by means of grades g ∈ N ∪ {∞}
applied to the existential path quantifier E.
    The obtained existential path operators E≥g ψ expresses that there are at least
g distinct paths satisfying ψ. Just as for CTL? , the syntax includes path-formulas,
expressing properties of paths, and state-formulas, expressing properties of states.
Definition 1 (GCTL∗f syntax). GCTL∗f formulas are inductively built from
a set of atomic propositions AP, by using the following grammar:
        φ := p | ¬φ | φ ∧ φ | E≥g ψ | E≥∞ ,          where p ∈ AP and g ∈ N
        ψ := φ | ¬ψ | ψ ∧ ψ | Xψ | ψUψ

    All the formulas generated by a φ-rule are called state-formulas, while the
formulas generated by a ψ-rule are called path-formulas. The temporal oper-
ators are X (read "next") and U (read "until"). The path quantifier is E ≥g
(read "there exists at least g distinct paths..."). We introduce the following ab-
breviations: A<g ψ = ¬E ≥g ¬ψ (read "all but less than g paths satisfy ψ"),
ψ1 Rψ2 = ¬(¬ψ1 U¬ψ2 ) (read "release"), Fψ = trueUψ (read "eventually"),
Gψ = f alseRψ (read "globally"), and ψ1 ∨ ψ2 = ¬(¬ψ1 ∧ ¬ψ2 ) (read "or").
    The semantics for GCTL∗f is defined w.r.t. a particular Kripke Structure in
which there are special states which we call check points. It is a structure similar
to a nondeterministic automaton and it is defined as follows.

Definition 2 (Kripke Structure System with check points). A Kripke
Structure System with check points (KSc, for short) is a tuple K = hSt, AP, λ, τ, s0 ,
Ci such that:

 – St is a finite non-empty set of states;
 – AP is a set of atomic propositions;
 – λ : St → 2AP is the labeling function mapping each state to the atomic
   propositions true in that state;
 – τ ⊆ St × St is a transition relation;
 – s0 ∈ St is an initial state;
 – C ⊆ St is a set of states called check points.

    A path ρ in K is a finite (resp., infinite) sequence of states ρ ∈ St∗ (resp., Stω )
such that, for all i ∈ [0, |ρ| − 1[ (resp., for all i ∈ N) it holds that (ρi , ρi+1 ) ∈ τ .
We define Pth(K) ⊆ Stω ∪ St∗ to denote the sets of paths π in K and we define
Pth(s) to denote the set of paths starting from s. The first element of π is denoted
by fst(π) , π0 , and its last by lst(π). Furthermore, we write (π)i , πi to denote
the i-th element of π.
    The semantics for GCTL∗f is defined w.r.t. KSc. The existential quantifiers
E≥g ψ express that there are at least g distinct paths ending in check points that
satisfy ψ. We distinguish finite paths π1 , π2 ∈ Pth(K) of K in the natural way:
two paths are distinct if they have different lengths, or if they have the same
length, say m, and there exists an index 0 ≤ i < m such that that π1 (i) 6= π2 (i).

Definition 3 (GCTL∗f Semantics). The semantics of GCTL∗f formulas is
recursively defined for a KSc K, a state s, a path π and a natural number i ∈ N.
    For state-formulas φ, φ1 , and φ2 :

 – K, s |= p if p ∈ λ(s);
 – K, s |= ¬φ if K, s 6|= φ;
 – K, s |= φ1 ∧ φ2 if both K, s |= φ1 and K, s |= φ2 ;
 – K, s |= E≥g ψ if there exists at least g distinct paths π in Pth(s) such that (a)
   lst(π) ∈ C and (b) K, π, 0 |= ψ;
 – K, s |= E≥∞ ψ if there exists infinitely many distinct paths π in Pth(s) such
   that (a) lst(π) ∈ C and (b) K, π, 0 |= ψ;

For path-formulas φ, ψ, ψ1 , and ψ2 :

 – K, π, i |= φ if K, (π)i |= φ;
 – K, π, i |= ¬ψ if K, π, i 6|= ψ;
 – K, π, i |= ψ1 ∧ ψ2 if both K, π, i |= ψ1 and K, π, i |= ψ2 ;
 – K, π, i |= Xψ if i + 1 < |π| and K, π, i + 1 |= ψ;
 – K, π, i |= ψ1 Uψ2 if there exists k ∈ N such that K, π, i + k |= ψ2 and K, π, i +
   j |= ψ1 , for all j ∈ [0, k[;

    We say that π satisfies the path formula ψ over K, and write K, π |= ψ, if
K, π, 0 |= ψ. Also, we say that K satisfies the state formula φ, and write K |= φ,
if K, s0 |= φ. We call a path formula without a path quantifier a flat path formula.

    Note that a finite path π satisfies Xψ at position i implies, in particular, that
i is not the last position in π.

Remark 1. The logic CTL∗f introduced in [4] is similar to GCTL∗f except that it
does not have graded quantifiers, only E. That logic is a fragment of ours. To see
this, simply restrict our logic to formulas in which every degree g is equal to 1.


4    Model Checking

In this section, we solve the model checking GCTL∗f and we provide an upper
bound on its computational complexity. First, we define the decision problem.

Definition 4. The model-checking problem for GCTL∗f is the following: given
a KSc K and a GCTL∗f formula φ decide if K |= φ.

   In order to measure the complexity, we need to define the size of the input
K and φ. The size of a structure K is its number of states, and the size of a
formula φ is defined as usual, except that |E≥g ψ| = 1 + |g| + |ψ| for g 6= ∞, and
|E≥∞ ψ| = 1 + |ψ|, i.e., the grades are represented in unary.
   The main result of this section is that model checking GCTL∗f is in PSpace.
Since model-checking CTL∗f is PSpace-hard [4], we get that model-checking
GCTL∗f is PSpace-complete.

Theorem 1. The Model Checking Problem of GCTL∗f is in PSpace.

    To prove this, we first provide an algorithm (Algorithm 1) that processes the
state sub-formulas ϕ of φ, starting from the innermost one and, for each state s
decides if (K, s) |= ϕ holds. The algorithm uses the following notions. A formula
ϕ is a maximal state-subformula of φ if ϕ is a state-subformula of φ and ϕ is
not a proper sub-formula of any other state sub-formula of φ. Every flat path
formula ψ of GCTL∗f formula φ can be viewed as an LTL formula whose atoms
Algorithm 1 ModelChecking
 1: function ModelChecking(K, φ). Returns the set of states s for which K, s |= φ
 2:    Introduce a new atom pφ
 3:    if φ = p ∈ AP then
 4:        return the set of states s such that p ∈ λ(s).
 5:    end if
 6:    if φ = ¬φ1 then
 7:        return the set of states s such that s 6∈ModelChecking(K, φ1 ).
 8:    end if
 9:    if φ = φ1 ∧ φ2 then                          T
10:        return the set of states s such that s ∈ i=1,2 ModelChecking(K, φi ).
11:    end if
12:    if φ = E≥g ψ then
13:        for all maximal state-subformulas ϕ of ψ do
14:           Introduce a fresh atom pϕ
15:           Redefine λ so that pϕ ∈ λ(s) iff s ∈ModelChecking(K, ϕ).
16:           Replace every occurrence of ϕ in ψ by pϕ .
17:        end for
18:        Convert ψ into an equivalent NFW N .
19:        Return the set of states s such that ExistsP aths(K, s0 , N , g)
20:    end if
21: end function




are elements of a maximal state-subformula φ as is usual for branching-time
logics, e.g., see [21].
    Looking at Algorithm 1, we see that atomic case and the Boolean operations
are immediate. For the path quantifier E≥g ψ the algorithm relabels each state by
a fresh atom pϕ iff the maximal state sub-formula ϕ of ψ holds in that state. This
is done recursively. It then treats ψ as flat path formula by replacing each ϕ by pϕ .
In Line 18, it converts ψ into an NFW accepting all strings (over the alphabet
2AP ) that satisfy the formula ψ. This can be done using an adaptation of the
classic Vardi-Wolper construction ([28]) for finite words [10]. In the last step,
thanks to the algorithm ExistsP aths (Algorithm 2) we verify (in NLogSpace
in |K| and |N | and PSpace in g) if there exist at least g distinct paths in K, each
of which starts with s and ends with some vertex in C, each one labeling a word
accepted by N . Note that the NFW may be of exponential size, but it can be
built on-the-fly, i.e., there is a PSpace algorithm that computes the transition
function of N (which is needed in Line 8 of Algorithm 2).
     We now describe the Algorithm 2 for counting paths. The algorithm uses
the following terminology: for a vertex v we let Adj(v) denote the set of vertices
v 0 such that (v, v 0 ) ∈ E. The idea of the algorithm is to guess g many different
paths in K. It does this step-by-step, only storing the last state of each path.
Note that to ease readability of the algorithm, there are implicit loops over the
indices i, j ≤ g, e.g., in line 2, we set Kcuri to be s for every i.
Algorithm 2 ExistsPaths
 1: function ExistsPaths(K, s, N , g) . Returns YES if there are at least g distinct
    paths in K = hSt, AP, λ, τ, s, Ci from s ∈ St to the vertices in C, each one labeling
    a word accepted by N = (AP, N, I, δ, F ).
 2:    Kcuri ← s                                                               . ∀i : i ≤ g
 3:    assign Ncuri ∈ I non-deterministically                                  . ∀i : i ≤ g
                        . endedi = ⊥ indicates that the current element i is not ended
 4:    endedi = ⊥                                                              . ∀i : i ≤ g
                          . Kdiffi,j = ⊥ indicates that the two paths are not different
 5:    Kdiffi,j = ⊥                                                     . ∀i, j : i 6= j ≤ g
 6:    while true do
 7:        if ¬endedi then                                                     . ∀i : i ≤ g
 8:            Replace Ncuri by an element of δ(Ncuri , λ(Kcuri ))                 . nondet
 9:        end if
10:        if ¬endedi and Kcuri ∈ C and Ncuri ∈ F then                         . ∀i : i ≤ g
11:            assign endedi ∈ {⊥, >} non-deterministically
12:        end if
13:        if ¬endedi and endedj then                                   . ∀i, j : i 6= j ≤ g
14:            Kdiffi,j ← >              . If one ends now but the other has not ended
15:        endV if           V
16:        if i endedi and i6=j≤g Kdiffi,j then
17:            Return YES
18:        end if
19:        if ¬endedi then                                                     . ∀i : i ≤ g
20:            Replace Kcuri by an element of Adj(Kcuri )                          . nondet
21:        end if
22:        if ¬endedi and ¬endedj and Kcuri 6= Kcurj then               . ∀i, j : i 6= j ≤ g
23:            Kdiffi,j ← > . If both have not ended, but they have different states
24:        end if
25:    end while
26: end function



Proposition 1 (Counting Paths). The Algorithm ExistsP aths(K, s, N , g)
decides if there exist at least g distinct paths in K, each of which starts with s
and ends with some vertex in C, each one labeling a word accepted by N . It works
in NLogSpace in |K| and |N |, and PSpace in g.

Proof. The variables Kcuri are used in order to store the last state in K; they
are initialised to s in line 2, and each path is advanced by one state in line 20
(i.e., if the path is not ended). The algorithm simultaneously also guesses g runs
in N , one for each of the guessed paths in K. The variable Ncuri are used to
store the last state of the ith guessed path in N ; it is initialised in line 3 by
non-deterministically assigning it an element of the set I of initial states, and
it is updated in line 8. In line 10, the algorithm also guesses when a given path
in K finishes, and remembers this fact by setting the flag endedi to true. These
flags initially are set to false in order to indicate that the ith path has not ended.
The algorithm updates the variable Kdiffi,j , initially set to false (indicating
that the two paths are not different) when it sees that the ith and jth path are
different. This happens in one of two cases: (1) in some step, the ith path ended
and the jth path did not (line 13), or (2) in some step, the current state of the
ith path and jth path are different (line 22). Thus, if the algorithm returns YES
(line 17) then there are g distinct paths in K, that (by guard 10) each end in
C and label words accepted by N . On the other hand, suppose there exists g
different sequences in K, each ending in C, and g corresponding sequences in N
whose states are labeled by a word accepted by the automaton. Then we can use
these paths to resolve the nondeterminism in lines 3, 8, 11 and 20, so that the
algorithm returns YES.
    Regarding the space complexity, first note that the algorithm is nondetermin-
istic. Now, to store a vertex of a graph with N vertices we need logspace in N .
The algorithm requires to store O(g) many such vertices. It also requires O(g 2 )
many boolean variables (for the variables endedi and Kdif fi,j ).               t
                                                                                u


5   Conclusion and Future Work

Recently, temporal logic formalisms restricted to finite computations have received
large attention in formal system verification. This concept is very important in
many areas of Artificial Intelligence. For example, one may think of business
processes that are modelled using finite path, or to automated planning in which
the executions are often finite. In this paper we introduced a variant of CTL? ,
namely GCTL∗f , in which the formulas are interpreted over finite paths that can
be selected by the logic by means of a graded modality. We addressed the model
checking problem for GCTL∗f and proved it to be PSpace-complete.
    Besides that, this articles opens several direction for future work. First,
we recall that graded modalities have been studied also in the context of the
modal µ-calculus, with and without backwards modalities [6]. It would be worth
reconsidering that logic under the finite path semantics as we have done in this
paper. Another interesting direction would be to consider enriching GCTL∗f
with knowledge operators. Also, recent work shows how to count the number of
strategies in a graph game [23,4], and extending our work to count strategies in
the finite-trace case is of interest.
    Finally, note that we have assumed in this paper that graded numbers used
along formulas are coded in unary. By using a binary coding we immediately
loose an exponent in the complexity of the model checking procedure. We leave
open the question of whether this blow-up is avoidable (cf. [5]).


References

 1. Benjamin Aminof, Vadim Malvone, Aniello Murano, and Sasha Rubin. Graded
    modalities in strategy logic. Information and Computation, 261:634 – 649, 2018.
 2. Benjamin Aminof, Aniello Murano, and Sasha Rubin. CTL* with graded path
    modalities. Information and Computation, 262 (Part 2):1 – 21, 2018.
 3. Everardo Bárcenas, Edgard Benítez-Guerrero, and Jesús Lavalle. On the model
    checking of the graded µ-calculus on trees. In MICAI 2015, volume 9413 of Lecture
    Notes in Computer Science, pages 178–189. Springer, 2015.
 4. Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, and Sasha Rubin.
    Alternating-time temporal logic on finite traces. In International Joint Conference
    on Artificial Intelligence, pages 77–83, 2018.
 5. A. Bianco, F. Mogavero, and A. Murano. Graded Computation Tree Logic. Trans-
    actions On Computational Logic, 13(3):25:1–53, 2012.
 6. P.A. Bonatti, C. Lutz, A. Murano, and M.Y. Vardi. The Complexity of Enriched
    muCalculi. Logical Methods in Computer Science, 4(3):1–27, 2008.
 7. E.M. Clarke and E.A. Emerson. Design and Synthesis of Synchronization Skeletons
    Using Branching-Time Temporal Logic. In Logic of Programs’81, LNCS 131, pages
    52–71. Springer, 1981.
 8. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT Press, 2002.
 9. Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. Reasoning on
    LTL on finite traces: Insensitivity to infiniteness. In AAAI, pages 1027–1033, 2014.
10. Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear
    dynamic logic on finite traces. In IJCAI 2013, pages 854–860. IJCAI/AAAI, 2013.
11. Giuseppe De Giacomo and Moshe Y. Vardi. Synthesis for LTL and LDL on
    finite traces. In Qiang Yang and Michael Wooldridge, editors, IJCAI 2015, pages
    1558–1564. AAAI Press, 2015.
12. Giuseppe De Giacomo and Moshe Y. Vardi. LTLf and LDLf synthesis under partial
    observability. In Subbarao Kambhampati, editor, IJCAI 2016, pages 1044–1050.
    IJCAI/AAAI Press, 2016.
13. E.A. Emerson and J.Y. Halpern. “Sometimes” and “Not Never” Revisited: On
    Branching Versus Linear Time. Journal of the ACM, 33(1):151–178, 1986.
14. A. Ferrante, A. Murano, and M. Parente. Enriched Mu-Calculi Module Checking.
    Logical Methods in Computer Science, 4(3):1–21, 2008.
15. A. Ferrante, M. Napoli, and M. Parente. Graded-ctl: Satisfiability and symbolic
    model checking. In ICFEM 2009, volume LNCS 5885, pages 306–325, 2009.
16. A. Ferrante, M. Napoli, and M. Parente. Model Checking for Graded CTL. Funda-
    menta Informaticae, 96(3):323–339, 2009.
17. M. Kaminski, S. Schneider, and G. Smolka. Terminating tableaux for graded hybrid
    logic with global modalities and role hierarchies. LMCS, 7(1), 2011.
18. Yevgeny Kazakov and Ian Pratt-Hartmann. A note on the complexity of the
    satisfiability problem for graded modal logics. In Symposium on Logic in Computer
    Science, pages 407–416, 2009.
19. Jeremy Kong and Alessio Lomuscio. Model checking multi-agent systems against
    LDLK specifications on finite traces. In AAMAS 2018, pages 166–174. IFAA-
    MAS/ACM, 2018.
20. O. Kupferman, U. Sattler, and M.Y. Vardi. The Complexity of the Graded mu-
    Calculus. In Conference on Automated Deduction’02, LNCS 2392, pages 423–437.
    Springer, 2002.
21. O. Kupferman, M.Y. Vardi, and P. Wolper. An Automata Theoretic Approach to
    Branching-Time Model Checking. Journal of the ACM, 47(2):312–360, 2000.
22. Vadim Malvone, Fabio Mogavero, Aniello Murano, and Loredana Sorrentino. Rea-
    soning about graded strategy quantifiers. Information and Computation, 259:390 –
    411, 2018.
23. Vadim Malvone, Aniello Murano, and Loredana Sorrentino. Additional winning
    strategies in reachability games. Fundam. Inform., 159(1-2):175–195, 2018.
24. A. Pnueli. The Temporal Logic of Programs. In Foundation of Computer Science’77,
    pages 46–57. IEEE Computer Society, 1977.
25. J.P. Queille and J. Sifakis. Specification and Verification of Concurrent Programs
    in Cesar. In Symposium on Programming’81, LNCS 137, pages 337–351. Springer,
    1981.
26. S. Tobies. PSPACE Reasoning for Graded Modal Logics. Journal of Logic and
    Computation, 11(1):85–106, 2001.
27. M. Y. Vardi and L. Stockmeyer. Lower bound in full (2EXPTIME-hardness for
    CTL-SAT). 1985.
28. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Inf. Comput.,
    115(1):1–37, 1994.