Patricia Bouyer

Orna Kupferman

Nicolas Markey

Bastien Maubert

Aniello Murano

Giuseppe Perelli

Reasoning about Quality and Fuzziness of Strategic Behaviors

Keywords: CCS Concepts:, Theory of computation → Logic and verification, Modal and temporal logics, Verification by model checking, Automata over infinite objects, Tree languages Synthesis, quantitative, fuzzy ACM Reference

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

Temporal logics

One of the significant developments in formal reasoning has been the use of temporal logics for the specification of on-going behaviors of reactive systems [START_REF] Clarke | Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic[END_REF][START_REF] Emerson | Sometimes" and "Not Never" Revisited: On Branching versus Linear Time Temporal Logic[END_REF][START_REF] Pnueli | The Temporal Semantics of Concurrent Programs[END_REF]. Traditional temporal Authors' addresses: Patricia Bouyer, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Gif-sur-Yvette, France; Orna Kupferman, Hebrew University, Jerusalem, Israel; Nicolas Markey, Irisa, CNRS & Inria & Université de Rennes, Rennes, France; Bastien Maubert, Università degli Studi di Napoli "Federico II", Naples, Italy; Aniello Murano, Università degli Studi di Napoli "Federico II", Naples, Italy; Giuseppe Perelli, Sapienza University of Rome, Rome, Italy. logics are interpreted over Kripke structures, modeling closed systems, and can quantify over the computations of the systems in a universal and existential manner. The need to reason about multiagent systems has led to the development of specification formalisms that enable the specification of on-going strategic behaviors in multi-agent systems [START_REF] Alur | Alternating-time Temporal Logic[END_REF][START_REF] Chatterjee | Strategy Logic[END_REF][START_REF] Mogavero | Reasoning About Strategies: On the Model-Checking Problem[END_REF]. These formalisms, most notably ATL, ATL ★ , and Strategy Logic (SL), include quantification over strategies of the different agents and of the computations they may force the system into, making it possible to specify concepts that have been traditionally studied in game theory, such as Nash equilibria.

The duration of games in classical game theory is finite and the outcome of the game depends on its final position [START_REF] Nisan | Algorithmic Mechanism Design[END_REF][START_REF] Nisan | Algorithmic Game Theory[END_REF]. In contrast, agents in multi-agent systems maintain an on-going interaction with each other [START_REF] Harel | On the development of reactive systems[END_REF], and reasoning about their behavior refers not to their final state (in fact, we consider non-terminating systems, with no final state) but rather to the language of infinite computations that they generate. The logics ATL ★ and SL both extend Linear-time Temporal Logic (LTL) [START_REF] Pnueli | The Temporal Semantics of Concurrent Programs[END_REF], and thus can express rich properties of on-going strategic behaviors. However, their semantics are Boolean: either a system satisfies a formula, or it fails to satisfy it. The Boolean nature of traditional temporal logic is a real obstacle in the context of strategic reasoning. Indeed, while many strategies may attain a desired objective, they may do so at different levels of quality or certainty. Consequently, designers would be willing to give up manual design and adopt automatic procedures only after being convinced that the latter generate systems of comparable quality and certainty. For this to happen, one should first extend the specification formalism to one that supports quantitative aspects of the systems and strategies. We propose such an extension in this work: we merge the most natural and expressive logic for strategic reasoning with a recent, very powerful quantitative extension of LTL, called LTL [F ].

The logic LTL[F ] is a fuzzy logic that augments LTL with quality operators [START_REF] Almagor | Formally Reasoning about Quality[END_REF]. The satisfaction value of an LTL[F ] formula is a real value in [0, 1], intended to measure the quality in which the computation satisfies the specification. For example, the set F may contain the min{𝑥, 𝑦}, max{𝑥, 𝑦}, and 1 -𝑥 functions, which are the standard quantitative analogues of the ∧, ∨, and ¬ operators, and are known in fuzzy logics as the Zadeh operators. The novelty of LTL [F ] is the ability to manipulate values by arbitrary functions. These can prioritize different scenarios or reduce the satisfaction value of computations that exhibit less desirable behaviors. For example, consider a "carrier" drone 𝑐 that tries to bring an artifact to a rescue point, while keeping it as far as possible from a "villain" adversarial drone 𝑣. They evolve in a three-dimensional unit cube, in which coordinates are triples ì 𝛾 = (𝛾 1 , 𝛾 2 , 𝛾 3 ) ∈ [0, 1] 3 . We use the triples of atomic propositions 𝑝 ì 𝛾 = (𝑝 𝛾 1 , 𝑝 𝛾 2 , 𝑝 𝛾 3 ) and 𝑞 ì 𝛾 = (𝑞 𝛾 1 , 𝑞 𝛾 2 , 𝑞 𝛾 3 ) to denote the coordinates of 𝑐 and 𝑣, respectively. Assume that F contains the function dist : [0, 1] 3 × [0, 1] 3 → [0, 1], which maps two points in the cube to the (normalized) distance between them, and let the (Boolean) atomic proposition "safe" characterize positions where the artifact has reached the rescue point. In this scenario, the quality of an execution, or path, can be formalized with the following LTL[F ] formula:

𝜓 rescue = dist(𝑝 ì 𝛾 , 𝑞 ì 𝛾 )
U safe where U is the classic "until" operator. Indeed, the satisfaction value of 𝜓 rescue is 0 on every path in which the artifact is never rescued, and otherwise it is the minimum distance between the carrier and the villain along the trajectory from the beginning until the rescue point is reached.

Our contributions

We introduce and study the logic SL[F ], which can be viewed both as an extension of LTL[F ] to the strategic setting and as an extension of SL to the quantitative setting. Thus, while both LTL[F ] and SL extend LTL, each in a different direction, SL[F ] merges both extensions. The result is a strong yet clean logic that enables the specification of quantitative strategic behaviors. Syntax-wise, SL[F ] lifts LTL [F ] to the strategic setting by introducing a strategy quantifier ⟨⟨𝑥⟩⟩, which returns the maximum satisfaction value of the formula in computations that are possible outcomes of the strategy 𝑥, and binding operator (𝑎, 𝑥), which assigns strategy 𝑥 to agent 𝑎. Then, SL[F ] also lifts SL to the quantitative setting by introducing quality operators as in LTL [F ]. The semantics of SL[F ] is defined with respect to weighted multi-agent systems, namely ones where atomic propositions have truth values in [0, 1], reflecting quality or certainty. In addition to introducing the logic, our main contribution is a model-checking procedure for SL [F ], which enables formal reasoning about both quality and fuzziness of strategic behaviors. In addition, the model-checking procedure can be used as a synthesis algorithm that produces witness strategies that maximize the value of the formula. As we shall elaborate below, the merging of the two extensions in one logic poses new technical challenges. In particular, the external quantifiers on the strategies makes it impossible to evaluate the formulas in a bottom-up manner.

1.2.1 Specifying strategies' quality. In the example from above, with the carrier drone trying to rescue an artifact and the villain drone trying to steal it, we can specify the quality of a strategy 𝑥 for the carrier as the minimal quality of the behaviors resulting from 𝑥 against any strategy 𝑦 of the villain. If the quality of a behavior is specified by formula 𝜓 rescue as above, then the quality of a strategy 𝑥 is 0 if the villain has a counter-strategy 𝑦 to steal the artifact (in which case it never reaches the rescue point); otherwise, it is the minimum distance between the carrier and the villain until the artifact is rescued over all possible counter-strategies 𝑦 of the villain. We are interested in maximizing the quality of carrier's strategies, which is formalized with the following formula (recall that 𝑐 and 𝑣 are agents corresponding to the carrier and the villain):

𝜑 rescue = ⟨⟨𝑥⟩⟩ [[𝑦]] (𝑐, 𝑥) (𝑣, 𝑦) A(dist(𝑝 ì 𝛾 , 𝑞 ì 𝛾 ) U safe) where [[𝑦]
] is the dual of ⟨⟨𝑦⟩⟩, which returns the minimum value of the subformula in its scope over all strategies 𝑦. Thus, given a strategy 𝑥, formula 𝜑 quality (𝑥) = [[𝑦]] (𝑐, 𝑥) (𝑣, 𝑦)A(dist(𝑝 ì 𝛾 , 𝑞 ì 𝛾 ) U safe) minimizes the quality over all possible strategies 𝑦 of the villain. It is therefore the minimal quality that strategy 𝑥 is guaranteed to enforce. In the end, formula 𝜑 rescue maximizes this value over all possible strategies 𝑥 of the carrier. Note that in this example, the formula 𝜑 quality (𝑥) does not simply specify the ability of the carrier to behave in some desired manner. Rather, it associates a satisfaction value in [0, 1] with strategy 𝑥. This suggests that SL[F ] can be used not only to specify strategic behaviors with quantitative objectives, but also for quantizing notions from game theory that are traditionally Boolean. For example. beyond specifying that a strategy profile is a Nash Equilibrium, we can specify how far it is from being such an equilibrium, namely how much an agent may gain by a deviation that witnesses the instability. As we explain later in Section 2.4, we can actually express concepts such as 𝜀-Nash Equilibria [START_REF] Nisan | Algorithmic Game Theory[END_REF].

1.2.2 Synthesizing optimal strategies. We consider the following generalisation of the classic model-checking problem: given a weighted concurrent game structure G, an SL[F ] formula 𝜑 and a predicate 𝑃 ⊆ [0, 1], does the satisfaction value of 𝜑 on G belong to 𝑃? To solve this problem, we employ an approach that recently proved handy in the study of a number of logics for strategic reasoning [START_REF] Berthon | Strategy logic with imperfect information[END_REF][START_REF] Fijalkow | Quantifying Bounds in Strategy Logic[END_REF][START_REF] Laroussinie | Augmenting ATL with strategy contexts[END_REF], and which consists in reducing the problem to the model checking of (some appropriate extension of) Quantified CTL ★ (the extension of CTL ★ with secondorder quantifiers on atomic propositions, QCTL ★ for short [START_REF] French | Decidability of quantifed propositional branching time logics[END_REF][START_REF] Kupferman | Augmenting branching temporal logics with existential quantification over atomic propositions[END_REF][START_REF] Kupferman | Open Systems in Reactive Environments: Control and Synthesis[END_REF][START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF][START_REF] Prasad | Theoretical Issues in the Design and Certification of Distributed Systems[END_REF]). This is, however, the first time this approach is used in a quantitative setting.

To do so, we first need to define a suitable quantitative extension of Quantified CTL ★ . We define QCTL ★ [F ] as the extension of CTL ★ [F ] [START_REF] Almagor | Formally Reasoning about Quality[END_REF] with quantifiers over atomic propositions where, similarly to strategy quantifiers in SL[F ], existential/universal quantifications on atomic propositions are seen as maximizations/minimizations over possible valuations of the quantified propositions on the models. We show that the ability to assign the quantified atomic propositions with arbitrary values in [0, 1] enables the specification of legal tiling of grids of unbounded dimensions, making the model-checking problem for QCTL ★ [F ] undecidable. For our purpose of SL[F ] model checking, however, where quantification over atomic propositions encodes quantification over strategies, we show that one can restrict attention to Booleanly-Quantified CTL ★ [F ] (BQCTL ★ [F ] for short), where the quantified atomic propositions are assigned Boolean values in {0, 1}. For BQCTL ★ [F ], we are able to solve the model-checking problem, providing a solution also to SL[F ] model checking. We also study additional properties of QCTL ★ [F ] and BQCTL ★ [F ], focusing on their Lipschitz continuity, namely the effect of perturbing the values of atomic propositions on the satisfaction value of formulas.

A general approach to CTL ★ model checking is to repeatedly evaluate the innermost state subformulas by viewing them as (existentially or universally quantified) LTL formulas, and replace them with fresh atomic propositions [START_REF] Emerson | Modalities for Model Checking: Branching Time Logic Strikes Back[END_REF]. This directly extends to CTL ★ [F ], using weighted fresh atomic propositions [START_REF] Almagor | Formally Reasoning about Quality[END_REF]. However this technique does not work for BQCTL ★ [F ]: indeed, the truth values of the innermost formulas depend on the values of the externally quantified atomic propositions. Therefore, we build upon both the automata-theoretic approach to CTL ★ model checking [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF] and the word-automata construction developed for LTL[F ] [START_REF] Almagor | Formally Reasoning about Quality[END_REF], extending the latter from infinite words to infinite trees. More precisely, given a BQCTL ★ [F ] formula 𝜑 and a predicate 𝑃 ⊆ [0, 1], we construct an alternating parity tree automaton that accepts exactly all the labeled trees 𝑡 such that the satisfaction value of 𝜑 on 𝑡 is in 𝑃. The translation, and hence the complexity of our model-checking algorithm, is non-elementary: we show that the problem is actually (𝑘 + 1)-Exptime-complete for formulas involving up to 𝑘 nested quantifications on atomic propositions; we show a similar complexity result for SL[F ], in terms of nesting of strategy quantifiers. Similarly to LTL[F ] [3], our complexity results hold as long as the quality operators in F can be computed in the complexity class considered. Otherwise, they are the computational bottleneck.

Finally we observe that, as is often the case for this sort of algorithms based on tree automata [START_REF] Vardi | Automata-Theoretic Techniques for Modal Logics of Programs[END_REF], whenever the answer to the model-checking problem is positive, we can synthesize (outermost existentially-quantified) witness strategies. More precisely, if a formula 𝜑 = ⟨⟨𝑥 1 ⟩⟩ . . . ⟨⟨𝑥 𝑛 ⟩⟩𝜓 starts with a sequence of existentially-quantified strategies, and it holds that the satisfaction value of 𝜑 in some weighted game G belongs to 𝑃 ⊆ [0, 1], then our algorithm can be used to synthesize strategies 𝑥 1 , . . . , 𝑥 𝑛 that maximize within 𝑃 the quality as specified by 𝜓 .

Related work

There have been long lines of works about games with quantitative objectives (in a broad sense), e.g. stochastic games [START_REF] Filar | Competitive Markov decision processes[END_REF][START_REF] Shapley | Stochastic games[END_REF], timed games [START_REF] Asarin | Controller Synthesis for Timed Automata[END_REF], or weighted games with various kinds of objectives (parity [START_REF] Emerson | Tree Automata, Mu-Calculus and Determinacy[END_REF], mean-payoff [START_REF] Ehrenfeucht | Positional strategies for mean payoff games[END_REF] or energy [START_REF] Bouyer | Infinite Runs in Weighted Timed Automata with Energy Constraints[END_REF][START_REF] Chakrabarti | Resource Interfaces[END_REF]). This does not limit to zero-sum games, but also includes the study of various solution concepts (see for instance [START_REF] Almagor | Synthesis of Controllable Nash Equilibria in Quantitative Objective Games[END_REF][START_REF] Brenguier | Admissibility in Quantitative Graph Games[END_REF][START_REF] Brihaye | On Equilibria in Quantitative Games with Reachability/ Safety Objectives[END_REF][START_REF] Bruyère | Secure Equilibria in Weighted Games[END_REF][START_REF] Ummels | Stochastic Multiplayer Games: Theory and Algorithms[END_REF]). Similarly, extensions of the classical temporal logics LTL and CTL with quantitative semantics have been studied in different contexts, with discounting [START_REF] Almagor | Discounting in LTL[END_REF][START_REF] Luca De Alfaro | Model checking discounted temporal properties[END_REF], averaging [START_REF] Bollig | Frequency Linear-time Temporal Logic[END_REF][START_REF] Bouyer | Averaging in LTL[END_REF], or richer constructs [START_REF] Almagor | Formally Reasoning about Quality[END_REF][START_REF] Boker | Temporal Specifications with Accumulative Values[END_REF]. In contrast, the study of quantitative temporal logics for strategic reasoning has remained rather limited: works on LTL[F ] include algorithms for synthesis and rational synthesis [START_REF] Almagor | Formally Reasoning about Quality[END_REF][START_REF] Almagor | High-Quality Synthesis Against Stochastic Environments[END_REF][START_REF] Almagor | Synthesis of Controllable Nash Equilibria in Quantitative Objective Games[END_REF][START_REF] Almagor | High-Quality Synthesis Against Stochastic Environments[END_REF], but no logics combine the quantitative aspect of LTL[F ] with the strategic reasoning offered by SL and, to the best of our knowledge, our model-checking algorithm for SL[F ] is the first decidability result for a quantitative extension of a strategic specification formalism (unless restricting to bounded-memory strategies).

Baier and others have focused on a variant of SL in a stochastic setting [START_REF] Baier | Stochastic Game Logic[END_REF]; model checking was proven decidable for memoryless strategies, and undecidable in the general case. A quantitative version of SL with Boolean goals over one-counter games has been considered in [START_REF] Bouyer | Weighted Strategy Logic with Boolean Goals over Onecounter Games[END_REF]; only a periodicity property was proven, and no model-checking algorithm is known in that setting as well. Finally, Graded SL [START_REF] Aminof | Graded modalities in Strategy Logic[END_REF] extends SL by quantifying on the number of strategies witnessing a given strategy quantifier, and is decidable.

The other quantitative extensions we know of concern ATL /ATL ★ , and most of the results are actually adaptations of similar (decidability) results for the corresponding extensions of CTL and CTL ★ ; this includes probabilistic ATL [START_REF] Chen | Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm[END_REF], timed ATL [START_REF] Brihaye | Timed Concurrent Game Structures[END_REF][START_REF] Henzinger | Timed Alternating-Time Temporal Logic[END_REF], multi-valued ATL [START_REF] Jamroga | Multi-Valued Verification of Strategic Ability[END_REF], and weighted versions of ATL [START_REF] Bulling | How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)[END_REF][START_REF] Laroussinie | Model-Checking Timed ATL for Durational Concurrent Game Structures[END_REF][START_REF] Vester | On the Complexity of Model-checking Branching and Alternating-time Temporal Logics in Onecounter systems[END_REF]. Finally, some works have considered non-quantitative ATL with quantitative constraints on the set of allowed strategies [START_REF] Alechina | Resource-bounded alternating-time temporal logic[END_REF][START_REF] Della | Parity-energy ATL for Qualitative and Quantitative Reasoning in MAS[END_REF], proving decidability of the model-checking problem.

QUANTITATIVE STRATEGY LOGIC

Let Σ be an alphabet. A finite (resp. infinite) word over Σ is an element of Σ * (resp. Σ 𝜔 ). The length of a finite word 𝑤 = 𝑤 0 𝑤 1 . . . 𝑤 𝑛 is |𝑤 | := 𝑛 + 1, and last(𝑤) := 𝑤 𝑛 is its last letter. Given a finite (resp. infinite) word 𝑤 and 0 ≤ 𝑖 < |𝑤 | (resp. 𝑖 ∈ N), we let 𝑤 𝑖 be the letter at position 𝑖 in 𝑤, 𝑤 ≤𝑖 = 𝑤 0 . . . 𝑤 𝑖 is the (nonempty) prefix of 𝑤 that ends at position 𝑖 and 𝑤 ≥𝑖 = 𝑤 𝑖 𝑤 𝑖+1 . . . is the suffix of 𝑤 that starts at position 𝑖. As usual, for any partial function 𝑓 , we write dom(𝑓 ) for the domain of 𝑓 .

Strategy logic with functions, denoted SL[F ], generalizes both SL [START_REF] Chatterjee | Strategy Logic[END_REF][START_REF] Mogavero | Reasoning About Strategies: On the Model-Checking Problem[END_REF] and LTL[F ] [3] by replacing the Boolean operators of SL with arbitrary functions over [0, 1]. The logic is actually a family of logics, each parameterised by a set F of functions.

Syntax

We build on the branching-time variant of SL [START_REF] Fijalkow | Quantifying Bounds in Strategy Logic[END_REF], which does not add expressiveness with respect to the classic semantics [START_REF] Mogavero | Reasoning About Strategies: On the Model-Checking Problem[END_REF] but presents several benefits (see [START_REF] Fijalkow | Quantifying Bounds in Strategy Logic[END_REF] for more details), one of them being that it makes the connection with Quantified CTL tighter. Formulas of type 𝜑 are called state formulas, those of type 𝜓 are called path formulas. Formulas ⟨⟨𝑥⟩⟩𝜑 are called strategy quantifications whereas formulas (𝑎, 𝑥)𝜑 are called bindings. Modalities X and U are temporal modalities, which take a specific quantitative semantics as we see below.

We may use ⊤, ∨, and ¬ to denote functions 1, max and 1 -𝑥, respectively. We can then define the following classic abbreviations:

⊥:= ¬⊤, 𝜑 ∧ 𝜑 ′ := ¬(¬𝜑 ∨ ¬𝜑 ′ ), 𝜑 → 𝜑 ′ := ¬𝜑 ∨ 𝜑 ′ , F𝜓 := ⊤U𝜓 , G𝜓 := ¬F¬𝜓 , A𝜓 := ¬E¬𝜓 and [[𝑥]]𝜑 := ¬⟨⟨𝑥⟩⟩¬𝜑.
Intuitively, the value of formula 𝜑 ∨ 𝜑 ′ is the maximal value of the two formulas 𝜑 and 𝜑 ′ , 𝜑 ∧ 𝜑 ′ takes the minimal value of the two formulas, and the value of ¬𝜑 is one minus that of 𝜑. The implication 𝜑 → 𝜑 ′ thus takes the maximal value between that of 𝜑 ′ and one minus that of 𝜑.

In a Boolean setting, we assume that the values of the atomic propositions are in {0, 1} (0 represents false whereas 1 represents true), and so are the output values of functions in F . One can then check that 𝜑 ∨ 𝜑 ′ , 𝜑 ∧ 𝜑 ′ , ¬𝜑 and 𝜑 → 𝜑 ′ take their usual Boolean meaning.

We will come back later to temporal modalities, strategy quantifications and bindings.

Semantics

While SL is evaluated on classic concurrent game structures with Boolean valuations for atomic propositions, SL[F ] formulas are interpreted on weighted concurrent game structures, in which atomic propositions have values in [0, 1]. We first define classic concurrent game structures, and then extend them to the quantitative setting.

Definition 2.2. A concurrent game structure (CGS) is a tuple G = ⟨Agt, Act, V, v 𝜄 , Δ⟩
where Agt is a finite set of agents, Act is a finite set of actions, V is a finite set of states, v 𝜄 ∈ V is an initial state and Δ : V × Act Agt → V is the transition function.

An element of Act Agt is a joint action, and we let succ

(v) = {v ′ ∈ V | ∃ì 𝑐 ∈ Act Agt . v ′ = Δ(v, ì 𝑐)} for each v ∈ V.
For the sake of simplicity, we assume in the sequel that succ(v) ≠ ∅ for all v ∈ V.

A play in G is an infinite sequence 𝜋 = (v 𝑖 ) 𝑖 ∈N of states in V such that v 0 = v 𝜄 and v 𝑖 ∈ succ(v 𝑖 -1 ) for all 𝑖 > 0. We write Play G for the set of plays in G, and Play G (𝑣) for the set of plays in G starting from 𝑣. In this and all similar notations, we might omit to mention G when it is clear from the context. A (strict) prefix of a play 𝜋 is a finite sequence 𝜌 = (v 𝑖 ) 0≤𝑖 ≤𝐿 , for some 𝐿 ∈ N, which we denote 𝜋 ≤𝐿 . We write Prefx(𝜋) for the set of strict prefixes of play 𝜋. Such finite prefixes are called histories, and we let Hist G (v) = Prefx(Play G (v)) and Hist G = v∈V Hist G (v). We extend the notion of strict prefixes and the notation Prefx to histories in the natural way, requiring in particular that 𝜌 ∉ Prefx(𝜌). A (finite) extension of a history 𝜌 is any history 𝜌 ′ such that 𝜌 ∈ Prefx(𝜌 ′ ).

A strategy is a mapping 𝜎 : Hist G → Act, and we write Str G for the set of strategies in G. An assignment is a partial function 𝜒 : Var ∪ Agt ⇀ Str G , that assigns strategies to variables and agents. The assignment 𝜒 [𝑎 ↦ → 𝜎] maps 𝑎 to 𝜎 and is equal to 𝜒 otherwise. Let 𝜒 be an assignment and 𝜌 a history. We define the set of outcomes of 𝜒 from 𝜌 as the set Out(𝜒, 𝜌) of plays 𝜋 = 𝜌 • v 1 v 2 . . . such that for every 𝑖 ∈ N, there exists a joint action ì 𝑐 ∈ Act Agt such that for each agent 𝑎 ∈ dom( 𝜒), ì 𝑐 (𝑎) = 𝜒 (𝑎) (𝜋 ≤ |𝜌 |+𝑖 -1 ) and v 𝑖+1 = Δ(v 𝑖 , ì 𝑐), where v 0 = last(𝜌).

Definition 2.3. A weighted concurrent game structure (WCGS) is a tuple G = ⟨AP, Agt, Act, V, v 𝜄 , Δ, w⟩ where AP is a finite set of atomic propositions, ⟨Agt, Act, V, v 𝜄 , Δ⟩ is a CGS, and w : V → [0, 1] AP is a weight function.

In a WCGS, for each position v ∈ V and atomic proposition 𝑝 ∈ AP, the value w(v) (𝑝) indicates the degree to which 𝑝 holds in v. We now define the semantics of SL[F ]. Definition 2.4. Consider a WCGS G = ⟨AP, Agt, Act, V, v 𝜄 , Δ, w⟩, a set of variables Var, and a partial assignment 𝜒 of strategies for Agt and Var. Given an SL[F ] state formula 𝜑 and a history 𝜌, we use { {𝜑 } } G 𝜒 (𝜌) to denote the satisfaction value of 𝜑 in the last state of 𝜌 under the assignment 𝜒. Given an SL[F ] path formula 𝜓 , a play 𝜋, and a point in time 𝑖 ∈ N, we use { {𝜓 } } G 𝜒 (𝜋, 𝑖) to denote the satisfaction value of 𝜓 in the suffix of 𝜋 that starts in position 𝑖. The satisfaction value is defined inductively as follows:

{{𝑝}} G 𝜒 (𝜌) = w(last(𝜌)) (𝑝) {{⟨⟨𝑥⟩⟩𝜑 }} G 𝜒 (𝜌) = sup 𝜎 ∈Str G {{𝜑 }} G 𝜒 [𝑥↦ →𝜎 ] (𝜌) {{(𝑎, 𝑥)𝜑 }} G 𝜒 (𝜌) = {{𝜑 }} G 𝜒 [𝑎↦ →𝜒 (𝑥 ) ] (𝜌) {{E𝜓 }} G 𝜒 (𝜌) = sup 𝜋 ∈Out( 𝜒,𝜌 ) {{𝜓 } } G 𝜒 (𝜋, |𝜌 | -1) { {𝑓 (𝜑 1 , . . . , 𝜑 𝑚 )}} G 𝜒 (𝜌) = 𝑓 ({{𝜑 1 }} G 𝜒 (𝜌), . . . , { {𝜑 𝑚 } } G 𝜒 (𝜌)) {{𝜑 }} G 𝜒 (𝜋, 𝑖) = {{𝜑 }} G 𝜒 (𝜋 ≤𝑖 ) {{X𝜓 }} G 𝜒 (𝜋, 𝑖) = {{𝜓 }} G 𝜒 (𝜋, 𝑖 + 1) {{𝜓 1 U𝜓 2 }} G 𝜒 (𝜋, 𝑖) = sup 𝑗 ≥𝑖 min {{𝜑 2 } } G 𝜒 (𝜋, 𝑗), min 𝑘 ∈ [𝑖,𝑗 -1] { {𝜑 1 } } G 𝜒 (𝜋, 𝑘) { {𝑓 (𝜓 1 , . . . ,𝜓 𝑚 )}} G 𝜒 (𝜋, 𝑖) = 𝑓 ({{𝜓 1 }} G 𝜒 (𝜋, 𝑖), . . . , { {𝜓 𝑚 } } G 𝜒 (𝜋, 𝑖))
Strategy quantification ⟨⟨𝑥⟩⟩𝜑 computes the maximal value a choice of strategy for variable 𝑥 can give to formula 𝜑. Dually, [[𝑥]]𝜑 computes the minimal value a choice of strategy for variable 𝑥 can give to formula 𝜑. Binding (𝑎, 𝑥)𝜑 just assigns strategy given by 𝑥 to agent 𝑎. The branching quantifier E𝜓 computes the supremum value on all possible outcomes of the strategies currently assigned. Temporal modality X𝜓 takes the value of 𝜓 at the next step of a given outcome, while 𝜓 1 U𝜓 2 maximizes, over all positions along the play, the minimum between the value of 𝜓 2 at that position and the minimal value of 𝜓 1 before this position.

In a Boolean setting, we recover the standard semantics of SL. Also the fragment of SL[F ] with only temporal operators and functions ∨ and ¬ corresponds to Fuzzy Linear-time Temporal Logic [START_REF] Frigeri | Fuzzy time in linear temporal logic[END_REF][START_REF] Ben | Using fuzzy temporal logic for monitoring behavior-based mobile robots[END_REF]. Note that by equipping F with adequate functions, we can capture various classic fuzzy interpretations of Boolean operators, such as the Zadeh, Gödel-Dummett or Łukasiewicz interpretations (see for instance [START_REF] Frigeri | Fuzzy time in linear temporal logic[END_REF]). However the interpretation of the temporal operators is fixed in our logic.

Remark 1. As we shall see, once we fix a finite set of possible satisfaction values for the atomic propositions in a formula 𝜑, as is the case when a model is chosen, the set of possible satisfaction values for subformulas of 𝜑 becomes finite. Therefore, the suprema in the above definition are in fact maxima.

For a state formula 𝜑 and a weighted game structure G, we write { {𝜑 } } G for { {𝜑 } } G ∅ (v 𝜄 ).

Model checking

The problem we are interested in is the following generalisation of the model checking problem, which is solved in [START_REF] Almagor | Formally Reasoning about Quality[END_REF] for LTL[F ] and CTL ★ [F ].

Definition 2.5 (Model-checking problem). Given an SL[F ] state formula 𝜑, a WCGS G and a predicate 𝑃 ⊆ [0, 1], decide whether {{𝜑 }} G ∈ 𝑃.

In the sequel, we require that deciding whether a rational value 𝑣 is in 𝑃 can be done in time polynomial in the size of the representation of 𝑣 and 𝑃. As a typical example, if 𝑃 is a finite union of intervals with rational bounds (given explicitly), then membership in 𝑃 can be decided in linear time.

The precise complexity of the model-checking problem will be stated in terms of block nesting depth of formulas, which we introduce as a relaxation of the usual nesting depth. While the nesting depth of a formula is the maximal number of nested quantifiers it contains, the block nesting depth of a formula 𝜑, written bnd(𝜑), counts blocks of quantifiers of the same polarity as one. This notion is quite close to the usual alternation depth, except that for block nesting depth each different nested block of quantifiers counts as one, even if they have the same polarity.

What can SL[F ] express?

SL[F ] naturally embeds SL. Indeed, if the values of the atomic propositions are in {0, 1} and the only allowed functions in F are ∨, ∧, and ¬, then the satisfaction value of the formula is in {0, 1} and coincides with the value of the corresponding SL formula. Below we illustrate how quantities enable the specification of rich strategic properties.

Drone battle.

A "carrier" drone 𝑐 helped by a "guard" drone 𝑔 try to bring an artifact to a rescue point and keep it away from the "villain" adversarial drone 𝑣. They evolve in a threedimensional unit cube, in which coordinates are triples ì 𝛾 = (𝛾 1 , 𝛾 2 , 𝛾 3 ) ∈ [0, 1] 3 . We use the triples of atomic propositions 𝑝 ì 𝛾 = (𝑝 𝛾 1 , 𝑝 𝛾 2 , 𝑝 𝛾 3 ) and 𝑞 ì 𝛾 = (𝑞 𝛾 1 , 𝑞 𝛾 2 , 𝑞 𝛾 3 ) to denote the coordinates of 𝑐 and 𝑣, respectively. Write dist : [0, 1] 3 × [0, 1] 3 → [0, 1] for the (normalized) distance between two points in the cube. Let the (Boolean) atomic proposition "safe" denote that the artifact has reached the rescue point. In SL[F ], we can capture the level of safety for the artifact, defined as the minimum distance between the carrier and the villain along a trajectory to reach the rescue point. Indeed, the formula 𝜑 rescue = ⟨⟨𝑥⟩⟩⟨⟨𝑦⟩⟩(𝑐, 𝑥) (𝑔, 𝑦) A(dist(𝑝 ì 𝛾 , 𝑞 ì 𝛾 )U safe) states that the carrier and guard drones cooperate to keep the villain as far as possible from the artifact, until it is rescued. Note that the satisfaction value of the LTL[F ] specification is 0 along any path in which the artifact is never rescued.

Notice that formula 𝜑 rescue above can be expressed in the extension ATL ★ [F ] of ATL ★ with functions. ATL ★ is a syntactic fragment of SL in which strategy quantifications are constrained to be of the following form: The strategies of the carrier and the guard being quantified before that of the villain implies that they are unaware of the villain's future moves. Now assume the guard is a double agent to whom the villain communicates its plan. Then its strategy can depend on the villain's strategy, which is captured by the following formula:

⟨⟨𝑥 1 ⟩⟩ • • • ⟨⟨𝑥 𝑘 ⟩⟩ [[𝑥 𝑘+1 ]] • • • [[𝑥 𝑛 ]] (𝑎 𝜈 (1) , 𝑥
𝜑 spy = ⟨⟨𝑥⟩⟩ [[𝑧]] ⟨⟨𝑦⟩⟩(𝑐, 𝑥) (𝑔, 𝑦) (𝑣, 𝑧) A(dist(𝑝 ì 𝛾 , 𝑞 ì 𝛾 ) U safe) Note that this formula 𝜑 spy cannot be expressed in ATL ★ [F ],
that cannot capture alternation of strategy quantification because each strategic quantifier resets previously assigned strategies, while SL[F ] inherits from SL the possibility to freely alternate existential and universal quantifications on strategies in a first-order fashion. In fact 𝜑 spy actually belongs to the fragment SL 1𝐺 [F ], which we study in Section 6.

Synthesis with quantitative objectives.

The problem of synthesis for LTL specifications dates back to [START_REF] Pnueli | On the Synthesis of a Reactive Module[END_REF]. The setting is simple: two agents, a controller and an environment, operate on two disjoint sets of variables in the system. The controller wants a given LTL specification 𝜓 to be satisfied in the infinite execution, while the environment wants to prevent it. The problem consists in synthesizing a strategy for the controller such that, no matter the behavior of the environment, the resulting execution satisfies 𝜓 . Recently, this problem has been addressed in the context of LTL[F ], where the controller aims at maximizing the value of an LTL[F ] formula 𝜓 , while the environment acts as minimizer. Both problems can be easily represented in SL and SL[F ] respectively, with the formula 𝜑 synt = ⟨⟨𝑥⟩⟩ [[𝑦]] (𝑐, 𝑥) (𝑒, 𝑦) A𝜓 where 𝑐 and 𝑒 are the controller and environment agent, respectively, and 𝜓 the temporal specification expressed in either LTL or LTL [F ].

Assume now that controller and environment are both composed of more than one agent, namely 𝑐 1 , . . . , 𝑐 𝑛 and 𝑒 1 , . . . , 𝑒 𝑛 , and each controller component has the power to adjust its strategic choice based on the strategies selected by the environmental agents of lower rank. That is, the strategy selected by agent 𝑐 𝑘 depends on the strategies selected by agents 𝑒 𝑗 , for every 𝑗 < 𝑘. We can write an SL[F ] formula to represent this generalized synthesis problem as follows:

𝜑 synt = ⟨⟨𝑥 1 ⟩⟩ [[𝑦 1 ]] • • • ⟨⟨𝑥 𝑛 ⟩⟩ [[𝑦 𝑛 ]] (𝑐 1 , 𝑥 1 ) (𝑒 1 , 𝑦 1 ) . . . (𝑐 𝑛 , 𝑥 𝑛 ) (𝑒 𝑛 , 𝑦 𝑛 ) A𝜓 .
Notice that every controller agent is bound to an existentially quantified variable, that makes it try to maximize the satisfaction value of the formula in its scope. On the other hand, environmental agents are bound to universally quantified variables, which makes them try to minimize the satisfaction value.

In general in SL, each alternation between existential and universal quantification on strategies yields an additional exponential in the complexity of the model-checking problem. In Section 6 we show that, for the special case of formulas of the form 𝜑 synt , such alternation does not affect the computational complexity of the model-checking problem.

2.4.3 Nash equilibria in weighted games. An important feature of SL in terms of expressiveness is that it captures Nash equilibria (NEs, for short) and other common solution concepts. This extends to SL[F ], but in a much stronger sense: first, objectives in SL[F ] are quantitative, so that profitable deviation is not a simple Boolean statement; second, the semantics of the logic is quantitative, so that being a NE is a quantitative property, and we can actually express how far a strategy profile is from being a NE.

Assume that the objective of each agent 𝑎 𝑖 ∈ Agt is given as an LTL[F ] formula 𝜓 𝑖 . Define function ⪯ : [0, 1]2 → [0, 1] such that (using infix notation) 𝛼 ⪯ 𝛽 equals 1 if 𝛼 ≤ 𝛽, and equals 0 otherwise. We define the following formula, for a family (𝑥 𝑖 ) 𝑎 𝑖 ∈Agt of variables:

𝜑 NE ((𝑥 𝑖 ) 𝑎 𝑖 ∈Agt ) = (𝑎 1 , 𝑥 1 ) . . . (𝑎 𝑛 , 𝑥 𝑛 ) 𝑎 𝑖 ∈Agt [[𝑦 𝑖 ]] ((𝑎 𝑖 , 𝑦 𝑖 ) A𝜓 𝑖 ) ⪯ A𝜓 𝑖 If assignment 𝜒
𝜑 ′ NE ((𝑥 𝑖 ) 𝑎 𝑖 ∈Agt ) = (𝑎 1 , 𝑥 1 ) . . . (𝑎 𝑛 , 𝑥 𝑛 ) 𝑎 𝑖 ∈Agt (⟨⟨𝑦 𝑖 ⟩⟩ (𝑎 𝑖 , 𝑦 𝑖 ) A𝜓 𝑖 ) ⪯ A𝜓 𝑖 2.
4.4 𝜀-equilibria in weighted games. Adopting a more quantitative point of view, we can measure how much agent 𝑖 can benefit from a selfish deviation using formula ⟨⟨𝑦 𝑖 ⟩⟩diff ((𝑎 𝑖 , 𝑦 𝑖 )𝜓 𝑖 ,𝜓 𝑖 ), where diff (𝑥, 𝑦) = max{0, 𝑥 -𝑦} 2 . The maximal benefit that some agent may get is then captured by the following formula:

𝜑 NE ((𝑥 𝑖 ) 𝑎 𝑖 ∈Agt ) = ⟨⟨𝑦⟩⟩ (𝑎 1 , 𝑥 1 ) . . . (𝑎 𝑛 , 𝑥 𝑛 ) 𝑎 𝑖 ∈Agt diff ((𝑎 𝑖 , 𝑦)A𝜓 𝑖 , A𝜓 𝑖 ).
As previously, a strategy profile (𝜎 𝑖 ) 𝑎 𝑖 ∈Agt is a NE if, and only if, under the assignment 𝜒 that maps each 𝑥 𝑖 to 𝜎 𝑖 , formula 𝜑 NE evaluates to 0. Interestingly, formula 𝜑 NE can be used to characterise 𝜀-NE: a strategy profile in 𝜒 is an 𝜀-NE if, and only if, 𝜑 NE takes value less than or equal to 𝜀 under assignment 𝜒.

2.4.5 Secure equilibria in weighted games. Secure equilibria [START_REF] Chatterjee | Games with secure equilibria[END_REF] are special kinds of NEs in twoplayer games, where besides improving their objectives, the agents also try to harm their opponent. Following the ideas above, we characterise secure equilibria in SL[F ] as follows:

𝜑 SE (𝑥 1 , 𝑥 2 ) = (𝑎 1 , 𝑥 1 ) (𝑎 2 , 𝑥 2 ) 𝑖 ∈ {1,2} [[𝑦]] ((𝑎 𝑖 , 𝑦)A𝜓 1 , (𝑎 𝑖 , 𝑦)A𝜓 2 ) ⪯ 𝑖 (A𝜓 1 , A𝜓 2 )
where

(𝛼 1 , 𝛼 2 ) ⪯ 𝑖 (𝛽 1 , 𝛽 2 ) is 1 when (𝛼 𝑖 ≤ 𝛽 𝑖 ) ∨ (𝛼 𝑖 = 𝛽 𝑖 ∧ 𝛼 3-𝑖 ≤ 𝛽 3-𝑖 )
, and 0 otherwise. Secure equilibria have also been studied in Q-weighted games [START_REF] Bruyère | Secure Equilibria in Weighted Games[END_REF]: in that setting, the objective of the agents is to optimize e.g. the (limit) infimum or supremum of the sequence of weights encountered along the play. We can characterise secure equilibria in such setting (after first applying an affine transformation to have all weights in [0, 1]): indeed, assuming that weights are encoded as the value of atomic proposition 𝑤, the value of formula G𝑤 is the infimum of the weights, while the value of FG𝑤 is the limit infimum. We can then characterise secure equilibria with (limit) infimum and supremum objectives by using those formulas as the objectives for the agents in formula 𝜑 SE .

Other classical properties of games can be expressed, such as doomsday equilibria (which generalise winning secure equilibria in 𝑛-player games) [START_REF] Chatterjee | Doomsday Equilibria for Omega-Regular Games[END_REF], robust Nash equilibria (considering profitable deviations of coalitions of agents) [START_REF] Brenguier | Robust Equilibria in Mean-Payoff Games[END_REF], or strategy dominance and admissibility [START_REF] Berwanger | Admissibility in Infinite Games[END_REF][START_REF] Brenguier | Assume-admissible synthesis[END_REF], to cite a few.

2.4.6 Rational synthesis. Weak rational synthesis [START_REF] Almagor | Synthesis of Controllable Nash Equilibria in Quantitative Objective Games[END_REF][START_REF] Fisman | Rational synthesis[END_REF][START_REF] Kupferman | Synthesis with rational environments[END_REF] aims at synthesizing a strategy profile for a controller 𝑐 0 and the 𝑛 components (𝑐 𝑖 ) 1≤𝑖 ≤𝑛 constituting the environment, in such a way that (1) the whole system satisfies some objective 𝜓 0 , and (2) under the strategy of the controller, the strategies of the 𝑛 components form a Nash equilibrium (or any given solution concept) for their own individual objectives (𝜓 𝑖 ) 1≤𝑖 ≤𝑛 .

That a given strategy profile (𝑥 𝑖 ) 𝑐 𝑖 ∈Agt satisfies the two conditions above can be expressed as follows:

𝜑 wRS ((𝑥 𝑖 ) 0≤𝑖 ≤𝑛 ) = (𝑐 0 , 𝑥 0 ) (𝑐 1 , 𝑥 1 ) . . . (𝑐 𝑛 , 𝑥 𝑛 ) [A𝜓 0 ∧ 𝜑 NE ((𝑥 𝑖 ) 1≤𝑖 ≤𝑛 )]
The formula returns the minimum between the satisfaction value of 𝜓 0 and that of 𝜑 NE ((𝑥 𝑖 ) 1≤𝑖 ≤𝑛 ). Thus, the satisfaction value of 𝜑 wRS is zero if the strategy profile (𝑥 𝑖 ) 1≤𝑖 ≤𝑛 is not a NE under strategy 𝑥 0 assigned to 𝑐 0 , and it returns the satisfaction value of 𝜓 0 under the whole strategy profile otherwise. Then the value of

⟨⟨𝑥 0 ⟩⟩⟨⟨𝑥 1 ⟩⟩ . . . ⟨⟨𝑥 𝑛 ⟩⟩ 𝜑 wRS ((𝑥 𝑖 ) 0≤𝑖 ≤𝑛 )
is the best value that the system can collectively achieve for 𝜓 0 under the condition that the components in the environment follow an NE. Obviously, we can go beyond NE and use any other solution concept that can be expressed in SL [F ].

The counterpart of weak rational synthesis is strong rational synthesis, which aims at synthesizing a strategy only for controller 𝑐 0 in such a way that the objective 𝜓 0 is maximized over the worst NE that can be played by the environment component over the strategy of 𝑐 0 itself. This can be expressed as follows:

𝜑 sRS (𝑥 0 ) = [[𝑥 1 ]] . . . [[𝑥 𝑛 ]] (𝑐 0 , 𝑥 0 ) (𝑐 1 , 𝑥 1 ) . . . (𝑐 𝑛 , 𝑥 𝑛 ) A[¬𝜑 NE ((𝑥 𝑖 ) 1≤𝑖 ≤𝑛 ) ∨ 𝜓 0 ]
The disjunction in this formula returns the maximum value between ¬𝜑 NE ((𝑥 𝑖 ) 1≤𝑖 ≤𝑛 ) and 𝜓 0 : if (𝑥 𝑖 ) 1≤𝑖 ≤𝑛 is a NE, it returns the value of 𝜓 0 , and it returns 1 otherwise. The value of𝜑 sRS (𝑥 0 ) then is the smallest value that 𝜓 0 may take when players (𝑎 𝑖 ) 1≤𝑖 ≤𝑛 play according to a NE (if any). Finally, the value of

⟨⟨𝑥 0 ⟩⟩𝜑 sRS (𝑥 0 )
is the best value of 𝜓 0 that the controller can achieve under the condition that the components in the environment are playing the NE that worsens it (or it is 1 if the controller can enforce that no NEs exist).

2.4.7 Social-welfare reasoning. As shown in [START_REF] Almagor | Synthesis of Controllable Nash Equilibria in Quantitative Objective Games[END_REF], the objective formula 𝜓 0 above can be used to capture well-studied social-welfare functions [START_REF] Nisan | Algorithmic Game Theory[END_REF]. Typical examples of that are the utilitarian social-welfare function

𝜓 util 0 = 1 𝑛 𝑛 ∑ 𝑖=1 𝜓 𝑖
taking the average payoff of the agents, and the egalitarian social-welfare function

𝜓 egal 0 = min 𝑖=1,...,𝑛 {𝜓 𝑖 }
taking the minimum among the payoffs of the agents. Generally, utilitarian and egalitarian functions reflects the two ends of the political spectrum in terms of economic view. Therefore, a combination of the two functions can be used to represent what lies in the middle. Observe that SL[F ] can also evaluate such combinations of the two functions. For instance, a linear combination is represented as

𝜓 linear 0 = 𝜆 • 𝜓 util 0 + (1 -𝜆) • 𝜓 egal 0
where the parameter 𝜆 ranges between 0 and 1. As noted in [START_REF] Almagor | Synthesis of Controllable Nash Equilibria in Quantitative Objective Games[END_REF], when 𝜓 0 represents a social-welfare function, the weak and strong Rational-Synthesis problems amount to maximizing the welfare in the collaborative and non-collaborative scenarios, respectively. The expressiveness of SL[F ] allows us to move even further. For a given social-welfare function represented by a formula 𝜓 0 and a strategy 𝑥 0 for the controller, the formula OPT(𝑥 0 ) = ⟨⟨𝑥 1 ⟩⟩ . . . ⟨⟨𝑥 𝑛 ⟩⟩(𝑐 1 , 𝑥 1 ) . . . (𝑐 𝑛 , 𝑥 𝑛 )𝜓 0 denotes the parameterised social optimum, that is, the best value of the social-welfare function, when the strategy 𝑥 0 of the controller 𝑐 0 is fixed.

For a given game, the Price of Stability (PoS) is defined as the ratio between the (parameterised) social optimum and the best value of the social-welfare function over the strategy profiles that constitute a Nash Equilibrium. On the other hand, the Price of Anarchy (PoA) is the ratio between the social optimum and the worst value of the social welfare over all Nash Equilibria of the game. Observe that, since the social optimum is the best value achievable, both ratios are greater than 1 3 . Thus, the inverses of PoS and PoA are between 0 and 1 and can then be represented in SL[F ] as follows:

PoS -1 (𝑥 0 ) = ⟨⟨𝑥 1 ⟩⟩ . . . ⟨⟨𝑥 𝑛 ⟩⟩(𝜑 NE (𝑥 1 , . . . , 𝑥 𝑛 ) ∧ 𝜓 0 ) OPT(𝑥 0 ) PoA -1 (𝑥 0 ) = [[𝑥 1 ]] . . . [[𝑥 𝑛 ]] (¬𝜑 NE (𝑥 1 , . . . , 𝑥 𝑛 ) ∨ 𝜓 0 ) OPT(𝑥 0 )
Therefore, equivalently to minimizing such prices, the controller is interested in maximizing their inverses. We have the following

BestPoS = ⟨⟨𝑥 0 ⟩⟩𝑃𝑜𝑆 (𝑥 0 ) BestPoA = ⟨⟨𝑥 0 ⟩⟩𝑃𝑜𝐴(𝑥 0 ) 2.
𝜑 core (𝑥 𝑖 ) 𝑎 𝑖 ∈Agt = 𝐶 ⊆Agt [[𝑦 𝑖 ]] 𝑎 𝑖 ∈𝐶 ⟨⟨𝑦 𝑖 ⟩⟩ 𝑎 𝑗 ∈Agt\𝐶 𝑎 𝑗 ∈𝐶 (𝑎 𝑖 , 𝑦 𝑖 ) 𝑎 𝑖 ∈Agt 𝜓 𝑗 ⪯ (𝑎 𝑖 , 𝑥 𝑖 ) 𝑎 𝑖 ∈Agt 𝜓 𝑗
The strategy profile (𝑥 𝑖 ) 𝑎 𝑖 ∈Agt is a core equilibrium if, and only if, the formula 𝜑 core (𝑥 𝑖 ) 𝑎 𝑖 ∈Agt evaluates to 1. The existence of a core equilibrium could then be expressed with the formula ⟨⟨𝑥 1 ⟩⟩ . . . ⟨⟨𝑥 𝑛 ⟩⟩𝜑 core (𝑥 𝑖 ) 𝑎 𝑖 ∈Agt , which takes value 1 if, and only if, there exists a core equilibrium.

2.4.9 Accumulated payoffs. One class of problems that cannot be captured by SL[F ] are those involving payoffs that are accumulated along time, such as mean payoff or discounted payoff games [START_REF] Zwick | The complexity of mean payoff games on graphs[END_REF]. To capture them we would need a way to express sums of payoffs over infinitely many time steps. While we could assume that F contains necessary arithmetic operations such as sum and product, finitary formulas could only express sums over finitely many time steps. On the other hand, the semantics of the until operator involves payoffs in infinitely many time steps, but its semantics does not allow computing any kind of sum over these.

QUANTIFIED CTL ★ [F ]

In this section we introduce Quantified CTL ★ [F ] (QCTL ★ [F ], for short) which extends both CTL ★ [F ] and QCTL ★ [START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF]. On the one hand, it extends CTL ★ [F ] with second order quantification over atomic propositions, on the other hand it extends QCTL ★ to the quantitative setting of CTL ★ [F ]. In the setting with quantitative atomic propositions, the natural semantics for propositional quantification is to range over the whole interval [0, 1]; however, it is also meaningful to have propositional quantification restricted to {0, 1}. This leads to two logics, QCTL ★ [F ] and BQCTL ★ [F ] respectively, that have different properties. In Section 4, we show that the modelchecking problem for BQCTL ★ [F ] is decidable. Then, in Section 5, we show that Boolean quantification is sufficient in order to capture quantification on strategies, and so we obtain the decidability of SL[F ] model checking by a reduction to BQCTL ★ [F ]. In order, however, to capture extensions of SL[F ] with quantitative strategies such as probabilistic strategies (see [START_REF] Aminof | Probabilistic strategy logic[END_REF] for a probabilistic extension of SL), one needs the full power of QCTL ★ [F ]. In Section 7.2, we show that the model-checking problem for QCTL ★ [F ] is undecidable when considering the tree semantics, which corresponds to strategies with perfect recall (see Section 3.3). where 𝑝 ranges over AP and 𝑓 over F . Formulas of type 𝜑 are called state formulas, those of type 𝜓 are called path formulas, and QCTL ★ [F ] consists of all the state formulas defined by the grammar. An atomic proposition which is not under the scope of a quantification is called free. If no atomic proposition is free in a formula 𝜑, then we say that 𝜑 is closed. We again use ⊤, ∨, and ¬ to denote functions 1, max and 1 -𝑥, as well as classic abbreviations already introduced for SL[F ].

Syntax

Let F ⊆ {𝑓 : [0, 1] 𝑚 → [0, 1] | 𝑚 ∈ N}

Semantics

QCTL ★ [F ] formulas are evaluated on unfoldings of weighted Kripke structures. Definition 3.2. A weighted Kripke structure (WKS) is a tuple K = ⟨AP, S, s 𝜄 , 𝑅, w⟩ where AP is a finite set of atomic propositions, S is a finite set of states, s 𝜄 ∈ S is an initial state, 𝑅 ⊆ S × S is a left-total 4 transition relation, and w : S → [0, 1] AP is a weight function.

A path in K is an infinite word 𝜋 = 𝜋 0 𝜋 1 . . . over 𝑆 such that 𝜋 0 = s 𝜄 and (𝜋 𝑖 , 𝜋 𝑖+1 ) ∈ 𝑅 for all 𝑖. By analogy with concurrent game structures we call finite prefixes of paths histories, and write Hist K for the set of all histories in K. We also let Val K = {w(s) (𝑝) | s ∈ S and 𝑝 ∈ AP} be the finite set of values appearing in K.

Given finite nonempty sets 𝐷 of directions, AP of atomic propositions, and V ⊆ [0, 1] of possible values, a V AP -labeled 𝐷-tree, (or (V AP , 𝐷)-tree for short, or V AP -tree when directions are understood), is a pair 𝑡 = (𝜏, w) where 𝜏 ⊆ 𝐷 + is closed under non-empty prefixes, all nodes 𝑢 ∈ 𝜏 start with the same direction 𝑟 , called the root, and have at least one child 𝑢 • 𝑑 ∈ 𝜏, and w : 𝜏 → V AP is a weight function. We let Val 𝑡 ⊆ V be the image of w on 𝜏. A branch 𝜆 = 𝑢 0 𝑢 1 . . . is an infinite sequence of nodes such that for all 𝑖 ≥ 0, 𝑢 𝑖+1 is a child of 𝑢 𝑖 . We let Br(𝑢) be the set of branches that start in node 𝑢.

A tree 𝑡 = (𝜏, w) is complete if for all node 𝑢 ∈ 𝜏 and direction 𝑑 ∈ 𝐷, we have 𝑢 • 𝑑 ∈ 𝜏. Given a V AP -labeled 𝐷-tree 𝑡 = (𝜏, w), we let 𝑡 = (𝜏, w) be the only complete V AP ∪ {•}-labeled 𝐷-tree such that for all 𝑢 ∈ 𝜏, w(𝑢) = w(𝑢), and for all 𝑢 ∈ 𝜏 \ 𝜏, w(𝑢) = {•}, where • is a fresh symbol that labels artificial nodes added to make the tree complete. The reason for this definition is that it is more convenient to define tree automata on complete trees. A pointed tree is a pair (𝑡, 𝑢) where 𝑢 is a node in 𝑡. We say that a tree 𝑡 = (𝜏, w) is Boolean in 𝑝 if for all 𝑢 ∈ 𝜏 we have w(𝑢) (𝑝) ∈ {0, 1}. As with weighted Kripke structures, we let Val 𝑡 = {w(𝑢) (𝑝) | 𝑢 ∈ 𝜏 and 𝑝 ∈ AP}.

Let 𝑝 ∈ AP. A 𝑝-labeling for a (V AP , 𝐷)-tree 𝑡 = (𝜏, w) is a mapping

ℓ 𝑝 : 𝜏 → [0, 1]. Letting V ′ = ℓ 𝑝 (𝜏), the composition of 𝑡 with ℓ 𝑝 is the ((V ∪ V ′ ) AP ,𝐷)-tree defined as 𝑡 ⊗ ℓ 𝑝 := (𝜏, w ′ ), where w ′ (𝑢) (𝑝) = ℓ 𝑝 (𝑢) and w ′ (𝑢) (𝑞) = w(𝑢) (𝑞) for 𝑞 ≠ 𝑝. If ℓ 𝑝 (𝜏) ⊆ {0, 1}, we call ℓ 𝑝 a Boolean 𝑝-labeling.
Finally, the tree unfolding of a weighted Kripke structure K over atomic propositions AP and states S is the Val AP K -labeled S-tree 𝑡 K = (Hist K , w ′ ), where w ′ (𝑢) = w(last(𝑢)) for every 𝑢 ∈ Hist K .

Definition 3.3 (Semantics). Consider finite sets 𝐷 of directions, AP of atomic propositions, and V ⊆ [0, 1] of possible values. We fix a V AP -labeled 𝐷-tree 𝑡 = (𝜏, w). Given a QCTL ★ [F ] state formula 𝜑 and a node 𝑢 of 𝑡, we use {{𝜑 }} 𝑡 (𝑢) to denote the satisfaction value of 𝜑 in node 𝑢. Given a QCTL ★ [F ] path formula 𝜓 and a branch 𝜆 of 𝜏, we use { {𝜓 } } 𝑡 (𝜆) to denote the satisfaction value of 𝜓 along 𝜆. The satisfaction value is defined inductively as follows:

{{𝑝}} 𝑡 (𝑢) = w(𝑢) (𝑝) {{∃𝑝. 𝜑 }} 𝑡 (𝑢) = sup ℓ 𝑝 : 𝜏→[0,1] {{𝜑 } } 𝑡 ⊗ℓ 𝑝 (𝑢) {{E𝜓 }} 𝑡 (𝑢) = sup 𝜆∈Br(𝑢 ) {{𝜓 }} 𝑡 (𝜆) { {𝑓 (𝜑 1 , . . . , 𝜑 𝑛 )}} 𝑡 (𝑢) = 𝑓 ({{𝜑 1 }} 𝑡 (𝑢), . . . , { {𝜑 𝑛 } } 𝑡 (𝑢)) {{𝜑 }} 𝑡 (𝜆) = {{𝜑 }} 𝑡 (𝜆 0 ) where 𝜆 0 is the first node of 𝜆 {{X𝜓 }} 𝑡 (𝜆) = {{𝜓 }} 𝑡 (𝜆 ≥1 ) {{𝜓 1 U𝜓 2 }} 𝑡 (𝜆) = sup 𝑖 ≥0 min({{𝜓 2 } } 𝑡 (𝜆 ≥𝑖 ), min 0≤ 𝑗 <𝑖 { {𝜓 1 } } 𝑡 (𝜆 ≥ 𝑗 )) { {𝑓 (𝜓 1 , . . . ,𝜓 𝑛 )}} 𝑡 (𝜆) = 𝑓 ({{𝜓 1 }} 𝑡 (𝜆), . . . , { {𝜓 𝑛 } } 𝑡 (𝜆))
BQCTL ★ has the same syntax as QCTL ★ . Its semantics, which we write { {.} } 𝑡 B (.), only differs with {{.}} 𝑡 (.) in the case of quantification on propositions, which is defined as follows: For a tree 𝑡 with root 𝑟 we write {{𝜑 }} 𝑡 for {{𝜑 }} 𝑡 (𝑟 ), for a weighted Kripke structure K we write {{𝜑 }} K for { {𝜑 } } 𝑡 K , and similarly for {{𝜑 }} 𝑡 B and {{𝜑 }} K B . We will also consider the logic QLTL[F ] and its fragment LTL[F ], which we define now. Definition 3.4. The syntax of QLTL[F ] is defined with respect to a finite set AP of atomic propositions, using the following grammar:

{{∃𝑝. 𝜑 }} 𝑡 B (𝑢) = sup ℓ 𝑝 : 𝜏→{0,1} { {𝜑 } } 𝑡 ⊗ℓ 𝑝 B (
𝜓 ::= 𝑝 | X𝜓 | 𝜓 U𝜓 | ∃𝑝. 𝜑 | 𝑓 (𝜓, . . . ,𝜓 )
where 𝑝 ranges over AP and 𝑓 over F .

The semantics of a QLTL[F ] formula is defined on an infinite sequence of weight assignments for atoms in AP: given a path 𝜋 ∈ ( [0, 1] AP ) 𝜔 , the satisfaction value of a QLTL formula 𝜓 over 𝜋 is defined as expected and written {{𝜓 }} (𝜋). We write 𝜓 ≡ 𝜓 ′ if { {𝜓 } } (𝜋) = { {𝜓 ′ } } (𝜋) for all 𝜋 ∈ ( [0, 1] AP ) 𝜔 , and we define the satisfaction value { {𝜓 } } (K) of a QLTL[F ] formula 𝜓 on a Kripke structure K as the infimum of its satisfaction value over all paths of K.

The logic LTL[F ] is the fragment of QLTL[F ] obtained by removing quantification on atomic propositions.

Discussion of the semantics

Several semantics for QCTL ★ exist, among which the structure semantics, in which valuations for quantified atomic propositions are chosen on the states of the Kripke structure, and the tree semantics, where the Kripke structure is first unfolded in an infinite tree and valuations are chosen independently on each node. The former allows reasoning about memoryless strategies, which only depend on the current position, while the latter can be used to reason about perfect recall strategies that depend on the entire history (see [START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF] for more detail). Since in this work we consider prefect-recall strategies, we based the semantics of QCTL ★ [F ] (and thus BQCTL ★ [F ]) on the tree semantics for QCTL ★ .

Actually, if F = {⊤, ∨, ¬}, then BQCTL ★ [F ] evaluated on Boolean Kripke structures corresponds precisely to QCTL ★ with tree semantics [START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF].

Note that even with quantification restricted to Boolean valuations, BQCTL ★ [F ] is still quantitative: instead of merely stating the existence of a satisfying Boolean 𝑝-labeling, ∃𝑝. 𝜑 maximizes the satisfaction value of 𝜑 over all possible Boolean 𝑝-labelings.

BQCTL ★ [F ] can be seen as a fragment of QCTL ★ [F ], if F contains a function to test whether atomic propositions have only Boolean values. More precisely, let Bool : [0, 1] → [0, 1] be the function that maps 𝑥 to 1 if 𝑥 ∈ {0, 1}, and to 0 otherwise. One can express Boolean second-order quantification using fuzzy second-order quantification and the Bool function as follows:

∃ B 𝑝.𝜑 := ∃𝑝.(AG Bool(𝑝) ∧ 𝜑)
We then have that for all 𝜑 ∈ QCTL ★ [F ] such that 𝜑 does not contain a propositional quantifier, for all (V AP , 𝐷)-tree 𝑡 and node 𝑢 ∈ 𝑡, {{∃ B 𝑝.𝜑 }} 𝑡 (𝑢) = { {∃𝑝.𝜑 } } 𝑡 B (𝑢). It follows that: Lemma 3.5. For every BQCTL ★ formula 𝜑, letting 𝜑 B be the QCTL ★ formula obtained from 𝜑 by replacing inductively each ∃𝑝.𝜑 ′ in 𝜑 with ∃ B 𝑝.𝜑 ′ B , we have that for all (V AP , 𝐷)-tree 𝑡 and node

𝑢 ∈ 𝑡, {{𝜑 }} 𝑡 B (𝑢) = {{𝜑 B } } 𝑡 (𝑢) Therefore BQCTL ★ [F ] ⊆ QCTL ★ [F ∪ {Bool}],
in the sense that every formula in BQCTL ★ [F ] has an equivalent in QCTL ★ [F ∪ {Bool}]. We now announce our main results on the modelchecking problem for these logics. Together, they imply that the latter inequality is strict, in the sense that there is no computable translation from QCTL ★ [F ] to BQCTL ★ [F ]. Similarly to SL[F ], the precise complexity of the model-checking problem will be stated in terms of block nesting depth of formulas, which counts the maximal number of nested blocks of propositional quantifiers of same polarity in a formula 𝜑, and is written bnd(𝜑).

We show that when quantification on propositions is restricted to Boolean values, then model checking is decidable for arbitrary quality operators (Theorem 3.7), but allowing quantification over arbitrary values leads to undecidability already for a very small set of simple quality operators (Theorem 3.8). The restriction to Boolean values allows us to establish a finiteness result about the possible satisfaction values of a formula (Lemma 4.3), which is central in our automata construction to solve the model-checking problem. In fact, restricting quantification to any fixed finite set of values would be enough to obtain the finiteness result, and thus Theorem 3.7 could be generalized to that case. The proof that we present in the next section can be extended easily, only by generalizing slightly the projection operation on tree automata (see Proposition 4.1) and adapting Lemma 4.

MODEL CHECKING BQCTL ★ [F ]

In this section we first set up usual definitions for automata on infinite trees. We then prove a technical lemma on the finiteness of possible satisfaction values for BQCTL ★ [F ], which is crucial in the automata construction that we then present to solve the model-checking problem.

Alternating parity tree automata

We recall alternating parity tree automata. We start with basic definitions for two-player turn-based parity games, or simply parity games, that we use to define the semantics of automata.

Parity games. A parity game is a structure 𝐺 = (𝑉 , 𝐸, v 𝜄 , 𝐶), where the set of states 𝑉 = 𝑉 𝐸 ⊎ 𝑉 𝐴 is partitioned between states of Eve (𝑉 𝐸 ) and those of Adam (𝑉 𝐴 ), 𝐸 ⊆ 𝑉 × 𝑉 is a set of moves, v 𝜄 is an initial state and 𝐶 : 𝑉 → N is a coloring function of finite codomain. In states 𝑉 𝐸 , Eve chooses the next state, while Adam chooses in states 𝑉 𝐴 . A play is an infinite sequence of states v 0 v 1 v 2 . . . such that v 0 = v 𝜄 and for all 𝑖 ≥ 0, (v 𝑖 , v 𝑖+1 ) ∈ 𝐸 (written v 𝑖 → v 𝑖+1 ). We assume that for every v ∈ 𝑉 there exists v ′ ∈ 𝑉 such that v → v ′ . A strategy for Eve is a partial function 𝑉 * ⇀ 𝑉 that maps each finite prefix of a play ending in a state v ∈ 𝑉 𝐸 to a next state v ′ such that v → v ′ . A play v 0 v 1 v 2 . . . follows a strategy 𝜎 of Eve if for every 𝑖 ≥ 0 such that v 𝑖 ∈ 𝑉 𝐸 , v 𝑖+1 = 𝜎 (v 0 . . . v 𝑖 ). A strategy 𝜎 is winning if every play that follows it satisfies the parity condition, i.e., the least color seen infinitely often along the play is even.

Parity tree automata. For a set 𝑍 , B + (𝑍 ) is the set of formulas built from the elements of 𝑍 as atomic propositions using the connectives ∨ and ∧, and with ⊤, ⊥∈ B + (𝑍 ). For convenience, we only define automata on complete trees.

Fix a set V ⊆ [0, 1]. An alternating parity tree automaton (APT) on (V AP , 𝐷)-trees is a tuple A = (𝑄, 𝛿, 𝑞 𝜄 , 𝐶) where 𝑄 is a finite set of states, 𝑞 𝜄 ∈ 𝑄 is an initial state, 𝛿 : 𝑄 × V AP → B + (𝐷 ×𝑄) is a transition function, and 𝐶 : 𝑄 → N is a coloring function. A nondeterministic (resp. universal) parity tree automaton (NPT, resp. UPT) is an APT A = (𝑄, 𝛿, 𝑞 𝜄 , 𝐶) such that for every 𝑞 ∈ 𝑄 and 𝑎 ∈ V AP , 𝛿 (𝑞, 𝑎) is written in disjunctive (resp. conjunctive) normal form and for every direction 𝑠 ∈ 𝐷 each disjunct (resp. conjunct) contains exactly one element of {𝑠} × 𝑄. 5 We may use N and U to denote, respectively, nondeterministic and universal automata. An NPT is deterministic if for each 𝑞 ∈ 𝑄 and 𝑎 ∈ 2 AP , 𝛿 (𝑞, 𝑎) consists of a single disjunct.

Acceptance of a pointed (V AP , 𝐷)-tree (𝑡, 𝑢 𝜄 ), where 𝑡 = (𝜏, w), by an APT A = (𝑄, 𝛿, 𝑞 𝜄 , 𝐶) is defined via the parity game 𝐺 (A, 𝑡, 𝑢 𝜄 ) = (𝑉 , 𝐸, v 𝜄 , 𝐶 ′ ) where 𝑉 = 𝜏 × 𝑄 × B + (𝐷 × 𝑄), state (𝑢, 𝑞, 𝛼) belongs to Eve if 𝛼 is of the form 𝛼 1 ∨ 𝛼 2 or [𝑠, 𝑞 ′ ], and to Adam otherwise, v 𝜄 = (𝑢 𝜄 , 𝑞 𝜄 , 𝛿 (𝑞 𝜄 , 𝑢 𝜄 )), and 𝐶 ′ (𝑢, 𝑞, 𝛼) = 𝐶 (𝑞). Moves in 𝐺 (A, 𝑡, 𝑢 𝜄 ) are defined by the following rules:

(𝑢, 𝑞, 𝛼 1 † 𝛼 2 ) → (𝑢, 𝑞, 𝛼 𝑖 ) where † ∈ {∨, ∧} and 𝑖 ∈ {1, 2}, (𝑢, 𝑞, [𝑠, 𝑞 ′ ]) → (𝑢 • 𝑠, 𝑞 ′ , 𝛿 (𝑞 ′ , w(𝑢 • 𝑠)))
States of the form (𝑢, 𝑞, ⊤) and (𝑢, 𝑞, ⊥) are sinks, winning for Eve and Adam respectively. A pointed tree (𝑡, 𝑢) is accepted by A if Eve has a winning strategy in 𝐺 (A, 𝑡, 𝑢), and the language of A is the set of pointed trees accepted by A, written L (A). We write 𝑡 ∈ L (A) if (𝑡, 𝑟 ) ∈ L (A), where 𝑟 is the root of 𝑡. We also write L for the complement of a language L.

The size |A| of an APT A is its number of states plus the sum of the sizes of all formulas appearing in the transition function. We also call index of an APT the number of priorities in its parity condition. Given two APT A and A ′ we denote A ∧ A ′ (resp. A ∨ A ′ ) the APT of size linear in |A| and |A ′ | that accepts the intersection (resp. union) of the languages of A and A ′ .

Word automata. We also consider word automata that we run on branches of trees. We assimilate infinite words with infinite trees over the singleton set of directions {next}. A parity word automaton is a parity tree automaton on (V AP , {next})-trees. In the case of a nondeterministic parity word automaton, transitions are represented as a mapping Δ : 𝑄 × V AP → 2 𝑄 which, in a state 𝑞 ∈ 𝑄, reading the label 𝑎 ∈ V AP of the current state in the word, indicates a set of states Δ(𝑞, 𝑎) from which Eve can choose to send in the next position of the word.

Operations on automata

We recall the following operations on automata.

Projections. The first two constructions are existential and universal projection. The classic projection of a nondeterministic tree automaton over an atomic proposition 𝑝, introduced by Rabin to deal with second-order monadic quantification [START_REF] Michael O Rabin | Decidability of second-order theories and automata on infinite trees[END_REF], consists in letting the nondeterministic tree automaton guess in each node a valuation for 𝑝. We obtain an automaton that accepts an input tree if and only if there exists a 𝑝-labeling for that tree that makes it accepted by the original automaton. Similarly, one can easily define universal projection of universal tree automata.

In our setting, we have the following: Proposition 4.1. Given an NPT N on V AP -labeled trees and an atomic proposition 𝑝 ∈ AP, one can build in linear time an NPT N ⇓ ∃ 𝑝 such that (𝑡, 𝑢) ∈ L (N ⇓ ∃ 𝑝 ) iff there exists a Boolean 𝑝-labeling ℓ 𝑝 for 𝑡 s.t. (𝑡 ⊗ ℓ 𝑝 , 𝑢) ∈ L (N ). Given a UPT N on V AP -labeled trees and an atomic proposition 𝑝 ∈ AP, one can build in linear time a UPT U ⇓ ∀ 𝑝 such that (𝑡, 𝑢) ∈ L (U ⇓ ∀ 𝑝 ) iff for all Boolean 𝑝-labelings ℓ 𝑝 for 𝑡, (𝑡 ⊗ ℓ 𝑝 , 𝑢) ∈ L (U).

Simulation. Before performing projections, we will need to turn alternating automata into nondeterministic or universal ones, via the classic simulation theorem.

Theorem 4.2 (Simulation [START_REF] Muller | Simulating Alternating Tree Automata by Nondeterministic Automata: New Results and New Proofs of the Theorems of Rabin, McNaughton and Safra[END_REF]). Given an APT A, one can build in exponential time an NPT N and a UPT U, both of exponential size and linear index, such that L (N ) = L (U) = L (A).

Remark 2. Note that the simulation theorem in [START_REF] Muller | Simulating Alternating Tree Automata by Nondeterministic Automata: New Results and New Proofs of the Theorems of Rabin, McNaughton and Safra[END_REF] is only stated for nondeterministic automata. However we can obtain easily the result for universal ones as follows: first, notice that universal automata are dual to nondeterministic automata, and that we can turn an NPT into a UPT of linear size that accepts the complement language of the original NPT. Now to build a UPT accepting the same language as an APT A, one first builds in linear time an APT A ′ that accepts L (A). Then, by the simulation theorem, one can build an NPT N of exponential size equivalent to A ′ . Finally one builds the linear-size UPT U accepting L (N ) = L (A).

Finiteness of possible satisfaction values

As in the case of LTL[F ] we show that since the set of possible satisfaction values of an atomic proposition is finite, so is the set of possible satisfaction values of each BQCTL ★ [F ] formula. This property allows using max instead of sup in Definition 3.3. The set of possible satisfaction values does not depend on the set of directions 𝐷, which we thus omit in the following lemma. Proof. We prove the result by mutual induction on 𝜑 and 𝜓 . Clearly, Val 𝑝 = V. For 𝜑 = ∃𝑝. 𝜑 ′ : let 𝑡 be a V AP -labeled tree and 𝑢 ∈ 𝑡. Since Val 𝑡 ⊆ V and by assumption V contains 0 and 1, for all Boolean 𝑝-valuation ℓ 𝑝 for 𝑡, Val 𝑡 ⊗ℓ 𝑝 ⊆ V. It follows by definition of Val 𝜑 ′ ,V that for all such ℓ 𝑝 we have {{𝜑 ′ }} 𝑡 ⊗ℓ 𝑝 (𝑢) ∈ Val 𝜑 ′ ,V . Therefore { {∃𝑝. 𝜑 ′ } } 𝑡 (𝑢) is the supremum of a subset of Val 𝜑 ′ ,V , which by induction hypothesis is of size at most |V | |𝜑 ′ | . It follows that the supremum is indeed a maximum, and that {{∃𝑝.

𝜑 ′ }} 𝑡 (𝑢) ∈ Val 𝜑 ′ ,V . Hence, Val ∃𝑝. 𝜑 ′ ,V ⊆ Val 𝜑 ′ ,V , and thus |Val ∃𝑝. 𝜑 ′ ,V | ≤ |Val 𝜑 ′ ,V | ≤ |V | |𝜑 ′ | ≤ |V | | ∃𝑝. 𝜑 ′ | .
For 𝜑 = E𝜓 , again {{E𝜓 }} 𝑡 (𝑢) is a supremum over a subset of Val 𝜓,V , which by induction hypothesis is of size at most For 𝜓 = 𝜑, the result follows by hypothesis of mutual induction.

V |𝜓 | . The supremum is thus reached, hence Val E𝜓,V ⊆ Val 𝜓,V and |Val E𝜓,V | ≤ |Val 𝜓,V | ≤ |V | |𝜓 | ≤ |V | |E𝜓 | . For 𝜑 = 𝑓 (𝜑 1 , . . . , 𝜑 𝑛 ), we have Val 𝜑,V = {𝑓 (𝑣 1 , . . . , 𝑣 𝑛 ) | 𝑣 𝑖 ∈ Val 𝜑 𝑖 ,V }, hence |Val 𝜑,V | is at most 𝑛 𝑖=1 |Val 𝜑 𝑖 ,V |.
For 𝜓 = X𝜓 ′ , we have that Val 𝜓,V = Val 𝜓 ′ ,V , and the result follows.

For 𝜓 = 𝜓 1 U𝜓 2 , the value of 𝜓 is defined via suprema and infima over possible values for 𝜓 1 and 𝜓 2 , which are finitely many by the induction hypothesis. The suprema and infima are thus maxima and minima, and

Val 𝜓,V ⊆ Val 𝜓 1 ,V ∪ Val 𝜓 2 ,V . Hence |Val 𝜓,V | ≤ |Val 𝜓 1 ,V | + |Val 𝜓 2 ,V |, by induction hypothesis |Val 𝜓 1 ,V | + |Val 𝜓 2 ,V | ≤ |V | |𝜓 1 | + |V | |𝜓 2 | , since V contains at least 0 and 1, |V | ≥ 2 and thus |V | |𝜓 1 | + |V | |𝜓 2 | ≤ |V | |𝜓 1 |+|𝜓 2 | , which is no greater than |V | |𝜓 | .
In all cases, the claim for over-approximations follows by the same reasoning as above. □

The finite over-approximation of the set of possible satisfaction values induces a finite alphabet for the automata used in our model-checking procedure, which we now describe.

Model-checking procedure

We extend the automata-based model-checking procedure for CTL ★ from [START_REF] Kupferman | An Automata-Theoretic Approach to Branching-Time Model Checking[END_REF]. Note that since the quantified atomic propositions may appear in different subformulas, we cannot extend the algorithm for CTL ★ [F ] from [START_REF] Almagor | Formally Reasoning about Quality[END_REF], as the latter applies the technique of [START_REF] Emerson | Modalities for Model Checking: Branching Time Logic Strikes Back[END_REF], where the evaluation of each subformula is independent. Proof. The proof proceeds by an induction on the structure of the formula 𝜑 and strengthens the induction statement as follows: one can construct an APT A V,𝑃 𝜑 such that for every V AP -labeled 𝐷-tree 𝑡, for every node 𝑢 ∈ 𝑡, we have that A V,𝑃 𝜑 accepts 𝑡 from node 𝑢 if and only if { {𝜑 } } 𝑡 (𝑢) ∈ 𝑃 (recall that 𝑡 is the complete tree obtained from 𝑡 by adding dummy nodes labeled with •).

If 𝜑 = 𝑝, the automaton has one state and accepts a tree 𝑡 = (𝜏, w) in node 𝑢 ∈ 𝜏 if w(𝑢) (𝑝) ∈ 𝑃, and rejects otherwise.

If 𝜑 = ∃𝑝. 𝜑 ′ , we want to check whether the maximal satisfaction value of 𝜑 ′ , over all possible 𝑝-labelings of the input tree, is in 𝑃. To do so we first compute a finite set Val 𝜑 ′ ,V of exponential size such that Val 𝜑 ′ ,V ⊆ Val 𝜑 ′ ,V , which we can do as established by Lemma 4.3. For each possible value 𝑣 ∈ Val 𝜑 ′ ,V ∩ 𝑃, we check whether this value is reached for some 𝑝-labeling, and if the value of 𝜑 ′ is less than or equal to 𝑣 for all 𝑝-labelings. For each 𝑣 ∈ Val 𝜑 ′ ,V ∩ 𝑃, inductively build the APTs A

V,{𝑣 } 𝜑 ′ and A V,[0,𝑣 ]∩𝑃 𝜑 ′
. Turn the first one into an NPT N =𝑣 and the second one into a UPT U ≤𝑣 (using Theorem 4.2). Project N =𝑣 existentially on 𝑝, and call the result N ′ =𝑣 . Project U ≤𝑣 universally on 𝑝, call the result U ′ ≤𝑣 . Finally, we can define the APT A V,𝑃 ∃𝑝.

𝜑 ′ := 𝑣 ∈ Val 𝜑 ′ ,V ∩𝑃 N ′ =𝑣 ∧ U ′ ≤𝑣 .
It is then easy to see that this automaton accepts a tree if and only if there exists a value in 𝑃 that is the maximum of the possible values taken by 𝜑 ′ for all 𝑝-labelings.

A block of existential quantifiers ∃𝑝 1 . . . ∃𝑝 𝑘 .𝜑 ′ can be treated similarly: compute Val 𝜑 ′ ,V , for each 𝑣 ∈ Val 𝜑 ′ ,V ∩ 𝑃 build the NPT N =𝑣 and the UPT U ≤𝑣 (incurring one exponential blowup), project N =𝑣 existentially on 𝑝 1 , . . . , 𝑝 𝑘 and project U ≤𝑣 universally on 𝑝 1 , . . . , 𝑝 𝑘 (these operations are polynomial), and combine the resulting automata into the final automaton.

If 𝜑 = E𝜓 : as in the classic automata construction for CTL ★ [START_REF] Kupferman | An automata-theoretic approach to branching-time model checking[END_REF], we first let atoms(𝜓 ) be the set of maximal state sub-formulas of 𝜓 (that we call atoms thereafter -which have to be distinguished from atomic propositions of the formula). In a first step we see elements of atoms(𝜓 ) as atomic propositions, and 𝜓 as an LTL[F ] formula over atoms(𝜓 ). According to Lemma 4.3 we can compute over-approximations Val 𝜑 ′ ,V for each 𝜑 ′ ∈ atoms(𝜓 ), and we thus let Val = 𝜑 ′ ∈atoms(𝜓 ) Val 𝜑 ′ ,V be a finite over-approximation of the set of possible values for atoms. It is proven in [ on all branches of its input. 6 We now define the APT A 𝑃 on Val atoms(𝜓 ) -trees as

A 𝑃 = 𝑣 ∈ Val E𝜓 ,V ∩𝑃 N 𝐸=𝑣 ∧ U 𝐴≤𝑣 .

Now to go from atoms to standard atomic propositions, we define an APT A V,𝑃

E𝜓 that simulates A 𝑃 by, in each state and each node of its input, guessing a value 𝑣 𝑖 in Val 𝜑 𝑖 for each formula 𝜑 𝑖 ∈ atoms(𝜓 ), simulating A 𝑃 on the resulting weight label, and launching a copy of A V,{𝑣 𝑖 } 𝜑 𝑖 for each 𝜑 𝑖 ∈ atoms(𝜓 ). Note that the automaton is alternating and thus may have to guess several times the satisfaction value of a formula 𝜑 𝑖 in a same node, but launching the A V,{𝑣 𝑖 } 𝜑 𝑖 forces it to always guess the same, correct value.

Finally, if 𝜑 = 𝑓 (𝜑 1 , ..., 𝜑 𝑛 ), we list all combinations (𝑣 1 , . . . , 𝑣 𝑛 ) of the possible satisfaction values for the subformulas 𝜑 𝑖 such that 𝑓 (𝑣 1 , . . . , 𝑣 𝑛 ) ∈ 𝑃, and we build automaton A V,𝑃 𝜑 as the disjunction over such (𝑣 1 , . . . , 𝑣 𝑛 ) of the conjunction of automata A V,{𝑣 𝑖 } 𝜑 𝑖 . The complexity of this procedure is non-elementary. More precisely, we claim that A V,𝑃 𝜑 has size at most (nd(𝜑) + 1)-exponential and index at most nd(𝜑)-exponential.

The case where 𝜑 is an atomic proposition is trivial.

For 𝜑 = ∃𝑝. 𝜑 ′ , we transform an exponential number of APTs into NPTs or UPTs. This entails an exponential blowup in the size of each automaton, while the index remains linear. By induction hypothesis, the resulting automaton A V,𝑃 ∃𝑝. 𝜑 ′ has at most (nd(𝜑 ′ ) + 2)-exponentially many states and index at most (nd(𝜑 ′ ) + 1)-exponential. Since nd(𝜑) = nd(𝜑 ′ ) + 1, the property holds.

If 𝜑 has the form 𝑓 (𝜑 1 , ..., 𝜑 𝑛 ), then the automaton for 𝜑 is a combination of the automata for all 𝜑 𝑖 , and for the various values those subformulas may take. By Lemma 4.3 there are at most

|V | |𝜑 1 |+...+|𝜑 𝑛 | ≤ |V | |𝜑 | different
combinations, so assuming (from the induction hypothesis) that 6 We take W 𝜓 [0,𝑣 ] universal because it is not possible to simulate a nondeterministic word automaton on all branches of a tree, but it is possible for a universal one. Note that we could also determinise W the automata for 𝜑 𝑖 have at most (nd(𝜑 𝑖 ) + 1)-exponentially many states and index at most nd(𝜑 𝑖 )exponential, the automaton for 𝜑 has at most (nd(𝜑) + 1)-exponentially many states and index at most nd(𝜑)-exponential (note that nd(𝜑 𝑖 ) = nd(𝜑)).

Finally for 𝜑 = E𝜓 : in [START_REF] Almagor | Formally Reasoning about Quality[END_REF], the automaton W 𝜓 𝑃 is a generalized Büchi automaton of size exponential in |𝜓 | 2 , and with at most |𝜓 | Büchi acceptance conditions. One can turn this automaton into an equivalent Büchi automaton still exponential in |𝜓 | 2 , which can be seen as a parity automaton with index 2. Then N 𝐸=𝑣 and U 𝐴≤𝑣 both also have sizes exponential in |𝜓 | 2 , and index 2. Finally, A 𝑃 , which combines an exponential number of the automata above, has size exponential in |𝜓 | 2 and index 2. The final automaton A V,𝑃 E𝜓 is obtained from that automaton by plugging the automata for A V,• 𝜑 𝑖 , whose sizes and indices are respectively (nd(𝜑 𝑖 ) + 1)-and nd(𝜑 𝑖 )-exponential, and dominate the size and index of A 𝑃 . Since nd(𝜑) = max 𝑖 nd(𝜑 𝑖 ), it follows that for 𝜑 = E𝜓 the size of A V,𝑃 𝜑 also is (nd(𝜑) + 1)-exponential, and its index is nd(𝜑)-exponential. □

To see that Theorem 3.8 follows from Proposition 4.4, recall that by definition { {𝜑 } } K = { {𝜑 } } 𝑡 K . Thus to check whether {{𝜑 }} K ∈ 𝑃, where atoms in K take values in V, it is enough to build A V,𝑃 𝜑 as in Proposition 4.4, take its product with a deterministic tree automaton that accepts only 𝑡 K , and check for emptiness of the product automaton. The formula complexity is (nd(𝜑) + 1)-exponential, but the structure complexity is polynomial.

For the lower bounds, consider the following fragment of QCTL ★ : EQ 𝑘 CTL ★ alt is the fragment containing all formulas of QCTL ★ that are in prenex normal form (i.e. with all quantifications on atomic propositions at the beginning), have at most 𝑘 alternations of propositional quantifiers, and start with an existential quantifier (see [60, page 8] for a formal definition); in EQ 𝑘 CTL ★ alt , quantifiers can be grouped together into at most 𝑘 blocks of quantifiers, each block containing only one type of quantifiers. The model-checking problem for EQ 𝑘 CTL ★ alt is proven to be (𝑘 + 1)-Exptime-hard in [START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF]. Now, assuming F contains disjunction max{𝑥, 𝑦} and negation 1 -𝑥, EQ 𝑘 CTL ★ alt can be translated in BQCTL ★ [F ] with formulas of linear size and block nesting depth at most 𝑘, which gives us the lower-bounds of Theorem 3.7.

MODEL CHECKING SL[F ]

In this section we show how to reduce the model-checking problem for SL [F ]

to that of QCTL ★ [F ].
This reduction is a rather straightforward adaptation of the usual one for qualitative variants of SL (see, e.g., [START_REF] Berthon | Strategy logic with imperfect information[END_REF][START_REF] Fijalkow | Quantifying Bounds in Strategy Logic[END_REF][START_REF] Laroussinie | Augmenting ATL with strategy contexts[END_REF]). We essentially observe that it can be lifted to the quantitative setting.

We let Agt be a finite set of agents, and AP be a finite set of atomic propositions. Models transformation. We first define for every WCGS G = ⟨AP, Agt, Act, V, v 𝜄 , Δ, w⟩ a WKS K G = ⟨S, s 𝜄 , 𝑅, w⟩ over some set AP ′ and a bijection 𝜌 ↦ → 𝑢 𝜌 between the set of histories starting in the initial state v 𝜄 of G and the set of nodes in 𝑡 K G . We consider propositions AP V = {𝑝 v | v ∈ V}, that we assume to be disjoint from AP. We let AP ′ = AP ∪ AP V . Define the Kripke structure K G = (S, s 𝜄 , 𝑅, w) where

• S = {s v | v ∈ V}, • s 𝜄 = s v 𝜄 , • 𝑅 = {(s v , s v ′ ) ∈ S 2 | ∃ì 𝑐 ∈ Act Agt s.t. Δ(v, ì 𝑐) = v ′ }, and
• w(𝑝) (s v ) =          1 if 𝑝 ∈ AP V and 𝑝 = 𝑝 v 0 if 𝑝 ∈ AP V and 𝑝 ≠ 𝑝 v w(𝑝) (v) otherwise .
For every history 𝜌 = v 0 . . . v 𝑘 , define the node 𝑢 𝜌 = s v 0 . . . s v 𝑘 in 𝑡 K G (which exists, by definition of K G and of tree unfoldings). Note that the mapping 𝜌 ↦ → 𝑢 𝜌 defines a bijection between the set of histories from v 𝜄 and the set of nodes in 𝑡 K G . Formulas translation. Given a game G = ⟨Act, V, v 𝜄 , Δ, w⟩ and a formula 𝜑 ∈ SL[F ], we define a QCTL ★ [F ] formula 𝜑 ′ such that {{𝜑 }} G = {{𝜑 ′ }} K G . More precisely, this translation is parameterised with a partial function 𝑔 : Agt ⇀ Var which records bindings of agents to strategy variables. Suppose that Act = {𝑐 1 , . . . , 𝑐 𝑚 }. We define the translation (•) 𝑔 by induction on state formulas 𝜑 and path formulas 𝜓 . Here is the definition of (•) 𝑔 for state formulas:

(𝑝) 𝑔 = 𝑝 ((𝑎, 𝑥)𝜑) 𝑔 = (𝜑) 𝑔[𝑎↦ →𝑥 ] (⟨⟨𝑥⟩⟩𝜑) 𝑔 = ∃𝑝 𝑥 𝑐 1 . . . ∃𝑝 𝑥 𝑐 𝑚 . 𝜑 str (𝑥) ∧ (𝜑) 𝑔 ,
where

𝜑 str (𝑥) = AG 𝑐 ∈Act (𝑝 𝑥 𝑐 ∧ 𝑐 ′ ≠𝑐 ¬𝑝 𝑥 𝑐 ′ ) (A𝜓 ) 𝑔 = A(𝜓 out (𝑔) → (𝜓 ) 𝑔 ) where 𝜓 out (𝑔) = G v∈V 𝑝 v → ì 𝑐 ∈Act Agt 𝑎∈dom(𝑓 ) 𝑝 𝑓 (𝑎) ì 𝑐 (𝑎) ∧ X𝑝 Δ(v,ì 𝑐 ) (𝑓 (𝜑 1 , . . . , 𝜑 𝑛 )) 𝑔 = 𝑓 ((𝜑 1 ) 𝑔 , . . . , (𝜑 𝑛 ) 𝑔 )
and for path formulas:

(𝜑) 𝑔 = (𝜑) 𝑔 (X𝜓 ) 𝑔 = X(𝜓 ) 𝑔 (𝜓 U𝜓 ′ ) 𝑔 = (𝜓 ) 𝑔 U(𝜓 ′ ) 𝑔 (𝑓 (𝜓 1 , . . . ,𝜓 𝑛 )) 𝑔 = 𝑓 ((𝜓 1 ) 𝑔 , . . . , (𝜓 𝑛 ) 𝑔 )
This translation is identical to that from branching-time SL to QCTL ★ in all cases, except for the case of functions which is straightforward. To see that it can be safely lifted to the quantitative setting, it suffices to observe the following: since quantification on atomic propositions is restricted in BQCTL ★ [F ] to Boolean values, and atoms in AP V also have Boolean values, 𝜑 str (𝑥) and 𝜓 out ( 𝜒) always have value 0 or 1 and thus they can play exactly the same role as in the qualitative setting: 𝜑 str (𝑥) holds if and only if the atomic propositions 𝑝 𝑥 𝑐 1 , . . . , 𝑝 𝑥 𝑐 𝑚 indeed code a strategy from the current state, and𝜓 out ( 𝜒) holds on a branch of 𝑡 K G if and only if in this branch each agent 𝑎 ∈ dom(𝑔) follows the strategies coded by atoms 𝑝 𝑥 𝑐 . As a result ∃𝑝 𝑥 𝑐 1 . . . ∃𝑝 𝑥 𝑐 𝑚 . 𝜑 str (𝑥) ∧ (𝜑) 𝑔 maximizes over those valuations for the 𝑝 𝑥 𝑐 𝑖 that code for strategies, other valuations yielding value 0. Similarly, formula A(𝜓 out (𝑔) → (𝜓 ) 𝑔 ) minimizes over branches that represent outcomes of strategies in 𝑔, as others yield value 1.

One can now see that the following holds, where 𝜑 is an SL[F ] formula.

Lemma 5.1. Let 𝜒 be an assignment and 𝑔 : Agt ⇀ Var such that dom(𝑔) = dom( 𝜒) ∩ Agt and for all 𝑎 ∈ dom(𝑔), 𝑔(𝑎) = 𝑥 implies 𝜒 (𝑎) = 𝜒 (𝑥). Then

{{𝜑 }} G 𝜒 (𝜌) = {{(𝜑) 𝑔 } } 𝑡 K G (𝑢 𝜌 )
As a result, the quantitative model-checking problem for an SL[F ] formula 𝜑, a weighted CGS G and a predicate 𝑃 ⊆ [0, 1] can be solved by computing the BQCTL ★ [F ] formula 𝜑 ′ = (𝜑) ∅ , which is of size polynomial in |𝜙, and the weighted Kripke structure K G , of size polynomial in |G|, and deciding whether {{𝜑 ′ }} K G ∈ 𝑃, which can be done by Theorem 3.8. To preserve block nesting depth, we observe that the above translation can be massaged so that each block of existential (resp. universal) strategy quantifiers results in a single block of existential (resp. universal) proposition quantifiers. We translate a block of existential strategy quantifiers as follows:

(⟨⟨𝑥 1 ⟩⟩ . . . ⟨⟨𝑥 𝑘 ⟩⟩𝜑) 𝑔 = ∃𝑝 𝑥 1 𝑐 1 . . . ∃𝑝 𝑥 1 𝑐 𝑚 . . . ∃𝑝 𝑥 𝑘 𝑐 1 . . . ∃𝑝 𝑥 𝑘 𝑐 𝑚 . 𝑘 𝑖=1 𝜑 str (𝑥 𝑖 ) ∧ (𝜑) 𝑔
This establishes the upper-bounds in Theorem 2.8. The reduction presented above is polynomial and preserves block nesting depth, so that we inherit the lower-bounds from BQCTL ★ [F ] established in Theorem 3.8.

Remark 3. Lemma 5.1 together with Lemma 4.3 imply that SL[F ] formulas also can take only exponentially many values when a finite domain is fixed for atomic propositions. This justifies the observation of Remark 1 that supremum and infimum in the semantics of SL[F ] can be replaced with maximum and minimum.

THE CASE OF SL 1𝐺 [F ]

We now study the fragment SL 1𝐺 [F ], which is the extension to the quantitative setting of the one-goal fragment SL 1𝐺 of SL [START_REF] Mogavero | What Makes ATL * Decidable? A Decidable Fragment of Strategy Logic[END_REF]. In the Boolean setting, SL 1𝐺 is of interest because it is strictly more expressive than ATL ★ but enjoys the same complexity. Indeed, both its model-checking and satisfiability are 2-Exptime-complete. In addition to ATL ★ it allows for arbitrary alternation of existential and universal strategy quantifications, and thus can express complex dependencies between strategies (see the last example in Section 2.4.1, which is similar to the Escape from Alcatraz example in [START_REF] Mogavero | What Makes ATL * Decidable? A Decidable Fragment of Strategy Logic[END_REF]). We show that in the quantitative setting, the one-goal fragment SL 1𝐺 [F ] also enjoys this better computational complexity.

In order to define the syntax, we need to introduce the notions of quantification prefix and binding prefix. A quantification prefix is a sequence

℘ = ⟨⟨𝑥 1 ]] . . . ⟨⟨𝑥 𝑛 ]], where ⟨⟨𝑥 𝑖 ]] ∈ {⟨⟨𝑥 𝑖 ⟩⟩, [[𝑥 𝑖 ]
]} is either an existential or universal quantification. For a fixed set of agents Agt = {𝑎 1 , . . . , 𝑎 𝑛 } a binding prefix is a sequence ♭ = (𝑎 1 , 𝑥 1 ), . . . (𝑎 𝑛 , 𝑥 𝑛 ), where every agent in Agt occurs exactly once. A combination ℘♭ is closed if every variable occurring in ♭ occurs in some quantifier of ℘. We can now give the definition of SL 1𝐺 [F ] syntax. Definition 6.1 (SL 1𝐺 [F ] Syntax). Let AP be a set of Boolean atomic propositions, and let F ⊆ {𝑓 : [0, 1] 𝑚 → [0, 1] | 𝑚 ∈ N} be a set of functions over [0, 1]. The set of SL 1𝐺 [F ] formulas is defined by the following grammar:

𝜑 := 𝑝 | 𝑓 (𝜑, . . . , 𝜑) | 𝜑 | X𝜑 | 𝜑U𝜑 | ℘♭𝜑,
where 𝑝 ∈ AP, 𝑓 ∈ F , and ℘♭ is a closed combination of a quantification prefix and of a binding prefix.

Note that all SL[F ] formulas are sentences, as all strategy variables are quantified immediately before being bound to some agent. The sentence nesting depth of an SL 1𝐺 [F ] formula is defined as follows:

• snd(𝑝) = 0 for every 𝑝 ∈ AP;

• snd(𝑓 (𝜑 1 , . . . , 𝜑 𝑛 )) = max 1≤𝑖 ≤𝑛 {snd(𝜑 𝑖 )}; • snd(X𝜓 ) = snd(𝜓 ); • snd(𝜓 1 U𝜓 2 ) = max{snd(𝜓 1 ), snd(𝜓 2 )}. • snd(℘♭𝜑) = snd(𝜑) + 1;
Intuitively, the sentence nesting depth measures the number of sentences, i.e., formulas with no free agent or variable, that are nested into each other in the formula.

In order to solve the model-checking problem for SL 1𝐺 [F ], we need the technical notion of concurrent multi-player parity game introduced in [START_REF] Vadim Malvone | Concurrent Multi-Player Parity Games[END_REF]. Definition 6.2. A concurrent multi-player parity game (CMPG) is a tuple P = ⟨Agt, Act, 𝑉 , v 𝜄 , Δ, p⟩, where Agt = 0, . . . , 𝑛 is a set of agents indexed with natural numbers, ⟨Agt, Act, 𝑉 , v 𝜄 , Δ⟩ is a CGS, and p : 𝑉 → N is a priority function.

In a CMPG, agents are split in two teams: each player 𝑖 with 𝑖 mod 2 = 0 is part of the existential (even) team, the other players are part of the universal (odd) team. The goal in a CMPG is to check whether there exists a strategy for 0 such that, for each strategy for 1, there exists a strategy for 2, and so forth, such that the induced plays satisfy the parity condition. Then, we say that the existential team wins the game. Otherwise the universal team wins the game.

As Proof. We let G = ⟨AP, Agt, Act, V, v 𝜄 , Δ, w⟩ be a WCGS and we consider a formula of the form ℘♭𝜑. We also assume, for simplicity, that ℘ = ⟨⟨𝑥 0 ⟩⟩ [[𝑥 1 ]], . . . , ⟨⟨𝑥 𝑘 ]], that is, quantifiers perfectly alternate between existential and universal. 7 Note that the formula ℘♭𝜑 is a sentence, therefore the choice of an assignment is useless. Moreover, recall that, by Lemma 5.1 and in particular Remark 3, the set 𝑉 (℘♭𝜑) of possible values is bounded by 2 |℘♭𝜑 | .

We proceed by induction on the sentence nesting depth. As base case let snd(℘♭𝜑) = 1, i.e., there is no occurrence of neither quantifiers nor bindings in 𝜑. Then, 𝜑 can be regarded as an LTL[F ] formula that can be interpreted over paths of the WKS K = ⟨AP, V, v 𝜄 , 𝑅, w⟩ where

𝑅 = {(v 1 , v 2 ) | ∃ì 𝑐 ∈ Act Agt . v 2 = Δ(v 1 , ì 𝑐)}
Now, thanks to [3, Theorem 2.9], for every value 𝑣 ∈ 𝑉 (℘♭𝜑), we can build a parity word automaton B K,𝜑,𝑃 𝑣 of size exponential in |𝜑 | 2 such that B K,𝜑,𝑃 𝑣 accepts a word 𝑤 ∈ ( Val atoms(𝜓 ) ) 𝜔 if, and

only if, { {𝜓 } }(𝑤) ∈ 𝑃 𝑣 = [𝑣, 1]
. Following [START_REF] Piterman | From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata[END_REF], we can convert B K,𝜑,𝑃 𝑣 into a deterministic parity word automaton A K,𝜑,𝑃 𝑣 = ⟨V, 𝑄, 𝑞 𝜄 , 𝛿, p⟩ of size doubly-exponential in the size of 𝜑 and index bounded by 2 |𝜑 | . At this point, define the following CMPG P = ⟨Agt ′ , Act, 𝑉 ′ , v ′ 𝜄 , Δ ′ , p ′ ⟩ such that • Agt ′ = {0, . . . , 𝑘 } is a set of agents, one for every variable occurring in ℘, ordered in the same way as in ℘ itself; • Act is the set of actions in G;

• 𝑉 ′ = V × 𝑄 is the product of the states of G and the automaton A K,𝜑,𝑃 𝑣 ;

• v ′ 𝜄 = (v 𝜄 , 𝑞 𝜄 )
is the pair given by the initial states of G and A K,𝜑,𝑡 , respectively;

• p ′ (v, 𝑞) = p(𝑞) mimics the parity function of A K,𝜑,𝑃 𝑣 ; • if ì 𝑐 ∈ Act Agt ′ , Δ ′ ((v, 𝑞), ì 𝑐) = (Δ(v, ♭(ì 𝑐)), 𝛿 (𝑞, w(v))
) mimics the execution of both G and A K,𝜑,𝑃 𝑣 .

The game emulates two things, one per each component of its state-space. In the first, it emulates a path 𝜋 generated in G. In the second, it emulates the execution of the automaton A K,𝜑,𝑃 𝑣 when it reads the path 𝜋 generated in the first component. By construction, it results that every execution (𝜋, 𝜂) ∈ V 𝜔 × 𝑄 𝜔 in P satisfies the parity condition determined by p ′ if, and only if, { {𝜑 } } K (𝜋) ∈ 𝑃 𝑣 . Moreover, observe that, since A K,𝜑,𝑃 𝑣 is deterministic, for every possible history 𝜌 in G, there is a unique partial run 𝜂 𝜌 that makes the partial execution (𝜌, 𝜂 𝜌 ) possible in P. This makes the sets of possible strategies Str G (v 𝜄 ) and Str P (v ′ 𝜄 ) in bijection. P has a winning strategy if and only if {{℘♭𝜑 } } G (v 𝜄 ) ∈ 𝑃 𝑣 . In order to compute the exact value of { {℘♭𝜑 } } G (v 𝜄 ), we repeat the procedure described above for every 𝑣 ∈ 𝑉 (℘♭𝜑) and take the maximum 𝑣 of those for which { {℘♭𝜑 } } G (v 𝜄 ) ∈ 𝑃 𝑣 . For the induction case, assume we can compute the satisfaction value of every SL 1𝐺 [F ] formula with sentence nesting depth at most 𝑛, and let snd(℘♭𝜑) = 𝑛 +1. Observe that, for every subsentence ℘ ′ ♭ ′ 𝜑 ′ of ℘♭𝜑, we have that snd(℘ ′ ♭ ′ 𝜑 ′ ) ≤ 𝑛 and so, by induction hypothesis, we can compute {{℘ ′ ♭ ′ 𝜑 ′ } } G (v) for every v ∈ V. Now, introduce a fresh atomic proposition 𝑝 (℘ ′ ♭ ′ 𝜑 ′ ) whose weight in G is defined as w(𝑣) (𝑝 (℘ ′ ♭ ′ 𝜑 ′ ) ) = {{℘ ′ ♭ ′ 𝜑 ′ }} G (𝑣) and a set of fresh atomic propositions 𝑝 v , one for every v ∈ V, whose weights in G are defined as w(v)

(𝑝 v ) = 1 and w(v) (𝑝 v ′ ) = 0 if v ≠ v ′ . Now, consider the Boolean formula Φ(℘ ′ ♭ ′ 𝜑 ′ ) = v∈V (𝑝 v ∧ 𝑝 (℘ ′ ♭ ′ 𝜑 ′ ) )
Observe that every disjunct is a conjunction of the form 𝑝 v ∧ 𝑝 (℘ ′ ♭ ′ 𝜑 ′ ) , whose satisfaction value on a state v ′ is the minimum among the weights of 𝑝 v and 𝑝 (℘ ′ ♭ ′ 𝜑 ′ ) . This can be either 0

, if v ≠ v ′ or {{℘ ′ ♭ ′ 𝜑 ′ } } G (v), if v = v ′ .
Now, the big disjunction takes the maximum among them. Therefore, we obtain that { {Φ(℘ ′ ♭ ′ 𝜑 ′ )}} G (v) = {{℘ ′ ♭ ′ 𝜑 ′ }} G (v). This allows us to replace every occurrence of ℘ ′ ♭ ′ 𝜑 ′ in 𝜑 with the Boolean combination Φ(℘ ′ ♭ ′ 𝜑 ′ ), making the resulting formula to be of sentence nesting depth 1. Thus, we can apply the procedure described in the base case, to compute {{℘♭𝜑 } } G (v).

Regarding the complexity, note that the size of P is |V| • |𝑄 | that is in turn linear with respect to the size of G and doubly exponential in the size of 𝜑. This is due to the fact that the automaton A K,𝜑,𝑃 𝑣 results from the construction of the NGBW B K,𝜑,𝑃 𝑣 , of size singly exponential in |𝜑 | and the transformation to a DPW, that adds up another exponential to the construction. On the other hand, the number of priorities in P is only singly exponential in |𝜑 |, and it is due to the fact that the transformation from NGBW to DPW requires a singly exponential number of priorities. Therefore, the CMPG P can be solved in time polynomial w.r.t. the size G and double exponential in |𝜑 |. Such a 2-Exptime procedure is executed a number of time exponential in 𝜑, which is still doubly exponential.

Hardness follows from that of SL 1𝐺 [START_REF] Mogavero | What Makes ATL * Decidable? A Decidable Fragment of Strategy Logic[END_REF]. □

ON QCTL ★ [F ] AND MSO[F ]

In this section we first study the expressiveness of QCTL ★ [F ]. It is shown in [START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF] that QCTL ★ is equivalent to MSO on trees. We extend this result by augmenting MSO with quality operators and showing that the resulting logic corresponds to QCTL ★ [F ] when second-order quantification is over fuzzy sets (in which case the logic is called MSO[F ]). If second-order quantification is over classic sets instead, then the logic (called BMSO[F ]) corresponds to BQCTL ★ [F ]. We then prove that, unlike BQCTL ★ [F ], the model-checking problem for QCTL ★ [F ] is undecidable even when F contains only two simple functions, namely (𝑥, 𝑦) ↦ → 𝑥 = 𝑦 and (𝑥, 𝑦) ↦ → 𝑦 = 𝑥/2. Finally we show that when all functions in F are Lipschitz-continuous, then so is the semantics of QCTL ★ [F ].

Equivalence with MSO[F ]

We extend MSO on trees with quality operators, and compare the expressiveness of the resulting logic with that of QCTL ★ [F ]. Multi-valued semantics of MSO have been proposed in the litterature, both on words and on trees [START_REF] Droste | Multi-Valued MSO Logics over Words and Trees[END_REF][START_REF] Droste | MK-fuzzy Automata and MSO Logics[END_REF][START_REF] Rahonis | Fuzzy Languages[END_REF], and links with fuzzy automata have been established. In [START_REF] Droste | Multi-Valued MSO Logics over Words and Trees[END_REF] the authors introduce a multi-valued version of MSO, in which the Boolean connectives are replaced by their fuzzy versions, as an extension of Łukasiewicz logic [START_REF] Łukasiewicz | O Logice Trójwartościowej[END_REF] to MSO. From such extension, they develop a corresponding automata theory, providing a multi-valued version of the Büchi theorem. Differently from our approach, however, the set of functions of this multi-valued MSO is limited to those deriving from the Boolean connectives. Instead, here we consider an arbibrary set of function, producing a more general setting than the one presented in [START_REF] Droste | Multi-Valued MSO Logics over Words and Trees[END_REF].

In [START_REF] Droste | MK-fuzzy Automata and MSO Logics[END_REF], the authors start from a 4-valued logic (MK-valued logic), taking also undefined and error values, together with classic true and false. Yhey define a fuzzy version of it, namely MK-fuzzy MSO, with truth values of propositions given by 4-tuples in [0, 1] 4 such that the four components always sum to 1. This is used to measure the degree of truth of a property that accounts for the levels of truth, falsity, undefinedness, and error. They introduce MK-fuzzy automata and solve some of the related problems. We conjecture that the classification of thruth values given there can be encoded in our formalism, and that we can embed reasoning in MK-fuzzy MSO in our setting. We leave this problem open for future investigation.

Let Var 1 and Var 2 be countable sets of first-order and second-order variables, respectively. where 𝑎 ∈ AP, 𝑥, 𝑦 ∈ Var 1 , 𝑋 ∈ Var 2 and 𝑓 ∈ F . Formulas of MSO[F ] are interpreted on infinite (V AP , 𝐷)-trees and first-order variables represent nodes of the tree. But instead of usual sets, second-order variables represent fuzzy sets, i.e., mappings 𝑋 : 𝜏 → [0, 1] indicating to which degree each node of the tree 𝜏 belongs to the set.

To evaluate formulas with free variables, we need interpretations: an interpretation I for a formula 𝜑 (𝑥 1 , . . . , 𝑥 𝑘 , 𝑋 1 , . . . , 𝑋 𝑙 ) with free first-order variables 𝑥 1 , . . . , 𝑥 𝑘 and free second-order variables 𝑋 1 , . . . , 𝑋 𝑙 maps each free first-order variable 𝑥 𝑖 to some node 𝑢 ∈ 𝜏 and each free secondorder variable 𝑋 𝑖 to some fuzzy set 𝑋 : 𝜏 → [0, 1]. The domain of I, denoted with dom(I), is the set {𝑥 1 , . . . , 𝑥 𝑘 , 𝑋 1 , . . . , 𝑋 𝑙 } of variables where I is defined. Below we prove that MSO[F ] and QCTL ★ [F ] have the same expressive power. As noticed in [START_REF] Laroussinie | Quantified CTL: Expressiveness and Complexity[END_REF], one important conceptual difference is that quantification in MSO[F ] refers to the whole tree, while QCTL ★ [F ] can only refer to the reachable part of the tree. As a consequence, MSO[F ] can express the fact that the current node is the root of the tree, while QCTL ★ [F ] cannot.

Formally, that both logics are equally expressive means that (1) for any (state-)formula 𝜑 ∈ QCTL ★ [F ], there is a formula φ (𝑥) ∈ MSO[F ] with one free first-order variable 𝑥 such that for any tree 𝑡 with root 𝑟 , it holds { {𝜑 } } 𝑡 (𝑟 ) = { { φ } } 𝑡 (𝑥 ↦ → 𝑟 ), and symmetrically, (2) for any formula 𝜑 (𝑥) ∈ MSO[F ] with one free first-order variable 𝑥, there is a formula φ ∈ QCTL ★ [F ] such that for any tree 𝑡 with root 𝑟 , it holds { { φ } } 𝑡 (𝑟 ) = { {𝜑 } } 𝑡 (𝑥 ↦ → 𝑟 ). We use the possibility to express Boolean second-order quantification to capture first-order quantification in elements in QCTL ★ [F ], and also to express path quantification in MSO[F ]. To see that the above translation is correct, note that if 𝑝 is Boolean in 𝑡 = (𝜏, w), then For the other direction, the usual translation from CTL ★ to MSO can be extended to a translation from CTL ★ [F ] to MSO[F ]. The only thing that we need to take care of is that quantification over paths must be translated using Boolean second-order quantification, which is expressible in MSO[F ] with formula ∃ B 𝑋 .𝜑. □

{{uniq(𝑝)}} 𝑡 = 1 if w -1 (1)
The above proof can be easily adapted to obtain the following result: As explained in the proof of Theorem 7.4, it seems hard to express quantification on paths in MSO[F ], or first-order quantification in QCTL ★ [F ], without the possibility to quantify on Boolean sets. We have seen that this quantification on Boolean sets can be expressed with fuzzy second-order quantification if we can use function Bool, but we do not know whether the converse is true, and we conjecture that it is not, meaning that MSO[{¬, ∧, Bool}] is strictly more expressive than MSO[{¬, ∧}] with ∃ B 𝑋 added as a basic construct. Note that if ∃ B 𝑋 and ∃ B 𝑝 are added as basic constructs of MSO[F ] and QCTL ★ [F ] respectively, then Theorem 7.4 holds as soon as F contains ¬ and ∧.

Undecidability of QCTL ★ [F ] model checking

In this section we show an undecidability result for the model checking of QCTL ★ [F ]. In fact we first prove it for the logic QLTL[F ] and then show that it entails undecidability of QCTL ★ [F ]. While in QCTL ★ [F ] second-order quantification is made at the level of state formulas, in QLTL[F ] such quantifications can depend on the path on which the formula is evaluated, which makes the proof easier. Theorem 7.6. Model checking QLTL[F ] (on a fixed Kripke structure) is undecidable, even when F only contains ¬, ∧ and the following two functions:

equal : [0, 1] 2 → {0, 1} half : [0, 1] 2 → {0, 1} (𝑥, 𝑦) ↦ → 1 if 𝑦 = 𝑥 (𝑥, 𝑦) ↦ → 1 if 𝑦 = 𝑥/2 (𝑥, 𝑦) ↦ → 0 otherwise (𝑥, 𝑦) ↦ → 0 otherwise
Proof. The proof consists in expressing a tiling problem as a QLTL[F ] model checking problem. In this setting, given a finite set C of colors, a tile is a 4-tuple of colors of C, seen as the four colors of the edges of a square. We write 𝑢 = ⟨top(𝑢), bottom(𝑢), left(𝑢), right(𝑢)⟩ for such a tile. Given a set 𝐵 of tiles, a tiling of a subset 𝑍 of N 2 with tiles of 𝐵 is a mapping 𝑡 : 𝑍 ↦ → 𝐵. Such a tiling is valid whenever the colors of neighboring tiles agree; formally, a tiling 𝑡 is valid if for any two positions 𝑝 = (𝑥, 𝑦) and

𝑝 ′ = (𝑥 ′ , 𝑦 ′ ) in 𝑍 , it holds • if 𝑥 ′ = 𝑥 and 𝑦 ′ = 𝑦 + 1, then top(𝑡 (𝑝)) = bottom(𝑡 (𝑝 ′ )); • if 𝑦 ′ = 𝑦 and 𝑥 ′ = 𝑥 + 1, then right(𝑡 (𝑝)) = left(𝑡 (𝑝 ′ )).
We encode the following tiling problem: Given a finite set of tiles 𝐵 = {𝑢 𝑖 | 1 ≤ 𝑖 ≤ 𝑛}, does any rectangular grid admit a valid tiling? This problem is undecidable [82, pages 213-214].

In our encoding, we consider the Kripke structure K depicted in Figure 1 (which does not depend on the set of tiles given as input). In that structure, there are three (Boolean) atomic propositions, and the name of each state indicates the only atomic proposition having value 1 in that state. We build two QLTL[F ] formulas in the sequel:

𝑝 𝑞 𝑟

• the first one will be true along any path that corresponds to some rectangular grid, as depicted on Figure 2; additionally, if the path corresponds to such a grid, it will "number" all lines using via the value of an atomic proposition 𝑡; • the second formula will rely on the numbering of lines to check the existence of a valid tiling.

For the first phase, we characterize the paths of K that encode a grid as shown on Figure 2. This is enforced using the conjunction of the following formulas:

• we label all states with a quantitative atomic proposition 𝑡 in such a way that the value of 𝑡 is divided by 2 as long as we only visit 𝑞-states, and it restarts from 1 at 𝑝-or 𝑟 -states: ∃𝑡 . G((¬𝑞) → 𝑡) ∧ G((X𝑞) → half(𝑡, X𝑡)).

For this formula to take value 1, alll 𝑝-and 𝑟 -states must have 𝑡 = 1, and the value of 𝑡 in a 𝑞-states must be half the value of 𝑡 in the previous state; Lemma 7.8. Let 𝜋 = (𝑠 𝑗 ) 𝑗 ∈N be an infinite path of the form (𝑝 • 𝑞 𝑙 ) 𝑚 • 𝑟 𝜔 for some 𝑙, 𝑚 ∈ N in the Kripke structure K of Figure 1. Assume that 𝜋 is labeled with atomic proposition 𝑡 in such a way that for any 𝑖 and 𝑗 in [0, 𝑚(𝑙 + 1) -1], it holds that ℓ (𝑠 𝑖 ) (𝑡) = ℓ (𝑠 𝑗 ) (𝑡) if, and only if, 𝑖 -𝑗 is a multiple of 𝑙 + 1. Then { {Ψ tiling }} (𝜋) = 1 if, and only if, the grid of size 𝑙 × 𝑚 admits a valid tiling with tiles in {𝑢 𝑖 | 1 ≤ 𝑖 ≤ 𝑛}.

To conclude the proof of Theorem 7.6, we let Ψ be the QLTL[{equal, half}] formula

Ψ = ∀𝑡 . ∃(𝑢 𝑖 ) 1≤𝑖 ≤𝑛 . (equal(𝜓 grid , ⊤) → equal(𝜓 tiling , ⊤)).
Then { {Ψ} } (K) = 1 if, and only if, any rectangular grid can be tiled with tiles {𝑢 𝑖 | 1 ≤ 𝑖 ≤ 𝑛}. □ Now to obtain undecidability of QCTL ★ [F ] we need to show that all quantifications on atomic propositions can be made at the beginning, as QCTL ★ [F ] does not allow mixing second-order quantification with temporal operators without requantifying on paths. To this aim notice that formula Ψ is almost in prenex form, but 𝜓 tiling still contains an existential quantification under a temporal modality. However, Ψ can be turned into prenex form, by noticing that for all QLTL[F ] formulas 𝜓 and 𝜓 ′ ,

G(𝜓 → ∃𝑣. 𝜓 ′ ) ≡ ∀𝑤 . ∃𝑣 . (uniq(𝑤) → G((𝜓 ∧ 𝑤) → 𝜓 ′ ))
where 𝑤 is a new atomic proposition, and uniq(𝑤) = equal(𝑤, ⊥) U (equal(𝑤, ⊤) ∧ XG equal(𝑤, ⊥)) requires 𝑤 to be Boolean and to only label one state of the path.

In the end, Ψ can be written as It is clear that { {Ψ} } (K) = 1 if and only if {{Φ}} (K) = 1, hence the following result: Theorem 7.9. Model checking QCTL ★ [F ] (on a fixed Kripke structure) is undecidable, even when F only contains ¬, ∧, equal and half.

Lipschitz continuity

Fuzzy logic is used to reason about imprecise information. In that setting, Lipschitz continuity guarantees a certain level of precision of the value of the formula depending on the level of precision of the information we have about the model [START_REF] Almagor | Latticed-LTL synthesis in the presence of noisy inputs[END_REF][START_REF] Majumdar | Robust discrete synthesis against unspecified disturbances[END_REF][START_REF] Topcu | On synthesizing robust discrete controllers under modeling uncertainty[END_REF]. In this section we show that when the quality functions in F are Lipschitz continuous, then so is the satisfaction value of QCTL ★ [F ] formulas.

Let 𝑃 ⊆ AP. A 𝑃-labeling for a tree 𝑡 = (𝜏, w) is a mapping ℓ 𝑃 : 𝑃 → (𝜏 → [0, 1]). For any two subsets 𝑃 and 𝑄 of AP, any 𝑃-labeling ℓ 𝑃 and 𝑄-labeling ℓ 𝑄 of 𝑡, we define their composition as the 𝑃 ∪ 𝑄-labeling defined as follows: Notice that, given ℓ 𝑃 , ℓ ′ 𝑃 and ℓ 𝑄 , it holds 𝑑 𝑃 ∪𝑄,𝑡 (ℓ 𝑃 ⊗ ℓ 𝑄 , ℓ ′ 𝑃 ⊗ ℓ 𝑄 ) ≤ 𝑑 𝑃,𝑡 (ℓ 𝑃 , ℓ ′ 𝑃 ). When 𝑡 and 𝑃 are clear from the context, we omit them from the notation.

Let 𝑡 = (𝜏, w) be a ( [0, 1] AP , 𝐷)-tree, and 𝑢 be a node of 𝑡. Let 𝜑 ∈ QCTL ★ [F ] be a state formula over AP. We define 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) : ( [0, 1] 𝜏 ) 𝑃 → [0, 1] ℓ 𝑃 ↦ → { {𝜑 } } (𝜏,w⊗ℓ 𝑃 ) (𝑢). Similarly, given an infinite branch 𝜆 of 𝑡 and a path formula 𝜓 ∈ QCTL ★ [F ], we define 𝐹 (𝑡, 𝜆, 𝑃,𝜓 ) : ( [0, 1] 𝜏 ) 𝑃 → [0, 1] ℓ 𝑃 ↦ → { {𝜓 } } (𝜏,w⊗ℓ 𝑃 ) (𝜆).

For two metric spaces (𝐷, 𝑑 𝐷 ) and (𝐼, 𝑑 𝐼 ), a function 𝑓 : 𝐷 → 𝐼 is 𝑘-Lipschitz continuous when, for every two elements 𝑋 and 𝑌 in 𝐷, it holds 𝑑 𝐼 (𝑓 (𝑋 ), 𝑓 (𝑌 )) ≤ 𝑘 • 𝑑 𝐷 (𝑋, 𝑌 ).

A QCTL ★ [F ] state formula 𝜑 is then 𝑘-Lipschitz continuous if, for every tree 𝑡, node 𝑢 of 𝑡 and subset 𝑃 ⊆ AP, the function 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) is 𝑘-Lipschitz continuous. The definition is extended to path formulas in the natural way. Proof. Consider a QCTL ★ [F ] formula 𝜑. The proof is by induction on the structure of 𝜑. The base case where 𝜑 is an atomic proposition 𝑝 is easy: pick a tree 𝑡, a node 𝑢 and a subset 𝑃 ⊆ AP; if 𝑝 ∉ 𝑃, then 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) is a constant function; if 𝑝 ∈ 𝑃, then 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) = ℓ 𝑃 (𝑝) (𝑢) for any 𝑃-labeling ℓ 𝑃 , so that |𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 )| = |ℓ 𝑃 (𝑝) (𝑢)ℓ ′ 𝑃 (𝑝) (𝑢)| ≤ 𝑑 (ℓ 𝑃 , ℓ ′ 𝑃 ) We now consider the other cases, assuming that the result holds for all subformulas of 𝜑:

• if 𝜑 = ∃𝑞.𝜓 , then for any tree 𝑡 = (𝜏, w), any node 𝑢, any subset 𝑃 ⊆ AP, and any 𝑃-labeling ℓ 𝑃 , we have 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) = sup ℓ 𝑞 {𝑞 }-labeling { {𝜓 } } (𝜏,w⊗ℓ 𝑃 ⊗ℓ 𝑞 ) (𝑢).

By definition of sup, for any 𝜀 > 0, there exists a 𝑞-labeling ℓ 𝜀 𝑞 such that 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) ≤ {{𝜓 }} (𝜏,w⊗ℓ 𝑃 ⊗ℓ 𝜀 𝑞 ) (𝑢) + 𝜀.

Moreover, for any 𝑃-labeling ℓ { {𝜓 } } (𝜏,w⊗ℓ 𝑃 ) (𝜆).

For any 𝜀 > 0, there is a branch 𝜆 𝜀 such that 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) ≤ {{𝜓 }} (𝜏,w⊗ℓ 𝑃 ) (𝜆 𝜀 ) + 𝜀.

Then for any 𝑃-labeling ℓ ′ 𝑃 , we have 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 ) ≤ {{𝜓 }} (𝜏,w⊗ℓ 𝑃 ) (𝜆 𝜀 ) -{ {𝜓 } } (𝜏,w⊗ℓ Otherwise, this minimum is reached at some index 𝑗 0 < 𝑖 𝜀 , and we have 𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ ′ 𝑃 ) ≤ {{𝜓 1 }} (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥ 𝑗 0 ) -{ {𝜓 1 } } (𝜏,w⊗ℓ ′ 𝑃 ) (𝜆 ≥ 𝑗 0 ) + 𝜀.

For both cases, thanks to the induction hypothesis and applying the same arguments as for previous cases, we end up with |𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ ′ 𝑃 )| ≤ max(1, 𝑘 𝑛 ) • 𝑑 (ℓ 𝑃 , ℓ ′ 𝑃 ). • if 𝜑 = X𝜓 , the result is straightforward. □ It is not hard to see that all the considerations in the proof of Theorem 7.10, in particular the case 𝜑 = ∃𝑞.𝜓 , apply also when the quantification is over Boolean atomic propositions, hence we also have the following. Theorem 7.11. If all functions in F are 𝑘-Lipschitz continuous, then every formula in BQCTL ★ [F ] having at most 𝑛 nested functions is max(1, 𝑘 𝑛 )-Lipschitz continuous.

FUTURE WORK

We introduced and studied SL[F ], a formalism for specifying quality and fuzziness of strategic on-going behavior. We demonstrated the expressiveness of SL[F ] through a number of examples from multi-agent systems, solved its model-checking problem and established its precise complexity. While it is non-elementary in general, we also identified an expressive fragment (SL 1𝐺 [F ]) that, as in the Boolean case, retains an elementary model-checking problem (it is 2-Exptime-complete).

As a means of studying SL[F ], we extended QCTL ★ to the quantitative setting, leading to the logics QCTL ★ [F ] and BQCTL ★ [F ] depending on whether quantified propositions range over [0, 1] or only over Boolean values {0, 1}. We described how the latter can be seen as a fragment of the former, and how they relate to MSO and Strategy Logic, with BQCTL ★ [F ] allowing to capture pure strategies, while QCTL ★ [F ] could be used to capture mixed ones. We showed that their semantics is Lipschitz-continuous when they use only Lipschitz-continuous functions. Finally we studied their model-checking problem and showed that it is undecidable for QCTL ★ [F ] but decidable for BQCTL ★ [F ], which allows us to prove decidability of model checking SL [F ].

Beyond the applications described in the paper, we highlight here some interesting directions for future research. In classical temporal-logic model checking, coverage and vacuity algorithms measure the sensitivity of the system and its specifications to mutations, revealing errors in the modeling of the system and lack of exhaustiveness of the specification [START_REF] Chockler | Coverage Metrics for Formal Verification[END_REF]. When applied to SL[F ], these algorithms can set the basis to a formal reasoning about classical notions in game theory, like the sensitivity of utilities to price changes, the effectiveness of burning money [START_REF] Costa | Mixed equilibrium in 2 × 2 normal form games: when burning money is rational[END_REF][START_REF] Hartline | Optimal mechanism design and money burning[END_REF] or tax increase [START_REF] Cole | How much can taxes help selfish routing?[END_REF], and more.

Definition 2 . 1 .

 21 Let F ⊆ {𝑓 : [0, 1] 𝑚 → [0, 1] | 𝑚 ∈ N} be a set of functions over [0, 1] of possibly different arities. The syntax of SL[F ] is defined with respect to a finite set of atomic propositions AP, a finite set of agents Agt and a set of strategy variables Var. The set of SL[F ] formulas is defined by the following grammar: 𝜑 ::= 𝑝 | ⟨⟨𝑥⟩⟩𝜑 | (𝑎, 𝑥)𝜑 | E𝜓 | 𝑓 (𝜑, . . . , 𝜑) 𝜓 ::= 𝜑 | X𝜓 | 𝜓 U𝜓 | 𝑓 (𝜓, . . . ,𝜓 ) where 𝑝 ∈ AP, 𝑥 ∈ Var, 𝑎 ∈ Agt, and 𝑓 ∈ F .

Definition 2 . 6 .Example 2 . 7 . 2 Theorem 2 . 8 .

 2627228 Formally, bnd(𝜑) is defined inductively as follows: bnd(𝑝) = 0 bnd(⟨⟨𝑥⟩⟩𝜑) = bnd(𝜑) if 𝜑 = ⟨⟨𝑦⟩⟩𝜑 ′ for some 𝑦 ∈ Var 1 + bnd(𝜑) otherwise bnd((𝑎, 𝑥)𝜑) = bnd(𝜑) bnd(𝑓 (𝜑 1 , • • • , 𝜑 𝑘 )) = max{bnd(𝜑 𝑖 ) | 1 ≤ 𝑖 ≤ 𝑘 } bnd(E𝜓 ) = bnd(𝜓 ) bnd(X𝜓 ) = bnd(𝜓 ) bnd(𝜓 U𝜓 ′ ) = max{bnd(𝜓 ), bnd(𝜓 ′ )}Here are a few examples of block-nesting depth of some formulas. bnd(⟨⟨𝑥⟩⟩⟨⟨𝑦⟩⟩(𝑎, 𝑥) (𝑏, 𝑦) EF𝑝) = 1 bnd(⟨⟨𝑥⟩⟩⟨⟨𝑦⟩⟩⟨⟨𝑧⟩⟩(𝑎, 𝑥) (𝑏, 𝑦) (𝑐, 𝑧) EF𝑝) = 1 bnd(⟨⟨𝑥⟩⟩⟨⟨𝑦⟩⟩ [[𝑧]] (𝑎, 𝑥) (𝑏, 𝑦) (𝑐, 𝑧) EF𝑝) = 2 bnd(⟨⟨𝑥⟩⟩⟨⟨𝑦⟩⟩(𝑎, 𝑥) (𝑏, 𝑦) EF ⟨⟨𝑧⟩⟩(𝑐, 𝑧) AG𝑞) = The model-checking problem for SL[F ] is decidable. It is (𝑘 + 1)-Exptime-complete for formulas of block nesting depth at most 𝑘.

  be a set of functions over [0, 1]. Definition 3.1. The syntax of QCTL ★ [F ] is defined with respect to a finite set AP of atomic propositions, using the following grammar: 𝜑 ::= 𝑝 | ∃𝑝. 𝜑 | E𝜓 | 𝑓 (𝜑, . . . , 𝜑) 𝜓 ::= 𝜑 | X𝜓 | 𝜓 U𝜓 | 𝑓 (𝜓, . . . ,𝜓 )

  𝑢) ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

3. 4

 4 Model-checking problem Definition 3.6. The quantitative model-checking problem for QCTL ★ [F ] (resp. BQCTL ★ [F ]) consists in, given a QCTL ★ [F ] state formula 𝜑, a weighted Kripke structure K, and a predicate 𝑃 ⊆ [0, 1], decide whether {{𝜑 }} K ∈ 𝑃 (resp. {{𝜑 }} K B ∈ 𝑃).

3 .Theorem 3 . 7 .Theorem 3 . 8 .

 33738 The quantitative model-checking problem for BQCTL ★ [F ] is decidable. It is (𝑘 + 1)-Exptime-complete for formulas of block nesting depth at most 𝑘. The quantitative model-checking problem for QCTL ★ [F ] is undecidable if F contains the functions (𝑥, 𝑦) ↦ → 𝑥 = 𝑦 and (𝑥, 𝑦) ↦ → 𝑦 = 𝑥/2. Theorem 3.7 is proved in the next section. Together with a reduction from SL[F ] to BQCTL ★ [F ] that we present in Section 5, it entails the decidability of model checking SL[F ] announced in Theorem 2.8. We prove Theorem 3.8 in Section 7.1, where we also establish some additional results on the expressivity and continuity of QCTL ★ [F ].

Lemma 4 . 3 .

 43 Let V ⊂ [0, 1] be a finite set of values with {0, 1} ⊆ V, let 𝜑 be a BQCTL ★ [F ] state formula and 𝜓 a BQCTL ★ [F ] path formula, with respect to AP. DefineVal 𝜑,V = {{{𝜑 }} 𝑡 (𝑢) | 𝑡 is a V AP -labeled tree and 𝑢 ∈ 𝑡 } be the set of values taken by 𝜑 in nodes of V AP -labeled trees. Similarly, define Val 𝜓,V = {{{𝜓 }} 𝑡 (𝜆) | 𝑡 is a V AP -labeled tree, 𝑢 ∈ 𝑡 and 𝜆 ∈ Br(𝑢)} Then, |Val 𝜑,V | ≤ |V | |𝜑 | and |Val 𝜓,V | ≤ |V | |𝜓 | , and one can compute sets Val 𝜑,V and Val 𝜓,V of size at most |V | |𝜑 | and |V | |𝜓 | respectively, and such that Val 𝜑,V ⊆ Val 𝜑,V and Val 𝜓,V ⊆ Val 𝜓,V .

Proposition 4 . 4 .

 44 Let V ⊂ [0, 1] be a finite set of values such that {0, 1} ⊆ V, and let 𝐷 be a finite set of directions. For every BQCTL ★ [F ] state formula 𝜑 and predicate 𝑃 ⊆ [0, 1], one can construct an APT A V,𝑃 𝜑 over (V AP ∪ {•})-trees such that for every V AP -labeled 𝐷-tree 𝑡, A V,𝑃 𝜑 accepts 𝑡 if and only if { {𝜑 } } 𝑡 ∈ 𝑃 .The APT A V,𝑃 𝜑 is of size at most (bnd(𝜑) + 1)-exponential in |𝜑 |, and its index is at most nd(𝜑)exponential in |𝜑 |.

𝜓 [ 0

 0 ,𝑣 ] , but it would cost one more exponential. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

  shown in [65, Theorem 4.1, Corollary 4.1], one can decide the winners of a CMPG P = ⟨Agt, Act, 𝑉 , v 𝜄 , Δ, p⟩ in time polynomial w.r.t. |𝑉 | and |Act|, and exponential w.r.t. |Agt| and 𝑘 = max p (the maximal priority). Theorem 6.3. The model-checking problem for closed formulas of SL 1𝐺 [F ] is decidable, and 2-Exptime-complete.

Definition 7 . 1 .

 71 The syntax of MSO[F ] is given by the following grammar:𝜑 ::= 𝑃 𝑎 (𝑥) | 𝑥 = 𝑦 | 𝑥 ∈ 𝑋 | 𝑆 (𝑥, 𝑦) | ∃𝑥𝜑 | ∃𝑋𝜑 | 𝑓 (𝜑, . . . , 𝜑)

Definition 7 . 2 (Lemma 7 . 3 .

 7273 Semantics). Given a (V AP , 𝐷)-tree 𝑡 = (𝜏, w), an MSO[F ] formula 𝜑 and an interpretation I for the free variables of 𝜑, the semantics of 𝜑 is defined as follows:{{𝑃 𝑎 (𝑥)}} 𝑡 (I) = w(I (𝑥)) (𝑎){{𝑥 = 𝑦}} 𝑡 (I) = 1 if I (𝑥) = I (𝑦) 0 otherwise {{𝑥 ∈ 𝑋 }} 𝑡 (I) = I (𝑋 ) (I (𝑥)) {{𝑆 (𝑥, 𝑦)}} 𝑡 (I) = 1 if I (𝑦) is a child of I (𝑥) 0 otherwise {{∃𝑥𝜑 }} 𝑡 (I) = sup 𝑢 ∈𝜏 {{𝜑 } } 𝑡 (I [𝑥 ↦ → 𝑢]) {{∃𝑋𝜑 }} 𝑡 (I) = sup 𝑌 : 𝜏→[0,1] { {𝜑 } } 𝑡 (I [𝑋 ↦ → 𝑌 ]) {{𝑓 (𝜑 1 , . . . , 𝜑 𝑛 )}} 𝑡 (I) = 𝑓 ({{𝜑 1 }} 𝑡 (I), . . . , { {𝜑 𝑛 } } 𝑡 (I))where I [𝛼 ↦ → 𝛽] is the interpretation J such that dom(J ) = dom(I) ∪ {𝛼 }, and J (𝛼) = 𝛽 and J (𝛾) = I (𝛾) for all 𝛾 ∈ dom(I) \ {𝛼 }.We also consider the case where set quantification is over classic sets instead of fuzzy ones. We call this logic BMSO[F ]. Its syntax is the same as MSO[F ] and the semantics, which we write { {•} } 𝑡 B , differs only in the case of second-order quantification, which is as follows: {{∃𝑋𝜑 }} 𝑡 B (I) = sup 𝑌 : 𝜏→{0,1} { {𝜑 } } 𝑡 B (I [𝑋 ↦ → 𝑌 ]) ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021. Recall that, if Bool is the function that maps 𝑥 to 1 if 𝑥 ∈ {0, 1}, and to 0 otherwise, then BQCTL ★ [F ] is a fragment of QCTL ★ [F ∪ {Bool}] (Lemma 3.5), and Boolean quantification on atoms can be expressed in QCTL ★ [F ] as ∃𝑝.(AG Bool(𝑝) ∧ 𝜑). Similarly, BMSO[F ] is a fragment of MSO[F ∪ {Bool}]: define Bool(𝑋 ) := ∀𝑥 . Bool(𝑥 ∈ 𝑋 ) ∃ B 𝑋 .𝜑 := ∃𝑋 . Bool(𝑋 ) ∧ 𝜑 It holds that: For every BMSO[F ] formula 𝜑, letting 𝜑 B be the MSO[F ] formula obtained from 𝜑 by replacing inductively each ∃𝑋 .𝜑 ′ in 𝜑 with ∃ B 𝑋 .𝜑 ′ B , we have that for all tree 𝑡 and interpretation I, {{∃ B 𝑋 .𝜑 } } 𝜏 (I) = { {∃𝑋 .𝜑 }} 𝜏 B (I).

Theorem 7 . 4 .

 74 If {¬, ∧, Bool} ∈ F then MSO[F ] has the same expressive power as QCTL ★ [F ].Proof. Translating QCTL ★ [F ] to MSO[F ] can be done as usual, using first-order quantifiers to express temporal operators, and second-order quantifiers to express quantification on atomic propositions. The only subtlety here is to express path quantification in MSO[F ]. The usual translation consists in using second-order quantification and express that the quantified set is a path, with the following formula:Path(𝑋 ) := ∀𝑥, 𝑦. (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → (𝑥 ⪯ 𝑦 ∨ 𝑦 ⪯ 𝑥) where 𝑥 ⪯ 𝑦 := ∀𝑋 . (𝑥 ∈ 𝑋 ∧ 𝑆-Closed(𝑋 ) → 𝑦 ∈ 𝑋 ) and 𝑆-Closed(𝑋 ) := ∀𝑥, 𝑦. (𝑥 ∈ 𝑋 ∧ 𝑆 (𝑥, 𝑦) → 𝑦 ∈ 𝑋 )The translation of E𝜓 is then defined as follows:(E𝜓 ) ′ := ∃𝑋 . Path(𝑋 ) ∧ 𝜓 ′ (𝑋 ) where 𝜓 ′ (𝑋 ) is the translation of 𝜓 in MSO[F ]. However in our context, for this translation to have the intended value which is the supremum of the satisfaction value of 𝜓 over all paths, formulas Path(𝑋 ) and 𝑥 ⪯ 𝑦 must have a Boolean value. We obtain this by using quantification on Boolean sets ∃ B 𝑋 defined above, letting 𝑥 ⪯ 𝑦 := ∀ B 𝑋 . (𝑥 ∈ 𝑋 ∧ 𝑆-Closed(𝑋 ) → 𝑦 ∈ 𝑋 ) and (E𝜓 ) ′ := ∃ B 𝑋 . Path(𝑋 ) ∧ 𝜓 ′ For the direction from MSO[F ] to QCTL ★ [F ], we adapt the translation from MSO to QCTL ★ presented in [60]: for 𝜑 ∈ MSO[F ], where free variable 𝑥 represents the root of the tree, we inductively define the QCTL ★ [F ] formula 𝜑 as follows: 𝑥 = 𝑦 := 𝑝 𝑦 𝑦 = 𝑧 := EF(𝑝 𝑦 ∧ 𝑝 𝑧 ) 𝑥 ∈ 𝑋 := 𝑝 𝑋 𝑦 ∈ 𝑋 := EF(𝑝 𝑦 ∧ 𝑝 𝑋 ) ∃𝑦.𝜑 ′ := ∃ B 𝑝 𝑦 . uniq(𝑝 𝑦 ) ∧ 𝜑 ′ ∃𝑋 .𝜑 ′ := ∃𝑝 𝑋 . 𝜑 ′ 𝑆 (𝑥, 𝑦) := EX𝑝 𝑦 𝑆 (𝑦, 𝑥) := 0 𝑆 (𝑦, 𝑧) := EF(𝑝 𝑦 ∧ EX𝑝 𝑧 ) 𝑓 (𝜑 1 , . . . , 𝜑 𝑛 ) := 𝑓 ( 𝜑 1 , . . . , 𝜑 𝑛 ) where uniq(𝑝) := EF𝑝 ∧ ∀ B 𝑞. (EF(𝑝 ∧ 𝑞) → AG(𝑝 → 𝑞))

  an interpretation I such that I (𝑥) is the root of 𝜏 we have that { {𝜑 } } 𝜏 (I) = { { 𝜑 } } 𝑡 , where 𝑡 = (𝜏, w) and w(𝑢) (𝑝 𝑦 ) = 1 if I (𝑦) = 𝑢, 0 otherwise, and w(𝑢) (𝑝 𝑋 ) = I (𝑋 ) (𝑢).

Theorem 7 . 5 .

 75 If {¬, ∧, Bool} ∈ F then BMSO[F ] has same expressive power as BQCTL ★ [F ].

Fig. 1 .Fig. 2 .

 12 Fig. 1. Kripke structure K

  ∀𝑡 . ∃(𝑢 𝑖 ) 1≤𝑖 ≤𝑛 . ∀𝑤 . ∃𝑣 . (equal(𝜓 grid , ⊤) → equal(𝜓 ′ tiling , ⊤)) where 𝜓 ′ tiling ∈ LTL[equal] is obtained by applying the transformation above. Now define the QCTL ★ [F ] formula Φ = ∀𝑡 . ∃(𝑢 𝑖 ) 1≤𝑖 ≤𝑛 . ∀𝑤 . ∃𝑣. A(equal(𝜓 grid , ⊤) → equal(𝜓 ′ tiling , ⊤))

ℓ

  𝑃 ⊗ ℓ 𝑄 : 𝑃 ∪ 𝑄 → [0, 1] 𝑝 ↦ → ℓ 𝑄 (𝑝) if 𝑝 ∈ 𝑄, and ℓ 𝑃 (𝑝) if 𝑝 ∈ 𝑃 \ 𝑄.The distance between two 𝑃-labelings of 𝑡 = (𝜏, w) is defined as𝑑 𝑃,𝑡 (ℓ 𝑃 , ℓ ′ 𝑃 ) = sup 𝑢 ∈𝜏 max 𝑞 ∈𝑃 |ℓ 𝑃 (𝑞) (𝑢)ℓ ′ 𝑃 (𝑞) (𝑢)|.

Theorem 7 . 10 .

 710 If all functions in F are 𝑘-Lipschitz continuous, then every formula in QCTL ★ [F ] having at most 𝑛 nested functions is max(1, 𝑘 𝑛 )-Lipschitz continuous.

  ), then 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) = 𝑓 (𝐹 (𝑡, 𝑢, 𝑃, 𝜑 1 )(ℓ 𝑃 ), ..., 𝐹 (𝑡, 𝑢, 𝑃, 𝜑 𝑚 ) (ℓ 𝑃 )).Because 𝑓 is 𝑘-Lipschitz continuous, we have |𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 )| ≤ 𝑘 • max 𝑖 (|𝐹 (𝑡, 𝑢, 𝑃, 𝜑 𝑖 ) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑 𝑖 ) (ℓ ′ 𝑃 )|) ≤ 𝑘 • max(1, 𝑘 𝑛-1 )𝑑 (ℓ 𝑃 , ℓ ′ 𝑃 ). • if 𝜑 = 𝜓 1 U𝜓 2 , then 𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ 𝑃 ) = sup 𝑖 ∈N min({{𝜓 2 }} (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥𝑖 ), min 𝑗 <𝑖 ({ {𝜓 1 } } (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥ 𝑗 ))) .Then for any 𝜀 > 0, there exists 𝑖 𝜀 such that 𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ 𝑃 ) ≤ min({{𝜓 2 }} (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥𝑖 𝜀 ), min𝑗 <𝑖 𝜀 ({ {𝜓 1 } } (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥ 𝑗 ))) + 𝜀. Then for any ℓ ′ 𝑃 , 𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ ′ 𝑃 ) ≤ min({{𝜓 2 }} (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥𝑖 𝜀 ), min 𝑗 <𝑖 𝜀 ({ {𝜓 1 } } (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥ 𝑗 )))min({{𝜓 2 }} (𝜏,w⊗ℓ ′ 𝑃 ) (𝜆 ≥𝑖 𝜀 ), min 𝑗 <𝑖 𝜀 ({ {𝜓 1 } } (𝜏,w⊗ℓ ′ 𝑃 ) (𝜆 ≥ 𝑗 ))) + 𝜀If the latter minimum is obtained for 𝜓 2 along 𝜆 ≥𝑖 𝜀 , then we get 𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝜆, 𝑃, 𝜑) (ℓ ′ 𝑃 ) ≤ {{𝜓 2 }} (𝜏,w⊗ℓ 𝑃 ) (𝜆 ≥𝑖 𝜀 ) -{ {𝜓 2 } } (𝜏,w⊗ℓ ′ 𝑃 ) (𝜆 ≥𝑖 𝜀 ) + 𝜀.

  𝑛] is a permutation. In other terms, existential strategy quantification in ATL ★ (and ATL ★ [F ]) assigns a new strategy to a subset of the players, and drops the strategies previously assigned to the other players. Notice that in 𝜑 rescue , the universal strategy quantification and assignment for Agent 𝑣 is implicit, and is actually hidden in the path quantifier A: 𝜑 rescue is equivalent to

	⟨⟨𝑥⟩⟩⟨⟨𝑦⟩⟩ [[𝑧]] (𝑐, 𝑥) (𝑔, 𝑦) (𝑣, 𝑧) A(dist(𝑝 ì 𝛾 , 𝑞 ì 𝛾 )U safe)

) • • • (𝑎 𝜈 (𝑛) , 𝑥 𝑛 ) 𝜑 where Agt = {𝑥 𝑖 | 1 ≤ 𝑖 ≤ 𝑛} and 𝜈 : [1, 𝑛] → [1,

  maps each 𝑥 𝑖 to some strategy 𝜎 𝑖 , then the strategy profile (𝜎 𝑖 ) 𝑎 𝑖 ∈Agt is a NE if, and only if, 𝜑 NE evaluates to 1 under assignment 𝜒. Indeed, because [[𝑦 𝑖 ]] minimizes its subformula over all strategies 𝑦 𝑖 , formula [[𝑦 𝑖 ]] ((𝑎 𝑖 , 𝑦 𝑖 ) A𝜓 𝑖 ) ⪯ A𝜓 𝑖 evaluates to 1 if, and only if, for all strategies 𝑦 𝑖 , ((𝑎 𝑖 , 𝑦 𝑖 ) A𝜓 𝑖 ) ⪯ A𝜓 𝑖 evaluates to 1, i.e., 𝑦 𝑖 is not a profitable deviation for agent 𝑎 𝑖 . Notice that, since ⟨⟨𝑦 𝑖 ⟩⟩ maximizes over 𝑦 𝑖 , formula 1 (⟨⟨𝑦 𝑖 ⟩⟩ (𝑎 𝑖 , 𝑦 𝑖 ) A𝜓 𝑖 ) ⪯ A𝜓 𝑖 evaluates to 1 if, and only if, the best deviation for 𝑎 𝑖 is not profitable, and thus no deviations are profitable. Thus we could equivalently characterise NEs with

  𝑎 𝑖 ∈Agt , a coalition 𝐶 ⊆ Agt has a beneficial deviation (𝑦 𝑖 ) 𝑎 𝑖 ∈𝐶 if, for all strategy profiles (𝑧 𝑖 ) 𝑎 𝑖 ∈Agt\𝐶 and for all 𝑎 𝑖 ∈ 𝐶, it holds that (𝑥 𝑖 ) 𝑎 𝑖 ∈Agt 𝜓 𝑖 ≺ (𝑦 𝑖 ) 𝑎 𝑖 ∈𝐶 (𝑧 𝑖 ) 𝑎 𝑖 ∈Agt\𝐶 𝜓 𝑖 . We say that a strategy profile (𝑥 𝑖 ) 𝑎 𝑖 ∈Agt is a core equilibrium if, for every coalition, there is no beneficial deviation.

4.8 Core equilibria. In cooperative game theory, core equilibrium is probably the best-known solution concept and sometimes related to the one of Nash Equilibrium for non-cooperative games. Differently from NEs (but similarly to Strong NEs) it accounts multilateral deviations (also called coalition deviations) that, in order to be beneficial, must improve the payoff of the deviating agents no matter what is the reaction of the opposite coalition. More formally, for a given strategy profile (𝑥 𝑖 ) This can be written in SL[F ] as follows:

  By induction hypothesis, we get that |Val 𝜑,V | ≤ 𝑛 𝑖=1 |V | |𝜑 𝑖 | , which in turn is no greater than |V | |𝜑 1 |+...+|𝜑 𝑛 | , which is no greater than |V | |𝜑 | .

  3, Theorem 2.9] that for every 𝑃 ⊆ [0, 1], one can build a nondeterministic parity word automaton W Val atoms(𝜓 ) ) 𝜔 if and only if { {𝜓 } }(𝑤) ∈ 𝑃. Now let us compute Val E𝜓,V (again using Lemma 4.3), and for each 𝑣 ∈ Val E𝜓,V ∩ 𝑃, construct an NPT N 𝐸=𝑣 that guesses a branch in its input and simulates W 𝜓 {𝑣 } on it (it rejects if it leaves the "real" tree, i.e., if it sees a node labeled with •). To obtain a universal word automaton of single exponential size that checks whether {{𝜓 }}(𝑤) ∈ [0, 𝑣], we first build a nondeterministic word automaton W 𝜓 (𝑣,1] following [3], and dualize it in linear time into a universal word automaton W 𝜓 [0,𝑣 ] . Then we construct a UPT U 𝐴≤𝑣 that executes W

	𝜓
	𝑃 of size
	exponential in |𝜓 | 2 such that W 𝜓 𝑃 accepts a word 𝑤 ∈ ( 𝜓
	[0,𝑣 ]

  ′ 𝑃 , we have 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 ) = supℓ 𝑞 {𝑞 }-labeling {{𝜓 }} (𝜏,w⊗ℓ ′ 𝑃 ⊗ℓ 𝑞 ) (𝑢) ≥ { {𝜓 } } (𝜏,w⊗ℓ ′ 𝜀 ≤ max(1, 𝑘 𝑛 ) • 𝑑 𝑃 ∪{𝑞 },𝑡 (ℓ 𝑃 ⊗ ℓ 𝜀 𝑞 , ℓ ′ 𝑃 ⊗ ℓ 𝜀 𝑞 ) + 𝜀 (by i.h.) ≤ max(1, 𝑘 𝑛 ) • 𝑑 𝑃,𝑡 (ℓ 𝑃 , ℓ ′ 𝑃 ) + 𝜀.By symmetry, we get |𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 )| ≤ max(1, 𝑘 𝑛 ) • 𝑑 (ℓ 𝑃 , ℓ ′ 𝑃 ) + 𝜀. As this holds for any positive 𝜀, we have |𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 )| ≤ max(1, 𝑘 𝑛 ) • 𝑑 (ℓ 𝑃 , ℓ ′ 𝑃 ). • if 𝜑 = E𝜓 , we apply similar arguments: 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) = sup 𝜆∈Br(𝑢 )

	𝑃 ⊗ℓ 𝜀 𝑞 ) (𝑢).

It follows 𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 ) ≤ {{𝜓 }} (𝜏,w⊗ℓ 𝑃 ⊗ℓ 𝜀 𝑞 ) (𝑢) -{ {𝜓 } } (𝜏,w⊗ℓ ′ 𝑃 ⊗ℓ 𝜀 𝑞 ) (𝑢) + ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

  ′ 𝑃 ) (𝜆 𝜀 ) + 𝜀 ≤ max(1, 𝑘 𝑛 ) • 𝑑 (ℓ 𝑃 , ℓ ′ 𝑃 ) + 𝜀. As previously, it follows that |𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ 𝑃 ) -𝐹 (𝑡, 𝑢, 𝑃, 𝜑) (ℓ ′ 𝑃 )| ≤ max(1, 𝑘 𝑛 ) • 𝑑 (ℓ 𝑃 , ℓ ′ 𝑃 ). • if 𝜑 = 𝑓 (𝜑 1 , ..., 𝜑 𝑚

ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

Notice how parentheses are placed differently here, including ⟨⟨𝑦 𝑖 ⟩⟩ in the first argument of ⪯.

We use max here only because our functions are required to return values in [0, 1]. In the way we use diff in 𝜑 NE , the first argument will always be larger than or equal to the second one. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

This is assuming that payoffs are always positive, which is the case in this paper. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

i.e., for all s ∈ S, there exists s ′ such that (s, s ′ ) ∈ 𝑅. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

What we call UPT here is sometimes referred to as comp{NPT} in the literature. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

To reduce to this case, one can add quantifications on dummy variables. ACM Trans. Comput. Logic, Vol. 1, No. 1, Article . Publication date: January 2021.

ACKNOWLEDGMENTS

This work is partially based on the paper [19], which appeared in IJCAI '19. This work is partially supported by the ERC Advanced Grant WhiteMech (No. 834228), by the EU ICT-48 2020 project TAILOR (No. 952215), by the PRIN project RIPER (No. 20203FFYLK), and by the JPMorgan AI Faculty Research Award "Resilience-based Generalized Planning and Strategic Reasoning".

• we enforce that we have a grid: all columns (of 𝑞-states) must have the same length: G((X𝑝) → equal(𝑡, X((X𝑞)U(𝑡 ∧ X¬𝑞)))).

This takes value 1 if, and only if, the value of 𝑡 in a state where X𝑝 holds (i.e., in the last state of all but the last column) equals the value of 𝑡 in the last state of the next column. We write Ψ grid for the conjunction of the two formulas above, and F𝑟 . Notice that Ψ grid can be written as ∃𝑡 . 𝜓 grid , with 𝜓 grid ∈ LTL[equal, half]. Figure 3 represents the path of Figure 2 when labeled with values for 𝑡 witnessing the fact that Ψ grid has value 1 along that path. The following lemma formalizes the meaning of Ψ grid : Lemma 7.7. For any infinite path 𝜋 in the Kripke structure K of Figure 1, it holds: { {Ψ grid } } (𝜋) = 1 if, and only if, 𝜋 has the form (𝑝 • 𝑞 𝑙 ) 𝑚 • 𝑟 𝜔 for some 𝑙, 𝑚 ∈ N.

We now encode the tiling problem on this grid: this is achieved by labeling all 𝑞-states with a (Boolean) atomic proposition from (𝑢 𝑖 ) 1≤𝑖 ≤𝑛 , and checking that neighboring tiles match:

• we first label 𝑞-states with the tiles 𝑢 𝑖 for all 1 ≤ 𝑖 ≤ 𝑛, in such a way that all cells of the grid receive a unique tile:

• we check vertical matching:

where v-match is a purely Boolean formula listing all combinations of formulas of the form 𝑢 𝑖 ∧ X𝑢 𝑗 where the bottom-color of tile 𝑢 𝑖 and the top-color of 𝑢 𝑗 match; • we check horizontal matching: for this we have to make the formula find the right-neighboring cell in the grid. For this, we add an extra labeling with another atomic proposition 𝑣; thanks to formula (equal(𝑡, G𝑣) ∧ equal(𝑡, F𝑣)), we force 𝑣 to take the same value as the current 𝑡-value in all future states. The right-neighbor then is the (strict) next 𝑞-state where 𝑡 and 𝑣 have the same value; in that state, we check that the colors match:

where h-match(𝑢 𝑖 ) is a disjunction of all tiles whose left-color matches the right-color of 𝑢 𝑖 .

Write Ψ tiling for the conjunction of the three formulas above. Notice that Ψ tiling can be written as ∃(𝑢 𝑖 ) 1≤𝑖 ≤𝑛 . 𝜓 tiling , with 𝜓 tiling ∈ QLTL [{equal}]. Then: