# Reasoning about Quality and Fuzziness of Strategic Behaviors

Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, Giuseppe Perelli

► To cite this version:

Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, et al. Reasoning about Quality and Fuzziness of Strategic Behaviors. ACM Transactions on Computational Logic, 2023, 24 (3), pp.1-38. 10.1145/3582498. hal-04219131

HAL Id: hal-04219131

https://inria.hal.science/hal-04219131v1

Submitted on 26 Sep 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
Reasoning about Quality and Fuzziness of Strategic Behaviors

PATRICIA BOUYER, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, France

ORNA KUPFERMAN, Hebrew University, Israel

NICOLAS MARKEY, Irisa, CNRS & Inria & Université de Rennes, France

BASTIEN MAUBERT, Università degli Studi di Napoli “Federico II”, Italy

ANIELLO MURANO, Università degli Studi di Napoli “Federico II”, Italy

GIUSEPPE PERELLI, Sapienza University of Rome, Italy

*Temporal logics* are extensively used for the specification of on-going behaviors of computer systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going *strategic* behaviors in multi-agent systems, and the transition of temporal logics to a *quantitative* setting, where different satisfaction values enable the specifier to formalize concepts such as certainty or quality. In the first class, SL (*Strategy Logic*) is one of the most natural and expressive logics describing strategic behaviors. In the second class, a notable logic is LTL[F], which extends LTL with *quality operators*.

In this work we introduce and study SL[F], which enables the specification of quantitative strategic behaviors. The satisfaction value of an SL[F] formula is a real value in [0, 1], reflecting “how much” or “how well” the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, showing how it can express and measure concepts like stability in multi-agent systems, and how it generalizes some fuzzy temporal logics. We also provide a model-checking algorithm for SL[F], based on a quantitative extension of Quantified CTL*. Our algorithm provides the first decidability result for a quantitative extension of Strategy Logic. In addition, it can be used for synthesizing strategies that maximize the quality of the systems’ behavior.

CCS Concepts: • **Theory of computation** → **Logic and verification; Modal and temporal logics; Verification by model checking; Automata over infinite objects; Tree languages.**

Additional Key Words and Phrases: Synthesis, quantitative, fuzzy

**ACM Reference Format:**

Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Aniello Murano, and Giuseppe Perelli.
2021. Reasoning about Quality and Fuzziness of Strategic Behaviors. *ACM Trans. Comput. Logic* 1, 1 (January 2021), 38 pages. https://doi.org/10.1145/--

# 1 INTRODUCTION

## 1.1 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 [34, 42, 72]. 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.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

© 2021 Association for Computing Machinery.

1529-3785/2021/1-ART $15.00

https://doi.org/10.1145/--
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 multi-agent systems has led to the development of specification formalisms that enable the specification of on-going strategic behaviors in multi-agent systems [8, 31, 67]. 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 [69, 70]. In contrast, agents in multi-agent systems maintain an on-going interaction with each other [50], 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) [72], 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[Ф].

The logic LTL[Ф] is a fuzzy logic that augments LTL with quality operators [3]. The satisfaction value of an LTL[Ф] formula is a real value in [0, 1], intended to measure the quality in which the computation satisfies the specification. For example, the set Ф may contain the min{x, y}, max{x, y}, and 1 - x 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[Ф] 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 c that tries to bring an artifact to a rescue point, while keeping it as far as possible from a “villain” adversarial drone v. They evolve in a three-dimensional unit cube, in which coordinates are triples $\vec{y} = (\gamma_1, \gamma_2, \gamma_3) \in [0, 1]^3$. We use the triples of atomic propositions $p_{\vec{y}} = (p_{\gamma_1}, p_{\gamma_2}, p_{\gamma_3})$ and $q_{\vec{y}} = (q_{\gamma_1}, q_{\gamma_2}, q_{\gamma_3})$ to denote the coordinates of c and v, respectively. Assume that Ф contains the function dist: [0, 1]³ × [0, 1]³ → [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[Ф] formula:

$$ \psi_{\text{rescue}} = \text{dist}(p_{\vec{y}}, q_{\vec{y}}) \text{ U safe} $$

where U is the classic “until” operator. Indeed, the satisfaction value of $\psi_{\text{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.

## 1.2 Our contributions

We introduce and study the logic SL[Ф], which can be viewed both as an extension of LTL[Ф] to the strategic setting and as an extension of SL to the quantitative setting. Thus, while both LTL[Ф] and SL extend LTL, each in a different direction, SL[Ф] merges both extensions. The result is a strong yet clean logic that enables the specification of quantitative strategic behaviors. Syntax-wise,
SL[$\mathcal{F}$] lifts LTL[$\mathcal{F}$] to the strategic setting by introducing a strategy quantifier $\langle\langle x \rangle\rangle$, which returns the maximum satisfaction value of the formula in computations that are possible outcomes of the strategy $x$, and binding operator $(a, x)$, which assigns strategy $x$ to agent $a$. Then, SL[$\mathcal{F}$] also lifts SL to the quantitative setting by introducing quality operators as in LTL[$\mathcal{F}$]. The semantics of SL[$\mathcal{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[$\mathcal{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 $x$ for the carrier as the minimal quality of the behaviors resulting from $x$ against any strategy $y$ of the villain. If the quality of a behavior is specified by formula $\psi_{\text{rescue}}$ as above, then the quality of a strategy $x$ is 0 if the villain has a counter-strategy $y$ 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 $y$ of the villain. We are interested in maximizing the quality of carrier's strategies, which is formalized with the following formula (recall that $c$ and $v$ are agents corresponding to the carrier and the villain):

$$ \varphi_{\text{rescue}} = \langle\langle x \rangle\rangle [[y]](c, x)(v, y) A(\text{dist}(p_{\vec{y}}, q_{\vec{y}}) \text{ U safe}) $$

where $[[y]]$ is the dual of $\langle\langle y \rangle\rangle$, which returns the minimum value of the subformula in its scope over all strategies $y$. Thus, given a strategy $x$, formula $\varphi_{\text{quality}}(x) = [[y]](c, x)(v, y)A(\text{dist}(p_{\vec{y}}, q_{\vec{y}}) \text{ U safe})$ minimizes the quality over all possible strategies $y$ of the villain. It is therefore the minimal quality that strategy $x$ is guaranteed to enforce. In the end, formula $\varphi_{\text{rescue}}$ maximizes this value over all possible strategies $x$ of the carrier.

Note that in this example, the formula $\varphi_{\text{quality}}(x)$ 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 $x$. This suggests that SL[$\mathcal{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 $\epsilon$-Nash Equilibria [70].

### 1.2.2 Synthesizing optimal strategies.
We consider the following generalisation of the classic model-checking problem: given a weighted concurrent game structure $\mathcal{G}$, an SL[$\mathcal{F}$] formula $\varphi$ and a predicate $P \subseteq [0, 1]$, does the satisfaction value of $\varphi$ on $\mathcal{G}$ belong to $P$? To solve this problem, we employ an approach that recently proved handy in the study of a number of logics for strategic reasoning [13, 45, 61], and which consists in reducing the problem to the model checking of (some appropriate extension of) Quantified CTL\* (the extension of CTL\* with second-order quantifiers on atomic propositions, QCTL\* for short [48, 54, 55, 60, 77]). 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\*[$\mathcal{F}$] as the extension of CTL\*[$\mathcal{F}$] [3] with quantifiers over atomic propositions where, similarly to strategy quantifiers in SL[$\mathcal{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*[$\mathcal{F}$] undecidable. For our purpose of SL[$\mathcal{F}$] model checking, however, where quantification over atomic propositions encodes quantification over strategies, we show that one can restrict attention to Booleanly-Quantified CTL*[$\mathcal{F}$] (BQCTL*[$\mathcal{F}$] for short), where the quantified atomic propositions are assigned Boolean values in {0, 1}. For BQCTL*[$\mathcal{F}$], we are able to solve the model-checking problem, providing a solution also to SL[$\mathcal{F}$] model checking. We also study additional properties of QCTL*[$\mathcal{F}$] and BQCTL*[$\mathcal{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 [44]. This directly extends to CTL*[$\mathcal{F}$], using weighted fresh atomic propositions [3]. However this technique does not work for BQCTL*[$\mathcal{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 [57] and the word-automata construction developed for LTL[$\mathcal{F}$] [3], extending the latter from infinite words to infinite trees. More precisely, given a BQCTL*[$\mathcal{F}$] formula $\varphi$ and a predicate $P \subseteq [0, 1]$, we construct an alternating parity tree automaton that accepts exactly all the labeled trees $t$ such that the satisfaction value of $\varphi$ on $t$ is in $P$. The translation, and hence the complexity of our model-checking algorithm, is non-elementary: we show that the problem is actually $(k+1)$-EXPTIME-complete for formulas involving up to $k$ nested quantifications on atomic propositions; we show a similar complexity result for SL[$\mathcal{F}$], in terms of nesting of strategy quantifiers. Similarly to LTL[$\mathcal{F}$] [3], our complexity results hold as long as the quality operators in $\mathcal{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 [80], whenever the answer to the model-checking problem is positive, we can synthesize (outermost existentially-quantified) witness strategies. More precisely, if a formula $\varphi = \langle\langle x_1 \rangle\rangle \dots \langle\langle x_n \rangle\rangle\psi$ starts with a sequence of existentially-quantified strategies, and it holds that the satisfaction value of $\varphi$ in some weighted game $G$ belongs to $P \subseteq [0, 1]$, then our algorithm can be used to synthesize strategies $x_1, \dots, x_n$ that maximize within $P$ the quality as specified by $\psi$.

## 1.3 Related work

There have been long lines of works about games with quantitative objectives (in a broad sense), e.g. stochastic games [46, 76], timed games [11], or weighted games with various kinds of objectives (parity [43], mean-payoff [41] or energy [17, 28]). This does not limit to zero-sum games, but also includes the study of various solution concepts (see for instance [6, 22, 24, 26, 79]). Similarly, extensions of the classical temporal logics LTL and CTL with quantitative semantics have been studied in different contexts, with discounting [2, 36], averaging [16, 20], or richer constructs [3, 15]. In contrast, the study of quantitative temporal logics for strategic reasoning has remained rather limited: works on LTL[$\mathcal{F}$] include algorithms for synthesis and rational synthesis [3, 4, 6, 7], but no logics combine the quantitative aspect of LTL[$\mathcal{F}$] with the strategic reasoning offered by SL and, to the best of our knowledge, our model-checking algorithm for SL[$\mathcal{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 [12]; 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 [18]; only a periodicity property was proven, and no model-checking algorithm is known in that setting as well. Finally, Graded SL [10] 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 [32], timed ATL [25, 52], multi-valued ATL [53], and weighted versions of ATL [27, 62, 81]. Finally, some works have considered non-quantitative ATL with quantitative constraints on the set of allowed strategies [1, 38], proving decidability of the model-checking problem.

## 2 QUANTITATIVE STRATEGY LOGIC

Let $\Sigma$ be an alphabet. A finite (resp. infinite) word over $\Sigma$ is an element of $\Sigma^*$ (resp. $\Sigma^\omega$). The length of a finite word $w = w_0w_1...w_n$ is $|w| := n + 1$, and last($w$) := $w_n$ is its last letter. Given a finite (resp. infinite) word $w$ and $0 \le i < |w|$ (resp. $i \in \mathbb{N}$), we let $w_i$ be the letter at position $i$ in $w$, $w_i = w_0...w_i$ is the (nonempty) prefix of $w$ that ends at position $i$ and $w_{\ge i} = w_iw_{i+1}...$ is the suffix of $w$ that starts at position $i$. As usual, for any partial function $f$, we write $\text{dom}(f)$ for the domain of $f$.

Strategy logic with functions, denoted SL[$\mathcal{F}$], generalizes both SL [31, 67] and LTL[$\mathcal{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 $\mathcal{F}$ of functions.

### 2.1 Syntax

We build on the branching-time variant of SL [45], which does not add expressiveness with respect to the classic semantics [67] but presents several benefits (see [45] for more details), one of them being that it makes the connection with Quantified CTL tighter.

**Definition 2.1.** Let $\mathcal{F} \subseteq \{f: [0, 1]^m \to [0, 1] \mid m \in \mathbb{N}\}$ be a set of functions over $[0, 1]$ of possibly different arities. The syntax of SL[$\mathcal{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[$\mathcal{F}$] formulas is defined by the following grammar:

$$ \varphi ::= p \mid \langle\langle x \rangle\rangle \varphi \mid (a, x) \varphi \mid E \psi \mid f(\varphi, \dots, \varphi) $$

$$ \psi ::= \varphi \mid X \psi \mid \psi U \psi \mid f(\psi, \dots, \psi) $$

where $p \in \text{AP}$, $x \in \text{Var}$, $a \in \text{Agt}$, and $f \in \mathcal{F}$.

Formulas of type $\varphi$ are called state formulas, those of type $\psi$ are called path formulas. Formulas $\langle\langle x \rangle\rangle \varphi$ are called strategy quantifications whereas formulas $(a, x)\varphi$ are called bindings. Modalities X and U are temporal modalities, which take a specific quantitative semantics as we see below.

We may use $\top$, $\vee$, and $\neg$ to denote functions 1, max and $1-x$, respectively. We can then define the following classic abbreviations: $\bot := \neg\top$, $\varphi \wedge \varphi' := \neg(\neg\varphi \vee \neg\varphi')$, $\varphi \to \varphi' := \neg\varphi \vee \varphi'$, $F\psi := \top U \psi$, $G\psi := \neg F\neg\psi$, $A\psi := \neg E\neg\psi$ and $[[x]]\psi := \neg\langle\langle x \rangle\rangle\neg\varphi$.

Intuitively, the value of formula $\varphi \vee \varphi'$ is the maximal value of the two formulas $\varphi$ and $\varphi'$, $\varphi \wedge \varphi'$ takes the minimal value of the two formulas, and the value of $\neg\varphi$ is one minus that of $\varphi$. The implication $\varphi \to \varphi'$ thus takes the maximal value between that of $\varphi'$ and one minus that of $\varphi$.
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 $\mathcal{F}$. One can then check that $\varphi \lor \varphi'$, $\varphi \land \varphi'$, $\neg \varphi$ and $\varphi \rightarrow \varphi'$ take their usual Boolean meaning.

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

## 2.2 Semantics

While SL is evaluated on classic concurrent game structures with Boolean valuations for atomic propositions, SL[$\mathcal{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 $\mathcal{G} = \langle \text{Agt}, \text{Act}, V, v_i, \Delta \rangle$ where Agt is a finite set of agents, Act is a finite set of actions, V is a finite set of states, $v_i \in V$ is an initial state and $\Delta: V \times \text{Act}^{\text{Agt}} \rightarrow V$ is the transition function.

An element of $\text{Act}^{\text{Agt}}$ is a *joint action*, and we let $\text{succ}(v) = \{v' \in V \mid \exists \vec{c} \in \text{Act}^{\text{Agt}}, v' = \Delta(v, \vec{c})\}$ for each $v \in V$. For the sake of simplicity, we assume in the sequel that $\text{succ}(v) \neq \emptyset$ for all $v \in V$.

A *play* in $\mathcal{G}$ is an infinite sequence $\pi = (v_i)_{i \in \mathbb{N}}$ of states in V such that $v_0 = v_i$ and $v_i \in \text{succ}(v_{i-1})$ for all $i > 0$. We write $\text{Play}_\mathcal{G}$ for the set of plays in $\mathcal{G}$, and $\text{Play}_\mathcal{G}(v)$ for the set of plays in $\mathcal{G}$ starting from $v$. In this and all similar notations, we might omit to mention $\mathcal{G}$ when it is clear from the context. A (strict) prefix of a play $\pi$ is a finite sequence $\rho = (v_i)_{0 \le i \le L}$, for some $L \in \mathbb{N}$, which we denote $\pi_{\le L}$. We write $\text{Prefix}(\pi)$ for the set of strict prefixes of play $\pi$. Such finite prefixes are called *histories*, and we let $\text{Hist}_\mathcal{G}(v) = \text{Prefix}(\text{Play}_\mathcal{G}(v))$ and $\text{Hist}_\mathcal{G} = \bigcup_{v \in V} \text{Hist}_\mathcal{G}(v)$. We extend the notion of strict prefixes and the notation $\text{Prefix}$ to histories in the natural way, requiring in particular that $\rho \notin \text{Prefix}(\rho)$. A (finite) extension of a history $\rho$ is any history $\rho'$ such that $\rho \in \text{Prefix}(\rho')$.

A *strategy* is a mapping $\sigma: \text{Hist}_\mathcal{G} \rightarrow \text{Act}$, and we write $\text{Str}_\mathcal{G}$ for the set of strategies in $\mathcal{G}$. An *assignment* is a partial function $\chi: \text{Var} \cup \text{Agt} \rightarrow \text{Str}_\mathcal{G}$, that assigns strategies to variables and agents. The assignment $\chi[a \mapsto \sigma]$ maps $a$ to $\sigma$ and is equal to $\chi$ otherwise. Let $\chi$ be an assignment and $\rho$ a history. We define the set of *outcomes* of $\chi$ from $\rho$ as the set $\text{Out}(\chi, \rho)$ of plays $\pi = \rho \cdot v_1v_2\dots$ such that for every $i \in \mathbb{N}$, there exists a joint action $\vec{c} \in \text{Act}^{\text{Agt}}$ such that for each agent $a \in \text{dom}(\chi)$, $\vec{c}(a) = \chi(a)(\pi_{\le |\rho|+i-1})$ and $v_{i+1} = \Delta(v_i, \vec{c})$, where $v_0 = \text{last}(\rho)$.

**Definition 2.3.** A weighted concurrent game structure (WCGS) is a tuple $\mathcal{G} = \langle \text{AP}, \text{Agt}, \text{Act}, V, v_i, \Delta, w \rangle$ where AP is a finite set of atomic propositions, $\langle \text{Agt}, \text{Act}, V, v_i, \Delta \rangle$ is a CGS, and $w: V \rightarrow [0, 1]^{\text{AP}}$ is a weight function.

In a WCGS, for each position $v \in V$ and atomic proposition $p \in \text{AP}$, the value $w(v)(p)$ indicates the degree to which $p$ holds in $v$. We now define the semantics of SL[$\mathcal{F}$].

**Definition 2.4.** Consider a WCGS $\mathcal{G} = \langle \text{AP}, \text{Agt}, \text{Act}, V, v_i, \Delta, w \rangle$, a set of variables Var, and a partial assignment $\chi$ of strategies for Agt and Var. Given an SL[$\mathcal{F}$] state formula $\varphi$ and a history $\rho$, we use $\langle \{\varphi\}^G_\chi(\rho) \rangle$ to denote the satisfaction value of $\varphi$ in the last state of $\rho$ under the assignment $\chi$. Given an SL[$\mathcal{F}$] path formula $\psi$, a play $\pi$, and a point in time $i \in \mathbb{N}$, we use $\langle \{\psi\}^G_\chi(\pi, i) \rangle$ to denote the satisfaction value of $\psi$ in the suffix of $\pi$ that starts in position $i$. The satisfaction value is defined inductively as follows:

$$ \langle p \rangle^G_\chi(\rho) = w(\text{last}(\rho))(p) $$

$$ \langle \langle x \rangle \rangle^G_\chi(\rho) = \sup_{\sigma \in \text{Str}_\mathcal{G}} \langle \varphi \rangle^G_\chi(x \mapsto \sigma)(\rho) $$

$$ \langle (a, x) \varphi \rangle^G_\chi(\rho) = \langle \varphi \rangle^G_\chi(x \mapsto \chi(x))(\rho) $$
$$
\begin{align*}
\{\{\mathrm{E}\psi\}\}_{\chi}^{\mathcal{G}}(\rho) &= \sup_{\pi \in \mathrm{Out}(\chi, \rho)} \{\{\psi\}\}_{\chi}^{\mathcal{G}}(\pi, |\rho| - 1) \\
\{\{f(\varphi_1, \dots, \varphi_m)\}\}_{\chi}^{\mathcal{G}}(\rho) &= f(\{\varphi_1\}_{\chi}^{\mathcal{G}}(\rho), \dots, \{\varphi_m\}_{\chi}^{\mathcal{G}}(\rho)) \\
\{\{\varphi\}\}_{\chi}^{\mathcal{G}}(\pi, i) &= \{\varphi\}_{\chi}^{\mathcal{G}}(\pi \le i) \\
\{\{\mathbf{X}\psi\}\}_{\chi}^{\mathcal{G}}(\pi, i) &= \{\psi\}_{\chi}^{\mathcal{G}}(\pi, i + 1) \\
\{\psi_1 \mathrm{U}\psi_2\}_{\chi}^{\mathcal{G}}(\pi, i) &= \sup_{j \ge i} \min_{k \in [i, j-1]} \left( \{\varphi_2\}_{\chi}^{\mathcal{G}}(\pi, j), \min_{k \in [i, j-1]} \{\varphi_1\}_{\chi}^{\mathcal{G}}(\pi, k) \right) \\
\{f(\psi_1, \dots, \psi_m)\}_{\chi}^{\mathcal{G}}(\pi, i) &= f(\{\psi_1\}_{\chi}^{\mathcal{G}}(\pi, i), \dots, \{\psi_m\}_{\chi}^{\mathcal{G}}(\pi, i))
\end{align*}
$$

Strategy quantification $\langle\langle x \rangle\rangle\varphi$ computes the maximal value a choice of strategy for variable $x$ can give to formula $\varphi$. Dually, $[[x]]\varphi$ computes the minimal value a choice of strategy for variable $x$ can give to formula $\varphi$. Binding $(a, x)\varphi$ just assigns strategy given by $x$ to agent $a$. The branching quantifier $\mathrm{E}\psi$ computes the supremum value on all possible outcomes of the strategies currently assigned. Temporal modality $\mathbf{X}\psi$ takes the value of $\psi$ at the next step of a given outcome, while $\psi_1\mathrm{U}\psi_2$ maximizes, over all positions along the play, the minimum between the value of $\psi_2$ at that position and the minimal value of $\psi_1$ before this position.

In a Boolean setting, we recover the standard semantics of SL. Also the fragment of SL[$\mathcal{F}$] with only temporal operators and functions $\vee$ and $\neg$ corresponds to Fuzzy Linear-time Temporal Logic [49, 59]. Note that by equipping $\mathcal{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 [49]). 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 $\varphi$, as is the case when a model is chosen, the set of possible satisfaction values for subformulas of $\varphi$ becomes finite. Therefore, the suprema in the above definition are in fact maxima.

For a state formula $\varphi$ and a weighted game structure $\mathcal{G}$, we write $\{\{\varphi\}\}^{\mathcal{G}}$ for $\{\{\varphi\}\}_{\emptyset}^{\mathcal{G}}(v_t)$.

## 2.3 Model checking

The problem we are interested in is the following generalisation of the model checking problem, which is solved in [3] for LTL[$\mathcal{F}$] and CTL*[[$\mathcal{F}$]].

**Definition 2.5 (Model-checking problem).** Given an SL[$\mathcal{F}$] state formula $\varphi$, a WCGS $\mathcal{G}$ and a predicate $P \subseteq [0, 1]$, decide whether $\{\{\varphi\}\}^{\mathcal{G}} \in P$.

In the sequel, we require that deciding whether a rational value $v$ is in $P$ can be done in time polynomial in the size of the representation of $v$ and $P$. As a typical example, if $P$ is a finite union of intervals with rational bounds (given explicitly), then membership in $P$ 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 $\varphi$, written $\mathrm{bnd}(\varphi)$, 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.
**Definition 2.6.** Formally, bnd($\varphi$) is defined inductively as follows:

$$
\begin{align*}
\text{bnd}(p) &= 0 \\
\text{bnd}(\langle\langle x \rangle\rangle \varphi) &= \begin{cases} \text{bnd}(\varphi) & \text{if } \varphi = \langle\langle y \rangle\rangle \varphi' \text{ for some } y \in \text{Var} \\ 1 + \text{bnd}(\varphi) & \text{otherwise} \end{cases} \\
\text{bnd}((a, x)\varphi) &= \text{bnd}(\varphi) \\
\text{bnd}(f(\varphi_1, \dots, \varphi_k)) &= \max\{\text{bnd}(\varphi_i) \mid 1 \le i \le k\} \\
\text{bnd}(E\psi) &= \text{bnd}(\psi) \\
\text{bnd}(X\psi) &= \text{bnd}(\psi) \\
\text{bnd}(\psi U \psi') &= \max\{\text{bnd}(\psi), \text{bnd}(\psi')\}
\end{align*}
$$

**Example 2.7.** Here are a few examples of block-nesting depth of some formulas.

$$
\begin{align*}
\text{bnd}(\langle\langle x \rangle\rangle \langle\langle y \rangle\rangle (a, x)(b, y) \text{EFp}) &= 1 \\
\text{bnd}(\langle\langle x \rangle\rangle \langle\langle y \rangle\rangle \langle\langle z \rangle\rangle (a, x)(b, y)(c, z) \text{EFp}) &= 1 \\
\text{bnd}(\langle\langle x \rangle\rangle \langle\langle y \rangle\rangle [[z]](a, x)(b, y)(c, z) \text{EFp}) &= 2 \\
\text{bnd}(\langle\langle x \rangle\rangle \langle\langle y \rangle\rangle (a, x)(b, y) \text{EF} \langle\langle z \rangle\rangle (c, z) \text{AGq}) &= 2
\end{align*}
$$

**THEOREM 2.8.** *The model-checking problem for SL[$\mathcal{F}$] is decidable. It is (k + 1)-EXPTIME-complete for formulas of block nesting depth at most k.*

**2.4 What can SL[$\mathcal{F}$] express?**

SL[$\mathcal{F}$] naturally embeds SL. Indeed, if the values of the atomic propositions are in {0, 1} and the only allowed functions in $\mathcal{F}$ are $\lor$, $\land$, and $\neg$, 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.

**2.4.1 Drone battle.** A “carrier” drone *c* helped by a “guard” drone *g* try to bring an artifact to a rescue point and keep it away from the “villain” adversarial drone *v*. They evolve in a three-dimensional unit cube, in which coordinates are triples $\vec{\gamma} = (\gamma_1, \gamma_2, \gamma_3) \in [0, 1]^3$. We use the triples of atomic propositions $p_{\vec{\gamma}} = (p_{\gamma_1}, p_{\gamma_2}, p_{\gamma_3})$ and $q_{\vec{\gamma}} = (q_{\gamma_1}, q_{\gamma_2}, q_{\gamma_3})$ to denote the coordinates of *c* and *v*, respectively. Write dist: $[0, 1]^3 \times [0, 1]^3 \rightarrow [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[$\mathcal{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

$$
\varphi_{\text{rescue}} = \langle\langle x \rangle\rangle \langle\langle y \rangle\rangle (c, x)(g, y) \text{ A}(\text{dist}(p_{\vec{\gamma}}, q_{\vec{\gamma}})\text{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[$\mathcal{F}$] specification is 0 along any path in which the artifact is never rescued.

Notice that formula $\varphi_{\text{rescue}}$ above can be expressed in the extension ATL\*[$\mathcal{F}$] of ATL\* with functions. ATL\* is a syntactic fragment of SL in which strategy quantifications are constrained to be of the following form:

$$
\langle\langle x_1 \rangle\rangle \cdots \langle\langle x_k \rangle\rangle [[x_{k+1}]] \cdots [[x_n]] (a_{v(1)}, x_1) \cdots (a_{v(n)}, x_n) \varphi
$$

where $Agt = \{x_i | 1 \le i \le n\}$ and $v: [1, n] \rightarrow [1, n]$ is a permutation. In other terms, existential strategy quantification in ATL\* (and ATL\*[$\mathcal{F}$]) assigns a new strategy to a subset of the players,
and drops the strategies previously assigned to the other players. Notice that in $\varphi_{\text{rescue}}$, the universal strategy quantification and assignment for Agent v is implicit, and is actually hidden in the path quantifier A: $\varphi_{\text{rescue}}$ is equivalent to

$$ \langle\langle x \rangle\rangle \langle\langle y \rangle\rangle [[z]] (c, x)(g, y)(v, z) A(\text{dist}(p_{\vec{y}}, q_{\vec{y}}) \text{U safe}) $$

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:

$$ \varphi_{\text{spy}} = \langle\langle x \rangle\rangle [[z]] \langle\langle y \rangle\rangle (c, x)(g, y)(v, z) A(\text{dist}(p_{\vec{y}}, q_{\vec{y}}) \text{U safe}) $$

Note that this formula $\varphi_{\text{spy}}$ cannot be expressed in ATL\*[$\mathcal{F}$], that cannot capture alternation of strategy quantification because each strategic quantifier resets previously assigned strategies, while SL[$\mathcal{F}$] inherits from SL the possibility to freely alternate existential and universal quantifications on strategies in a first-order fashion. In fact $\varphi_{\text{spy}}$ actually belongs to the fragment SL$_{1G}$[$\mathcal{F}$], which we study in Section 6.

### 2.4.2 Synthesis with quantitative objectives.
The problem of synthesis for LTL specifications dates back to [73]. 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 $\psi$ 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 $\psi$. Recently, this problem has been addressed in the context of LTL[$\mathcal{F}$], where the controller aims at maximizing the value of an LTL[$\mathcal{F}$] formula $\psi$, while the environment acts as minimizer. Both problems can be easily represented in SL and SL[$\mathcal{F}$] respectively, with the formula

$$ \varphi_{\text{synt}} = \langle\langle x \rangle\rangle [[y]] (c, x)(e, y) A\psi $$

where c and e are the controller and environment agent, respectively, and $\psi$ the temporal specification expressed in either LTL or LTL[$\mathcal{F}$].

Assume now that controller and environment are both composed of more than one agent, namely $c_1, \dots, c_n$ and $e_1, \dots, e_n$, 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 $c_k$ depends on the strategies selected by agents $e_j$, for every $j < k$. We can write an SL[$\mathcal{F}$] formula to represent this generalized synthesis problem as follows:

$$ \varphi_{\text{synt}} = \langle\langle x_1 \rangle\rangle [[y_1]] \dots \langle\langle x_n \rangle\rangle [[y_n]] (c_1, x_1)(e_1, y_1) \dots (c_n, x_n)(e_n, y_n) A\psi. $$

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 $\varphi_{\text{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[$\mathcal{F}$], but in a much stronger sense: first, objectives in SL[$\mathcal{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 $a_i \in \text{Agt}$ is given as an LTL[$\mathcal{F}$] formula $\psi_i$. Define function $\leq: [0, 1]^2 \to [0, 1]$ such that (using infix notation) $\alpha \leq \beta$ equals 1 if $\alpha \leq \beta$, and equals 0 otherwise. We define the following formula, for a family $(x_i)_{a_i \in \text{Agt}}$ of variables:

$$ \varphi_{\text{NE}}((x_i)_{a_i \in \text{Agt}}) = (a_1, x_1) \dots (a_n, x_n) \bigwedge_{a_i \in \text{Agt}} [[y_i]] ((a_i, y_i) \mathbf{A} \psi_i) \leq \mathbf{A} \psi_i $$

If assignment $\chi$ maps each $x_i$ to some strategy $\sigma_i$, then the strategy profile $(\sigma_i)_{a_i \in \text{Agt}}$ is a NE if, and only if, $\varphi_{\text{NE}}$ evaluates to 1 under assignment $\chi$. Indeed, because $[[y_i]]$ minimizes its subformula over all strategies $y_i$, formula $[[y_i]]$ $((a_i, y_i) \mathbf{A} \psi_i) \leq \mathbf{A} \psi_i$ evaluates to 1 if, and only if, for all strategies $y_i$, $((a_i, y_i) \mathbf{A} \psi_i) \leq \mathbf{A} \psi_i$ evaluates to 1, i.e., $y_i$ is not a profitable deviation for agent $a_i$. Notice that, since $\langle\langle y_i \rangle\rangle$ maximizes over $y_i$, formula<fnref n="1" /> $\langle\langle y_i \rangle\rangle$ $(a_i, y_i) \mathbf{A} \psi_i) \leq \mathbf{A} \psi_i$ evaluates to 1 if, and only if, the best deviation for $a_i$ is not profitable, and thus no deviations are profitable. Thus we could equivalently characterise NEs with

$$ \varphi'_{\text{NE}}((x_i)_{a_i \in \text{Agt}}) = (a_1, x_1) \dots (a_n, x_n) \bigwedge_{a_i \in \text{Agt}} (\langle\langle y_i \rangle\rangle (a_i, y_i) \mathbf{A} \psi_i) \leq \mathbf{A} \psi_i $$

**2.4.4 $\varepsilon$-equilibria in weighted games.** Adopting a more quantitative point of view, we can measure how much agent $i$ can benefit from a selfish deviation using formula $\langle\langle y_i \rangle\rangle \text{diff}((a_i, y_i)\psi_i, \psi_i)$, where $\text{diff}(x, y) = \max\{0, x - y\}^2$. The maximal benefit that some agent may get is then captured by the following formula:

$$ \varphi_{\overline{\text{NE}}}((x_i)_{a_i \in \text{Agt}}) = \langle\langle y \rangle\rangle (a_1, x_1) \dots (a_n, x_n) \bigvee_{a_i \in \text{Agt}} \text{diff}((a_i, y)\mathbf{A}\psi_i, \mathbf{A}\psi_i). $$

As previously, a strategy profile $(\sigma_i)_{a_i \in \text{Agt}}$ is a NE if, and only if, under the assignment $\chi$ that maps each $x_i$ to $\sigma_i$, formula $\varphi_{\overline{\text{NE}}}$ evaluates to 0. Interestingly, formula $\varphi_{\overline{\text{NE}}}$ can be used to characterise $\varepsilon$-NE: a strategy profile in $\chi$ is an $\varepsilon$-NE if, and only if, $\varphi_{\overline{\text{NE}}}$ takes value less than or equal to $\varepsilon$ under assignment $\chi$.

**2.4.5 Secure equilibria in weighted games.** Secure equilibria [30] are special kinds of NEs in two-player games, where besides improving their objectives, the agents also try to harm their opponent. Following the ideas above, we characterise secure equilibria in SL[$\mathcal{F}$] as follows:

$$ \varphi_{\text{SE}}(x_1, x_2) = (a_1, x_1)(a_2, x_2) \bigwedge_{i \in \{1, 2\}} [[y]] ((a_i, y)\mathbf{A}\psi_1, (a_i, y)\mathbf{A}\psi_2) \leq_i (\mathbf{A}\psi_1, \mathbf{A}\psi_2) $$

where $(\alpha_1, \alpha_2) \leq_i (\beta_1, \beta_2)$ is 1 when $(\alpha_i \leq \beta_i) \lor (\alpha_i = \beta_i \land \alpha_{3-i} \leq \beta_{3-i})$, and 0 otherwise.

Secure equilibria have also been studied in $\mathbb{Q}$-weighted games [26]: 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 $w$, the value of formula $\mathbf{G}w$ is the infimum of the weights, while the value of $\mathbf{F}Gw$ 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 $\varphi_{\text{SE}}$.

<footnote n="1">¹Notice how parentheses are placed differently here, including $\langle\langle y_i \rangle\rangle$ in the first argument of $\leq$.</footnote>

<footnote n="2">²We use max here only because our functions are required to return values in $[0, 1]$. In the way we use diff in $\varphi_{\overline{\text{NE}}}$, the first argument will always be larger than or equal to the second one.</footnote>
Other classical properties of games can be expressed, such as doomsday equilibria (which generalise winning secure equilibria in n-player games) [29], robust Nash equilibria (considering profitable deviations of coalitions of agents) [21], or strategy dominance and admissibility [14, 23], to cite a few.

### 2.4.6 Rational synthesis.
Weak rational synthesis [6, 47, 56] aims at synthesizing a strategy profile for a controller $c_0$ and the $n$ components $(c_i)_{1 \le i \le n}$ constituting the environment, in such a way that (1) the whole system satisfies some objective $\psi_0$, and (2) under the strategy of the controller, the strategies of the $n$ components form a Nash equilibrium (or any given solution concept) for their own individual objectives $(\psi_i)_{1 \le i \le n}$.

That a given strategy profile $(x_i)_{c_i \in \mathcal{A}_{\text{gt}}}$ satisfies the two conditions above can be expressed as follows:

$$ \varphi_{\text{wRS}}((x_i)_{0 \le i \le n}) = (c_0, x_0)(c_1, x_1) \dots (c_n, x_n) [\mathbf{A}\psi_0 \wedge \varphi_{\text{NE}}((x_i)_{1 \le i \le n})] $$

The formula returns the minimum between the satisfaction value of $\psi_0$ and that of $\varphi_{\text{NE}}((x_i)_{1 \le i \le n})$. Thus, the satisfaction value of $\varphi_{\text{wRS}}$ is zero if the strategy profile $(x_i)_{1 \le i \le n}$ is not a NE under strategy $x_0$ assigned to $c_0$, and it returns the satisfaction value of $\psi_0$ under the whole strategy profile otherwise. Then the value of

$$ \langle\langle x_0 \rangle\rangle \langle\langle x_1 \rangle\rangle \dots \langle\langle x_n \rangle\rangle \varphi_{\text{wRS}}((x_i)_{0 \le i \le n}) $$

is the best value that the system can collectively achieve for $\psi_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[$\mathcal{F}$].

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

$$ \varphi_{\text{sRS}}(x_0) = [[x_1]] \dots [[x_n]] (c_0, x_0)(c_1, x_1) \dots (c_n, x_n) \mathbf{A}[\neg \varphi_{\text{NE}}((x_i)_{1 \le i \le n}) \lor \psi_0] $$

The disjunction in this formula returns the maximum value between $\neg \varphi_{\text{NE}}((x_i)_{1 \le i \le n})$ and $\psi_0$: if $(x_i)_{1 \le i \le n}$ is a NE, it returns the value of $\psi_0$, and it returns 1 otherwise. The value of $\varphi_{\text{sRS}}(x_0)$ then is the smallest value that $\psi_0$ may take when players $(a_i)_{1 \le i \le n}$ play according to a NE (if any). Finally, the value of

$$ \langle\langle x_0 \rangle\rangle \varphi_{\text{sRS}}(x_0) $$

is the best value of $\psi_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 [6], the objective formula $\psi_0$ above can be used to capture well-studied social-welfare functions [70]. Typical examples of that are the *utilitarian social-welfare function*

$$ \psi_0^{\text{util}} = \frac{1}{n} \sum_{i=1}^{n} \psi_i $$

taking the average payoff of the agents, and the *egalitarian social-welfare function*

$$ \psi_0^{\text{egal}} = \min_{i=1,\dots,n} \{\psi_i\} $$

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[$\mathcal{F}$] can also
evaluate such combinations of the two functions. For instance, a linear combination is represented as

$$ \psi_0^{\text{linear}} = \lambda \cdot \psi_0^{\text{util}} + (1 - \lambda) \cdot \psi_0^{\text{egal}} $$

where the parameter $\lambda$ ranges between 0 and 1. As noted in [6], when $\psi_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[$\mathcal{F}$] allows us to move even further. For a given social-welfare function represented by a formula $\psi_0$ and a strategy $x_0$ for the controller, the formula

$$ \text{OPT}(x_0) = \langle\langle x_1 \rangle\rangle \dots \langle\langle x_n \rangle\rangle (c_1, x_1) \dots (c_n, x_n) \psi_0 $$

denotes the parameterised social optimum, that is, the best value of the social-welfare function, when the strategy $x_0$ of the controller $c_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[$\mathcal{F}$] as follows:

$$ \begin{aligned} \text{PoS}^{-1}(x_0) &= \frac{\langle\langle x_1 \rangle\rangle \dots \langle\langle x_n \rangle\rangle (\varphi_{\text{NE}}(x_1, \dots, x_n) \land \psi_0)}{\text{OPT}(x_0)} \\ \text{PoA}^{-1}(x_0) &= \frac{[[x_1]] \dots [[x_n]] (\neg \varphi_{\text{NE}}(x_1, \dots, x_n) \lor \psi_0)}{\text{OPT}(x_0)} \end{aligned} $$

Therefore, equivalently to minimizing such prices, the controller is interested in maximizing their inverses. We have the following

$$ \text{BestPoS} = \langle\langle x_0 \rangle\rangle \text{PoS}(x_0) $$

$$ \text{BestPoA} = \langle\langle x_0 \rangle\rangle \text{PoA}(x_0) $$

### 2.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 $(x_i)_{a_i \in \text{Agt}}$, a coalition $C \subseteq \text{Agt}$ has a beneficial deviation $(y_i)_{a_i \in C}$ if, for all strategy profiles $(z_i)_{a_i \in \text{Agt} \setminus C}$ and for all $a_i \in C$, it holds that $(x_i)_{a_i \in \text{Agt}} \psi_i < (y_i)_{a_i \in C} (z_i)_{a_i \in \text{Agt} \setminus C} \psi_i$. We say that a strategy profile $(x_i)_{a_i \in \text{Agt}}$ is a core equilibrium if, for every coalition, there is no beneficial deviation. This can be written in SL[$\mathcal{F}$] as follows:

$$ \varphi_{\text{core}}(x_i)_{a_i \in \text{Agt}} = \bigwedge_{C \subseteq \text{Agt}} [[y_i]]_{a_i \in C} \langle\langle y_i \rangle\rangle_{a_j \in \text{Agt} \setminus C} \left( \bigwedge_{a_j \in C} (a_i, y_i)_{a_i \in \text{Agt}} \psi_j \le (a_i, x_i)_{a_i \in \text{Agt}} \psi_j \right) $$

The strategy profile $(x_i)_{a_i \in \text{Agt}}$ is a core equilibrium if, and only if, the formula $\varphi_{\text{core}}(x_i)_{a_i \in \text{Agt}}$ evaluates to 1. The existence of a core equilibrium could then be expressed with the formula $\langle\langle x_1 \rangle\rangle \dots \langle\langle x_n \rangle\rangle \varphi_{\text{core}}(x_i)_{a_i \in \text{Agt}}$, which takes value 1 if, and only if, there exists a core equilibrium.

<footnote>$^3$This is assuming that payoffs are always positive, which is the case in this paper.</footnote>
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 [83]. 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.

3 QUANTIFIED CTL*[F]

In this section we introduce Quantified CTL*[F] (QCTL*[F], for short) which extends both CTL*[F] and QCTL* [60]. 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 model-checking 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 [9] 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).

3.1 Syntax

Let $\mathcal{F} \subseteq \{f : [0, 1]^m \to [0, 1] \mid m \in \mathbb{N}\}$ 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:

$$ \varphi ::= p \mid \exists p. \varphi \mid E\psi \mid f(\varphi, \dots, \varphi) $$

$$ \psi ::= \varphi \mid X\psi \mid \psi U \psi \mid f(\psi, \dots, \psi) $$

where *p* ranges over AP and *f* over *F*.

Formulas of type $\varphi$ are called *state formulas*, those of type $\psi$ 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 $\varphi$, then we say that $\varphi$ is *closed*. We again use $\top$, $\vee$, and $\neg$ to denote functions 1, max and 1-x, as well as classic abbreviations already introduced for SL[F].

3.2 Semantics

QCTL*[F] formulas are evaluated on unfoldings of weighted Kripke structures.

*Definition 3.2.* A *weighted Kripke structure* (WKS) is a tuple $\mathcal{K} = \langle \mathrm{AP}, S, s_i, R, w \rangle$ where AP is a finite set of atomic propositions, S is a finite set of states, $s_i \in S$ is an initial state, $R \subseteq S \times S$ is a left-total<fnref n="4" /> transition relation, and $w: S \to [0, 1]^{\mathrm{AP}}$ is a weight function.

<footnote n="4">⁴i.e., for all $s \in S$, there exists $s'$ such that $(s, s') \in R$.</footnote>
A path in $\mathcal{K}$ is an infinite word $\pi = \pi_0\pi_1...$ over $S$ such that $\pi_0 = s_l$ and $(\pi_i, \pi_{i+1}) \in R$ for all $i$. By analogy with concurrent game structures we call finite prefixes of paths *histories*, and write $\text{Hist}_{\mathcal{K}}$ for the set of all histories in $\mathcal{K}$. We also let $\text{Val}_{\mathcal{K}} = \{\text{w}(s)(p) \mid s \in S \text{ and } p \in \text{AP}\}$ be the finite set of values appearing in $\mathcal{K}$.

Given finite nonempty sets $D$ of directions, AP of atomic propositions, and $\mathcal{V} \subseteq [0, 1]$ of possible values, a $\mathcal{V}^{\text{AP}}$-labeled $D$-tree, (or $(\mathcal{V}^{\text{AP}}, D)$-tree for short, or $\mathcal{V}^{\text{AP}}$-tree when directions are understood), is a pair $t = (\tau, w)$ where $\tau \subseteq D^+$ is closed under non-empty prefixes, all nodes $u \in \tau$ start with the same direction $r$, called the *root*, and have at least one child $u \cdot d \in \tau$, and $w : \tau \to \mathcal{V}^{\text{AP}}$ is a *weight function*. We let $\text{Val}_t \subseteq \mathcal{V}$ be the image of $w$ on $\tau$. A branch $\lambda = u_0u_1...$ is an infinite sequence of nodes such that for all $i \ge 0$, $u_{i+1}$ is a child of $u_i$. We let $\text{Br}(u)$ be the set of branches that start in node $u$.

A tree $t = (\tau, w)$ is *complete* if for all node $u \in \tau$ and direction $d \in D$, we have $u \cdot d \in \tau$. Given a $\mathcal{V}^{\text{AP}}$-labeled $D$-tree $t = (\tau, w)$, we let $\bar{t} = (\bar{\tau}, \bar{w})$ be the only complete $\mathcal{V}^{\text{AP}} \cup \{\bullet\}$-labeled $D$-tree such that for all $u \in \tau$, $\bar{w}(u) = w(u)$, and for all $u \in \bar{\tau} \setminus \tau$, $\bar{w}(u) = \{\bullet\}$, where $\bullet$ 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 $(t, u)$ where $u$ is a node in $t$. We say that a tree $t = (\tau, w)$ is *Boolean in $p$* if for all $u \in \tau$ we have $w(u)(p) \in \{0, 1\}$. As with weighted Kripke structures, we let $\text{Val}_t = \{\text{w}(u)(p) \mid u \in \tau \text{ and } p \in \text{AP}\}$.

Let $p \in \text{AP}$. A *p-labeling* for a $(\mathcal{V}^{\text{AP}}, D)$-tree $t = (\tau, w)$ is a mapping $\ell_p : \tau \to [0, 1]$. Letting $\mathcal{V}' = \ell_p(\tau)$, the composition of $t$ with $\ell_p$ is the $((\mathcal{V} \cup \mathcal{V}')^{\text{AP}}, D)$-tree defined as $t \otimes \ell_p := (\tau, w')$, where $w'(u)(p) = \ell_p(u)$ and $w'(u)(q) = w(u)(q)$ for $q \ne p$. If $\ell_p(\tau) \subseteq \{0, 1\}$, we call $\ell_p$ a *Boolean p-labeling*.

Finally, the *tree unfolding of a weighted Kripke structure* $\mathcal{K}$ over atomic propositions AP and states $S$ is the $\text{Val}_{\mathcal{K}}^{\text{AP}}$-labeled $S$-tree $t_{\mathcal{K}} = (\text{Hist}_{\mathcal{K}}, w')$, where $w'(u) = w(\text{last}(u))$ for every $u \in \text{Hist}_{\mathcal{K}}$.

**Definition 3.3 (Semantics).** Consider finite sets $D$ of directions, AP of atomic propositions, and $\mathcal{V} \subseteq [0, 1]$ of possible values. We fix a $\mathcal{V}^{\text{AP}}$-labeled $D$-tree $t = (\tau, w)$. Given a $\text{QCTL}^*[\mathcal{F}]$ state formula $\varphi$ and a node $u$ of $t$, we use $\{\varphi\}^t(u)$ to denote the satisfaction value of $\varphi$ in node $u$. Given a $\text{QCTL}^*[\mathcal{F}]$ path formula $\psi$ and a branch $\lambda$ of $\tau$, we use $\{\psi\}^t(\lambda)$ to denote the satisfaction value of $\psi$ along $\lambda$. The satisfaction value is defined inductively as follows:

$$
\begin{align*}
\{\!\{p\}\!\}^t(u) &= w(u)(p) \\
\{\!\exists p. \varphi\!\}^t(u) &= \sup_{\ell_p : \tau \to [0,1]} \{\varphi\}^{t \otimes \ell_p}(u) \\
\{\!\text{E}\psi\!\}^t(u) &= \sup_{\lambda \in \text{Br}(u)} \{\psi\}^t(\lambda) \\
\{\!f(\varphi_1, \dots, \varphi_n)\!\}^t(u) &= f(\{\!\varphi_1\!\}^t(u), \dots, \{\!\varphi_n\!\}^t(u)) \\
\{\!\varphi\!\}^t(\lambda) &= \{\!\varphi\!\}^t(\lambda_0) \text{ where } \lambda_0 \text{ is the first node of } \lambda \\
\{\!\mathbf{X}\psi\!\}^t(\lambda) &= \{\!\psi\!\}^t(\lambda_{\ge 1}) \\
\{\!\psi_1\mathbf{U}\psi_2\!\}^t(\lambda) &= \sup_{i \ge 0} \min(\{\!\psi_2\!\}^t(\lambda_{\ge i}), \min_{0 \le j < i} \{\!\psi_1\!\}^t(\lambda_{\ge j})) \\
\{\!f(\psi_1, \dots, \psi_n)\!\}^t(\lambda) &= f(\{\!\psi_1\!\}^t(\lambda), \dots, \{\!\psi_n\!\}^t(\lambda))
\end{align*}
$$

$\text{BQCTL}^*$ has the same syntax as $\text{QCTL}^*$. Its semantics, which we write $\{\!\cdot\!\}^t_{\text{B}}(\cdot)$, only differs with $\{\!\cdot\!\}^t(\cdot)$ in the case of quantification on propositions, which is defined as follows:

$$
\{\!\exists p. \varphi\!\}^t_{\text{B}}(u) = \sup_{\ell_p : \tau \to \{0,1\}} \{\varphi\}^{t \otimes \ell_p}_{\text{B}}(u)
$$
For a tree $t$ with root $r$ we write $\{\phi\}^t$ for $\{\phi\}^t(r)$, for a weighted Kripke structure $\mathcal{K}$ we write $\{\phi\}^\mathcal{K}$ for $\{\phi\}^{t_\mathcal{K}}$, and similarly for $\{\phi\}_B^t$ and $\{\phi\}_B^\mathcal{K}$.

We will also consider the logic QLTL[$\mathcal{F}$] and its fragment LTL[$\mathcal{F}$], which we define now.

**Definition 3.4.** The syntax of QLTL[$\mathcal{F}$] is defined with respect to a finite set AP of atomic propositions, using the following grammar:

$$ \psi ::= p \mid X\psi \mid \psi U\psi \mid \exists p. \varphi \mid f(\psi, \dots, \psi) $$

where $p$ ranges over AP and $f$ over $\mathcal{F}$.

The semantics of a QLTL[$\mathcal{F}$] formula is defined on an infinite sequence of weight assignments for atoms in AP: given a path $\pi \in ([0, 1]^{\mathrm{AP}})^\omega$, the satisfaction value of a QLTL formula $\psi$ over $\pi$ is defined as expected and written $\{\psi\}(\pi)$. We write $\psi \equiv \psi'$ if $\{\psi\}(\pi) = \{\psi'\}(\pi)$ for all $\pi \in ([0, 1]^{\mathrm{AP}})^\omega$, and we define the satisfaction value $\{\psi\}(\mathcal{K})$ of a QLTL[$\mathcal{F}$] formula $\psi$ on a Kripke structure $\mathcal{K}$ as the infimum of its satisfaction value over all paths of $\mathcal{K}$.

The logic LTL[$\mathcal{F}$] is the fragment of QLTL[$\mathcal{F}$] obtained by removing quantification on atomic propositions.

## 3.3 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 [60] for more detail). Since in this work we consider perfect-recall strategies, we based the semantics of QCTL\*[$\mathcal{F}$] (and thus BQCTL\*[$\mathcal{F}$]) on the tree semantics for QCTL\*.

Actually, if $\mathcal{F} = \{\tau, \vee, \neg\}$, then BQCTL\*[$\mathcal{F}$] evaluated on Boolean Kripke structures corresponds precisely to QCTL\* with tree semantics [60].

Note that even with quantification restricted to Boolean valuations, BQCTL\*[$\mathcal{F}$] is still quantitative: instead of merely stating the existence of a satisfying Boolean $p$-labeling, $\exists p. \varphi$ maximizes the satisfaction value of $\varphi$ over all possible Boolean $p$-labelings.

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

$$ \exists^{\mathrm{B}} p. \varphi := \exists p. (\mathrm{AG} \ \mathrm{Bool}(p) \wedge \varphi) $$

We then have that for all $\varphi \in \mathrm{QCTL}^*[$\mathcal{F}$] such that $\varphi$ does not contain a propositional quantifier, for all $(\mathcal{V}^{\mathrm{AP}}, \mathrm{D})$-tree $t$ and node $u \in t$, $\{\exists^{\mathrm{B}} p. \varphi\}^t(u) = \{\exists p. \varphi\}_B^t(u)$. It follows that:

**LEMMA 3.5.** For every BQCTL\* formula $\varphi$, letting $\varphi_B$ be the QCTL\* formula obtained from $\varphi$ by replacing inductively each $\exists p. \varphi'$ in $\varphi$ with $\exists^{\mathrm{B}} p. \varphi'_B$, we have that for all $(\mathcal{V}^{\mathrm{AP}}, \mathrm{D})$-tree $t$ and node $u \in t$,

$$ \{\varphi\}_B^t(u) = \{\varphi_B\}^t(u) $$

Therefore BQCTL\*[$\mathcal{F}$] $\subseteq$ QCTL\*[$\mathcal{F} \cup \{\mathrm{Bool}\}$], in the sense that every formula in BQCTL\*[$\mathcal{F}$] has an equivalent in QCTL\*[$\mathcal{F} \cup \{\mathrm{Bool}\}$]. We now announce our main results on the model-checking problem for these logics. Together, they imply that the latter inequality is strict, in the sense that there is no computable translation from QCTL\*[$\mathcal{F}$] to BQCTL\*[$\mathcal{F}$].
## 3.4 Model-checking problem

*Definition 3.6.* The quantitative model-checking problem for QCTL\*[$\mathcal{F}$] (resp. BQCTL\*[$\mathcal{F}$]) consists in, given a QCTL\*[$\mathcal{F}$] state formula $\varphi$, a weighted Kripke structure $\mathcal{K}$, and a predicate $P \subseteq [0, 1]$, decide whether $\{\varphi\}^\mathcal{K} \in P$ (resp. $\{\varphi\}^\mathcal{B}^\mathcal{K} \in P$).

Similarly to SL[$\mathcal{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 $\varphi$, and is written bnd($\varphi$).

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.3.

**THEOREM 3.7.** *The quantitative model-checking problem for BQCTL\*[$\mathcal{F}$] is decidable. It is (k + 1)-EXPTIME-complete for formulas of block nesting depth at most k.*

**THEOREM 3.8.** *The quantitative model-checking problem for QCTL\*[$\mathcal{F}$] is undecidable if $\mathcal{F}$ contains the functions $(x, y) \mapsto x = y$ and $(x, y) \mapsto y = x/2$.*

Theorem 3.7 is proved in the next section. Together with a reduction from SL[$\mathcal{F}$] to BQCTL\*[$\mathcal{F}$] that we present in Section 5, it entails the decidability of model checking SL[$\mathcal{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\*[$\mathcal{F}$].

# 4 MODEL CHECKING BQCTL\*[$\mathcal{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\*[$\mathcal{F}$], which is crucial in the automata construction that we then present to solve the model-checking problem.

## 4.1 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 $G = (V, E, v_i, C)$, where the set of states $V = V_E \uplus V_A$ is partitioned between states of Eve ($V_E$) and those of Adam ($V_A$), $E \subseteq V \times V$ is a set of *moves*, $v_i$ is an initial state and $C: V \to \mathbb{N}$ is a *coloring function* of finite codomain. In states $V_E$, Eve chooses the next state, while Adam chooses in states $V_A$. A play is an infinite sequence of states $v_0v_1v_2...$ such that $v_0 = v_i$ and for all $i \ge 0$, $(v_i, v_{i+1}) \in E$ (written $v_i \to v_{i+1}$). We assume that for every $v \in V$ there exists $v' \in V$ such that $v \to v'$. A strategy for Eve is a partial function $V^* \to V$ that maps each finite prefix of a play ending in a state $v \in V_E$ to a next state $v'$ such that $v \to v'$. A play $v_0v_1v_2...$ *follows* a strategy $\sigma$ of Eve if for every $i \ge 0$ such that $v_i \in V_E$, $v_{i+1} = \sigma(v_0...v_i)$. A strategy $\sigma$ 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 $Z$, $\mathbb{B}^+(Z)$ is the set of formulas built from the elements of $Z$ as atomic propositions using the connectives $\lor$ and $\land$, and with $\top, \bot \in \mathbb{B}^+(Z)$. For convenience, we only define automata on complete trees.

Fix a set $\mathcal{V} \subseteq [0, 1]$. An alternating parity tree automaton (APT) on $(\mathcal{V}^{\text{AP}}, D)$-trees is a tuple $\mathcal{A} = (Q, \delta, q_t, C)$ where $Q$ is a finite set of states, $q_t \in Q$ is an initial state, $\delta: Q \times \mathcal{V}^{\text{AP}} \to \mathbb{B}^+(D \times Q)$ is a transition function, and $C: Q \to \mathbb{N}$ is a coloring function. A nondeterministic (resp. universal) parity tree automaton (NPT, resp. UPT) is an APT $\mathcal{A} = (Q, \delta, q_t, C)$ such that for every $q \in Q$ and $a \in \mathcal{V}^{\text{AP}}$, $\delta(q, a)$ is written in disjunctive (resp. conjunctive) normal form and for every direction $s \in D$ each disjunct (resp. conjunct) contains exactly one element of $\{s\} \times Q$.<fnref n="5" /> We may use $\mathcal{N}$ and $\mathcal{U}$ to denote, respectively, nondeterministic and universal automata. An NPT is deterministic if for each $q \in Q$ and $a \in 2^{\text{AP}}$, $\delta(q, a)$ consists of a single disjunct.

Acceptance of a pointed $(\mathcal{V}^{\text{AP}}, D)$-tree $(t, u_t)$, where $t = (\tau, w)$, by an APT $\mathcal{A} = (Q, \delta, q_t, C)$ is defined via the parity game $G(\mathcal{A}, t, u_t) = (V, E, v_t, C')$ where $V = \tau \times Q \times \mathbb{B}^+(D \times Q)$, state $(u, q, \alpha)$ belongs to Eve if $\alpha$ is of the form $\alpha_1 \lor \alpha_2$ or $[s, q']$, and to Adam otherwise, $v_t = (u_t, q_t, \delta(q_t, u_t))$, and $C'(u, q, \alpha) = C(q)$. Moves in $G(\mathcal{A}, t, u_t)$ are defined by the following rules:

$$ (u, q, \alpha_1 \dagger \alpha_2) \rightarrow (u, q, \alpha_i) \quad \text{where } \dagger \in \{\lor, \land\} \text{ and } i \in \{1, 2\}, \\ (u, q, [s, q']) \rightarrow (u \cdot s, q', \delta(q', w(u \cdot s))) $$

States of the form $(u, q, \top)$ and $(u, q, \bot)$ are sinks, winning for Eve and Adam respectively.

A pointed tree $(t, u)$ is accepted by $\mathcal{A}$ if Eve has a winning strategy in $G(\mathcal{A}, t, u)$, and the language of $\mathcal{A}$ is the set of pointed trees accepted by $\mathcal{A}$, written $\mathcal{L}(\mathcal{A})$. We write $t \in \mathcal{L}(\mathcal{A})$ if $(t, r) \in \mathcal{L}(\mathcal{A})$, where $r$ is the root of $t$. We also write $\overline{\mathcal{L}}$ for the complement of a language $\mathcal{L}$.

The size $|\mathcal{A}|$ of an APT $\mathcal{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 $\mathcal{A}$ and $\mathcal{A}'$ we denote $\mathcal{A} \wedge \mathcal{A}'$ (resp. $\mathcal{A} \vee \mathcal{A}'$) the APT of size linear in $|\mathcal{A}|$ and $|\mathcal{A}'|$ that accepts the intersection (resp. union) of the languages of $\mathcal{A}$ and $\mathcal{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 $\{\text{next}\}$. A parity word automaton is a parity tree automaton on $(\mathcal{V}^{\text{AP}}, \{\text{next}\})$-trees. In the case of a nondeterministic parity word automaton, transitions are represented as a mapping $\Delta: Q \times \mathcal{V}^{\text{AP}} \to 2^Q$ which, in a state $q \in Q$, reading the label $a \in \mathcal{V}^{\text{AP}}$ of the current state in the word, indicates a set of states $\Delta(q, a)$ from which Eve can choose to send in the next position of the word.

## 4.2 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 $p$, introduced by Rabin to deal with second-order monadic quantification [74], consists in letting the nondeterministic tree automaton guess in each node a valuation for $p$. We obtain an automaton that accepts an input tree if and only if there exists a $p$-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:

<footnote n="5">⁵What we call UPT here is sometimes referred to as comp{NPT} in the literature.</footnote>
**PROPOSITION 4.1.** Given an NPT $\mathcal{N}$ on $\mathcal{V}^{\text{AP}}$-labeled trees and an atomic proposition $p \in \text{AP}$, one can build in linear time an NPT $\mathcal{N} \mathcal{V}^{\exists p}$ such that

$(t, u) \in \mathcal{L}(\mathcal{N} \mathcal{V}^{\exists p}) \text{ iff there exists a Boolean } p\text{-labeling } \ell_p \text{ for } t \text{ s.t. } (t \otimes \ell_p, u) \in \mathcal{L}(\mathcal{N}).$

Given a UPT $\mathcal{N}$ on $\mathcal{V}^{\text{AP}}$-labeled trees and an atomic proposition $p \in \text{AP}$, one can build in linear time a UPT $\mathcal{U} \mathcal{V}^{\forall p}$ such that

$(t, u) \in \mathcal{L}(\mathcal{U} \mathcal{V}^{\forall p}) \text{ iff for all Boolean } p\text{-labelings } \ell_p \text{ for } t, (t \otimes \ell_p, u) \in \mathcal{L}(\mathcal{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 [68]).** Given an APT $\mathcal{A}$, one can build in exponential time an NPT $\mathcal{N}$ and a UPT $\mathcal{U}$, both of exponential size and linear index, such that $\mathcal{L}(\mathcal{N}) = \mathcal{L}(\mathcal{U}) = \mathcal{L}(\mathcal{A})$.

**Remark 2.** Note that the simulation theorem in [68] 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 $\mathcal{A}$, one first builds in linear time an APT $\mathcal{A}'$ that accepts $\overline{\mathcal{L}(\mathcal{A})}$. Then, by the simulation theorem, one can build an NPT $\mathcal{N}$ of exponential size equivalent to $\mathcal{A}'$. Finally one builds the linear-size UPT $\mathcal{U}$ accepting $\overline{\mathcal{L}(\mathcal{N})} = \mathcal{L}(\mathcal{A})$.

## 4.3 Finiteness of possible satisfaction values

As in the case of LTL $[\mathcal{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\*[$\mathcal{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 $D$, which we thus omit in the following lemma.

**LEMMA 4.3.** Let $\mathcal{V} \subset [0, 1]$ be a finite set of values with $\{0, 1\} \subseteq \mathcal{V}$, let $\varphi$ be a BQCTL\*[$\mathcal{F}$] state formula and $\psi$ a BQCTL\*[$\mathcal{F}$] path formula, with respect to AP. Define

$$ \mathrm{Val}_{\varphi, \mathcal{V}} = \{ \{\varphi\}^t(u) \mid t \text{ is a } \mathcal{V}^{\mathrm{AP}}\text{-labeled tree and } u \in t \} $$

be the set of values taken by $\varphi$ in nodes of $\mathcal{V}^{\mathrm{AP}}$-labeled trees. Similarly, define

$$ \mathrm{Val}_{\psi, \mathcal{V}} = \{ \{\psi\}^t(\lambda) \mid t \text{ is a } \mathcal{V}^{\mathrm{AP}}\text{-labeled tree, } u \in t \text{ and } \lambda \in \mathrm{Br}(u) \} $$

Then, $|\mathrm{Val}_{\varphi, \mathcal{V}}| \le |\mathcal{V}|^{|\varphi|}$ and $|\mathrm{Val}_{\psi, \mathcal{V}}| \le |\mathcal{V}|^{|\psi|}$, and one can compute sets $\overline{\mathrm{Val}}_{\varphi, \mathcal{V}}$ and $\overline{\mathrm{Val}}_{\psi, \mathcal{V}}$ of size at most $|\mathcal{V}|^{|\varphi|}$ and $|\mathcal{V}|^{|\psi|}$ respectively, and such that $\mathrm{Val}_{\varphi, \mathcal{V}} \subseteq \overline{\mathrm{Val}}_{\varphi, \mathcal{V}}$ and $\mathrm{Val}_{\psi, \mathcal{V}} \subseteq \overline{\mathrm{Val}}_{\psi, \mathcal{V}}$.

**PROOF.** We prove the result by mutual induction on $\varphi$ and $\psi$. Clearly, $\mathrm{Val}_p = \mathcal{V}$.

For $\varphi = \exists p. \varphi'$: let $t$ be a $\mathcal{V}^{\mathrm{AP}}$-labeled tree and $u \in t$. Since $\mathrm{Val}_t \subseteq \mathcal{V}$ and by assumption $\mathcal{V}$ contains 0 and 1, for all Boolean $p$-valuation $\ell_p$ for $t$, $\mathrm{Val}_{t \otimes \ell_p} \subseteq \mathcal{V}$. It follows by definition of $\mathrm{Val}_{\varphi', \mathcal{V}}$ that for all such $\ell_p$ we have $\{\varphi'\}^{t \otimes \ell_p}(u) \in \mathrm{Val}_{\varphi', \mathcal{V}}$. Therefore $\{\exists p. \varphi'\}^t(u)$ is the supremum of a subset of $\mathrm{Val}_{\varphi', \mathcal{V}}$, which by induction hypothesis is of size at most $|\mathcal{V}|^{|\varphi'|}$. It follows that the supremum is indeed a maximum, and that $\{\exists p. \varphi'\}^t(u) \in \mathrm{Val}_{\varphi', \mathcal{V}}$. Hence, $\mathrm{Val}_{\exists p. \varphi', \mathcal{V}} \subseteq \mathrm{Val}_{\varphi', \mathcal{V}}$, and thus $|\mathrm{Val}_{\exists p. \varphi', \mathcal{V}}| \le |\mathrm{Val}_{\varphi', \mathcal{V}}| \le |\mathcal{V}|^{|\varphi'|} \le |\mathcal{V}|^{\exists p. \varphi'}$.

For $\varphi = \mathrm{E}\psi$, again $\{\mathrm{E}\psi\}^t(u)$ is a supremum over a subset of $\mathrm{Val}_{\psi, \mathcal{V}}$, which by induction hypothesis is of size at most $|\mathcal{V}|^{|\psi|}$. The supremum is thus reached, hence $\mathrm{Val}_{\mathrm{E}\psi, \mathcal{V}} \subseteq \mathrm{Val}_{\psi, \mathcal{V}}$ and $|\mathrm{Val}_{\mathrm{E}\psi, \mathcal{V}}| \le |\mathrm{Val}_{\psi, \mathcal{V}}| \le |\mathcal{V}|^{|\psi|} \le |\mathcal{V}|^{\mathrm{E}\psi}$.
For $\varphi = f(\varphi_1, \dots, \varphi_n)$, we have $Val_{\varphi, \mathcal{V}} = \{f(v_1, \dots, v_n) \mid v_i \in Val_{\varphi_i, \mathcal{V}}\}$, hence $|Val_{\varphi, \mathcal{V}}|$ is at most $\prod_{i=1}^n |Val_{\varphi_i, \mathcal{V}}|$. By induction hypothesis, we get that $|Val_{\varphi, \mathcal{V}}| \le \prod_{i=1}^n |\mathcal{V}|^{|\varphi_i|}$, which in turn is no greater than $|\mathcal{V}|^{|\varphi_1|+\dots+|\varphi_n|}$, which is no greater than $|\mathcal{V}|^{|\varphi|}$.

For $\psi = \varphi$, the result follows by hypothesis of mutual induction.

For $\psi = X\psi'$, we have that $Val_{\psi, \mathcal{V}} = Val_{\psi', \mathcal{V}}$, and the result follows.

For $\psi = \psi_1 U \psi_2$, the value of $\psi$ is defined via suprema and infima over possible values for $\psi_1$ and $\psi_2$, which are finitely many by the induction hypothesis. The suprema and infima are thus maxima and minima, and $Val_{\psi, \mathcal{V}} \subseteq Val_{\psi_1, \mathcal{V}} \cup Val_{\psi_2, \mathcal{V}}$. Hence $|Val_{\psi, \mathcal{V}}| \le |Val_{\psi_1, \mathcal{V}}| + |Val_{\psi_2, \mathcal{V}}|$, by induction hypothesis $|Val_{\psi_1, \mathcal{V}}| + |Val_{\psi_2, \mathcal{V}}| \le |\mathcal{V}|^{|\psi_1|} + |\mathcal{V}|^{|\psi_2|}$, since $\mathcal{V}$ contains at least 0 and 1, $|\mathcal{V}| \ge 2$ and thus $|\mathcal{V}|^{|\psi_1|} + |\mathcal{V}|^{|\psi_2|} \le |\mathcal{V}|^{|\psi_1|+|\psi_2|}$, which is no greater than $|\mathcal{V}|^{|\psi|}$.

In all cases, the claim for over-approximations follows by the same reasoning as above. $\square$

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.

## 4.4 Model-checking procedure

We extend the automata-based model-checking procedure for CTL\* from [57]. Note that since the quantified atomic propositions may appear in different subformulas, we cannot extend the algorithm for CTL\*[$\mathcal{F}$] from [3], as the latter applies the technique of [44], where the evaluation of each subformula is independent.

**PROPOSITION 4.4.** Let $\mathcal{V} \subseteq [0, 1]$ be a finite set of values such that $\{0, 1\} \subseteq \mathcal{V}$, and let $D$ be a finite set of directions. For every BQCTL\*[$\mathcal{F}$] state formula $\varphi$ and predicate $P \subseteq [0, 1]$, one can construct an APT $\mathcal{A}_{\varphi}^{\mathcal{V}, P}$ over $(\mathcal{V}^{\mathrm{AP}} \cup \{\bullet\})$-trees such that for every $\mathcal{V}^{\mathrm{AP}}$-labeled $D$-tree $t$,

$$ \mathcal{A}_{\varphi}^{\mathcal{V}, P} \text{ accepts } \bar{t} \text{ if and only if } \llbracket \varphi \rrbracket^t \in P. $$

The APT $\mathcal{A}_{\varphi}^{\mathcal{V}, P}$ is of size at most $(\mathrm{bnd}(\varphi) + 1)$-exponential in $|\varphi|$, and its index is at most $\mathrm{nd}(\varphi)$-exponential in $|\varphi|$.

**PROOF.** The proof proceeds by an induction on the structure of the formula $\varphi$ and strengthens the induction statement as follows: one can construct an APT $\mathcal{A}_{\varphi}^{\mathcal{V}, P}$ such that for every $\mathcal{V}^{\mathrm{AP}}$-labeled $D$-tree $t$, for every node $u \in t$, we have that $\mathcal{A}_{\varphi}^{\mathcal{V}, P}$ accepts $\bar{t}$ from node $u$ if and only if $\llbracket \varphi \rrbracket^t(u) \in P$ (recall that $\bar{t}$ is the complete tree obtained from $t$ by adding dummy nodes labeled with $\bullet$).

If $\varphi = p$, the automaton has one state and accepts a tree $t = (\tau, w)$ in node $u \in \tau$ if $w(u)(p) \in P$, and rejects otherwise.

If $\varphi = \exists p. \varphi'$, we want to check whether the maximal satisfaction value of $\varphi'$, over all possible $p$-labelings of the input tree, is in $P$. To do so we first compute a finite set $\widetilde{Val}_{\varphi', \mathcal{V}}$ of exponential size such that $Val_{\varphi', \mathcal{V}} \subseteq \widetilde{Val}_{\varphi', \mathcal{V}}$, which we can do as established by Lemma 4.3. For each possible value $v \in \widetilde{Val}_{\varphi', \mathcal{V}} \cap P$, we check whether this value is reached for some $p$-labeling, and if the value of $\varphi'$ is less than or equal to $v$ for all $p$-labelings. For each $v \in \widetilde{Val}_{\varphi', \mathcal{V}} \cap P$, inductively build the APTs $\mathcal{A}_{\varphi', \{v\}}$ and $\mathcal{A}_{\varphi', [0,v] \cap P}$. Turn the first one into an NPT $N_{=v}$ and the second one into a UPT $U_{\le v}$ (using Theorem 4.2). Project $N_{=v}$ existentially on $p$, and call the result $N'_{=v}$. Project $U_{\le v}$ universally on $p$, call the result $U'_{\le v}$. Finally, we can define the APT $\mathcal{A}_{\exists p. \varphi'}^{\mathcal{V}, P} := \bigvee_{v \in \widetilde{Val}_{\varphi', \mathcal{V}} \cap P} N'_{=v} \wedge U'_{\le v}$. It is then easy to see that this automaton accepts a tree if and only if there exists a value in $P$ that is the maximum of the possible values taken by $\varphi'$ for all $p$-labelings.

A block of existential quantifiers $\exists p_1 \dots \exists p_k. \varphi'$ can be treated similarly: compute $\widetilde{Val}_{\varphi', \mathcal{V}}$, for each $v \in \widetilde{Val}_{\varphi', \mathcal{V}} \cap P$ build the NPT $N_{=v}$ and the UPT $U_{\le v}$ (incurring one exponential blowup),
project $\mathcal{N}=v$ existentially on $p_1, \dots, p_k$ and project $\mathcal{U}_{\leq v}$ universally on $p_1, \dots, p_k$ (these operations are polynomial), and combine the resulting automata into the final automaton.

If $\varphi = E\psi$: as in the classic automata construction for CTL$^*$ [58], we first let atoms($\psi$) be the set of maximal state sub-formulas of $\psi$ (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($\psi$) as atomic propositions, and $\psi$ as an LTL[$\mathcal{F}$] formula over atoms($\psi$). According to Lemma 4.3 we can compute over-approximations $\overline{\mathrm{Val}}_{\varphi', \nu}$ for each $\varphi' \in \mathrm{atoms}(\psi)$, and we thus let $\overline{\mathrm{Val}} = \bigcup_{\varphi' \in \mathrm{atoms}(\psi)} \overline{\mathrm{Val}}_{\varphi', \nu}$ be a finite over-approximation of the set of possible values for atoms. It is proven in [3, Theorem 2.9] that for every $P \subseteq [0, 1]$, one can build a nondeterministic parity word automaton $\mathcal{W}_P^\psi$ of size exponential in $|\psi|^2$ such that $\mathcal{W}_P^\psi$ accepts a word $w \in (\overline{\mathrm{Val}}^{\mathrm{atoms}(\psi)})^\omega$ if and only if $\{\psi\}(w) \in P$. Now let us compute $\overline{\mathrm{Val}}_{E\psi, \nu}$ (again using Lemma 4.3), and for each $v \in \overline{\mathrm{Val}}_{E\psi, \nu} \cap P$, construct an NPT $\mathcal{N}^{E=v}$ that guesses a branch in its input and simulates $\mathcal{W}_{\{v\}}^\psi$ on it (it rejects if it leaves the “real” tree, i.e., if it sees a node labeled with $\bullet$). To obtain a universal word automaton of single exponential size that checks whether $\{\psi\}(w) \in [0, v]$, we first build a nondeterministic word automaton $\mathcal{W}_{(v,1]}^\psi$ following [3], and dualize it in linear time into a universal word automaton $\mathcal{W}_{[0,v]}^\psi$. Then we construct a UPT $\mathcal{U}^{A \leq v}$ that executes $\mathcal{W}_{[0,v]}^\psi$ on all branches of its input.<fnref n="6" /> We now define the APT $\mathcal{A}^P$ on $\overline{\mathrm{Val}}^{\mathrm{atoms}(\psi)}$-trees as

$$ \mathcal{A}^P = \bigvee_{v \in \overline{\mathrm{Val}}_{E\psi, \nu} \cap P} \mathcal{N}^{E=v} \wedge \mathcal{U}^{A \leq v}. $$

Now to go from atoms to standard atomic propositions, we define an APT $\mathcal{A}_{E\psi}^{V,P}$ that simulates $\mathcal{A}^P$ by, in each state and each node of its input, guessing a value $v_i$ in $\overline{\mathrm{Val}}_{\varphi_i}$ for each formula $\varphi_i \in \mathrm{atoms}(\psi)$, simulating $\mathcal{A}^P$ on the resulting weight label, and launching a copy of $\mathcal{A}_{\varphi_i}^{V, \{v_i\}}$ for each $\varphi_i \in \mathrm{atoms}(\psi)$. Note that the automaton is alternating and thus may have to guess several times the satisfaction value of a formula $\varphi_i$ in a same node, but launching the $\mathcal{A}_{\varphi_i}^{V, \{v_i\}}$ forces it to always guess the same, correct value.

Finally, if $\varphi = f(\varphi_1, \dots, \varphi_n)$, we list all combinations $(v_1, \dots, v_n)$ of the possible satisfaction values for the subformulas $\varphi_i$ such that $f(v_1, \dots, v_n) \in P$, and we build automaton $\mathcal{A}_{\varphi}^{V,P}$ as the disjunction over such $(v_1, \dots, v_n)$ of the conjunction of automata $\mathcal{A}_{\varphi_i}^{V, \{v_i\}}$.

The complexity of this procedure is non-elementary. More precisely, we claim that $\mathcal{A}_{\varphi}^{V,P}$ has size at most $(\mathrm{nd}(\varphi) + 1)$-exponential and index at most $\mathrm{nd}(\varphi)$-exponential.

The case where $\varphi$ is an atomic proposition is trivial.

For $\varphi = \exists p. \varphi'$, 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 $\mathcal{A}_{\exists p. \varphi, \varphi'}^{V,P}$ has at most $(\mathrm{nd}(\varphi') + 2)$-exponentially many states and index at most $(\mathrm{nd}(\varphi') + 1)$-exponential. Since $\mathrm{nd}(\varphi) = \mathrm{nd}(\varphi') + 1$, the property holds.

If $\varphi$ has the form $f(\varphi_1, \dots, \varphi_n)$, then the automaton for $\varphi$ is a combination of the automata for all $\varphi_i$, and for the various values those subformulas may take. By Lemma 4.3 there are at most $|\mathcal{V}|^{|\varphi_1|+\dots+|\varphi_n|} \leq |\mathcal{V}|^{|\varphi|}$ different combinations, so assuming (from the induction hypothesis) that

<footnote n="6">⁶We take $\mathcal{W}_{[0,v]}^\psi$ 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 determine $\mathcal{W}_{[0,v]}^\psi$, but it would cost one more exponential.</footnote>
the automata for $\varphi_i$ have at most $(\text{nd}(\varphi_i) + 1)$-exponentially many states and index at most $\text{nd}(\varphi_i)$-exponential, the automaton for $\varphi$ has at most $(\text{nd}(\varphi) + 1)$-exponentially many states and index at most $\text{nd}(\varphi)$-exponential (note that $\text{nd}(\varphi_i) = \text{nd}(\varphi)$).

Finally for $\varphi = E\psi$: in [3], the automaton $W_P^\psi$ is a generalized Büchi automaton of size exponential in $|\psi|^2$, and with at most $|\psi|$ Büchi acceptance conditions. One can turn this automaton into an equivalent Büchi automaton still exponential in $|\psi|^2$, which can be seen as a parity automaton with index 2. Then $\mathcal{N}^{E=\psi}$ and $\mathcal{U}^{A\le\psi}$ both also have sizes exponential in $|\psi|^2$, and index 2. Finally, $\mathcal{A}^P$, which combines an exponential number of the automata above, has size exponential in $|\psi|^2$ and index 2. The final automaton $\mathcal{A}_{E\psi}^{V,P}$ is obtained from that automaton by plugging the automata for $\mathcal{A}_{\varphi_i}^{V,\bullet}$, whose sizes and indices are respectively $(\text{nd}(\varphi_i) + 1)$- and $\text{nd}(\varphi_i)$-exponential, and dominate the size and index of $\mathcal{A}^P$. Since $\text{nd}(\varphi) = \max_i \text{nd}(\varphi_i)$, it follows that for $\varphi = E\psi$ the size of $\mathcal{A}_{\varphi}^{V,P}$ also is $(\text{nd}(\varphi) + 1)$-exponential, and its index is $\text{nd}(\varphi)$-exponential. $\square$

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

For the lower bounds, consider the following fragment of QCTL*: EQ$^k$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 $k$ alternations of propositional quantifiers, and start with an existential quantifier (see [60, page 8] for a formal definition); in EQ$^k$CTL$^*_alt$, quantifiers can be grouped together into at most $k$ blocks of quantifiers, each block containing only one type of quantifiers. The model-checking problem for EQ$^k$CTL$^*_alt$ is proven to be $(k+1)$-EXPTIME-hard in [60]. Now, assuming $\mathcal{F}$ contains disjunction $\max\{x, y\}$ and negation $1-x$, EQ$^k$CTL$^*_alt$ can be translated in BQCTL*[ $\mathcal{F}$] with formulas of linear size and block nesting depth at most $k$, which gives us the lower-bounds of Theorem 3.7.

# 5 MODEL CHECKING SL[$\mathcal{F}$]

In this section we show how to reduce the model-checking problem for SL[$\mathcal{F}$] to that of QCTL*[ $\mathcal{F}$]. This reduction is a rather straightforward adaptation of the usual one for qualitative variants of SL (see, e.g., [13, 45, 61]). 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 WCG $\mathcal{G} = \langle \text{AP}, \text{Agt}, \text{Act}, V, v_t, \Delta, w \rangle$ a WKS $\mathcal{K}_\mathcal{G} = \langle S, s_t, R, w \rangle$ over some set AP' and a bijection $\rho \mapsto u_\rho$ between the set of histories starting in the initial state $v_t$ of $\mathcal{G}$ and the set of nodes in $t_{\mathcal{K}_\mathcal{G}}$. We consider propositions $AP_V = \{p_V \mid v \in V\}$, that we assume to be disjoint from AP. We let $AP' = AP \cup AP_V$. Define the Kripke structure $\mathcal{K}_\mathcal{G} = (S, s_t, R, w)$ where

* $S = \{s_V \mid v \in V\}$,

* $s_t = s_{v_t}$,

* $R = \{(s_V, s_{v'}) \in S^2 \mid \exists \vec{c} \in \text{Act}^{\text{Agt}} \text{ s.t. } \Delta(v, \vec{c}) = v'\}$, and

* $w(p)(s_V) = \begin{cases} 1 & \text{if } p \in AP_V \text{ and } p = p_V \\ 0 & \text{if } p \in AP_V \text{ and } p \neq p_V. \\ w(p)(v) & \text{otherwise} \end{cases}$
For every history $\rho = v_0 \dots v_k$, define the node $u_\rho = s_{v_0} \dots s_{v_k}$ in $t_{\mathcal{K}_G}$ (which exists, by definition of $\mathcal{K}_G$ and of tree unfoldings). Note that the mapping $\rho \mapsto u_\rho$ defines a bijection between the set of histories from $v_i$ and the set of nodes in $t_{\mathcal{K}_G}$.

Formulas translation. Given a game $\mathcal{G} = \langle \text{Act}, \mathcal{V}, v_1, \Delta, \mathcal{w} \rangle$ and a formula $\varphi \in \text{SL}[\mathcal{F}]$, we define a QCTL\*[$\mathcal{F}$] formula $\varphi'$ such that $\llbracket \varphi \rrbracket^\mathcal{G} = \llbracket \varphi' \rrbracket^\mathcal{K}_G$. More precisely, this translation is parameterised with a partial function $g : \text{Agt} \to \text{Var}$ which records bindings of agents to strategy variables. Suppose that Act = $\{c_1, \dots, c_m\}$. We define the translation $(\cdot)^g$ by induction on state formulas $\varphi$ and path formulas $\psi$. Here is the definition of $(\cdot)^g$ for state formulas:

$$ (p)^g = p \qquad ((a, x)\varphi)^g = (\varphi)^{g[a \to x]} \\ (\llbracket x \rrbracket\varphi)^g = \exists p_{c_1}^x \dots \exists p_{c_m}^x (\varphi_{\text{str}}(x) \wedge (\varphi)^g), \\ \text{where } \varphi_{\text{str}}(x) = \mathbf{A}\mathbf{G} (\bigvee_{c \in \text{Act}} (p_c^x \wedge \bigwedge_{c' \neq c} \neg p_{c'}^x)) \\ (A\psi)^g = A(\psi_{\text{out}}(g) \to (\psi)^g) \\ \text{where } \psi_{\text{out}}(g) = \mathbf{G} \left( \bigwedge_{v \in \mathcal{V}} \left( p_v \to \bigvee_{\vec{c} \in \text{Act}^\text{Agt}} \left( \bigwedge_{a \in \text{dom}(f)} p_{\vec{c}(a)}^{f(a)} \wedge X_p p_{\Delta(v, \vec{c})} \right) \right) \right) \\ (f(\varphi_1, \dots, \varphi_n))^g = f((\varphi_1)^g, \dots, (\varphi_n)^g) $$

and for path formulas:

$$ (\varphi)^g = (\varphi)^g \qquad (X\psi)^g = X(\psi)^g \\ (\psi U \psi')^g = (\psi)^g U(\psi')^g \qquad (f(\psi_1, \dots, \psi_n))^g = f((\psi_1)^g, \dots, (\psi_n)^g) $$

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\*[$\mathcal{F}$] to Boolean values, and atoms in $AP_V$ also have Boolean values, $\varphi_{\text{str}}(x)$ and $\psi_{\text{out}}(\chi)$ always have value 0 or 1 and thus they can play exactly the same role as in the qualitative setting: $\varphi_{\text{str}}(x)$ holds if and only if the atomic propositions $p_{c_1}^x, \dots, p_{c_m}^x$ indeed code a strategy from the current state, and $\psi_{\text{out}}(\chi)$ holds on a branch of $t_{\mathcal{K}_G}$ if and only if in this branch each agent $a \in \text{dom}(g)$ follows the strategies coded by atoms $p_c^x$. As a result $\exists p_{c_1}^x \dots \exists p_{c_m}^x (\varphi_{\text{str}}(x) \wedge (\varphi)^g)$ maximizes over those valuations for the $p_{c_i}^x$ that code for strategies, other valuations yielding value 0. Similarly, formula $A(\psi_{\text{out}}(g) \to (\psi)^g)$ minimizes over branches that represent outcomes of strategies in $g$, as others yield value 1.

One can now see that the following holds, where $\varphi$ is an SL[$\mathcal{F}$] formula.

**LEMMA 5.1.** Let $\chi$ be an assignment and $g : \text{Agt} \to \text{Var}$ such that $\text{dom}(g) = \text{dom}(\chi) \cap \text{Agt}$ and for all $a \in \text{dom}(g)$, $g(a) = x$ implies $\chi(a) = \chi(x)$. Then

$$ \llbracket \varphi \rrbracket_{\chi}^{\mathcal{G}}(\rho) = \llbracket (\varphi)^g \rrbracket^{t_{\mathcal{K}_G}} (u_{\rho}) $$

As a result, the quantitative model-checking problem for an SL[$\mathcal{F}$] formula $\varphi$, a weighted CGS $\mathcal{G}$ and a predicate $P \subseteq [0, 1]$ can be solved by computing the BQCTL\*[$\mathcal{F}$] formula $\varphi' = (\varphi)^0$, which is of size polynomial in $|\varphi|$, and the weighted Kripke structure $\mathcal{K}_G$, of size polynomial in $|\mathcal{G}|$, and deciding whether $\llbracket \varphi' \rrbracket^\mathcal{K}_G \in P$, 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:

$$ (\langle\langle x_1 \rangle\rangle \dots \langle\langle x_k \rangle\rangle \varphi)^g = \exists p_{c_1}^{x_1} \dots \exists p_{c_m}^{x_m} \dots \exists p_{c_1}^{x_1} \dots \exists p_{c_m}^{x_m} \left( \bigwedge_{i=1}^{k} \varphi_{\text{str}}(x_i) \wedge (\varphi)^g \right) $$

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\*[$\mathcal{F}$] established in Theorem 3.8.

Remark 3. Lemma 5.1 together with Lemma 4.3 imply that SL[$\mathcal{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[$\mathcal{F}$] can be replaced with maximum and minimum.

# 6 THE CASE OF SL<sub>1G</sub>[$\mathcal{F}$]

We now study the fragment SL<sub>1G</sub>[$\mathcal{F}$], which is the extension to the quantitative setting of the one-goal fragment SL<sub>1G</sub> of SL [66]. In the Boolean setting, SL<sub>1G</sub> 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 [66]). We show that in the quantitative setting, the one-goal fragment SL<sub>1G</sub>[$\mathcal{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 $\varphi = \langle\langle x_1 \rangle\rangle \dots \langle\langle x_n \rangle\rangle$, where $\langle\langle x_i \rangle\rangle \in \{\langle\langle x_i \rangle\rangle, [[x_i]]\}$ is either an existential or universal quantification. For a fixed set of agents Agt = {$a_1, \dots, a_n$} a binding prefix is a sequence $b = (a_1, x_1), \dots, (a_n, x_n)$, where every agent in Agt occurs exactly once. A combination $\varphi b$ is closed if every variable occurring in $b$ occurs in some quantifier of $\varphi$. We can now give the definition of SL<sub>1G</sub>[$\mathcal{F}$] syntax.

**Definition 6.1 (SL<sub>1G</sub>[$\mathcal{F}$] Syntax).** Let AP be a set of Boolean atomic propositions, and let $\mathcal{F} \subseteq \{f : [0, 1]^m \to [0, 1] \mid m \in \mathbb{N}\}$ be a set of functions over $[0, 1]$. The set of SL<sub>1G</sub>[$\mathcal{F}$] formulas is defined by the following grammar:

$$ \varphi := p \mid f(\varphi, \dots, \varphi) \mid \varphi \mid X\varphi \mid \varphi U\varphi \mid \varphi b\varphi, $$

where $p \in \text{AP}$, $f \in \mathcal{F}$, and $\varphi b$ is a closed combination of a quantification prefix and of a binding prefix.

Note that all SL[$\mathcal{F}$] formulas are sentences, as all strategy variables are quantified immediately before being bound to some agent. The sentence nesting depth of an SL<sub>1G</sub>[$\mathcal{F}$] formula is defined as follows:

* $\text{snd}(p) = 0$ for every $p \in \text{AP}$;

* $\text{snd}(f(\varphi_1, \dots, \varphi_n)) = \max_{1 \le i \le n} \{\text{snd}(\varphi_i)\}$;

* $\text{snd}(X\psi) = \text{snd}(\psi)$;

* $\text{snd}(\psi_1 U \psi_2) = \max\{\text{snd}(\psi_1), \text{snd}(\psi_2)\}$.

* $\text{snd}(\varphi b\varphi) = \text{snd}(\varphi) + 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<sub>1G</sub>[$\mathcal{F}$], we need the technical notion of concurrent multi-player parity game introduced in [65].
**Definition 6.2.** A concurrent multi-player parity game (CMPG) is a tuple $P = \langle \text{Agt}, \text{Act}, V, v_t, \Delta, p \rangle$, where $\text{Agt} = 0, \dots, n$ is a set of agents indexed with natural numbers, $\langle \text{Agt}, \text{Act}, V, v_t, \Delta \rangle$ is a CGS, and $p: V \to \mathbb{N}$ is a priority function.

In a CMPG, agents are split in two teams: each player $i$ with $i \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 shown in [65, Theorem 4.1, Corollary 4.1], one can decide the winners of a CMPG $P = \langle \text{Agt}, \text{Act}, V, v_t, \Delta, p \rangle$ in time polynomial w.r.t. $|V|$ and $|\text{Act}|$, and exponential w.r.t. $|\text{Agt}|$ and $k = \max p$ (the maximal priority).

**THEOREM 6.3.** *The model-checking problem for closed formulas of SL<sub>1G</sub>[F] is decidable, and 2-EXPTIME-complete.*

**PROOF.** We let $\mathcal{G} = \langle \text{AP}, \text{Agt}, \text{Act}, V, v_t, \Delta, w \rangle$ be a WCGS and we consider a formula of the form $\wp\mathcal{b}\wp$. We also assume, for simplicity, that $\wp = \langle\langle x_0 \rangle\rangle[[x_1]], \dots, \langle\langle x_k \rangle\rangle$, that is, quantifiers perfectly alternate between existential and universal.<fnref n="7" /> Note that the formula $\wp\mathcal{b}\wp$ 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 $V(\wp\mathcal{b}\wp)$ of possible values is bounded by $2^{|\wp\mathcal{b}\wp|}$.

We proceed by induction on the sentence nesting depth. As base case let $\text{snd}(\wp\mathcal{b}\wp) = 1$, i.e., there is no occurrence of neither quantifiers nor bindings in $\wp$. Then, $\wp$ can be regarded as an LTL$[\mathcal{F}]$ formula that can be interpreted over paths of the WKS $\mathcal{K} = \langle \text{AP}, V, v_t, R, w \rangle$ where

$$R = \{(v_1, v_2) \mid \exists \vec{c} \in \text{Act}^{\text{Agt}}. v_2 = \Delta(v_1, \vec{c})\}$$

Now, thanks to [3, Theorem 2.9], for every value $v \in V(\wp\mathcal{b}\wp)$, we can build a parity word automaton $\mathcal{B}_{\mathcal{K},\wp,P_v}$ of size exponential in $|\wp|^2$ such that $\mathcal{B}_{\mathcal{K},\wp,P_v}$ accepts a word $w \in (\overline{\text{Val}}^{\text{atoms}(\wp)})^\omega$ if, and only if, $\langle\langle \psi \rangle\rangle(w) \in P_v = [v, 1]$. Following [71], we can convert $\mathcal{B}_{\mathcal{K},\wp,P_v}$ into a deterministic parity word automaton $\mathcal{A}_{\mathcal{K},\wp,P_v} = \langle V, Q, q_t, \delta, p \rangle$ of size doubly-exponential in the size of $\wp$ and index bounded by $2^{|\wp|}$.

At this point, define the following CMPG $P = \langle \text{Agt}', \text{Act}, V', v'_t, \Delta', p' \rangle$ such that

* $\text{Agt}' = \{0, \dots, k\}$ is a set of agents, one for every variable occurring in $\wp$, ordered in the same way as in $\wp$ itself;

* $\text{Act}$ is the set of actions in $\mathcal{G}$;

* $V' = V \times Q$ is the product of the states of $\mathcal{G}$ and the automaton $\mathcal{A}_{\mathcal{K},\wp,P_v}$;

* $v'_t = (v_t, q_t)$ is the pair given by the initial states of $\mathcal{G}$ and $\mathcal{A}_{\mathcal{K},\wp,t}$, respectively;

* $p'(v, q) = p(q)$ mimics the parity function of $\mathcal{A}_{\mathcal{K},\wp,P_v}$;

* if $\vec{c} \in \text{Act}^{\text{Agt}'}$, $\Delta'((v, q), \vec{c}) = (\Delta(v, b(\vec{c})), \delta(q, w(v)))$ mimics the execution of both $\mathcal{G}$ and $\mathcal{A}_{\mathcal{K},\wp,P_v}$.

The game emulates two things, one per each component of its state-space. In the first, it emulates a path $\pi$ generated in $\mathcal{G}$. In the second, it emulates the execution of the automaton $\mathcal{A}_{\mathcal{K},\wp,P_v}$ when it reads the path $\pi$ generated in the first component. By construction, it results that every execution $(\pi, \eta) \in V^\omega \times Q^\omega$ in $P$ satisfies the parity condition determined by $p'$ if, and only if, $\langle\langle \wp \rangle\rangle(\pi) \in P_v$. Moreover, observe that, since $\mathcal{A}_{\mathcal{K},\wp,P_v}$ is deterministic, for every possible history $\rho$ in $\mathcal{G}$, there is a unique partial run $\eta_\rho$ that makes the partial execution $(\rho, \eta_\rho)$ possible in $P$. This makes the sets of possible strategies $\text{Str}_\mathcal{G}(v_t)$ and $\text{Str}_\mathcal{P}(v'_t)$ in bijection. $P$ has a winning strategy if and only if

<footnote n="7">⁷To reduce to this case, one can add quantifications on dummy variables.</footnote>
$\{\phi b\phi\}^G(v_i) \in P_v$. In order to compute the exact value of $\{\phi b\phi\}^G(v_i)$, we repeat the procedure described above for every $v \in V(\phi b\phi)$ and take the maximum $v$ of those for which $\{\phi b\phi\}^G(v_i) \in P_v$.

For the induction case, assume we can compute the satisfaction value of every $SL_{1G}[\mathcal{F}]$ formula with sentence nesting depth at most $n$, and let $snd(\phi b\phi) = n+1$. Observe that, for every subsentence $\phi'$'b'\phi'$ of $\phi b\phi$, we have that $snd(\phi' b'\phi') \le n$ and so, by induction hypothesis, we can compute $\{\phi' b'\phi'\}^G(v)$ for every $v \in V$. Now, introduce a fresh atomic proposition $p_{(\phi' b'\phi')}^v$ whose weight in $\mathcal{G}$ is defined as $w(v)(p_{(\phi' b'\phi')}^v) = \{\phi' b'\phi'\}^G(v)$ and a set of fresh atomic propositions $p_v$, one for every $v \in V$, whose weights in $\mathcal{G}$ are defined as $w(v)(p_v) = 1$ and $w(v)(p_{v'}) = 0$ if $v \ne v'$. Now, consider the Boolean formula

$$ \Phi(\phi' b' \phi') = \bigvee_{v \in V} (p_v \wedge p_{(\phi' b' \phi')}) $$

Observe that every disjunct is a conjunction of the form $p_v \wedge p_{(\phi' b'\phi')}^v$, whose satisfaction value on a state $v'$ is the minimum among the weights of $p_v$ and $p_{(\phi' b'\phi')}^v$. This can be either 0, if $v \ne v'$ or $\{\phi' b'\phi'\}^G(v)$, if $v = v'$. Now, the big disjunction takes the maximum among them. Therefore, we obtain that $\{\Phi(\phi' b'\phi')\}^G(v) = \{\phi' b'\phi'\}^G(v)$. This allows us to replace every occurrence of $\phi' b'\phi'$ in $\phi$ with the Boolean combination $\Phi(\phi' b'\phi')$, making the resulting formula to be of sentence nesting depth 1. Thus, we can apply the procedure described in the base case, to compute $\{\phi b\phi\}^G(v)$.

Regarding the complexity, note that the size of P is $|V| \cdot |Q|$ that is in turn linear with respect to the size of $\mathcal{G}$ and doubly exponential in the size of $\phi$. This is due to the fact that the automaton $\mathcal{A}_{K,\phi,P_v}$ results from the construction of the NGBW $\mathcal{B}_{K,\phi,P_v}$, of size singly exponential in $|\phi|$ 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 $|\phi|$, 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 $\mathcal{G}$ and double exponential in $|\phi|$. Such a 2-EXPTIME procedure is executed a number of time exponential in $\phi$, which is still doubly exponential.

Hardness follows from that of $SL_{1G}$ [66]. □

## 7 ON QCTL*[F] AND MSO[F]

In this section we first study the expressiveness of $QCTL*[F]$. It is shown in [60] 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 $(x, y) \mapsto x = y$ and $(x, y) \mapsto y = x/2$. Finally we show that when all functions in $F$ are Lipschitz-continuous, then so is the semantics of $QCTL*[F]$.

### 7.1 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 literature, both on words and on trees [39, 40, 75], and links with fuzzy automata have been established. In [39] 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 [63] 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 arbitrary set of function, producing a more general setting than the one presented in [39].

In [40], the authors start from a 4-valued logic (MK-valued logic), taking also undefined and error values, together with classic true and false. They 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 truth 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 $\mathcal{V}ar_1$ and $\mathcal{V}ar_2$ be countable sets of first-order and second-order variables, respectively.

**Definition 7.1.** The syntax of MSO[$\mathcal{F}$] is given by the following grammar:

$$ \varphi ::= P_a(x) \mid x = y \mid x \in X \mid S(x, y) \mid \exists x \varphi \mid \exists X \varphi \mid f(\varphi, \dots, \varphi) $$

where $a \in \mathcal{AP}$, $x, y \in \mathcal{V}ar_1$, $X \in \mathcal{V}ar_2$ and $f \in \mathcal{F}$.

Formulas of MSO[$\mathcal{F}$] are interpreted on infinite $(\mathcal{V}^{\text{AP}}, \mathcal{D})$-trees and first-order variables represent nodes of the tree. But instead of usual sets, second-order variables represent fuzzy sets, i.e., mappings $X: \tau \to [0, 1]$ indicating to which degree each node of the tree $\tau$ belongs to the set.

To evaluate formulas with free variables, we need interpretations: an interpretation $\mathcal{I}$ for a formula $\varphi(x_1, \dots, x_k, X_1, \dots, X_l)$ with free first-order variables $x_1, \dots, x_k$ and free second-order variables $X_1, \dots, X_l$ maps each free first-order variable $x_i$ to some node $u \in \tau$ and each free second-order variable $X_i$ to some fuzzy set $X: \tau \to [0, 1]$. The domain of $\mathcal{I}$, denoted with $\text{dom}(\mathcal{I})$, is the set $\{x_1, \dots, x_k, X_1, \dots, X_l\}$ of variables where $\mathcal{I}$ is defined.

**Definition 7.2 (Semantics).** Given a $(\mathcal{V}^{\text{AP}}, \mathcal{D})$-tree $t = (\tau, w)$, an MSO[$\mathcal{F}$] formula $\varphi$ and an interpretation $\mathcal{I}$ for the free variables of $\varphi$, the semantics of $\varphi$ is defined as follows:

$$ \begin{align*} \{P_a(x)\}^t(\mathcal{I}) &= w(\mathcal{I}(x))(a) \\ \{x=y\}^t(\mathcal{I}) &= \begin{cases} 1 & \text{if } \mathcal{I}(x) = \mathcal{I}(y) \\ 0 & \text{otherwise} \end{cases} \\ \{x \in X\}^t(\mathcal{I}) &= \mathcal{I}(X)(\mathcal{I}(x)) \\ \{S(x, y)\}^t(\mathcal{I}) &= \begin{cases} 1 & \text{if } \mathcal{I}(y) \text{ is a child of } \mathcal{I}(x) \\ 0 & \text{otherwise} \end{cases} \\ \{\exists x \varphi\}^t(\mathcal{I}) &= \sup_{u \in \tau} \{\varphi\}^t(\mathcal{I}[x \mapsto u]) \\ \{\exists X \varphi\}^t(\mathcal{I}) &= \sup_{Y: \tau \to [0,1]} \{\varphi\}^t(\mathcal{I}[X \mapsto Y]) \\ \{f(\varphi_1, \dots, \varphi_n)\}^t(\mathcal{I}) &= f(\{\varphi_1\}^t(\mathcal{I}), \dots, \{\varphi_n\}^t(\mathcal{I})) \end{align*} $$

where $\mathcal{I}[\alpha \mapsto \beta]$ is the interpretation $\mathcal{J}$ such that $\text{dom}(\mathcal{J}) = \text{dom}(\mathcal{I}) \cup \{\alpha\}$, and $\mathcal{J}(\alpha) = \beta$ and $\mathcal{J}(\gamma) = \mathcal{I}(\gamma)$ for all $\gamma \in \text{dom}(\mathcal{I}) \setminus \{\alpha\}$.

We also consider the case where set quantification is over classic sets instead of fuzzy ones. We call this logic BMSO[$\mathcal{F}$]. Its syntax is the same as MSO[$\mathcal{F}$] and the semantics, which we write $\{\cdot\}_B^t$, differs only in the case of second-order quantification, which is as follows:

$$ \{\exists X \varphi\}_B^t(\mathcal{I}) = \sup_{Y: \tau \to \{0,1\}} \{\varphi\}_B^t(\mathcal{I}[X \mapsto Y]) $$
Recall that, if Bool is the function that maps $x$ to $1$ if $x \in \{0, 1\}$, and to $0$ otherwise, then $\text{BQCTL}^*[\mathcal{F}]$ is a fragment of $\text{QCTL}^*[\mathcal{F}] \cup \{\text{Bool}\}$ (Lemma 3.5), and Boolean quantification on atoms can be expressed in $\text{QCTL}^*[\mathcal{F}]$ as $\exists p.(\text{AG } \text{Bool}(p) \land \varphi)$. Similarly, $\text{BMSO}[\mathcal{F}]$ is a fragment of $\text{MSO}[\mathcal{F} \cup \{\text{Bool}\}]:$ define

$$ \text{Bool}(X) := \forall x. \text{Bool}(x \in X) \qquad \exists^{\mathcal{B}} X. \varphi := \exists X. \text{Bool}(X) \land \varphi $$

It holds that:

**LEMMA 7.3.** For every $\text{BMSO}[\mathcal{F}]$ formula $\varphi$, letting $\varphi_B$ be the $\text{MSO}[\mathcal{F}]$ formula obtained from $\varphi$ by replacing inductively each $\exists X. \varphi'$ in $\varphi$ with $\exists^{\mathcal{B}} X. \varphi'_B$, we have that for all tree $t$ and interpretation $\mathcal{I}$, $\{\exists^{\mathcal{B}} X. \varphi\}^{\tau}(\mathcal{I}) = \{\exists X. \varphi\}^{\tau}_B(\mathcal{I})$.

Below we prove that $\text{MSO}[\mathcal{F}]$ and $\text{QCTL}^*[\mathcal{F}]$ have the same expressive power. As noticed in [60], one important conceptual difference is that quantification in $\text{MSO}[\mathcal{F}]$ refers to the whole tree, while $\text{QCTL}^*[\mathcal{F}]$ can only refer to the reachable part of the tree. As a consequence, $\text{MSO}[\mathcal{F}]$ can express the fact that the current node is the root of the tree, while $\text{QCTL}^*[\mathcal{F}]$ cannot.

Formally, that both logics are equally expressive means that

(1) for any (state-)formula $\varphi \in \text{QCTL}^*[\mathcal{F}]$, there is a formula $\tilde{\varphi}(x) \in \text{MSO}[\mathcal{F}]$ with one free first-order variable $x$ such that for any tree $t$ with root $r$, it holds $\{\varphi\}^t(r) = \{\tilde{\varphi}\}^t(x \mapsto r)$, and symmetrically,

(2) for any formula $\varphi(x) \in \text{MSO}[\mathcal{F}]$ with one free first-order variable $x$, there is a formula $\hat{\varphi} \in \text{QCTL}^*[\mathcal{F}]$ such that for any tree $t$ with root $r$, it holds $\{\hat{\varphi}\}^t(r) = \{\varphi\}^t(x \mapsto r)$.

We use the possibility to express Boolean second-order quantification to capture first-order quantification in elements in $\text{QCTL}^*[\mathcal{F}]$, and also to express path quantification in $\text{MSO}[\mathcal{F}]$.

**THEOREM 7.4.** If $\{\neg, \wedge, \text{Bool}\} \in \mathcal{F}$ then $\text{MSO}[\mathcal{F}]$ has the same expressive power as $\text{QCTL}^*[\mathcal{F}]$.

**PROOF.** Translating $\text{QCTL}^*[\mathcal{F}]$ to $\text{MSO}[\mathcal{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 $\text{MSO}[\mathcal{F}]$. The usual translation consists in using second-order quantification and express that the quantified set is a path, with the following formula:

$$ \text{Path}(X) := \forall x, y. (x \in X \land y \in X) \rightarrow (x \leq y \lor y \leq x) $$

where

$$ x \leq y := \forall X. (x \in X \land \text{S-Closed}(X) \rightarrow y \in X) $$

and

$$ \text{S-Closed}(X) := \forall x, y. (x \in X \land \text{S}(x, y) \rightarrow y \in X) $$

The translation of $\text{E}\psi$ is then defined as follows:

$$ (\text{E}\psi)' := \exists X. \text{Path}(X) \land \psi'(X) $$

where $\psi'(X)$ is the translation of $\psi$ in $\text{MSO}[\mathcal{F}]$. However in our context, for this translation to have the intended value which is the supremum of the satisfaction value of $\psi$ over all paths, formulas $\text{Path}(X)$ and $x \leq y$ must have a Boolean value. We obtain this by using quantification on Boolean sets $\exists^{\mathcal{B}} X$ defined above, letting

$$ x \leq y := \forall^{\mathcal{B}} X. (x \in X \land \text{S-Closed}(X) \rightarrow y \in X) $$

and

$$ (\text{E}\psi)' := \exists^{\mathcal{B}} X. \text{Path}(X) \land \psi' $$
For the direction from MSO[$\mathcal{F}$] to QCTL*[$\mathcal{F}$], we adapt the translation from MSO to QCTL* presented in [60]: for $\varphi \in$ MSO[$\mathcal{F}$], where free variable x represents the root of the tree, we inductively define the QCTL*[$\mathcal{F}$] formula $\hat{\varphi}$ as follows:

$$ \overline{x=y} := p_y \qquad \overline{y=z} := \mathrm{EF}(p_y \wedge p_z) $$

$$ x \in \overline{X} := p_X \qquad y \in \overline{X} := \mathrm{EF}(p_y \wedge p_X) $$

$$ \exists \overline{y.\varphi'} := \exists^{\mathcal{B}} p_y. \mathrm{uniq}(p_y) \wedge \hat{\varphi}' $$

$$ \exists \overline{X.\varphi'} := \exists p_X. \hat{\varphi}' $$

$$ \overline{S(x, y)} := \mathrm{EX} p_y \qquad \overline{S(y, x)} := 0 $$

$$ \overline{S(y, z)} := \mathrm{EF}(p_y \wedge \mathrm{EX} p_z) $$

$$ f(\overline{\varphi_1, \dots, \varphi_n}) := f(\overline{\hat{\varphi}_1, \dots, \hat{\varphi}_n}) $$

where

$$ \mathrm{uniq}(p) := \mathrm{EF} p \wedge \forall^{\mathcal{B}} q. (\mathrm{EF}(p \wedge q) \rightarrow \mathrm{AG}(p \rightarrow q)) $$

To see that the above translation is correct, note that if $p$ is Boolean in $t = (\tau, w)$, then

$$ \{\mathrm{uniq}(p)\}^t = \begin{cases} 1 & \text{if } w^{-1}(1) \text{ is a singleton} \\ 0 & \text{otherwise} \end{cases} $$

For an interpretation $\mathcal{I}$ such that $\mathcal{I}(x)$ is the root of $\tau$ we have that $\{\varphi\}^\tau(\mathcal{I}) = \{\overline{\hat{\varphi}}\}^t$, where $t = (\tau, w)$ and $w(u)(p_y) = 1$ if $\mathcal{I}(y) = u, 0$ otherwise, and $w(u)(p_X) = \mathcal{I}(X)(u)$.

For the other direction, the usual translation from CTL* to MSO can be extended to a translation from CTL*[$\mathcal{F}$] to MSO[$\mathcal{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[$\mathcal{F}$] with formula $\exists^{\mathcal{B}} X. \varphi$. $\square$

The above proof can be easily adapted to obtain the following result:

**THEOREM 7.5.** If $\{\neg, \wedge, \mathrm{Bool}\} \in \mathcal{F}$ then BMSO[$\mathcal{F}$] has same expressive power as BQCTL*[$\mathcal{F}$].

As explained in the proof of Theorem 7.4, it seems hard to express quantification on paths in MSO[$\mathcal{F}$], or first-order quantification in QCTL*[$\mathcal{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[$\{\neg, \wedge, \mathrm{Bool}\}$] is strictly more expressive than MSO[$\{\neg, \wedge\}$] with $\exists^{\mathcal{B}} X$ added as a basic construct. Note that if $\exists^{\mathcal{B}} X$ and $\exists^{\mathcal{B}} p$ are added as basic constructs of MSO[$\mathcal{F}$] and QCTL*[$\mathcal{F}$] respectively, then Theorem 7.4 holds as soon as $\mathcal{F}$ contains $\neg$ and $\wedge$.

## 7.2 Undecidability of QCTL*[$\mathcal{F}$] model checking

In this section we show an undecidability result for the model checking of QCTL*[$\mathcal{F}$]. In fact we first prove it for the logic QLTL[$\mathcal{F}$] and then show that it entails undecidability of QCTL*[$\mathcal{F}$]. While in QCTL*[$\mathcal{F}$] second-order quantification is made at the level of state formulas, in QLTL[$\mathcal{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[$\mathcal{F}$] (on a fixed Kripke structure) is undecidable, even when $\mathcal{F}$ only contains $\neg$, $\wedge$ and the following two functions:*

$$ equal: [0, 1]^2 \to \{0, 1\} $$

$(x, y) \mapsto 1 \quad \text{if } y = x$

$(x, y) \mapsto 0 \quad \text{otherwise}$

$$ half: [0, 1]^2 \to \{0, 1\} $$

$(x, y) \mapsto 1 \quad \text{if } y = x/2$

$(x, y) \mapsto 0 \quad \text{otherwise}$

**PROOF.** The proof consists in expressing a tiling problem as a QLTL[$\mathcal{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 $u = (\text{top}(u), \text{bottom}(u), \text{left}(u), \text{right}(u))$ for such a tile. Given a set $B$ of tiles, a tiling of a subset $Z$ of $\mathbb{N}^2$ with tiles of $B$ is a mapping $t: Z \to B$. Such a tiling is valid whenever the colors of neighboring tiles agree; formally, a tiling $t$ is valid if for any two positions $p = (x, y)$ and $p' = (x', y')$ in $Z$, it holds

* if $x' = x$ and $y' = y + 1$, then $\text{top}(t(p)) = \text{bottom}(t(p'))$;

* if $y' = y$ and $x' = x + 1$, then $\text{right}(t(p)) = \text{left}(t(p'))$.

We encode the following tiling problem:

Given a finite set of tiles $B = \{u_i | 1 \le i \le n\}$, does any rectangular grid admit a valid tiling?

This problem is undecidable [82, pages 213-214].

In our encoding, we consider the Kripke structure $\mathcal{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.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Kripke structure $\mathcal{K}$</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>Fig. 2. A run of $\mathcal{K}$</figcaption></figure>

We build two QLTL[$\mathcal{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 $t$;

* 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 $\mathcal{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 $t$ in such a way that the value of $t$ is divided by 2 as long as we only visit $q$-states, and it restarts from 1 at $p$- or $r$-states:

$$ \exists t. G((\neg q) \to t) \wedge G((Xq) \to \text{half}(t, Xt)). $$

For this formula to take value 1, all $p$- and $r$-states must have $t = 1$, and the value of $t$ in a $q$-states must be half the value of $t$ in the previous state;
* we enforce that we have a grid: all columns (of q-states) must have the same length:

$$G((Xp) \rightarrow \text{equal}(t, X((Xq)U(t \wedge X \neg q))))).$$

This takes value 1 if, and only if, the value of $t$ in a state where $Xp$ holds (i.e., in the last state of all but the last column) equals the value of $t$ in the last state of the next column.

We write $\Psi_{\text{grid}}$ for the conjunction of the two formulas above, and $\text{Fr}$. Notice that $\Psi_{\text{grid}}$ can be written as $\exists t. \psi_{\text{grid}}$, with $\psi_{\text{grid}} \in \text{LTL}[\text{equal, half}]$. Figure 3 represents the path of Figure 2 when labeled with values for $t$ witnessing the fact that $\Psi_{\text{grid}}$ has value 1 along that path.

<figure><img src="image_4.png" /><figcaption>Fig. 3. A run of $K$, labeled with values for $t$</figcaption></figure>

The following lemma formalizes the meaning of $\Psi_{\text{grid}}$:

LEMMA 7.7. For any infinite path $\pi$ in the Kripke structure $K$ of Figure 1, it holds: $\{\Psi_{\text{grid}}\}(\pi) = 1$ if, and only if, $\pi$ has the form $(p \cdot q^l)^m \cdot r^\omega$ for some $l, m \in \mathbb{N}$.

We now encode the tiling problem on this grid: this is achieved by labeling all q-states with a (Boolean) atomic proposition from $(u_i)_{1 \le i \le n}$, and checking that neighboring tiles match:

* we first label q-states with the tiles $u_i$ for all $1 \le i \le n$, in such a way that all cells of the grid receive a unique tile:

$$\exists(u_i)_{1 \le i \le n} \cdot G\left(q \rightarrow \left( \bigvee_{1 \le i \le n} \left(\text{equal}(u_i, \top) \wedge \bigwedge_{\substack{j \le n \\ j \ne i}} \text{equal}(u_j, \bot)\right) \right) \wedge G\left(\neg q \rightarrow \bigwedge_{1 \le j \le n} \text{equal}(u_j, \bot)\right)\right)$$

* we check vertical matching:

$$G((q \wedge Xq) \rightarrow \text{v-match})$$

where v-match is a purely Boolean formula listing all combinations of formulas of the form $u_i \wedge Xu_j$ where the bottom-color of tile $u_i$ and the top-color of $u_j$ 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 $v$; thanks to formula $(\text{equal}(t, Gv) \wedge \text{equal}(t, Fv))$, we force $v$ to take the same value as the current $t$-value in all future states. The right-neighbor then is the (strict) next q-state where $t$ and $v$ have the same value; in that state, we check that the colors match:

$$\bigwedge_{1 \le i \le n} G(u_i \rightarrow \exists v. \text{ equal}(t, Gv) \wedge \text{ equal}(t, Fv) \wedge X(\neg \text{ equal}(t, v)) \wedge \text{ equal}(t, v) \wedge \text{ h-match}(u_i)))$$

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

Write $\Psi_{\text{tiling}}$ for the conjunction of the three formulas above. Notice that $\Psi_{\text{tiling}}$ can be written as $\exists(u_i)_{1 \le i \le n}. \psi_{\text{tiling}}$, with $\psi_{\text{tiling}} \in \text{QLTL}[\{\text{equal}\}]$. Then:
LEMMA 7.8. Let $\pi = (s_j)_{j \in \mathbb{N}}$ be an infinite path of the form $(p \cdot q^l)^m \cdot r^\omega$ for some $l, m \in \mathbb{N}$ in the Kripke structure $\mathcal{K}$ of Figure 1. Assume that $\pi$ is labeled with atomic proposition $t$ in such a way that for any $i$ and $j$ in $[0, m(l+1)-1]$, it holds that $\ell(s_i)(t) = \ell(s_j)(t)$ if, and only if, $i-j$ is a multiple of $l+1$. Then $\{\Psi_{tiling}\}(\pi) = 1$ if, and only if, the grid of size $l \times m$ admits a valid tiling with tiles in $\{u_i \mid 1 \le i \le n\}$.

To conclude the proof of Theorem 7.6, we let $\Psi$ be the QLTL$\{\text{equal, half}\}$ formula

$$ \Psi = \forall t. \exists(u_i)_{1 \le i \le n}. (\text{equal}(\psi_{\text{grid}}, \tau) \rightarrow \text{equal}(\psi_{\text{tiling}}, \tau)). $$

Then $\{\Psi\}(\mathcal{K}) = 1$ if, and only if, any rectangular grid can be tiled with tiles $\{u_i \mid 1 \le i \le n\}$. $\square$

Now to obtain undecidability of QCTL\*[$\mathcal{F}$] we need to show that all quantifications on atomic propositions can be made at the beginning, as QCTL\*[$\mathcal{F}$] does not allow mixing second-order quantification with temporal operators without requantifying on paths. To this aim notice that formula $\Psi$ is almost in prenex form, but $\psi_{tiling}$ still contains an existential quantification under a temporal modality. However, $\Psi$ can be turned into prenex form, by noticing that for all QLTL[$\mathcal{F}$] formulas $\psi$ and $\psi'$,

$$ G(\psi \rightarrow \exists v. \psi') \equiv \forall w. \exists v. (\text{uniq}(w) \rightarrow G((\psi \wedge w) \rightarrow \psi')) $$

where $w$ is a new atomic proposition, and

$$ \text{uniq}(w) = \text{equal}(w, \perp) \cup \text{equal}(w, \tau) \wedge \text{XG equal}(w, \perp) $$

requires $w$ to be Boolean and to only label one state of the path.

In the end, $\Psi$ can be written as

$$ \forall t. \exists(u_i)_{1 \le i \le n}. \forall w. \exists v. (\text{equal}(\psi_{\text{grid}}, \tau) \rightarrow \text{equal}(\psi'_{\text{tiling}}, \tau)) $$

where $\psi'_{tiling} \in \text{LTL}[\text{equal}]$ is obtained by applying the transformation above.

Now define the QCTL\*[$\mathcal{F}$] formula

$$ \Phi = \forall t. \exists(u_i)_{1 \le i \le n}. \forall w. \exists v. A(\text{equal}(\psi_{\text{grid}}, \tau) \rightarrow \text{equal}(\psi'_{\text{tiling}}, \tau)) $$

It is clear that $\{\Psi\}(\mathcal{K}) = 1$ if and only if $\{\Phi\}(\mathcal{K}) = 1$, hence the following result:

THEOREM 7.9. Model checking QCTL\*[$\mathcal{F}$] (on a fixed Kripke structure) is undecidable, even when $\mathcal{F}$ only contains $\neg$, $\wedge$, equal and half.

## 7.3 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 [5, 64, 78]. In this section we show that when the quality functions in $\mathcal{F}$ are Lipschitz continuous, then so is the satisfaction value of QCTL\*[$\mathcal{F}$] formulas.

Let $P \subseteq \text{AP}$. A $P$-labeling for a tree $t = (\tau, w)$ is a mapping $\ell_P: P \rightarrow (\tau \rightarrow [0, 1])$. For any two subsets $P$ and $Q$ of AP, any $P$-labeling $\ell_P$ and $Q$-labeling $\ell_Q$ of $t$, we define their composition as the $P \cup Q$-labeling defined as follows:

$$ \begin{array}{rcl} \ell_P \otimes \ell_Q: P \cup Q & \rightarrow & [0, 1] \\ p & \mapsto & \begin{cases} \ell_Q(p) & \text{if } p \in Q, \text{ and} \\ \ell_P(p) & \text{if } p \in P \setminus Q. \end{cases} \end{array} $$
The distance between two P-labelings of $t = (\tau, w)$ is defined as

$$d_{P,t}(\ell_P, \ell'_P) = \sup_{u \in \tau} \max_{q \in P} |\ell_P(q)(u) - \ell'_P(q)(u)|.$$

Notice that, given $\ell_P, \ell'_P$ and $\ell_Q$, it holds

$$d_{P \cup Q, t}(\ell_P \otimes \ell_Q, \ell'_P \otimes \ell_Q) \le d_{P,t}(\ell_P, \ell'_P).$$

When $t$ and $P$ are clear from the context, we omit them from the notation.

Let $t = (\tau, w)$ be a $([0, 1]^\text{AP}, D)$-tree, and $u$ be a node of $t$. Let $\varphi \in \text{QCTL}^*[\mathcal{F}]$ be a state formula over AP. We define

$$F(t, u, P, \varphi) : ([0, 1]^\tau)^P \to [0, 1] \\ \ell_P \mapsto \{\varphi\}^{(\tau, w \otimes \ell_P)}(u).$$

Similarly, given an infinite branch $\lambda$ of $t$ and a path formula $\psi \in \text{QCTL}^*[\mathcal{F}]$, we define

$$F(t, \lambda, P, \psi) : ([0, 1]^\tau)^P \to [0, 1] \\ \ell_P \mapsto \{\psi\}^{(\tau, w \otimes \ell_P)}(\lambda).$$

For two metric spaces $(D, d_D)$ and $(I, d_I)$, a function $f: D \to I$ is $k$-Lipschitz continuous when, for every two elements $X$ and $Y$ in $D$, it holds

$$d_I(f(X), f(Y)) \le k \cdot d_D(X, Y).$$

A $\text{QCTL}^*[\mathcal{F}]$ state formula $\varphi$ is then $k$-Lipschitz continuous if, for every tree $t$, node $u$ of $t$ and subset $P \subseteq \text{AP}$, the function $F(t, u, P, \varphi)$ is $k$-Lipschitz continuous. The definition is extended to path formulas in the natural way.

**THEOREM 7.10.** If all functions in $\mathcal{F}$ are $k$-Lipschitz continuous, then every formula in $\text{QCTL}^*[\mathcal{F}]$ having at most $n$ nested functions is $\max(1, k^n)$-Lipschitz continuous.

**PROOF.** Consider a $\text{QCTL}^*[\mathcal{F}]$ formula $\varphi$. The proof is by induction on the structure of $\varphi$. The base case where $\varphi$ is an atomic proposition $p$ is easy: pick a tree $t$, a node $u$ and a subset $P \subseteq \text{AP}$; if $p \notin P$, then $F(t, u, P, \varphi)$ is a constant function; if $p \in P$, then $F(t, u, P, \varphi)(\ell_P) = \ell_P(p)(u)$ for any P-labeling $\ell_P$, so that

$$|F(t, u, P, \varphi)(\ell_P) - F(t, u, P, \varphi)(\ell'_P)| = |\ell_P(p)(u) - \ell'_P(p)(u)| \le d(\ell_P, \ell'_P)$$

We now consider the other cases, assuming that the result holds for all subformulas of $\varphi$:

* if $\varphi = \exists q. \psi$, then for any tree $t = (\tau, w)$, any node $u$, any subset $P \subseteq \text{AP}$, and any $P$-labeling $\ell_P$, we have

$$F(t, u, P, \varphi)(\ell_P) = \sup_{\ell_q \{q\}-\text{labeling}} \{\psi\}^{(\tau, w \otimes \ell_P \otimes \ell_q)}(u).$$

By definition of $\sup$, for any $\varepsilon > 0$, there exists a $q$-labeling $\ell_q^\varepsilon$ such that

$$F(t, u, P, \varphi)(\ell_P) \le \{\psi\}^{(\tau, w \otimes \ell_P \otimes \ell_q^\varepsilon)}(u) + \varepsilon.$$

Moreover, for any $P$-labeling $\ell'_P$, we have

$$F(t, u, P, \varphi)(\ell'_P) = \sup_{\ell_q \{q\}-\text{labeling}} \{\psi\}^{(\tau, w \otimes \ell'_P \otimes \ell_q)}(u) \ge \{\psi\}^{(\tau, w \otimes \ell'_P \otimes \ell_q^\varepsilon)}(u).$$

It follows

$$\begin{align*}
F(t, u, P, \varphi)(\ell_P) - F(t, u, P, \varphi)(\ell'_P) &\le \{\psi\}^{(\tau, w \otimes \ell_P \otimes \ell_q^\varepsilon)}(u) - \{\psi\}^{(\tau, w \otimes \ell'_P \otimes \ell_q^\varepsilon)}(u) + \varepsilon \\
&\le \max(1, k^n) \cdot d_{P \cup \{q\}, t}(\ell_P \otimes \ell'_q, \ell'_P \otimes \ell_q^\varepsilon) + \varepsilon \quad \text{(by i.h.)} \\
&\le \max(1, k^n) \cdot d_{P, t}(\ell_P, \ell'_P) + \varepsilon.
\end{align*}$$
By symmetry, we get

$$|F(t, u, P, \varphi)(\ell_P) - F(t, u, P, \varphi)(\ell'_P)| \le \max(1, k^n) \cdot d(\ell_P, \ell'_P) + \varepsilon.$$

As this holds for any positive $\varepsilon$, we have

$$|F(t, u, P, \varphi)(\ell_P) - F(t, u, P, \varphi)(\ell'_P)| \le \max(1, k^n) \cdot d(\ell_P, \ell'_P).$$

• if $\varphi = E\psi$, we apply similar arguments:

$$F(t, u, P, \varphi)(\ell_P) = \sup_{\lambda \in \text{Br}(u)} \{\psi\}^{(\tau, w \otimes \ell_P)}(\lambda).$$

For any $\varepsilon > 0$, there is a branch $\lambda_\varepsilon$ such that

$$F(t, u, P, \varphi)(\ell_P) \le \{\psi\}^{(\tau, w \otimes \ell_P)}(\lambda_\varepsilon) + \varepsilon.$$

Then for any P-labeling $\ell'_P$, we have

$$F(t, u, P, \varphi)(\ell_P) - F(t, u, P, \varphi)(\ell'_P) \le \{\psi\}^{(\tau, w \otimes \ell_P)}(\lambda_\varepsilon) - \{\psi\}^{(\tau, w \otimes \ell'_P)}(\lambda_\varepsilon) + \varepsilon \\ \le \max(1, k^n) \cdot d(\ell_P, \ell'_P) + \varepsilon.$$

As previously, it follows that

$$|F(t, u, P, \varphi)(\ell_P) - F(t, u, P, \varphi)(\ell'_P)| \le \max(1, k^n) \cdot d(\ell_P, \ell'_P).$$

• if $\varphi = f(\varphi_1, ..., \varphi_m)$, then

$$F(t, u, P, \varphi)(\ell_P) = f(F(t, u, P, \varphi_1)(\ell_P), ..., F(t, u, P, \varphi_m)(\ell_P)).$$

Because $f$ is $k$-Lipschitz continuous, we have

$$|F(t, u, P, \varphi)(\ell_P) - F(t, u, P, \varphi)(\ell'_P)| \le k \cdot \max_i \{ |F(t, u, P, \varphi_i)(\ell_P) - F(t, u, P, \varphi_i)(\ell'_P)| \} \\ \le k \cdot \max(1, k^{n-1}) d(\ell_P, \ell'_P).$$

• if $\varphi = \psi_1 U \psi_2$, then

$$F(t, \lambda, P, \varphi)(\ell_P) = \sup_{i \in \mathbb{N}} \left\{ \min(\{\psi_2\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge i}), \min_{j<i}(\{\psi_1\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge j})) \right\}.$$

Then for any $\varepsilon > 0$, there exists $i_\varepsilon$ such that

$$F(t, \lambda, P, \varphi)(\ell_P) \le \min(\{\psi_2\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge i_\varepsilon}), \min_{j<i_\varepsilon}(\{\psi_1\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge j}))) + \varepsilon.$$

Then for any $\ell'_P$,

$$F(t, \lambda, P, \varphi)(\ell_P) - F(t, \lambda, P, \varphi)(\ell'_P) \le \min(\{\psi_2\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge i_\varepsilon}), \min(\{\psi_1\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge j})) - \\ \min(\{\psi_2\}^{(\tau, w \otimes \ell'_P)}(\lambda_{\ge i_\varepsilon}), \min(\{\psi_1\}^{(\tau, w \otimes \ell'_P)}(\lambda_{\ge j}))) + \varepsilon.$$

If the latter minimum is obtained for $\psi_2$ along $\lambda_{\ge i_\varepsilon}$, then we get

$$F(t, \lambda, P, \varphi)(\ell_P) - F(t, \lambda, P, \varphi)(\ell'_P) \le \{\psi_2\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge i_\varepsilon}) - \{\psi_2\}^{(\tau, w \otimes \ell'_P)}(\lambda_{\ge i_\varepsilon}) + \varepsilon.$$

Otherwise, this minimum is reached at some index $j_0 < i_\varepsilon$, and we have

$$F(t, \lambda, P, \varphi)(\ell_P) - F(t, \lambda, P, \varphi)(\ell'_P) \le \{\psi_1\}^{(\tau, w \otimes \ell_P)}(\lambda_{\ge j_0}) - \{\psi_1\}^{(\tau, w \otimes \ell'_P)}(\lambda_{\ge j_0}) + \varepsilon.$$

For both cases, thanks to the induction hypothesis and applying the same arguments as for previous cases, we end up with

$$|F(t, \lambda, P, \varphi)(\ell_P) - F(t, \lambda, P, \varphi)(\ell'_P)| \le \max(1, k^n) \cdot d(\ell_P, \ell'_P).$$

• if $\varphi = X\psi$, 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 $\varphi = \exists q.\psi$, apply also when the quantification is over Boolean atomic propositions, hence we also have the following.

**THEOREM 7.11.** If all functions in $\mathcal{F}$ are $k$-Lipschitz continuous, then every formula in $\text{BQCTL}^*[\mathcal{F}]$ having at most $n$ nested functions is $\max(1, k^n)$-Lipschitz continuous.

# 8 FUTURE WORK

We introduced and studied $\text{SL}[\mathcal{F}]$, a formalism for specifying quality and fuzziness of strategic on-going behavior. We demonstrated the expressiveness of $\text{SL}[\mathcal{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 ($\text{SL}_{1G}[\mathcal{F}]$) that, as in the Boolean case, retains an elementary model-checking problem (it is 2-EXPTIME-complete).

As a means of studying $\text{SL}[\mathcal{F}]$, we extended $\text{QCTL}^*$ to the quantitative setting, leading to the logics $\text{QCTL}^*[\mathcal{F}]$ and $\text{BQCTL}^*[\mathcal{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 $\text{BQCTL}^*[\mathcal{F}]$ allowing to capture pure strategies, while $\text{QCTL}^*[\mathcal{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 $\text{QCTL}^*[\mathcal{F}]$ but decidable for $\text{BQCTL}^*[\mathcal{F}]$, which allows us to prove decidability of model checking $\text{SL}[\mathcal{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 [33]. When applied to $\text{SL}[\mathcal{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 [37, 51] or tax increase [35], and more.

# 9 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".

# REFERENCES

[1] Natasha Alechina, Brian Logan, Nguyen Hoang Nga, and Abdur Rakib. 2010. Resource-bounded alternating-time temporal logic. In *Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'10)*, Wiebe van der Hoek, Gal A. Kaminka, Yves Lespérance, Michael Luck, and Sandeep Sen (Eds.). International Foundation for Autonomous Agents and Multiagent Systems, 481–488.

[2] Shaull Almagor, Udi Boker, and Orna Kupferman. 2014. Discounting in LTL. In *Proceedings of the 20th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'14)* (Lecture Notes in Computer Science, Vol. 8413), Erikz Ábrahám and Klaus Havelund (Eds.). Springer-Verlag, 424–439. https://doi.org/10.1007/978-3-642-54862-8_37

[3] Shaull Almagor, Udi Boker, and Orna Kupferman. 2016. Formally Reasoning about Quality. *J. ACM* 63, 3 (Sept. 2016), 24:1–24:56. https://doi.org/10.1145/2875421

[4] Shaull Almagor and Orna Kupferman. 2016. High-Quality Synthesis Against Stochastic Environments. In *Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL'16)* (Leibniz International Proceedings in Informatics, Vol. 62), Jean-Marc Talbot and Laurent Regnier (Eds.). Leibniz-Zentrum für Informatik, 28:1–28:17. https://doi.org/10.4230/LIPIcs.CSL.2016.28
[5] Shaull Almagor and Orna Kupferman. 2017. Latticed-LTL synthesis in the presence of noisy inputs. *Discrete Event Dynamic Systems* 27, 3 (2017), 547–572. https://doi.org/10.1007/s10626-017-0242-0

[6] Shaull Almagor, Orna Kupferman, and Giuseppe Perelli. 2018. Synthesis of Controllable Nash Equilibria in Quantitative Objective Games. In *Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI'18)*, Jérôme Lang (Ed.). IJCAI organization, 35–41. https://doi.org/10.24963/ijcai.2018/5

[7] Shaull Almagor, Orna Kupferman, Jan Oliver Ringert, and Yaron Velner. 2017. High-Quality Synthesis Against Stochastic Environments. In *Proceedings of the 29th International Conference on Computer Aided Verification (CAV'17)* (Lecture Notes in Computer Science, Vol. 10427), Rupak and Majumdar (Ed.). Springer-Verlag, 353–374. https://doi.org/10.1007/978-3-319-63390-9_19

[8] Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 2002. Alternating-time Temporal Logic. *J. ACM* 49, 5 (Sept. 2002), 672–713. https://doi.org/10.1145/585265.585270

[9] Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, and Sasha Rubin. 2019. Probabilistic strategy logic. In *Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI'19)*. IJCAI, IJCAI organization, 32–38. https://doi.org/10.24963/ijcai.2019/5

[10] Benjamin Aminof, Vadim Malvone, Aniello Murano, and Sasha Rubin. 2018. Graded modalities in Strategy Logic. *Information and Computation* 261, 4 (Aug. 2018), 634–649. https://doi.org/10.1016/j.ic.2018.02.021

[11] Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. 1998. Controller Synthesis for Timed Automata. In *Proceedings of the 5th IFAC Cconference on System Structure and Control (SSC'98)*. Elsevier, 469–474.

[12] Christel Baier, Tomáš Brázdil, Marcus Größer, and Antonín Kučera. 2012. Stochastic Game Logic. *Acta Informatica* 49, 4 (June 2012), 203–224. https://doi.org/10.1007/s00236-012-0156-0

[13] Raphaël Berthon, Bastien Maubert, Aniello Murano, Sasha Rubin, and Moshe Y. Vardi. 2017. Strategy logic with imperfect information. In *Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'17)*. IEEE Computer Society, 1–12. https://doi.org/10.1109/LICS.2017.8005136

[14] Dietmar Berwanger. 2007. Admissibility in Infinite Games. In *Proceedings of the 24th Annual Symposium on Theoretical Aspects of Computer Science (STACS'07)* (Lecture Notes in Computer Science, Vol. 4393). Springer, 188–199. https://doi.org/10.1007/978-3-540-70918-3_17

[15] Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. 2014. Temporal Specifications with Accumulative Values. *ACM Transactions on Computational Logic* 15, 4 (Aug. 2014), 27:1–27:25. https://doi.org/10.1145/2629686

[16] Benedikt Bollig, Normann Decker, and Martin Leucker. 2012. Frequency Linear-time Temporal Logic. In *Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE'12)*, Tiziana Margaria, Zongyang Qiu, and Hongli Yang (Eds.). IEEE Comp. Soc. Press, 85–92. https://doi.org/10.1109/TASE.2012.43

[17] Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jiri Srba. 2008. Infinite Runs in Weighted Timed Automata with Energy Constraints. In *Proceedings of the 6th International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS'08)* (Lecture Notes in Computer Science, Vol. 5215), Franck Cassez and Claude Jard (Eds.). Springer-Verlag, 33–47. https://doi.org/10.1007/978-3-540-85778-5_4

[18] Patricia Bouyer, Patrick Gardy, and Nicolas Markey. 2015. Weighted Strategy Logic with Boolean Goals over One-counter Games. In *Proceedings of the 35th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'15)* (Leibniz International Proceedings in Informatics, Vol. 45), Prahladh Harsha and G. Ramalingam (Eds.). Leibniz-Zentrum für Informatik, 69–83. https://doi.org/10.4230/LIPIcs.FSTTCS.2015.69

[19] Patricia Bouyer, Orna Kupferman, Nicolas Markey, Bastien Maubert, Nello Murano, and Giuseppe Perelli. 2019. Reasoning about Quality and Fuzziness of Strategic Behaviours. In *Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI'19)*. IJCAI organization, 1588–1594. https://doi.org/10.24963/ijcai.2019/220

[20] Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. 2014. Averaging in LTL. In *Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14)* (Lecture Notes in Computer Science, Vol. 8704), Paolo Baldan and Daniele Gorla (Eds.). Springer-Verlag, 266–280. https://doi.org/10.1007/978-3-662-44584-6_19

[21] Romain Brenguier. 2016. Robust Equilibria in Mean-Payoff Games. In *Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'16)* (Lecture Notes in Computer Science, Vol. 9634). Springer, 217–233. https://doi.org/10.1007/978-3-662-49630-5_13

[22] Romain Brenguier, Guillermo A. Pérez, Jean-François Raskin, and Mathieu Sassolas. 2016. Admissibility in Quantitative Graph Games. In *Proceedings of the 36th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'16)* (Leibniz International Proceedings in Informatics), S. Akshay, Akash Lal, Saket Saurabh, and Sandeep Sen (Eds.). Leibniz-Zentrum für Informatik, 42:1–42:14. https://doi.org/10.4230/LIPIcs.FSTTCS.2016.42

[23] Romain Brenguier, Jean-François Raskin, and Ocan Sankur. 2017. Assume-admissible synthesis. *Acta Informatica* 54, 1 (2017), 41–83. https://doi.org/10.1007/s00236-016-0273-2

[24] Thomas Brihaye, Véronique Bruyère, and Julie De Pril. 2014. On Equilibria in Quantitative Games with Reachability/ Safety Objectives. *Theory of Computing Systems* 54, 2 (Feb. 2014), 150–189. https://doi.org/10.1007/s00224-013-9495-7
[25] Thomas Brihaye, François Laroussinie, Nicolas Markey, and Ghassan Oreiby. 2007. Timed Concurrent Game Structures. In *Proceedings of the 18th International Conference on Concurrency Theory (CONCUR'07)* (Lecture Notes in Computer Science, Vol. 4703), Luís Caires and Vasco T. Vasconcelos (Eds.). Springer-Verlag, 445–459. https://doi.org/10.1007/978-3-540-74407-8_30

[26] Véronique Bruyère, Noëmie Meunier, and Jean-François Raskin. 2014. Secure Equilibria in Weighted Games. In *Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic In Computer Science (CSL/LICS'14)*. ACM Press. https://doi.org/10.1145/2603088.2603109

[27] Nils Bulling and Valentin Goranko. 2013. How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract). In *Proceedings of the 1st International Workshop on Strategic Reasoning (SR'13)* (Electronic Proceedings in Theoretical Computer Science, Vol. 112). 33–41. https://doi.org/10.4204/EPTCS.112.8

[28] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. 2003. Resource Interfaces. In *Proceedings of the 3rd International Conference on Embedded Software (EMSOFT'03)* (Lecture Notes in Computer Science, Vol. 2855), Rajeev Alur and Insup Lee (Eds.). Springer-Verlag, 117–133. https://doi.org/10.1007/978-3-540-45212-6_9

[29] Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot, and Jean-François Raskin. 2014. Doomsday Equilibria for Omega-Regular Games. In *Proceedings of the 15th International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI'14)* (Lecture Notes in Computer Science, Vol. 8318), Kenneth L. McMillan and Xavier Rival (Eds.). Springer-Verlag, 78–97. https://doi.org/10.1007/978-3-642-54013-4_5

[30] Krishnendu Chatterjee, Thomas A Henzinger, and Marcin Jurdziński. 2006. Games with secure equilibria. *Theoretical Computer Science* 365, 1-2 (2006), 67–82. https://doi.org/10.1016/j.tcs.2006.07.032

[31] Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. 2010. Strategy Logic. *Information and Computation* 208, 6 (June 2010), 677–693. https://doi.org/10.1016/j.ic.2009.07.004

[32] Taolue Chen and Jian Lu. 2007. Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm. In *Proceedings of the 4th International Conference on Fuzzy Systems and Knowledge Discovery (FSKD'07)*, J. Lei (Ed.). IEEE Comp. Soc. Press, 35–39. https://doi.org/10.1109/FSKD.2007.458

[33] Hana Chockler, Orna Kupferman, and Moshe Y. Vardi. 2006. Coverage Metrics for Formal Verification. *Software Tools for Technology Transfer* 8, 4-5 (2006), 373–386. https://doi.org/10.1007/s10703-006-0001-6

[34] Edmund M. Clarke and E. Allen Emerson. 1982. Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In *Proceedings of the 3rd Workshop on Logics of Programs (LOP'81)* (Lecture Notes in Computer Science, Vol. 131), Dexter C. Kozen (Ed.). Springer-Verlag, 52–71. https://doi.org/10.1007/BFb0025774

[35] Richard Cole, Yevgeniy Dodis, and Tim Roughgarden. 2006. How much can taxes help selfish routing? *J. Comput. System Sci.* 72, 3 (2006), 444–467. https://doi.org/10.1016/j.jcsc.2005.09.010

[36] Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. 2005. Model checking discounted temporal properties. *Theoretical Computer Science* 345, 1 (Nov. 2005), 139–170. https://doi.org/10.1016/j.tcs.2005.07.033

[37] Filipe Costa de Souza and Leandro Chaves Rego. 2016. Mixed equilibrium in 2 × 2 normal form games: when burning money is rational. *Pesquisa Operacional* 36 (04 2016), 81–99.

[38] Dario Della Monica and Aniello Murano. 2018. Parity-energy ATL for Qualitative and Quantitative Reasoning in MAS. In *Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'18)*, Elisabeth André, Sven Koenig, Mehdi Dastani, and Gita Sukthankar (Eds.). International Foundation for Autonomous Agents and Multiagent Systems, 1441–1449.

[39] Manfred Droste, Werner Kuich, and George Rahonis. 2008. Multi-Valued MSO Logics over Words and Trees. *Fundamenta Informaticae* 84, 13-4 (2008), 305–327.

[40] Manfred Droste, Temur Kutsia, George Rahonis, and Wolfgang Schreiner. 2017. MK-fuzzy Automata and MSO Logics. In *Proceedings of the 8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF'17)* (Electronic Proceedings in Theoretical Computer Science, Vol. 256), Patricia Bouyer, Andrea Orlandini, and Pierluigi San Pietro (Eds.). 106–120. https://doi.org/10.4204/EPTCS.256.8

[41] Andrzej Ehrenfeucht and Jan Mycielski. 1979. Positional strategies for mean payoff games. *International Journal of Game Theory* 8, 2 (June 1979), 109–113. https://doi.org/10.1007/BF01768705

[42] E. Allen Emerson and Joseph Y. Halpern. 1986. "Sometimes" and "Not Never" Revisited: On Branching versus Linear Time Temporal Logic. *J. ACM* 33, 1 (Jan. 1986), 151–178.

[43] E. Allen Emerson and Charanjit S. Jutla. 1991. Tree Automata, Mu-Calculus and Determinacy. In *Proceedings of the 32nd Annual Symposium on Foundations of Computer Science (FOCS'91)*. IEEE Comp. Soc. Press, 368–377. https://doi.org/10.1109/SFCS.1991.185392

[44] E. Allen Emerson and Chin-Laung Lei. 1987. Modalities for Model Checking: Branching Time Logic Strikes Back. *Science of Computer Programming* 8 (1987), 275–306. https://doi.org/10.1016/0167-6423(87)90036-0
[45] Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. 2018. Quantifying Bounds in Strategy Logic. In *Proceedings of the 27th EACSL Annual Conference on Computer Science Logic (CSL'18)* (Leibniz International Proceedings in Informatics, Vol. 119). Leibniz-Zentrum für Informatik, 23:1–23:23. https://doi.org/10.4230/LIPIcs.CSL.2018.23

[46] Jerzy Filar and Koos Vrieze. 1997. *Competitive Markov decision processes*. Springer-Verlag.

[47] Dana Fisman, Orna Kupferman, and Yoad Lustig. 2010. Rational synthesis. In *Proceedings of the 16th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'10)* (Lecture Notes in Computer Science, Vol. 6015), Javier Esparza and Rupak Majumdar (Eds.). Springer-Verlag, 190–204. https://doi.org/10.1007/978-3-642-12002-2_16

[48] Tim French. 2001. Decidability of quantified propositional branching time logics. In *Proceedings of the 14th Australian Joint Conference on Artificial Intelligence (AJCAI'01)*. 165–176. https://doi.org/10.1007/3-540-45656-2_15

[49] Achille Frigeri, Liliana Pasquale, and Paola Spoletini. 2014. Fuzzy time in linear temporal logic. *ACM Transactions on Computational Logic* 15, 4 (2014), 30. https://doi.org/10.1145/2629606

[50] David Harel and Amir Pnueli. 1985. On the development of reactive systems. In *Logics and Models of Concurrent Systems*. NATO Advanced Summer Institutes, Vol. F-13. Springer, 477–498.

[51] Jason D. Hartline and Tim Roughgarden. 2008. Optimal mechanism design and money burning. In *Proceedings of the 40th ACM Symposium on Theory of Computing (STOC'08)*. 75–84. https://doi.org/10.1145/1374376.1374390

[52] Thomas A. Henzinger and Vinayak S. Prabhu. 2006. Timed Alternating-Time Temporal Logic. In *Proceedings of the 4th International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS'06)* (Lecture Notes in Computer Science, Vol. 4202), Eugene Asarin and Patricia Bouyer (Eds.). Springer-Verlag, 1–17. https://doi.org/10.1007/11867340_1

[53] Wojciech Jamroga, Beata Konikowska, and Wojciech Penczek. 2016. Multi-Valued Verification of Strategic Ability. In *Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'16)*, Catholijn M. Jonker, Stacy Marsella, John Thangarajah, and Karl Tuyls (Eds.). International Foundation for Autonomous Agents and Multiagent Systems, 1180–1189.

[54] Orna Kupferman. 1999. Augmenting branching temporal logics with existential quantification over atomic propositions. *Journal of Logic and Computation* 9, 2, 135–147. https://doi.org/10.1093/logcom/9.2.135

[55] Orna Kupferman, Parthasarathy Madhusudan, Pazhamaneri Subramaniam Thiagarajan, and Moshe Y. Vardi. 2000. Open Systems in Reactive Environments: Control and Synthesis. In *Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00)*. 92–107. https://doi.org/10.1007/3-540-44618-4_9

[56] Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. 2016. Synthesis with rational environments. *Annals of Mathematics and Artificial Intelligence* 78, 1 (2016), 3–20. https://doi.org/10.1007/s10472-016-9508-8

[57] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. 2000. An Automata-Theoretic Approach to Branching-Time Model Checking. *Journal of the ACM* 47, 2 (2000), 312–360. https://doi.org/10.1145/333979.333987

[58] Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. 2000. An automata-theoretic approach to branching-time model checking. *Journal of the ACM* 47, 2 (2000), 312–360. https://doi.org/10.1145/333979.333987

[59] Khaled Ben Lamine and Froduald Kabanza. 2000. Using fuzzy temporal logic for monitoring behavior-based mobile robots. In *Proc. of IASTED Int. Conf. on Robotics and Applications*. 116–121.

[60] François Laroussinie and Nicolas Markey. 2014. Quantified CTL: Expressiveness and Complexity. *Logical Methods in Computer Science* 10, 4 (2014). https://doi.org/10.2168/LMCS-10(4:17)2014

[61] François Laroussinie and Nicolas Markey. 2015. Augmenting ATL with strategy contexts. *Information and Computation* 245 (2015), 98–123. https://doi.org/10.1016/j.ic.2014.12.020

[62] François Laroussinie, Nicolas Markey, and Ghassan Oreibi. 2006. Model-Checking Timed ATL for Durational Concurrent Game Structures. In *Proceedings of the 4th International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS'06)* (Lecture Notes in Computer Science, Vol. 4202), Eugene Asarin and Patricia Bouyer (Eds.). Springer-Verlag, 245–259. https://doi.org/10.1007/11867340_18

[63] Jan Łukasiewicz. 1920. O Logice Trójwartościowej. *Studia Filozoficzne* (1920).

[64] Rupak Majumdar, Elaine Render, and Paulo Tabuada. 2011. Robust discrete synthesis against unspecified disturbances. In *Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC'11)*. ACM, 211–220. https://doi.org/10.1145/1967701.1967732

[65] Vadim Malvone, Aniello Murano, and Loredana Sorrentino. 2016. Concurrent Multi-Player Parity Games. In *Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems (AAMAS'16)*. ACM, 689–697.

[66] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. 2012. What Makes ATL* Decidable? A Decidable Fragment of Strategy Logic. In *Proceedings of the 23rd International Conference on Concurrency Theory (CONCUR'12)* (Lecture Notes in Computer Science, Vol. 7454), Maciej Koutny and Irek Ulidowski (Eds.). Springer-Verlag, 193–208. https://doi.org/10.1007/978-3-642-32940-1_15

[67] Fabio Mogavero, Aniello Murano, Giuseppe Perelli, and Moshe Y. Vardi. 2014. Reasoning About Strategies: On the Model-Checking Problem. *ACM Transactions on Computational Logic* 15, 4 (Aug. 2014), 34:1–34:47. https://doi.org/10.1145/2631917
[68] David E. Muller and Paul E. Schupp. 1995. Simulating Alternating Tree Automata by Nondeterministic Automata: New Results and New Proofs of the Theorems of Rabin, McNaughton and Safra. *Theoretical Computer Science* 141, 1&2 (1995), 69–107. https://doi.org/10.1016/0304-3975(94)00214-4

[69] Noam Nisan and Amir Ronen. 1999. Algorithmic Mechanism Design. In *Proceedings of the 31st ACM Symposium on Theory of Computing (STOC'99)*. ACM, 129–140. https://doi.org/10.1145/301250.301287

[70] Noam Nisan, Tim Roughgarden, Éva Tardos, and Vijay V. Vazirani. 2007. *Algorithmic Game Theory*. Cambridge University Press. https://doi.org/10.1017/CBO9780511800481

[71] Nir Piterman. 2007. From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. *Logical Methods in Computer Science* 3, 3 (2007), 1–21. https://doi.org/10.2168/LMCS-3(3:5)2007

[72] Amir Pnueli. 1981. The Temporal Semantics of Concurrent Programs. *Theoretical Computer Science* 13 (1981), 45–60. https://doi.org/10.1016/0304-3975(81)90110-9

[73] Amir Pnueli and Roni Rosner. 1989. On the Synthesis of a Reactive Module. In *Conference Record of the 16th ACM Symposium on Principles of Programming Languages (POPL '89)*. ACM Press, 179–190. https://doi.org/10.1145/75277.75293

[74] Michael O Rabin. 1969. Decidability of second-order theories and automata on infinite trees. *TAMS* 141 (1969), 1–35. https://doi.org/10.1090/S0002-9947-1969-0246760-1

[75] George Rahonis. 2009. Fuzzy Languages. In *Handbook of Weighted Automata*, Manfred Droste, Werner Kuich, and Walter Vogler (Eds.). Springer-Verlag, Chapter 12, 481–517. https://doi.org/10.1007/978-3-642-01492-512

[76] Lloyd S. Shapley. 1953. Stochastic games. *Proceedings of the National Academy of Sciences* 39, 10 (Oct. 1953), 1095–1100. https://doi.org/10.1073/pnas.39.10.1095

[77] A Prasad Sistla. 1983. *Theoretical Issues in the Design and Certification of Distributed Systems*. Ph.D. Dissertation. Harvard University, Cambridge, MA, USA.

[78] Ufuk Topcu, Necmiye Ozay, Jun Liu, and Richard M. Murray. 2012. On synthesizing robust discrete controllers under modeling uncertainty. In *Proceedings of the 15th ACM international conference on Hybrid Systems: Computation and Control (HSCC'12)*. ACM, 85–94. https://doi.org/10.1145/2185632.2185648

[79] Michael Ummels. 2010. *Stochastic Multiplayer Games: Theory and Algorithms*. Master's thesis. RWTH Aachen, Germany.

[80] M.Y. Vardi and P. Wolper. 1986. Automata-Theoretic Techniques for Modal Logics of Programs. *Journal of Computer and Systems Science* 32, 2 (1986), 182–221. https://doi.org/10.1016/0022-0000(86)90026-7

[81] Steen Vester. 2015. On the Complexity of Model-checking Branching and Alternating-time Temporal Logics in One-counter systems. In *Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA'15) (Lecture Notes in Computer Science, Vol. 9364)*, Bernd Finkbeiner, Geguang Pu, and Lijun Zhang (Eds.). Springer-Verlag, 361–377. https://doi.org/10.1007/978-3-319-24953-7_27

[82] Hao Wang. 1990. *Computation, Logic, Philosophy*. Mathematics ans its applications, Vol. 2. Springer-Verlag. https://doi.org/10.1007/978-94-009-2356-0

[83] Uri Zwick and Mike Paterson. 1996. The complexity of mean payoff games on graphs. *Theoretical Computer Science* 158, 1-2 (1996), 343–359.