Abstract We consider the problem of controlling a multi-mode system with respect to a safety goal in the Filippov sliding-mode semantics. When the goal can be enforced, we present a symbolic algorithm that enhances the previously known solution. When the goal cannot be enforced, we compare different natural best-effort criteria, identify the most promising one, and design a symbolic algorithm that synthesizes the corresponding myopically optimal control policy. We prove that the synthesized policy enjoys a regularity property known as a tame topology .

As schema languages for RDF data become more mature, we are seeing efforts to extend them with recursive semantics, applying diverse ideas from logic programming and description logics. While ShEx has an official recursive semantics based on greatest fixpoints (GFP), the discussion for SHACL is ongoing and seems to be converging towards least fixpoints (LFP). A practical study we perform shows that, indeed, ShEx validators implement GFP, whereas SHACL validators are more heterogeneous. This situation creates tension between ShEx and SHACL, as their semantic commitments appear to diverge, potentially undermining interoperability and predictability. We aim to clarify this design space by comparing the main semantic options in a principled yet accessible way, hoping to engage both theoreticians and practicioners, especially those involved in developing tools and standards. We present a unifying formal semantics that treats LFP, GFP, and supported model semantics (SMS), clarifying their relationships and highlighting a duality between LFP and GFP on stratified fragments. Next, we investigate to which extent the directions taken by SHACL and ShEx are compatible. We show that, although ShEx and SHACL seem to be going in different directions, they include large fragments with identical expressive power. Moreover, there is a strong correspondence between these fragments through the aforementioned principle of duality. Finally, we present a complete picture of the data and combined complexity of ShEx and SHACL validation under LFP, GFP, and SMS, showing that SMS comes at a higher computational cost under standard complexity-theoretic assumptions.

A central goal of language theory is to compare formalisms by understanding both their expressive overlaps and their relative expressive power. One particularly challenging question in this direction is the problem of determining the common fragment of two formalisms F₁ and F₂, that is, effectively characterise the class F₁∩ F₂ of properties that can be expressed in both formalisms. This question can be equally phrased as a decision problem: given a property expressed in F₁ or F₂, decide whether the same property can be also expressed in F₁∩ F₂. A question closely related to this is the membership problem, denoted F₁ ↦ F₂, which asks whether a property expressed in F₁ can be also expressed in F₂. These problems become particularly difficult when branching-time formalisms are involved, in general due to the lack of equivalent algebraic characterizations. In this work, we prove that LTL ∩ PCTL is decidable, where PCTL denotes CTL extended with past operators. We do this by showing that both membership problems, LTL ↦ PCTL and PCTL ↦ LTL, are decidable. The direction PCTL ↦ LTL follows from suitable combinations of known results. The converse direction, LTL ↦ PCTL, requires an automata-theoretic characterisation of PCTL. Specifically, we introduce a new class of automata, called counter-free hesitant weak tree automata (HWT_cf) that capture precisely the expressiveness of PCTL, and that are obtained by combining two orthogonal restrictions on alternating parity tree automata, namely, counter-free hesitancy and weakness. We then prove that, for every word language L defined by an LTL formula, the associated tree language △[L] is recognisable by an HWT_cf if and only if L is recognized by a deterministic Büchi word automaton. Since the latter recognisability problem is known to be decidable, so is the former. This result advances the longstanding open problem of deciding LTL ∩ CTL. Indeed, that problem can now be reduced to PCTL ↦ CTL, that is, the question of when past operators can be eliminated.

Graphs have emerged as a foundation for a variety of applications, including capturing factual knowledge, semantic data integration, social networks, and informing machine learning algorithms. Formalising properties of the data and ensuring data quality requires describing schemas of such graphs. Driven by diverse applications, the Semantic Web and database communities developed not only different graph data models-RDF and property graphs-but also different graph schema languages-SHACL, ShEx, and PG-Schema. Each language has its unique approach to defining constraints and validating graph data, leaving potential users in the dark about their commonalities and differences. In this paper, we provide concise formal definitions of the core components of these languages, employ a uniform framework to facilitate a comprehensive comparison between them, and identify a common set of functionalities, shedding light on both overlapping and distinctive features.

Characterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and verification of properties in formal methods. While complete connections have been established for the linear-time case between temporal logics, predicate logics, algebraic models, and automata, the situation in the branching-time case remains considerably more fragmented. In this work, we provide an automata-theoretic characterisation of some important branching-time temporal logics, namely CTL* and ECTL* interpreted on arbitrary-branching trees, by identifying two variants of Hesitant Tree Automata that are proved equivalent to those logics. The characterisations also apply to Monadic Path Logic and the bisimulation-invariant fragment of Monadic Chain Logic, again interpreted over trees. These results widen the characterisation landscape of the branching-time case and solve a forty-year-old open question.

We propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, namely small progress measures and quasi dominions. We show that the integration of the two notions can be highly beneficial and significantly speeds up convergence to the problem solution. Experiments show that the resulting algorithm performs orders of magnitude better than the asymptotically-best solution algorithm currently known, without sacrificing on the worst-case complexity.

Monadic Second-Order Logic (MSO) extends First-Order Logic (FO) with variables ranging over sets and quantifications over those variables. We introduce and study Monadic Tree Logic (MTL), a fragment of MSO interpreted on infinite-tree models, where the sets over which the variables range are arbitrary subtrees of the original model. We analyse the expressiveness of MTL compared with variants of MSO and MPL, namely MSO with quantifications over paths. We also discuss the connections with temporal logics, by providing non-trivial fragments of the Graded µ-CALCULUS that can be embedded into MTL and by showing that MTL is enough to encode temporal logics for reasoning about strategies with FO-definable goals.

Hintikka and Sandu originally proposed Independence Friendly Logic (IF) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language.The logic allows for expressing independence constraints among quantified variables, in a similar vein to Henkin quantifiers, and has a nice game-theoretic semantics in terms of imperfect information games.However, the IF semantics exhibits some limitations, at least from a purely logical perspective.It treats the players asymmetrically, considering only one of the two players as having imperfect information when evaluating truth, resp., falsity, of a sentence.In addition, truth and falsity of sentences coincide with the existence of a uniform winning strategy for one of the two players in the semantic imperfect information game.As a consequence, IF does admit undetermined sentences, which are neither true nor false, thus failing the law of excluded middle.These idiosyncrasies limit its expressive power to the existential fragment of Second Order Logic (Sol).In this paper, we investigate an extension of IF, called Alternating Dependence/Independence Friendly Logic (ADIF), tailored to overcome these limitations.To this end, we introduce a novel compositional semantics, generalising the one based on trumps proposed by Hodges for IF.The new semantics (i) allows for meaningfully restricting both players at the same time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers the law of excluded middle for sentences, and (iv) grants ADIF the full descriptive power of Sol.We also provide an equivalent Herbrand-Skolem semantics and a gametheoretic semantics for the prenex fragment of ADIF, the latter being defined in terms of a determined infinite-duration game that precisely captures the other two semantics on finite structures.

Strategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-Complete, respectively.

An extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables. This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game-theoretic concepts. Inspired by the work on logics of dependence and independence, we provide a new compositional semantics for QPTL that allows for expressing such functional dependencies among variables. The fragment where only restricted quantifications are considered, called behavioral quantifications , allows for linear-time properties that are satisfiable if and only if they are realisable in the Pnueli-Rosner sense. This fragment can be decided, for both model checking and satisfiability , in 2 Exp Time and is expressively equivalent to QPTL , though significantly less succinct.

The Shapes Constraint Language (SHACL) is the recent W3C recommendation language for validating RDF data, by verifying certain shapes on graphs. Previous work has largely focused on the validation problem, while the standard decision problems of satisfiability and containment, crucial for design and optimisation purposes, have only been investigated for simplified versions of SHACL. Moreover, the SHACL specification does not define the semantics of recursively-defined constraints, which led to several alternative recursive semantics being proposed in the literature. The interaction between these different semantics and important decision problems has not been investigated yet. In this article we provide a comprehensive study of the different features of SHACL, by providing a translation to a new first-order language, called SCL, that precisely captures the semantics of SHACL. We also present MSCL, a second-order extension of SCL, which allows us to define, in a single formal logic framework, the main recursive semantics of SHACL. Within this language we also provide an effective treatment of filter constraints which are often neglected in the related literature. Using this logic we provide a detailed map of (un)decidability and complexity results for the satisfiability and containment decision problems for different SHACL fragments. Notably, we prove that both problems are undecidable for the full language, but we present decidable combinations of interesting features, even in the face of recursion.

Abstract We propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, small progress measures and quasi dominions. We show that the integration of the two notions can be highly beneficial and significantly speeds up convergence to the problem solution. Experiments show that the resulting algorithm performs orders of magnitude better than the asymptotically-best solution algorithm currently known, without sacrificing on the worst-case complexity.

In the design of complex systems, model-checking and satisfiability arise as two prominent decision problems. While model-checking requires the designed system to be provided in advance, satisfiability allows to check if such a system even exists. With very few exceptions, the second problem turns out to be harder than the first one from a complexity-theoretic standpoint. In this paper, we investigate the connection between the two problems for a non-trivial fragment of Strategy Logic (SL, for short). SL extends LTL with first-order quantifications over strategies, thus allowing to explicitly reason about the strategic abilities of agents in a multi-agent system. Satisfiability for the full logic is known to be highly undecidable, while model-checking is non-elementary.The SL fragment we consider is obtained by preventing strategic quantifications within the scope of temporal operators. The resulting logic is quite powerful, still allowing to express important game-theoretic properties of multi-agent systems, such as existence of Nash and immune equilibria, as well as to formalize the rational synthesis problem. We show that satisfiability for such a fragment is PSPACE-COMPLETE, while its model-checking complexity is 2EXPTIME-HARD. The result is obtained by means of an elegant encoding of the problem into the satisfiability of conjunctive-binding first-order logic, a recently discovered decidable fragment of first-order logic.

Cyber-Physical Systems (CPSs) are integrations of distributed computing systems with physical processes via a networking with actuators and sensors, where feedback loops among the components allow the physical processes to affect the computations and vice versa. Although CPSs can be found in several complex and sometimes critical real-world domains, their verification and validation often relies on simulation-test systems rather then automatic methodologies to formally verify safety requirements. In this work, we prove the decidability of the reachability problem for discrete-time linear CPSs whose physical process in isolation has a periodic behavior, up to an initial transitory phase.

Conjunctive-query containment is the problem of deciding whether the answers of a given conjunctive query on an arbitrary database instance are always contained in the answers of a second query on the same instance. This is a very relevant question in query optimization, data integration, and other data management and artificial intelligence areas. The problem has been deeply studied and understood for the, so-called, set-semantics, i.e., when query answers and database instances are modelled as sets of tuples. In particular, it has been shown by Chandra and Merlin to be NPTIME-COMPLETE. On the contrary, when investigated under bag-semantics, a.k.a. multiset semantics, which allows for replicated tuples both in the underlying instance and in the query answers, it is not even clear whether the problem is decidable. Since this is exactly the standard interpretation for commercial relational database systems, the question turns out to be an important one. Multiple works on variations and restrictions of the bag-containment problem have been reported in the literature and, although the general problem is still open, we contribute with this article by solving a special case that has been identified as a major open problem on its own. More specifically, we study projection-free queries, i.e., queries without existentially quantified variables, and show decidability for the bag-containment problem of a projection-free conjunctive query into a generic conjunctive query. We prove indeed that deciding containment in this setting is in ¶i^p_2. Our approach relies on the solution of a special case of the Diophantine inequality problem via a reduction to the linear inequality problem and clearly exposes inherent difficulties in the analysis of the general question.

We consider a setting where a user wants to pose a query against a dataset where background knowledge, expressed as logical sentences, is available, but only a subset of the information can be used to answer the query. We thus want to reformulate the user query against the subvocabulary, arriving at a query equivalent to the user’s query assuming the background theory, but using only the restricted vocabulary. We consider two variations of the problem, one where we want any such reformulation and another where we restrict the size. We present a classification of the complexity of the problem, then provide algorithms for solving the problems in practice and evaluate their performance.

A structure enjoys the Herbrand property if, whenever it satisfies an equality between some terms, these terms are unifiable. On such structures the expressive power of equalities becomes trivial, as their semantic satisfiability is reduced to a purely syntactic check. In this work, we introduce the notion of Herbrand property and develop it in a finite model-theoretic perspective. We provide, indeed, a canonical realization of the new concept by what we call quasi-Herbrand models and observe that, in stark contrast with the naive implementation of the property via standard Herbrand models, their universe can be finite even in presence of functions in the vocabulary. We exploit this feature to decide and collapse the general and finite version of the satisfiability and entailment problems for previously unsettled fragments of first-order logic. We take advantage of the Herbrand property also to establish novel and tight complexity results for the aforementioned decision questions. In particular, we show that the finite containment problem for quantified conjunctive queries is NPTIME-complete, tightening along two dimensions the known 3EXPTIME upper bound for the general version of the problem (Chen, Madelaine, and Martin, LICS'08). We finally present an alternative view on this result by generalizing to such queries the classic characterization of conjunctive query containment via polynomial-time verifiable homomorphisms (Chandra and Merlin, STOC'77).

Temporal logics are a well-investigated formalism for the specification, verification and synthesis of reactive systems. Within this family, Alternating-Time Temporal Logic (A tl *) has been introduced as a useful generalization of classical linear and branching-time temporal logics, by allowing temporal operators to be indexed by coalitions of agents. Classically, temporal logics are memoryless: once a path in the computation tree is quantified at a given node, the computation that has led to that node is forgotten. Recently, mC tl * has been defined as a memoryful variant of C tl *, where path quantification is memoryful. In the context of multi-agent planning, memoryful quantification enables agents to ‘relent’ and change their goals and strategies depending on the histories of evolutions. In this article, we introduce Relentful A tl *(RA tl *), a kind of temporally memoryful extension of A tl *, in which a formula is satisfied at a certain node of a play by taking into account both its future and past. We study the expressive power of RA tl *, its succinctness, as well as related decision problems. We investigate the relationship between memoryful quantifications and past modalities and prove their equivalence. We also show that both the relentful and the past extensions come without any computational price; indeed, we prove that both the satisfiability and the model-checking problems are 2E xp T ime-complete , as for A tl *.

Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.

In game theory, a classic qualitative question is to check whether a designated set of players has a winning strategy. In several safety-critical applications, however, it is important to ensure that some redundant strategies also exist, to be possibly used in case of some fault. In this paper, we introduce Graded Strategy Logic (GSL), an extension of Strategy Logic (SL) with graded quantifiers. SL is a powerful formalism that allows to describe useful game concepts in multi-agent settings by explicitly quantifying over strategies treated as first-order citizens. In GSL, by means of the existential construct 〈〈x ≥ g〉〉φ one can enforce that there exist at least g strategies satisfying φ. Dually, via the universal construct [[x <; g]]φ one can ensure that all but less than g strategies satisfy φ. As different strategies may induce the same outcome, although looking different, they need to be counted as one. While this interpretation is natural, it heavily complicates the definition and thus the reasoning about GSL. In order to accomplish this specific way of counting, we formally introduce a suitable equivalence relation over profiles based on the strategic behavior they induce. To give evidence of GSL usability, we investigate basic questions of one of its vanilla fragment, namely GSL[1G]. In particular, we report on positive results about the determinacy of games and the related model-checking problem, which we show to be PTIME-COMPLETE.

Parity games are infinite-duration two-player turn-based games that provide powerful formal-method techniques for the automatic synthesis and verification of distributed and reactive systems. This kind of game emerges as a natural evaluation technique for the solution of the μ-calculus model-checking problem and is closely related to alternating ω-automata. Due to these strict connections, parity games are a well-established environment to describe liveness properties such as “every request that occurs infinitely often is eventually responded”. Unfortunately, the classical form of such a condition suffers from the strong drawback that there is no bound on the effective time that separates a request from its response, i.e., responses are not promptly provided. Recently, to overcome this limitation, several variants of parity game have been proposed, in which quantitative requirements are added to the classic qualitative ones. In this paper, we make a general study of the concept of promptness in parity games that allows to put under a unique theoretical framework several of the cited variants along with new ones. Also, we describe simple polynomial reductions from all these conditions to either Büchi or parity games, which simplify all previous known procedures. In particular, they allow to lower the complexity class of cost and bounded-cost parity games recently introduced. Indeed, we provide solution algorithms showing that determining the winner of these games is in UPTIME ∩ COUPTIME.

Many decision problems in formal verification and design can be suitably formulated in game-theoretic terms. This is the case for the model checking of open and closed systems and both controller and reactive synthesis. Interpreted in this context, these problems require one to find a strategy (i.e., a plan) to force the system to fulfill some desired goal, no matter what the opponent (e.g., the environment) does. A strategy essentially constrains the possible behaviors of the system to those that are compatible with the decisions dictated by the plan itself. Therefore, finding a strategy to meet some goal basically reduces to identifying a portion of the model of interest (i.e., one of its substructures) that satisfies that goal. In this view, the ability to reason about substructures becomes a crucial aspect for several fundamental problems. In this article, we present and study a new branching-time temporal logic, called Substructure Temporal Logic (STL * for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. The logic is obtained by adding four new temporal-like operators to CTL *, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL * turns out to be very expressive and allows one to capture in a very natural way many well-known problems, such as module checking, reactive synthesis, and reasoning about games in a wide sense. A formal account of the model-theoretic properties of the new logic and results about (un)decidability and complexity of related decision problems are also provided.

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multiagent games, such as Atl, Atl*, and the like. Recently, Chatterjee, Henzinger, and Piterman introducedStrategy Logic, which we denote here by CHP-Sl, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-Slis obtained by using first-order quantifications over strategies and has been investigated in the very specific setting of two-agents turned-based games, where a nonelementary model-checking algorithm has been provided. While CHP-Slis a very expressive logic, we claim that it does not fully capture the strategic aspects of multiagent systems. In this article, we introduce and study a more general strategy logic, denoted Sl, for reasoning about strategies in multiagent concurrent games. As a key aspect, strategies in Slare not intrinsically glued to a specific agent, but an explicit binding operator allows an agent to bind to a strategy variable. This allows agents to share strategies or reuse one previously adopted. We prove that Slstrictly includes CHP-Sl, while maintaining a decidable model-checking problem. In particular, the algorithm we propose is computationally not harder than the best one known for CHP-Sl. Moreover, we prove that such a problem for Slis NonElementary. This negative result has spurred us to investigate syntactic fragments of Sl, strictly subsuming Atl*, with the hope of obtaining an elementary model-checking problem. Among others, we introduce and study the sublogics Sl[ng], Sl[bg], and Sl[1g]. They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean combinations of goals, and, a single goal at a time. Intuitively, for a goal, we mean a sequence of bindings, one for each agent, followed by an Ltlformula. We prove that the model-checking problem for Sl[1g] is 2ExpTime-complete, thus not harder than the one for Atl*. In contrast, Sl[ng] turns out to be NonElementary-hard, strengthening the corresponding result for Sl. Regarding Sl[bg], we show that it includes CHP-Sland its model-checking is decidable with a 2ExpTimelower-bound. It is worth enlightening that to achieve the positive results about Sl[1g], we introduce a fundamental property of the semantics of this logic, calledbehavioral, which allows to strongly simplify the reasoning about strategies. Indeed, in a nonbehavioral logic such as Sl[bg] and the subsuming ones, to satisfy a formula, one has to take into account that a move of an agent, at a given moment of a play, may depend on the moves taken by any agent in another counterfactual play.

In formal verification and design, reasoning about substructures is a crucial aspect for several fundamental problems, whose solution often requires to select a portion of the model of interest on which to verify a specific property. In this paper, we present a new branching-time temporal logic, called Substructure Temporal Logic (STL*, for short), whose distinctive feature is to allow for quantifying over the possible substructure of a given structure. This logic is obtained by adding two new operators to CTL*, whose interpretation is given relative to the partial order induced by a suitable substructure relation. STL* turns out to be very expressive and allows to capture in a very natural way many well known problems, such as module checking, reactive synthesis and reasoning about games. A formal account of the model theoretic properties of the new logic and results about (un)decidability and complexity of related decision problems are also provided.

In the setting of multi-agent games, considerable effort has been devoted to the definition of modal logics for strategic reasoning. In this area, a recent contribution is given by the introduction of Strategy Logic (SL, for short) by Mogavero, Murano, and Vardi. This logic allows to reason explicitly about strategies as first order objects and express in a very natural and elegant way several solution concepts like Nash, resilient, and secure equilibria, dominant strategies, etc. The price that one has to pay for the high expressiveness of SL semantics is that agents strategies it admits may be not behavioral, i.e., a choice of an agent, at a given moment of a play, may depend on the choices another agent can make in another counterfactual play. As the latter moves are unpredictable, this kind of strategies cannot be synthesized in practice. In this paper, we investigate two syntactical fragments of SL, namely the conjunctive-goal and disjunctive-goal, called SL[CG] and SL[DG] for short, and prove that their semantics admit behavioral strategies only. These logics are obtained by forcing SL formulas to be only of the form of conjunctions or disjunctions of goals, which are temporal assertions associated with a binding of agents with strategies. As SL formulas with any Boolean combination of goals turn out to be non behavioral, we have that SL[CG] and SL[DG] represent the maximal fragments of SL describing agent behaviors that are synthesizable. As a consequence of the above results, the model-checking problem for both SL[CG] and SL[DG] is shown to be solvable in 2EXPTIME, as it is for the subsumed logic ATL*.

In modal logics, graded (world) modalities have been deeply investigated as a useful framework for generalizing standard existential and universal modalities in such a way that they can express statements about a given number of immediately accessible worlds. These modalities have been recently investigated with respect to the μCalculus, which have provided succinctness, without affecting the satisfiability of the extended logic, that is, it remains solvable in ExpTime. A natural question that arises is how logics that allow reasoning about paths could be affected by considering graded path modalities . In this article, we investigate this question in the case of the branching-time temporal logic CTL (GCTL, for short). We prove that, although GCTL is more expressive than CTL, the satisfiability problem for GCTL remains solvable in ExpTime, even in the case that the graded numbers are coded in binary. This result is obtained by exploiting an automata-theoretic approach, which involves a model of alternating automata with satellites. The satisfiability result turns out to be even more interesting as we show that GCTL is at least exponentially more succinct than graded μCalculus.

In modal logics, graded (world) modalities have been deeply investigated as a useful framework for generalizing standard existential and universal modalities in such a way that they can express statements about a given number of immediately accessible worlds. These modalities have been recently investigated with respect to the mu-calculus, which have provided succinctness, without affecting the satisfiability of the extended logic, i.e., it remains solvable in ExpTime. A natural question that arises is how logics that allow reasoning about paths could be affected by considering graded path modalities. In this paper, we investigate this question in the case of the branching-time temporal logic CTL (GCTL, for short). We prove that, although GCTL is more expressive than CTL, the satisfiability problem for GCTL remains solvable in ExpTime. This result is obtained by exploiting an automata-theoretic approach. In particular, we introduce the class of partitioning alternating Buumlchi tree automata and show that the emptiness problem for them is ExpTime-Complete. The satisfiability result turns even more interesting as we show that GCTL is exponentially more succinct than graded mu-calculus.