Reasoning about Quality and Fuzziness of Strategic Behaviours

TL;DR

This paper introduces FSL, a quantitative extension of Strategy Logic that assigns real-valued satisfaction levels to strategic behaviors in multi-agent systems, enabling nuanced reasoning about quality and fuzziness.

Contribution

It presents FSL, a novel logic combining strategic reasoning with quantitative satisfaction, and provides a model-checking algorithm for this expressive framework.

Findings

FSL can express stability concepts in multi-agent systems.

FSL generalizes fuzzy temporal logics.

A model-checking algorithm for FSL is developed.

Abstract

Temporal logics are extensively used for the specification of on-going behaviours of reactive systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviours in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalise concepts such as certainty or quality. We introduce and study FSL---a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an FSL 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 FSL in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for our logic, based on a quantitative extension of Quantified CTL*.

Equations

$$\phi$$

$$\psi$$

$$[[p{]]}_{\chi }^{\text{calG}}(\rho )$$

$$[[⟨⟨x⟩⟩\phi {]]}_{\chi }^{\text{calG}}(\rho )$$

$$[[(a,x)\phi {]]}_{\chi }^{\text{calG}}(\rho )$$

$$[[\mathsf{A}\psi {]]}_{\chi }^{\text{calG}}(\rho )$$

$$[[f({\phi }_1,\dots ,{\phi }_m){]]}_{\chi }^{\text{calG}}(\rho )$$

$$[[\phi {]]}_{\chi }^{\text{calG}}(\pi ,i)$$

$$[[\mathsf{X}\psi {]]}_{\chi }^{\text{calG}}(\pi ,i)$$

$$[[{\psi }_1\mathsf{U}{\psi }_2{]]}_{\chi }^{\text{calG}}(\pi ,i)$$

$$[[f({\psi }_1,\dots ,{\psi }_m){]]}_{\chi }^{\text{calG}}(\pi ,i)$$

$${\phi }_{\text{rescue}}=⟨⟨x⟩⟩⟨⟨y⟩⟩(c,x)(g,y)\mathsf{A}(\text{dist}(p_{\vec{\gamma }},q_{\vec{\gamma }})\mathsf{U}\text{safe})$$

$${\phi }_{\text{spy}}=⟨⟨x⟩⟩[[z]]⟨⟨y⟩⟩(c,x)(g,y)(v,z)\mathsf{A}(\text{dist}(p_{\vec{\gamma }},q_{\vec{\gamma }})\mathsf{U}\text{safe})$$

$${\phi }_{\mathtt{synt}}=⟨⟨x⟩⟩[[y]](c,x)(e,y)\mathsf{A}\psi$$

$${\phi }_{\mathtt{synt}}=⟨⟨x_1⟩⟩[[y_1]]\cdots ⟨⟨x_n⟩⟩[[y_n]](c_1,x_1)(e_1,y_1)\dots (c_n,x_n)(e_n,y_n)\mathsf{A}\psi .$$

$${\phi }_{\mathsf{NE}}((x_i{)}_{a_i\in \text{Agt}})=(a_1,x_1)\dots (a_n,x_n)\underset{a_i\in \text{Agt}}{\bigwedge }⟨⟨y_i⟩⟩((a_i,y_i)\mathsf{A}{\phi }_i)⪯\mathsf{A}{\phi }_i$$

$${\phi }_{\overline{\mathsf{NE}}}((x_i{)}_{a_i\in \text{Agt}})=⟨⟨y⟩⟩(a_1,x_1)\dots (a_n,x_n)\underset{a_i\in \text{Agt}}{\bigvee }\text{diff}((a_i,y)\mathsf{A}{\phi }_i,\mathsf{A}{\phi }_i).$$

$${\phi }_{\mathsf{SE}}(x_1,x_2)=(a_1,x_1)(a_2,x_2)\underset{i\in \{1,2\}}{\bigwedge }⟨⟨y⟩⟩((a_i,y)\mathsf{A}{\phi }_1,(a_i,y)\mathsf{A}{\phi }_2){⪯}_i(\mathsf{A}{\phi }_1,\mathsf{A}{\phi }_2)$$

$${\phi }_{\text{wRS}}((x_i{)}_{0\le i\le n})$$

$$⟨⟨x_0⟩⟩⟨⟨x_1⟩⟩\dots ⟨⟨x_n⟩⟩{\phi }_{\text{wRS}}((x_i{)}_{0\le i\le n})$$

$${\phi }_{\text{sRS}}(x_0)$$

$$⟨⟨x_0⟩⟩{\phi }_{\text{sRS}}(x_0)$$

$${\phi }_{\text{core}}(x_i{)}_{a_i\in \text{Agt}}$$

$$\phi$$

$$\psi$$

$$[[p{]]}^t(u)$$

$$[[\exists p.\phi {]]}^t(u)$$

$$[[\mathsf{E}\psi {]]}^t(u)$$

$$[[f({\phi }_1,\dots ,{\phi }_n){]]}^t(u)$$

$$[[\phi {]]}^t(\lambda )$$

$$[[\mathsf{X}\psi {]]}^t(\lambda )$$

$$[[{\psi }_1\mathsf{U}{\psi }_2{]]}^t(\lambda )$$

$$[[f({\psi }_1,\dots ,{\psi }_n){]]}^t(\lambda )$$

$$V_{\phi }=\{[[\phi {]]}^t(u)\mid t\text{is a (AP,V)-labelled tree}\text{and}u\in t\}$$

$$V_{\psi }=\{[[\psi {]]}^t(\lambda )\mid t\text{is a (AP,V)-labelled tree},u\in t\text{and}\lambda \in \text{Br}(u)\}$$

$${\mathcal{A}}^P=\underset{v\in {\tilde{V}}_{\mathsf{E}\psi }\cap P}{\bigvee }{\mathcal{N}}^{E=v}\wedge {\mathcal{U}}^{A\le v}.$$

$$\begin{array}[]{lr}(p)^{\,g}=p&((a,x)\varphi)^{\,g}=(\varphi)^{\,g[a\mapsto x]}\\ \lx@intercol(\langle\!\langle x\rangle\!\rangle\varphi)^{\,g}=\exists p_{c_{1}}^{x}\ldots\exists p_{c_{m}}^{x}.\Big{(}\varphi_{\text{str}}(x)\wedge(\varphi)^{\,g}\Big{)},\hfil\lx@intercol\\[10.0pt] \lx@intercol\hfil\mbox{where }\varphi_{\text{str}}(x)={{\mathsf{A}}}{{\mathsf{G}}}\Big{(}\bigvee_{c\in\Act}(p_{c}^{x}\wedge\bigwedge_{c^{\prime}\neq c}\neg p_{c^{\prime}}^{x})\Big{)}\lx@intercol\\ \lx@intercol({{\mathsf{A}}}\psi)^{\,g}={{\mathsf{A}}}(\psi_{\text{out}}(g)\rightarrow(\psi)^{\,g})\hfil\lx@intercol\\[10.0pt] \lx@intercol\hfil\quad\quad\quad\mbox{where }\psi_{\text{out}}(g)={{\mathsf{G}}}\left(\bigwedge_{\textsf{v}\in\textsf{V}}\left(p_{\textsf{v}}\rightarrow\bigvee_{\vec{c}\in\Act^{\Agt}}\left(\bigwedge_{a\in\mathsf{dom}(f)}p_{\vec{c}(a)}^{f(a)}\wedge{{\mathsf{X}}}p_{\Delta(\textsf{v},\vec{c})}\right)\right)\right)\lx@intercol\\[10.0pt] \lx@intercol(f(\varphi_{1},\ldots,\varphi_{n}))^{\,g}=f((\varphi_{1})^{\,g},\ldots,(\varphi_{n})^{\,g})\hfil\lx@intercol\end{array}$$

$$(\phi {)}^g$$

$$(\psi \mathsf{U}{\psi }^{\prime }{)}^g$$

Full text

Reasoning about Quality and Fuzziness of Strategic Behaviours

Patricia Bouyer

  

Orna Kupferman

  

Nicolas Markey

  

Bastien Maubert

  

Aniello Murano

  

Giuseppe Perelli

1 Introduction

One of the significant developments in formal reasoning has been the use of temporal logics for the specification of on-going behaviours of reactive systems [61, 31, 37]. Traditional temporal logics are interpreted over Kripke structures, modelling closed systems, and can quantify the computations of the systems in a universal and existential manner. The need to reason about multi-agents systems has led to the development of specification formalisms that enable the specification of on-going strategic behaviours in multi-agent systems [7, 28, 57]. Essentially, these formalisms, most notably ATL, $\textsf{{ATL}}^{\star}$, and Strategy Logic (SL), include quantification of 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.

The duration of games in game theory is typically finite and the outcome of the game depends on its final position [58, 59]. In contrast, agents in multi-agent systems maintain an on-going interaction with each other [44], and reasoning about their behaviour refers not to their final state (in fact, we consider non-terminating systems, with no final state) but rather to the language of computations that they generate. While SL, which subsumes $\textsf{{ATL}}^{\star}$ enables the specification of rich on-going strategic behaviours, its semantics is Boolean: a system may satisfy a specification or it may not. 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 only after being convinced that the automatic procedure that replaces it generates 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 the strategies.

The logic ${\textsf{LTL}}{[\mathcal{F}]}$ is a multi-valued logic that augments LTL with quality operators [3]. The satisfaction value of an ${\textsf{LTL}}{[\mathcal{F}]}$ formula is a real value in $[0,1]$, where the higher the value, the higher the quality in which the computation satisfies the specification. The quality operators in $\mathcal{F}$ can prioritise different scenarios or reduce the satisfaction value of computations in which delays occur. For example, the set $\mathcal{F}$ may contain the $\min\{x,y\}$, $\max\{x,y\}$, and $1-x$ functions, which are the standard quantitative analogues of the $\wedge$, $\vee$, and $\neg$ operators. The novelty of ${\textsf{LTL}}{[\mathcal{F}]}$ is the ability to manipulate values by arbitrary functions. For example, $\mathcal{F}$ may contain the weighted-average function $\oplus_{\lambda}$. The satisfaction value of the formula $\psi_{1}\oplus_{\lambda}\psi_{2}$ is the weighted (according to $\lambda$) average between the satisfaction values of $\psi_{1}$ and $\psi_{2}$. This enables the specification of the quality of the system to interpolate different aspects of it. As an example, consider the ${\textsf{LTL}}{[\mathcal{F}]}$ formula ${{\mathsf{G}}}({\it req}\rightarrow({\it grant}\oplus_{\frac{2}{3}}{{\mathsf{X}}}{\it grant}))$. The formula states that we want requests to be granted immediately and the grant to hold for two transactions. When this always holds, the satisfaction value is $\frac{2}{3}+\frac{1}{3}=1$. We are quite okay with grants that are given immediately and last for only one transaction, in which case the satisfaction value is $\frac{2}{3}$, and less content when grants arrive with a delay, in which case the satisfaction value is $\frac{1}{3}$.

We introduce and study ${\textsf{{SL}}}{[\mathcal{F}]}$: an analogous multi-valued extension of SL. In addition to the quantitative semantics that arises from the functions in $\mathcal{F}$, another important element of ${\textsf{{SL}}}{[\mathcal{F}]}$ is that its semantics is defined with respect to weighted multi-agent systems, namely ones where atomic propositions have truth values in $[0,1]$, reflecting quality or certainty. Thus, a model-checking procedure for ${\textsf{{SL}}}{[\mathcal{F}]}$, which is our main contribution, enables formal reasoning about both quality and fuzziness of strategic behaviours.

As a motivating example, consider security drones that may patrol different height levels. Using ${\textsf{{SL}}}{[\mathcal{F}]}$, we can specify, for example (see specific formulas in Section 2.4), the quality of strategies for the drones whose objectives are to fly above and below all uncontrollable drones and perform certain actions when uncontrollable drones exhibit some disallowed behaviour. Indeed, the multi-valued atomic propositions are used to specify the different heights, temporal operators are used for specifying on-going behaviours, the functions in $\mathcal{F}$ may be used to refer to these behaviours in a quantitative manner, for example to compare heights and to specify the satisfaction level that the designer gives to different possible scenarios. Note that the ${\textsf{{SL}}}{[\mathcal{F}]}$ formula does not specify the ability of the drones to behave in some desired manner. Rather, it associates a satisfaction value in $[0,1]$ with each behaviour. This suggests that ${\textsf{{SL}}}{[\mathcal{F}]}$ can be used not only for a quantitative specification of strategic behaviours but also for quantizing notions from game theory that are traditionally Boolean. For example (see specific formulas in Section 2.4), beyond specifying that the agents are in a Nash Equilibrium, we can specify how far they are from an equilibrium, namely how much an agent may gain by a deviation that witnesses the instability. As a result we can express concepts such as $\epsilon$-Nash Equilibria [59].

The logic ${\textsf{{SL}}}{[\mathcal{F}]}$ enables the quantification of strategies for the agents. We show that the quantification of strategies can be reduced to a Boolean quantification of atomic propositions, which enables us to reduce the model-checking problem of ${\textsf{{SL}}}{[\mathcal{F}]}$ to that of \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} – an extension of \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}} [3] with quantified Boolean atomic propositions. A general technique for $\textsf{{CTL}}^{\star}$ model-checking algorithms is to repeatedly evaluate the innermost state subformula by viewing it as an (existentially or universally quantified) LTL formula, and add a fresh atomic proposition that replaces this subformula [39]. This general technique is applied also to \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}}, with the fresh atomic propositions being weighted [3]. For \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} formulas, however, one cannot apply it. Indeed, the externally quantified atomic propositions may appear in different subformulas, and we cannot evaluate them one by one without fixing the same assignment for the quantified atomic propositions. Instead, we extend the automaton-theoretic approach to $\textsf{{CTL}}^{\star}$ model-checking [49] to handle quantified propositions: given a \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} formula $\psi$ and predicate $P\subseteq[0,1]$, we construct an alternating parity tree automaton that accepts exactly all the weighted trees $t$ such that the satisfaction value of $\psi$ in $t$ is in $P$. The translation, and hence the complexity of the model-checking problem, is non-elementary. More precisely we show that it is $(k+1)$-Exptime -complete for formulas involving at most $k$ quantifications on atomic propositions, and we show a similar complexity result for ${\textsf{{SL}}}{[\mathcal{F}]}$, in terms of nesting of strategy quantifiers.

Related works.

There have been long lines of works about games with quantitative objectives (in a broad sense), e.g. stochastic games [63, 41], timed games [9], or weighted games with various kinds of objectives (parity [38], mean-payoff [36] or energy [25, 15]). This does not limit to zero-sum games, but also includes the study of various solution concepts (see for instance [64, 23, 21, 19, 5]). Similarly, extensions of the classical temporal logics LTL and CTL with quantitative semantics have been studied in different contexts, with discounting [33, 2], averaging [14, 17], or richer constructs [13, 3]. In contrast, the study of quantitative temporal logics for strategic reasoning has remained rather limited: works on ${\textsf{LTL}}{[\mathcal{F}]}$ include algorithms for synthesis and rational synthesis [3, 4, 5, 6], but no logic combines the quantitative aspect of ${\textsf{LTL}}{[\mathcal{F}]}$ with the strategic reasoning offered by SL. Thus, to the best of our knowledge, our model-checking algorithm for ${\textsf{{SL}}}{[\mathcal{F}]}$ is the first decidability result for a quantitative extension of a strategic specification formalism (without restricting to bounded-memory strategies).

Baier and others have focused on a variant of SL in a stochastic setting [10]; 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 [16]; only a periodicity property was proven, and no model-checking algorithm is known in that setting as well. Finally, Graded SL [8] 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 [29], timed ATL [46, 22], multi-valued ATL [47], and weighted versions of ATL [54, 24, 65]. Finally, some works have considered non-quantitative ATL with quantitative constraints on the set of allowed strategies [1, 35], 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_{0}w_{1}\ldots w_{n}$ is $|w|:=n+1$, and $\mbox{{last}}(w):=w_{n}$ is its last letter. Given a finite (resp. infinite) word $w$ and $0\leq i<|w|$ (resp. $i\in\mathbb{N}$), we let $w_{i}$ be the letter at position $i$ in $w$, $w_{\leq i}=w_{0}\ldots w_{i}$ is the (nonempty) prefix of $w$ that ends at position $i$ and $w_{\geq i}=w_{i}w_{i+1}\ldots$ is the suffix of $w$ that starts at position $i$. As usual, for any partial function $f$, we write $\mathsf{dom}(f)$ for the domain of $f$. Strategy logic with functions, denoted ${\textsf{{SL}}}{[\mathcal{F}]}$, generalises both SL [28, 57] and ${\textsf{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 [40], which does not add expressiveness with respect to the classic semantics [57] but presents several benefits (see [40] for more details), one of them being that it makes the connection with Quantified CTL tighter.

Definition 2.1** (Syntax).**

Let $\mathcal{F}\subseteq\{f\colon[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 ${\textsf{{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 ${\textsf{{SL}}}{[\mathcal{F}]}$ formulas is defined by the following grammar:

[TABLE]

where $p\in\AP$, $x\in\Var$, $a\in\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 ${{\mathsf{X}}}$ and ${{\mathsf{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: ${\perp\colonequals\neg\top}$, ${\varphi\wedge\varphi^{\prime}\colonequals\neg(\neg\varphi\vee\neg\varphi^{\prime})}$, ${\varphi\rightarrow\varphi^{\prime}\colonequals\neg\varphi\vee\varphi^{\prime}}$, ${{{\mathsf{F}}}\psi\colonequals\top{{\mathsf{U}}}\psi}$, ${{{\mathsf{G}}}\psi\colonequals\neg{{\mathsf{F}}}\neg\psi}$ and ${[\![x]\!]\varphi\colonequals\neg\langle\!\langle x\rangle\!\rangle\neg\varphi}$. Intuitively, the value of formula $\varphi\vee\varphi^{\prime}$ is the maximal value of the two formulas $\varphi$ and $\varphi^{\prime}$, $\varphi\wedge\varphi^{\prime}$ takes the minimal value of the two formulas, and the value of $\neg\varphi$ is one minus that of $\varphi$. The implication $\varphi\rightarrow\varphi^{\prime}$ thus takes the maximal value between that of $\varphi^{\prime}$ and one minus that of $\varphi$. In a Boolean setting, we assume that the values of the atomic propositions are in $\{0,1\}$ ([math] represents false whereas $1$ represents true), and so are the output values of functions in $\mathcal{F}$. One can then check that $\varphi\vee\varphi^{\prime}$, $\varphi\wedge\varphi^{\prime}$, $\neg\varphi$ and $\varphi\rightarrow\varphi^{\prime}$ 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, ${\textsf{{SL}}}{[\mathcal{F}]}$ formulas are interpreted on weighted concurrent game structures, in which atomic propositions have values in $[0,1]$, and that we now present.

Definition 2.2**.**

A weighted concurrent game structure (WCGS) is a tuple $\calG=(\penalty 10000\AP,\Agt,\penalty-1000\Act,\penalty-1000\textsf{V},\penalty-1000\textsf{v}_{\iota},\penalty-1000\Delta,\textsf{{w}}\penalty 10000)$ where $\AP$ is a finite set of atomic propositions, $\Agt$ is a finite set of agents, $\Act$ is a finite set of actions, V is a finite set of states, $\textsf{v}_{\iota}\in\textsf{V}$ is an initial state, $\Delta\colon\textsf{V}\times\Act^{\Agt}\to\textsf{V}$ is the transition function, and $\textsf{{w}}\colon\textsf{V}\to[0,1]^{\AP}$ is a weight function.

An element of $\Act^{\Agt}$ is a joint action. For ${\textsf{v}\in\textsf{V}}$, we let $\succs(\textsf{v})$ be the set $\{\textsf{v}^{\prime}\in\textsf{V}\mid\exists\vec{c}\in\Act^{\Agt}.\ \textsf{v}^{\prime}=\Delta(\textsf{v},\vec{c})\}$. For the sake of simplicity, we assume in the sequel that $\succs(\textsf{v})\not=\varnothing$ for all $\textsf{v}\in\textsf{V}$. A play in $\calG$ is an infinite sequence $\pi=(\textsf{v}_{i})_{i\in\bbN}$ of states in V such that $\textsf{v}_{0}=\textsf{v}_{\iota}$ and $\textsf{v}_{i}\in\succs(\textsf{v}_{i-1})$ for all $i>0$. We write $\Play_{\calG}$ for the set of plays in $\calG$, and $\Play_{\calG}(v)$ for the set of plays in $\calG$ starting from $v$. In this and all similar notations, we might omit to mention $\calG$ when it is clear from the context. A (strict) prefix of a play $\pi$ is a finite sequence $\rho=(\textsf{v}_{i})_{0\leq i\leq L}$, for some $L\in\bbN$, which we denote $\pi_{\leq L}$. We write $\Prefx(\pi)$ for the set of strict prefixes of play $\pi$. Such finite prefixes are called histories, and we let $\Hist_{\calG}(\textsf{v})=\Prefx(\Play_{\calG}(\textsf{v}))$ and $\Hist_{\calG}=\bigcup_{\textsf{v}\in\textsf{V}}\Hist_{\calG}(\textsf{v})$. We extend the notion of strict prefixes and the notation $\Prefx$ to histories in the natural way, requiring in particular that $\rho\notin\Prefx(\rho)$. A (finite) extension of a history $\rho$ is any history $\rho^{\prime}$ such that $\rho\in\Prefx(\rho^{\prime})$. A strategy is a mapping $\sigma\colon\Hist_{\calG}\to\Act$, and we write ${{\mathrm{Str}}}_{\calG}$ for the set of strategies in $\calG$. An assignment is a partial function $\chi\colon\Var\cup\Agt\rightharpoonup{{\mathrm{Str}}}_{\calG}$, 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 $\Out(\chi,\rho)$ of plays $\pi=\rho\cdot\textsf{v}_{1}\textsf{v}_{2}\ldots$ such that for every ${i\in\bbN}$, there exists a joint action $\vec{c}\in\Act^{\Agt}$ such that for each agent $a\in\mathsf{dom}(\chi),\vec{c}(a)=\chi(a)(\pi_{\leq|\rho|+i-1})$ and $\textsf{v}_{i+1}=\Delta(\textsf{v}_{i},\vec{c})$, where $\textsf{v}_{0}=\mbox{{last}}(\rho)$.

Definition 2.3** (Semantics).**

Consider a WCGS $\calG=(\penalty 10000\AP,\Agt,\penalty-1000\Act,\penalty-1000\textsf{V},\penalty-1000\textsf{v}_{\iota},\penalty-1000\Delta,\textsf{{w}}\penalty 10000)$, a set of variables $\Var$, and a partial assignment $\chi$ of strategies for $\Agt$ and $\Var$. Given an ${\textsf{{SL}}}{[\mathcal{F}]}$ state formula $\varphi$ and a history $\rho$, we use $\llbracket\varphi\rrbracket^{\calG}_{\chi}(\rho)$ to denote the satisfaction value of $\varphi$ in the last state of $\rho$ under the assignment $\chi$. Given an ${\textsf{{SL}}}{[\mathcal{F}]}$ path formula $\psi$, a play $\pi$, and a point in time $i\in\mathbb{N}$, we use $\llbracket\psi\rrbracket^{\calG}_{\chi}(\pi,i)$ 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:

[TABLE]

Strategy quantification $\langle\!\langle x\rangle\!\rangle\varphi$ computes the optimal 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$. Temporal modality ${{\mathsf{X}}}\psi$ takes the value of $\psi$ at the next step, while $\psi_{1}{{\mathsf{U}}}\psi_{2}$ maximises, 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 ${\textsf{{SL}}}{[\mathcal{F}]}$ with only temporal operators and functions $\vee$ and $\neg$ corresponds to Fuzzy Linear-time Temporal Logic [51, 43]. 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 [43]). However the interpretation of the temporal operators is fixed in our logic.

Remark 2.4**.**

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 infima and suprema in the above definition are in fact minima and maxima.

For a state formula $\varphi$ and a weighted game structure $\calG$, we write $\llbracket\varphi\rrbracket^{\calG}$ for $\llbracket\varphi\rrbracket^{\calG}_{\emptyset}(\textsf{v}_{\iota})$.

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 \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}}.

Definition 2.5** (Model-checking problem).**

Given an ${\textsf{{SL}}}{[\mathcal{F}]}$ state formula $\varphi$, a WCGS $\calG$ and a predicate $P\subseteq[0,1]$, decide whether $\llbracket\varphi\rrbracket^{\calG}\in P$.

Note that $P$ should be finitely represented, typically as a threshold or an interval. The precise complexity of the model-checking problem will be stated in terms of nesting depth of formulas, which counts the maximal number of strategy quantifiers in a formula $\varphi$, and is written $\text{nd}(\varphi)$. We establish the following result in Section 5:

Theorem 2.6**.**

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

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

${\textsf{{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 $\vee,\wedge$, 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.

Drone battle

A “carrier” drone $c$ helped by a “guard” drone $g$ try to bring an artefact to a rescue point and keep it away from the “villain” adversarial drone $v$. They evolve in a three dimensional cube of side length $1$ unit, 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 $\textsf{dist}\colon[0,1]^{3}\times[0,1]^{3}\to[0,1]$ for the (normalized) distance between two points in the cube. Let the atomic proposition safe denote that the artefact has reached the rescue point. In ${\textsf{{SL}}}{[\mathcal{F}]}$, we can express the level of safety for the artefact defined as the minimum distance between the carrier and the villain along a trajectory to reach the rescue point. Indeed, the formula

[TABLE]

states that the carrier and guard drones cooperate to keep the villain as far as possible from the artefact, until it is rescued. Note that the satisfaction value of the ${\textsf{LTL}}{[\mathcal{F}]}$ specification is [math] if there is a path in which the artefact is never rescued. 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 his plan. Then his strategy can depend on the villain’s strategy, which is captured by the following formula:

[TABLE]

Note that the formula $\varphi_{\text{rescue}}$ can be written in ${\textsf{{ATL}}}{[\mathcal{F}]}$ , whereas $\varphi_{\text{spy}}$ requires ${\textsf{{SL}}}{[\mathcal{F}]}$. In fact $\varphi_{\text{spy}}$ actually belongs to the fragment {\textsf{SL{}_{\textsf{1G}}}}{[\mathcal{F}]}, which we study in Section 6.

Synthesis with quantitative objectives

The problem of synthesis for LTL specifications dates back to [62]. 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 into synthesising a strategy for the controller such that, no matter the behaviour of the environment, the resulting execution satisfies $\psi$. Recently, this problem has been addressed in the context of ${\textsf{LTL}}{[\mathcal{F}]}$, where the controller aims at maximising the value of an ${\textsf{LTL}}{[\mathcal{F}]}$ formula $\varphi$, while the environment acts as minimiser. Both problems can be easily represented in SL and ${\textsf{{SL}}}{[\mathcal{F}]}$ respectively, with the formula

[TABLE]

where $c$ and $e$ are the controller and environment agent, respectively, and $\psi$ the temporal specification expressed in either LTL or ${\textsf{LTL}}{[\mathcal{F}]}$. Assume now that controller and environment are both composed of more than one agent, namely $c_{1},\ldots,c_{n}$ and $e_{1},\ldots,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 a ${\textsf{{SL}}}{[\mathcal{F}]}$ formula to represent this generalised synthesis problem as follows:

[TABLE]

Notice that every controller agent is bound to an existentially quantified variable, that makes it to maximise the satisfaction value of the formula in its scope. On the other hand, the environmental agents are bound to a universally quantified variable, that makes them to minimise the satisfaction value. Notice that in general each alternation between existential and universal quantification yields an additional exponential in the complexity of the model-checking problem, as we show in the overall quantification alternates from existential to universal $2n-1$ times, which would induce a . In section 6, we show that, for the special case of these formulas, such alternation does not affect the computational complexity of the model-checking problem.

NE in weighted games

An important feature of SL in terms of expressiveness is that it captures Nash equilibria (NE, for short) and other common solution concepts. This extends to ${\textsf{{SL}}}{[\mathcal{F}]}$, but in a much stronger sense: first, objectives in ${\textsf{{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. Consider a strategy profile $(x_{i})_{a_{i}\in\Agt}$. Assuming all agents follow their strategies in that profile, a NE can be characterised by the fact that all agents play one of their best responses against their opponents’ strategies. We would then write

[TABLE]

where $\alpha\preceq\beta$ equals $1$ if $\alpha\leq\beta$ and zero otherwise. Strategy profile $(x_{i})_{a_{i}\in\Agt}$ is a NE if, and only if, $\varphi_{{{\mathsf{NE}}}}((x_{i})_{a_{i}\in\Agt})$ evaluates to $1$. 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\textsf{diff}((a_{i},y_{i})\varphi_{i},\varphi_{i})$, where $\textsf{diff}(x,y)=\max\{0,x-y\}$. The maximal benefit that some agent may get is then captured by the following formula:

[TABLE]

Formula $\varphi_{\overline{{{\mathsf{NE}}}}}$ can be used to characterise $\varepsilon$-NE, by requiring that $\varphi_{\overline{{{\mathsf{NE}}}}}$ has value less than or equal to $\varepsilon$; of course it also characterises classical NE as a special case.

Secure equilibria in weighted games

Secure equilibria [27] 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 ${\textsf{{SL}}}{[\mathcal{F}]}$ as follows:

[TABLE]

where $(\alpha_{1},\alpha_{2})\preceq_{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 [math] otherwise. Secure equilibria have also been studied in $\mathbb{Q}$-weighted games [23]: in that setting, the objective of the agents is to optimise 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 ${{\mathsf{G}}}w$ is the infimum of the weights, while the value of ${{\mathsf{F}}}{{\mathsf{G}}}w$ 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_{{{\mathsf{SE}}}}$. Other classical properties of games can be expressed, such as doomsday equilibria (which generalise winning secure equilibria in $n$-player games) [26], robust NE (considering profitable deviations of coalitions of agents) [18], or strategy dominance and admissibility [12, 20], to cite a few.

Rational synthesis

Weak rational synthesis [42, 48, 5] aims at synthesising a strategy profile for a controller $C_{0}$ and the $n$ components $(C_{i})_{1\leq i\leq n}$ constituting the environment, in such a way that (1) the whole system satisfies some objective $\varphi_{0}$, and (2) under the strategy of the controller, the strategies of the $n$ components form an NE (or any given solution concept) for their own individual objectives $(\varphi_{i})_{1\leq i\leq n}$. That a given strategy profile $(x_{i})_{C_{i}\in\Agt}$ satisfies the two conditions above can be expressed as follows:

[TABLE]

The formula returns the minimum between the satisfaction value of $\varphi_{0}$ and that of $\varphi_{{{\mathsf{NE}}}}((x_{i})_{1\leq i\leq n})$. Thus, the satisfaction value of $\varphi_{\textsf{wRS}}$ is zero if the strategy profile $(x_{i})_{1\leq i\leq n}$ is not a NE under strategy $x_{0}$ assigned to $C_{0}$, and it returns the satisfaction value of $\varphi_{0}$ under the whole strategy profile otherwise. Then the value of

[TABLE]

is the best value of $\varphi_{0}$ that the system can collectively achieve under the condition that the components in the environment are in an NE. Obviously, we can go beyond NE and use any other solution concept that can be expressed in ${\textsf{{SL}}}{[\mathcal{F}]}$. The counterpart of weak rational synthesis is strong rational synthesis, that aims at synthesising a strategy only for controller $C_{0}$ in such a way that the objective $\varphi_{0}$ is maximised 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:

[TABLE]

The formula in the scope of the quantifications and bindings returns the maximum value between $\neg\varphi_{{{\mathsf{NE}}}}((x_{i})_{1\leq i\leq n})$ and $\varphi_{0}$. Given that the former is $1$ if there is no NE and [math] otherwise, the disjunction takes value $1$ over the path with no NEs and the value of $\varphi_{0}$, otherwise. Given that the environment components have universally quantified strategies, the formula $\varphi_{\textsf{sRS}}$ amounts at minimising such disjunction. Thus, the components will select (if any) the NE that minimises the satisfaction value of $\varphi_{0}$. Then the value of

[TABLE]

is the best value of $\varphi_{0}$ that the controller can achieve under the condition that the components in the environment are playing the Nash Equilibrium that worsens it.

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 noncooperative 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\Agt}$, a coalition $C\subseteq\Agt$ has a beneficial deviation $(y_{i})_{a_{i}\in C}$ if, for all strategy profiles $(z_{i})_{a_{i}\in\Agt\setminus C}$ it holds that $(x_{i})_{a_{i}\in\Agt}\varphi_{i}\prec(y_{i})_{a_{i}\in C}(z_{i})_{a_{i}\in\Agt\setminus C}\varphi_{i}$, for every $a_{i}\in C$. We say that a strategy profile $(x_{i})_{a_{i}\in\Agt}$ is a core equilibrium if, for every coalition, there is no beneficial deviation. This can be written in ${\textsf{{SL}}}{[\mathcal{F}]}$ as follows:

[TABLE]

The strategy profile $(x_{i})_{a_{i}\in\Agt}$ is a core equilibrium if, and only if, the formula $\varphi_{\textsf{core}}(x_{i})_{a_{i}\in\Agt}$ evaluates to $1$. The existence of a core equilibrium could be than expressed with the formula $\langle\!\langle x_{1}\rangle\!\rangle\ldots\langle\!\langle x_{n}\rangle\!\rangle\varphi_{\textsf{core}}(x_{i})_{a_{i}\in\Agt}$, which takes value $1$ if and only if there exists a core equilibrium.

3 Booleanly Quantified \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}}

In this section we introduce Booleanly Quantified \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}} (\textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}}, for short) which extends both \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}} and $\textsf{{QCTL}}^{\star}$ [52]. On the one hand, it extends \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}} with second order quantification over Boolean atomic propositions, on the other hand it extends $\textsf{{QCTL}}^{\star}$ to the quantitative setting of \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}}. While \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} formulas are interpreted over weighted Kripke structures, thus with atomic propositions having values in $[0,1]$, the possible assignment for the quantified propositions are Boolean.

3.1 Syntax

Let $\mathcal{F}\subseteq\{f\colon[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 \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} is defined with respect to a finite set \APof atomic propositions, using the following grammar: *

[TABLE]

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

Formulas of type $\varphi$ are called state formulas, those of type $\psi$ are called path formulas, and \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{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 ${\textsf{{SL}}}{[\mathcal{F}]}$, plus ${{\mathsf{A}}}\psi\colonequals\neg{{\mathsf{E}}}\neg\psi$.

3.2 Semantics

\textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} formulas are evaluated on unfoldings of weighted Kripke structures.Note that the terminology Boolean only concerns the quantification of atomic propositions (which is restricted to Boolean atomic propositions), and that formulas are interpreted over weighted Kripke structures.

Definition 3.2**.**

A weighted Kripke structure (WKS) is a tuple $\mathcal{K}=(\penalty 10000\AP,{\textsf{S}},\penalty-1000{\textsf{s}}_{\iota},\penalty-1000R,\textsf{{w}}\penalty 10000)$ where $\AP$ is a finite set of atomic propositions, S is a finite set of states, ${\textsf{s}}_{\iota}\in{\textsf{S}}$ is an initial state, $R\subseteq{\textsf{S}}\times{\textsf{S}}$ is a left-total transition relation111i.e., for all ${\textsf{s}}\in{\textsf{S}}$, there exists ${\textsf{s}}^{\prime}$ such that $({\textsf{s}},{\textsf{s}}^{\prime})\in R$., and $\textsf{{w}}\colon{\textsf{S}}\to[0,1]^{\AP}$ is a weight function.

A path in $\mathcal{K}$ is an infinite word $\pi=\pi_{0}\pi_{1}\ldots$ over $S$ such that $\pi_{0}={\textsf{s}}_{\iota}$ 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 $\Hist_{\mathcal{K}}$ for the set of all histories in $\mathcal{K}$. We also let $V_{\mathcal{K}}=\{\textsf{{w}}({\textsf{s}})(p)\mid{\textsf{s}}\in{\textsf{S}}\mbox{ and }p\in\AP\}$ be the finite set of values appearing in $\mathcal{K}$.

Trees

Given finite sets $D$ of directions, $\AP$ of atomic propositions, and $V\subseteq[0,1]$ of possible values, an $(\AP,V)$-labelled $D$-tree, (or tree for short when the parameters are understood or irrelevant), is a pair $t=(\tau,\textsf{{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 $\textsf{{w}}:\tau\to V^{\AP}$ is a weight function. A branch $\lambda=u_{0}u_{1}\ldots$ is an infinite sequence of nodes such that for all $i\geq 0$, we have that $u_{i+1}$ is a child of $u_{i}$. We let $\text{Br}(u)$ be the set of branches that start in node $u$. Given a tree $t=(\tau,\textsf{{w}})$ and a node $u\in\tau$, we define the subtree of $t$ rooted in $u$ as the tree $t_{u}=(\tau_{u},\textsf{{w}}^{\prime})$ where $\tau_{u}=\{v\in{\textsf{S}}^{+}:u\preccurlyeq v\}$ ($\preccurlyeq$ denotes the non-strict prefix relation) and $\textsf{{w}}^{\prime}$ is w restricted to $\tau_{u}$. We say that a tree $t=(\tau,\textsf{{w}})$ is Boolean in $p$, written $\text{Bool}(t,p)$, if for all $u\in\tau$ we have $\textsf{{w}}(u)(p)\in\{0,1\}$. As with weighted Kripke structures, we let $V_{t}=\{\textsf{{w}}(u)(p)\mid u\in\tau\mbox{ and }p\in\AP\}$. Given two $(\AP,V)$-labelled $D$-trees $t,t^{\prime}$ and $p\in\AP$, we write $t\equiv_{p}t^{\prime}$ if $t$ and $t^{\prime}$ differ only in assignments to $p$, which must be Boolean in $t^{\prime}$: formally, $t=(\tau,\textsf{{w}})$, $t^{\prime}=(\tau,\textsf{{w}}^{\prime})$, for the same domain $\tau$, $\text{Bool}(t^{\prime},p)$, and for all $p^{\prime}\in\AP$ such that $p^{\prime}\neq p$ and all $u\in\tau$, we have $\textsf{{w}}(u)(p^{\prime})=\textsf{{w}}^{\prime}(u)(p^{\prime})$.

Finally, we define the tree unfolding of a weighted Kripke structure $\mathcal{K}$ over atomic propositions $\AP$ and states S as the $(\AP,V_{\mathcal{K}})$-labelled S-tree $t_{\mathcal{K}}=(\Hist_{\mathcal{K}},\textsf{{w}}^{\prime})$, where $\textsf{{w}}^{\prime}(u)=\textsf{{w}}(\mbox{{last}}(u))$ for every $u\in\Hist_{\mathcal{K}}$.

Definition 3.3** (Semantics).**

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

[TABLE]

Remark 3.4**.**

As with ${\textsf{{SL}}}{[\mathcal{F}]}$, we will see that the suprema in the above definition can be replaced with maxima (see Lemma 4.1 below).

First, we point out that if $\mathcal{F}=\{\top,\vee,\neg\}$, then \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} evaluated on boolean Kripke structures corresponds to classic $\textsf{{QCTL}}^{\star}$ [52]. Note also that the quantifier on propositions does not range over arbitrary values in $[0,1]$. Instead, as in $\textsf{{QCTL}}^{\star}$, it quantifies only on Boolean valuations. It is still quantitative though, in the sense that instead of merely stating the existence of a valuation, $\exists p.\,\varphi$ maximises the value of $\varphi$ over all possible (Boolean) valuations of $p$. For a tree $t$ with root $r$ we write $\llbracket\varphi\rrbracket^{{t}}$ for $\llbracket\varphi\rrbracket^{{t}}(r)$, and for a weighted Kripke structure $\mathcal{K}$ we write $\llbracket\varphi\rrbracket^{{\mathcal{K}}}$ for $\llbracket\varphi\rrbracket^{{t_{\mathcal{K}}}}$. Note that this semantics is an extension of the tree semantics of $\textsf{{QCTL}}^{\star}$, in which the valuation of quantified atomic propositions is chosen on the unfolding of the Kripke structure instead of the states. This allows us to capture the semantics of Strategy Logic based on strategies with perfect recall, where moves can depend on the history, as apposed to the memoryless semantics, where strategies can only depend on the current state (see [52] for more detail). As for ${\textsf{{SL}}}{[\mathcal{F}]}$, we are interested in the following model-checking problem:

Definition 3.5**.**

Given a \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} state formula $\varphi$, a weighted Kripke structure $\mathcal{K}$, and a predicate $P\subseteq[0,1]$, decide whether $\llbracket\varphi\rrbracket^{{\mathcal{K}}}\in P$.

Similarly to ${\textsf{{SL}}}{[\mathcal{F}]}$, the precise complexity of the model-checking problem will be stated in terms of nesting depth of formulas, which counts the maximal number of nested propositional quantifiers in a formula $\varphi$, and is written $\text{nd}(\varphi)$. In the next section we establish our main technical contribution, which is the following:

Theorem 3.6**.**

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

This result, together with a reduction from ${\textsf{{SL}}}{[\mathcal{F}]}$ to \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} that we present in Section 5, entails the decidability of model checking ${\textsf{{SL}}}{[\mathcal{F}]}$ announced in Theorem 2.6.

4 Model checking \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}}

We start by proving that, as has been the case for LTL[$\mathcal{F}$], since the set of possible satisfaction values of an atomic proposition is finite, so is the set of satisfaction values of each \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} formula. This property allows to use $\max$ instead of $\sup$ in Definition 3.3.

Lemma 4.1**.**

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

[TABLE]

be the set of values taken by $\varphi$ in nodes of $(\AP,V)$-labelled trees. Similarly, define

[TABLE]

Then, $|V_{\varphi}|\leq|V|^{|\varphi|}$ and $|V_{\psi}|\leq|V|^{|\psi|}$. Moreover, one can compute sets $\widetilde{V}_{\varphi}$ and $\widetilde{V}_{\psi}$ such that $V_{\varphi}\subseteq\widetilde{V}_{\varphi}$ and $V_{\psi}\subseteq\widetilde{V}_{\psi}$ of size at most $|V|^{|\varphi|}$ and $|V|^{|\psi|}$, respectively.

Proof 4.2**.**

We prove the result by mutual induction on $\varphi$ and $\psi$. Clearly, $V_{p}=V$. For $\varphi=\exists p.\,\varphi^{\prime}$, observe that if $V_{t}\subseteq V$ and $u\in t$, then for all trees $t^{\prime}$ such that $t^{\prime}\equiv_{p}t$ it is also the case that $V_{t^{\prime}}\subseteq V$ (by assumption $V$ contains 0 and 1). It follows that $\llbracket\exists p.\,\varphi^{\prime}\rrbracket^{{t}}(u)$ is defined as the supremum of a subset of $V_{\varphi^{\prime}}$, which by induction hypothesis is of size at most $|V|^{|\varphi^{\prime}|}$, and thus the supremum is indeed a maximum. It follows that $\llbracket\exists p.\,\varphi^{\prime}\rrbracket^{{t}}(u)\in V_{\varphi^{\prime}}$. Hence, $V_{\exists p.\,\varphi^{\prime}}\subseteq V_{\varphi^{\prime}}$, and thus $|V_{\exists p.\,\varphi^{\prime}}|\leq|V_{\varphi^{\prime}}|\leq|V|^{|\varphi^{\prime}|}\leq|V|^{|\exists p.\,\varphi^{\prime}|}$. For $\varphi={{\mathsf{E}}}\psi$, again $\llbracket{{\mathsf{E}}}\psi\rrbracket^{{t}}(u)$ is a supremum over a subset of $V_{\psi}$, which by induction hypothesis is of size at most $V^{|\psi|}$. The supremum is thus reached, hence $V_{{{\mathsf{E}}}\psi}\subseteq V_{\psi}$ and $|V_{{{\mathsf{E}}}\psi}|\leq|V_{\psi}|\leq|V|^{|\psi|}\leq|V|^{|{{\mathsf{E}}}\psi|}$. For $\varphi=f(\varphi_{1},\ldots,\varphi_{n})$, we have $V_{\varphi}=\{f(v_{1},\ldots,v_{n})\mid v_{i}\in V_{\varphi_{i}}\}$, hence $|V_{\varphi}|$ is at most $\prod_{i=1}^{n}|V_{\varphi_{i}}|$. By induction hypothesis, we get $|V_{\varphi}|\leq\prod_{i=1}^{n}|V|^{|\varphi_{i}|}\leq|V|^{|\varphi_{1}|+\ldots+|\varphi_{n}|}\leq|V|^{|\varphi|}$. For $\psi=\varphi$, the result follows by hypothesis of mutual induction. For $\psi={{\mathsf{X}}}\psi^{\prime}$, we have that $V_{\psi}=V_{\psi^{\prime}}$, and the result follows. For $\psi=\psi_{1}{{\mathsf{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 $V_{\psi}\subseteq V_{\psi_{1}}\cup V_{\psi_{2}}$. Hence, $|V_{\psi}|\leq|V_{\psi_{1}}|+|V_{\psi_{2}}|\leq|V|^{|\psi_{1}|}+|V|^{|\psi_{2}|}\leq|V|^{|\psi_{1}|+|\psi_{2}|}\leq|V|^{|\psi|}$ (since $|V|\geq 2$). In all cases, the claim for over-approximations follows by the same reasoning as above.

The finite over-approximation of the set of possible satisfaction values induces a finite alphabet for the automata our model-checking procedure uses. In the following, we use alternating parity tree automata (APT in short), and their purely non-deterministic (resp. universal) variants, denoted NPT (resp. UPT). Given two APT $\mathcal{A}$ and $\mathcal{A}^{\prime}$ we denote $\mathcal{A}\wedge\mathcal{A}^{\prime}$ (resp. $\mathcal{A}\vee\mathcal{A}^{\prime}$) the APT of size linear in $|\mathcal{A}|$ and $|\mathcal{A}^{\prime}|$ that accepts the intersection (resp. union) of the languages of $\mathcal{A}$ and $\mathcal{A}^{\prime}$, and we call index of an automaton the number of priorities in its parity condition. We refer the reader to for a detailed exposition of alternating parity tree automata. We extend the automata-based model-checking procedure for $\textsf{{CTL}}^{\star}$ from [49]. Note that since the quantified atomic propositions may appear in different subformulas, we cannot extend the algorithm for \textsf{{CTL}}^{\star}\textsf{{[\mathcal{F}]}} from [3], as the latter applies the technique of [39], where the evaluation of each subformula is independent.

Proposition 4.3**.**

Let $V\subset[0,1]$ be a finite set of values such that $\{0,1\}\subseteq V$, and let $D$ be a finite set of directions. For every \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} state formula $\varphi$ and predicate $P\subseteq[0,1]$, one can construct an APT $\mathcal{A}^{V,P}_{\varphi}$ such that for every $(\AP,V)$-labelled $D$-tree $t$, $\mathcal{A}^{V,P}_{\varphi}$ accepts $t$ if and only if $\llbracket\varphi\rrbracket^{{t}}\in P$. The APT $\mathcal{A}^{V,P}_{\varphi}$ has at most $(\text{nd}(\varphi)+1)$-exponentially many states, and its index is at most $\text{nd}(\varphi)$-exponential.

Proof 4.4**.**

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}^{V,P}_{\varphi}$ such that for every $(\AP,V)$-labelled $D$-tree $t$, for every node $u\in t$, we have that $\mathcal{A}^{V,P}_{\varphi}$ accepts $t$ from node $u$ if and only if $\llbracket\varphi\rrbracket^{{t}}(u)\in P$. If $\varphi=p$, the automaton has one state and accepts a tree $t=(\tau,\textsf{{w}})$ in node $u\in\tau$ if $\textsf{{w}}(u)(p)\in P$, and rejects otherwise. In addition, $V_{p}=V$. If $\varphi=\exists p.\,\varphi^{\prime}$, we want to check whether the maximal satisfaction value of $\varphi^{\prime}$ for all possible Boolean valuations of $p$ is in $P$. To do so we first compute a finite set $\widetilde{V}_{\varphi^{\prime}}$ of exponential size such that $V_{\varphi^{\prime}}\subseteq\widetilde{V}_{\varphi^{\prime}}$, which we can do as established by Lemma 4.1. For each possible value $v\in\widetilde{V}_{\varphi^{\prime}}\cap P$, we check whether this value is reached for some $p$-valuation, and if the value of $\varphi^{\prime}$ is less than or equal to $v$ for all $p$-valuations. For each $v\in\widetilde{V}_{\varphi^{\prime}}\cap P$, inductively build the APTs $\mathcal{A}^{V,\{v\}}_{\varphi^{\prime}}$ and $\mathcal{A}^{V,[0,v]\cap P}_{\varphi^{\prime}}$. Turn the first one into a NPT $\mathcal{N}_{=v}$ and the second one into a UPT $\mathcal{U}_{\leq v}$. Project $\mathcal{N}_{=v}$ existentially on $p$, and call the result $\mathcal{N}^{\prime}_{=v}$. Project $\mathcal{U}_{\leq v}$ universally on $p$, call the result $\mathcal{U}^{\prime}_{\leq v}$. Finally, we can define the APT $\mathcal{A}^{V,P}_{\exists p.\,\varphi^{\prime}}:=\bigvee_{v\in\widetilde{V}_{\varphi^{\prime}}\cap P}\mathcal{N}^{\prime}_{=v}\wedge\mathcal{U}^{\prime}_{\leq 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^{\prime}$ for all $p$-valuations. If $\varphi={{\mathsf{E}}}\psi$: as in the classic automata construction for $\textsf{{CTL}}^{\star}$ [50], we first let $\mathsf{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 $\mathsf{atoms}(\psi)$ as atomic propositions, and $\psi$ as an LTL[$\mathcal{F}$] formula over $\mathsf{atoms}(\psi)$. According to Lemma 4.1 we can compute over-approximations $\widetilde{V}_{\varphi^{\prime}}$ for each $\varphi^{\prime}\in\mathsf{atoms}(\psi)$, and we thus let $\widetilde{V}=\bigcup_{\varphi^{\prime}\in\mathsf{atoms}(\psi)}\widetilde{V}_{\varphi^{\prime}}$ be a finite over-approximation of the set of possible values for atoms. It is proven in [3] that for every $P\subseteq[0,1]$, one can build a nondeterministic parity automaton $\mathcal{W}_{P}^{\psi}$ of size exponential in $|\psi|^{2}$ such that $\mathcal{W}_{P}^{\psi}$ accepts a word $w\in(\widetilde{V}^{\mathsf{atoms}(\psi)})^{\omega}$ if and only if $\llbracket\psi\rrbracket(w)\in P$. Now let us compute $\widetilde{V}_{{{\mathsf{E}}}\psi}$ (again using Lemma 4.1), and for each $v\in\widetilde{V}_{{{\mathsf{E}}}\psi}\cap P$, construct an NPT $\mathcal{N}^{E=v}$ that guesses a branch in its input and simulates $\mathcal{W}_{\{v\}}^{\psi}$ on it. To obtain a universal word automaton of single exponential size that checks whether $\llbracket\psi\rrbracket(w)\in[0,v]$, first build the nondeterministic automaton $\mathcal{W}^{\psi}_{(v,1]}$ from [3], and dualize it in linear time. From the resulting universal automaton $\mathcal{W}_{[0,v]}^{\psi}$ we build a UPT $\mathcal{U}^{A\leq v}$ that executes $\mathcal{W}_{[0,v]}^{\psi}$ on all branches of its input.222We 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 determinise $\mathcal{W}_{[0,v]}^{\psi}$, but it would cost one more exponential. We now define the APT $\mathcal{A}^{P}$ on $\widetilde{V}^{\mathsf{atoms}(\psi)}$-trees as

[TABLE]

Now to go from atoms to standard atomic propositions, we define an APT $\mathcal{A}^{V,P}_{{{\mathsf{E}}}\psi}$ that simulates $\mathcal{A}^{P}$ by, in each state and each node of its input, guessing a value $v_{i}$ in $\widetilde{V}_{\varphi_{i}}$ for each formula $\varphi_{i}\in\mathsf{atoms}(\psi)$, simulating ${\mathcal{A}^{P}}$ on the resulting label, and launching a copy of $\mathcal{A}_{\varphi_{i}}^{V,\{v_{i}\}}$ for each $\varphi_{i}\in\mathsf{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},...,\varphi_{n})$, we list all combinations $(v_{1},\ldots,v_{n})$ of the possible satisfaction values for the subformulas $\varphi_{i}$ such that $f(v_{1},\ldots,v_{n})\in P$, and we build automaton $\mathcal{A}^{V,P}_{\varphi}$ as the disjunction over such $(v_{1},\ldots,v_{n})$ of the conjunction of automata $\mathcal{A}^{V,v_{i}}_{\varphi_{i}}$. The complexity of this procedure is non-elementary. More precisely, we claim that $\mathcal{A}_{\varphi}^{V,P}$ has size at most $(\text{nd}(\varphi)+1)$-exponential and index (i.e., number of priorities for the parity condition) at most $\text{nd}(\varphi)$-exponential. The case where $\varphi$ is an atomic proposition is trivial. For $\varphi=\exists p.\,\varphi^{\prime}$, we transform an exponential number of APTs into NPTs or UPTs. This entails an exponential blowup in the size and index of each automaton. The resulting automaton $\mathcal{A}^{V,P}_{\exists p.\,\varphi^{\prime}}$ has at most $(\text{nd}(\varphi^{\prime})+2)$-exponentially many states and index at most $(\text{nd}(\varphi^{\prime})+1)$-exponential. Since $\text{nd}(\varphi)=\text{nd}(\varphi^{\prime})+1$, the inductive property is preserved. If $\varphi$ has the form $f(\varphi_{1},...,\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.1 there are at most $|V|^{|\varphi_{1}|+\ldots+|\varphi_{n}|}\leq|V|^{|\varphi|}$ different combinations, so assuming (from the induction hypothesis) that the automata for $\varphi_{i}$ have at most $(\text{nd}(\varphi_{i})+1)$-exponentially many states and index at most $h(\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={{\mathsf{E}}}\psi$: following [3], the size of $\mathcal{W}_{P}^{\psi}$ is exponential in $|\psi|^{2}$, and 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=v}$ and $\mathcal{U}^{A\leq v}$ 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}^{V,P}_{{{\mathsf{E}}}\psi}$ is obtained from that automaton by plugging the automata for $\mathcal{A}_{\varphi_{i}}^{V,\bullet}$, whose sizes and indices are dominating the size and index of $\mathcal{A}^{P}$. It follows that, for $\varphi={{\mathsf{E}}}\psi$, the size of $\mathcal{A}^{V,P}_{\varphi}$ also is $(\text{nd}(\varphi)+1)$-exponential, and its index is $\text{nd}(\varphi)$-exponential.

To see that Theorem 3.6 follows from Proposition 4.3, recall that by definition $\llbracket\varphi\rrbracket^{{\mathcal{K}}}=\llbracket\varphi\rrbracket^{{t_{\mathcal{K}}}}$. Thus to check whether $\llbracket\varphi\rrbracket^{{\mathcal{K}}}\in P$, where atoms in $\mathcal{K}$ takes values in $V$, it is enough to build $\mathcal{A}^{V,P}_{\varphi}$ as in Proposition 4.3, take its product with a deterministic tree automaton that accepts only $t_{\mathcal{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 fragment $\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{\star}$ of $\textsf{{QCTL}}^{\star}$ which consists in formulas in prenex normal form, i.e. with all quantifications on atomic propositions at the beginning, with at most $k$ alternations between existential and universal quantifiers, counting the first quantifier as one alternation (see [52, p.8] for a formal definition). Clearly, $\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{\star}$ can be translated in \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} with formulas of linear size and nesting depth at most $k$ (alternation is simply coded by placing function $\neg$ between quantifiers). It is proved in [52] that model checking $\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{\star}$ is $(k+1)$-Exptime -hard.

5 Model checking quantitative strategic logics

In this section we show how to reduce the model-checking problem for ${\textsf{{SL}}}{[\mathcal{F}]}$ to that of \textsf{{QCTL}}^{\star}\textsf{{[\mathcal{F}]}}. This reduction is a rather straightforward adaptation of the usual one for qualitative variants of SL (see e.g.  [53, 11, 40]). We essentially observe that it can be lifted to the quantitative setting. We let $\Agt$ be a finite set of agents, and $\AP$ be a finite set of atomic propositions.

Models transformation.

We first define for every WCGS $\calG=(\penalty 10000\Act,\textsf{V},\penalty-1000\textsf{v}_{\iota},\penalty-1000\Delta,\textsf{{w}}\penalty 10000)$ over $\Agt$ and $\AP$ a WKS $\mathcal{K}_{\calG}=(\penalty 10000{\textsf{S}},{\textsf{s}}_{\iota},\penalty-1000R,\textsf{{w}}\penalty 10000)$ over some set $\AP^{\prime}$ and a bijection $\rho\mapsto u_{\rho}$ between the set of histories starting in the initial state $\textsf{v}_{\iota}$ of $\calG$ and the set of nodes in $t_{\mathcal{K}_{\calG}}$. We consider propositions $\AP_{\textsf{V}}=\{p_{\textsf{v}}\mid\textsf{v}\in\textsf{V}\}$, that we assume to be disjoint from $\AP$. We let $\AP^{\prime}=\AP\cup\AP_{\textsf{V}}$. Define the Kripke structure $\mathcal{K}_{\calG}=({\textsf{S}},{\textsf{s}}_{\iota},R,\textsf{{w}})$ where

• •

${\textsf{S}}=\{{\textsf{s}}_{\textsf{v}}\mid\textsf{v}\in\textsf{V}\}$,

• •

${\textsf{s}}_{\iota}={\textsf{s}}_{\textsf{v}_{\iota}}$,

• •

$R=\{({\textsf{s}}_{\textsf{v}},{\textsf{s}}_{\textsf{v}^{\prime}})\in{\textsf{S}}^{2}\mid\exists\vec{c}\in\Act^{\Agt}\mbox{ s.t. }\Delta(\textsf{v},\vec{c})=\textsf{v}^{\prime}\}$, and

• •

$\textsf{{w}}(p)({\textsf{s}}_{\textsf{v}})=\begin{cases}1&\mbox{if }p\in\AP_{\textsf{V}}\mbox{ and }p=p_{\textsf{v}}\\ 0&\mbox{if }p\in\AP_{\textsf{V}}\mbox{ and }p\neq p_{\textsf{v}}\\ \textsf{{w}}(p)(\textsf{v})&\mbox{otherwise}\end{cases}$.

For every history $\rho=\textsf{v}_{0}\ldots\textsf{v}_{k}$, define the node $u_{\rho}={\textsf{s}}_{\textsf{v}_{0}}\ldots{\textsf{s}}_{\textsf{v}_{k}}$ in $t_{\mathcal{K}_{\calG}}$ (which exists, by definition of $\mathcal{K}_{\calG}$ and of tree unfoldings). Note that the mapping $\rho\mapsto u_{\rho}$ defines a bijection between the set of histories from $\textsf{v}_{\iota}$ and the set of nodes in $t_{\mathcal{K}_{\calG}}$.

Formulas translation.

Given a game $\calG=(\penalty 10000\Act,\textsf{V},\penalty-1000\textsf{v}_{\iota},\penalty-1000\Delta,\textsf{{w}}\penalty 10000)$ and a formula $\varphi\in{\textsf{{SL}}}{[\mathcal{F}]}$, we define a \textsf{{QCTL}}^{\star}\textsf{{[\mathcal{F}]}} formula $\varphi^{\prime}$ such that $\llbracket\varphi\rrbracket^{\calG}=\llbracket\varphi^{\prime}\rrbracket^{{\mathcal{K}_{\calG}}}$. More precisely, this translation is parameterised with a partial function $g:\Agt\rightharpoonup\Var$ which records bindings of agents to strategy variables. Suppose that $\Act=\{c_{1},\ldots,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:

[TABLE]

and for path formulas:

[TABLE]

This translation is identical to that from branching-time SL to $\textsf{{QCTL}}^{\star}$ 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 \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} to Boolean values, and atoms in $\AP_{\textsf{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},\ldots,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}_{\calG}}$ if and only if in this branch each agent $a\in\mathsf{dom}(g)$ follows the strategies coded by atoms $p_{c}^{x}$. As a result \exists p_{c_{1}}^{x}\ldots\exists p_{c_{m}}^{x}.\Big{(}\varphi_{\text{str}}(x)\wedge(\varphi)^{\,g}\Big{)} maximises over those valuations for the $p_{c_{i}}^{x}$ that code for strategies, other valuations yielding value 0. Similarly, formula ${{\mathsf{A}}}(\psi_{\text{out}}(g)\rightarrow(\psi)^{\,g})$ minimises 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 ${\textsf{{SL}}}{[\mathcal{F}]}$ formula.

Lemma 5.1**.**

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

[TABLE]

As a result, the quantitative model-checking problem for an ${\textsf{{SL}}}{[\mathcal{F}]}$ formula $\varphi$, a weighted CGS $\calG$ and a predicate $P\subseteq[0,1]$ can be solved by computing the \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} formula $\varphi^{\prime}=(\varphi)^{\,\emptyset}$ and the weighted Kripke structure $\mathcal{K}_{\calG}$, and deciding whether $\llbracket\varphi^{\prime}\rrbracket^{{\mathcal{K}_{\calG}}}\in P$, which can be done by Theorem 3.6. This establishes the upper-bounds in Theorem 2.6. As in the case of \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}}, the lower-bounds are obtained by reduction from the model-checking problem for $\textnormal{{EQ}}^{k}\textnormal{{CTL}}^{\star}$. This reduction is an adaptation of the one from $\textsf{{QCTL}}^{\star}$ to ATL with strategy context in [53], and that preserves nesting depth.

Remark 5.2**.**

Lemma 5.1 together with Lemma 4.1 imply that ${\textsf{{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 2.4 that supremum and infimum in the semantics of ${\textsf{{SL}}}{[\mathcal{F}]}$ can be replaced with maximum and minimum.

6 The case of {\textsf{SL{}_{\textsf{1G}}}}{[\mathcal{F}]}

We now study the fragment {\textsf{SL{}{\textsf{1G}}}}{[\mathcal{F}]}, which is the extension to the quantitative setting of the one-goal fragment SL${}_{\textsf{1G}}$ of SL [56]. In order to define the syntax, we need to introduce the notions of quantification prefix and binding prefix. A quantification prefix is a sequence \wp=\mbox{\langle!\langle}x_{1}\mbox{]>!!]}\ldots\mbox{\langle!\langle}x_{n}\mbox{]>!!]}, where \mbox{\langle!\langle}x_{i}\mbox{]>!!]}\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},\ldots,a_{n}\}$ a binding prefix is a sequence $\flat=(a_{1},x_{1}),\ldots(a_{n},x_{n})$, where every agent in $\Agt$ occurs exactly once. A combination $\wp\flat$ is closed if every variable occurring in $\flat$ occurs in some quantifier of $\wp$. We can now give the definition of {\textsf{SL{}{\textsf{1G}}}}{[\mathcal{F}]} syntax.

Definition 6.1** ({\textsf{SL{}_{\textsf{1G}}}}{[\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 {\textsf{SL{}_{\textsf{1G}}}}{[\mathcal{F}]} formulas is defined by the following grammar:

[TABLE]

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

Note that all ${\textsf{{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 {\textsf{SL{}_{\textsf{1G}}}}{[\mathcal{F}]} formula is defined as follows:

• •

${{\mathsf{SntNest}}}(p)=0$ for every $p\in\AP$;

• •

${{\mathsf{SntNest}}}(f(\varphi_{1},\ldots,\varphi_{n}))=\max_{1\leq i\leq n}\{{{\mathsf{SntNest}}}(\varphi_{i})\}$;

• •

${{\mathsf{SntNest}}}({{\mathsf{X}}}\psi)={{\mathsf{SntNest}}}(\psi)$;

• •

${{\mathsf{SntNest}}}(\psi_{1}{{\mathsf{U}}}\psi_{2})=\max\{{{\mathsf{SntNest}}}(\psi_{1}),{{\mathsf{SntNest}}}(\psi_{2})\}$.

• •

${{\mathsf{SntNest}}}(\wp\flat\varphi)={{\mathsf{SntNest}}}(\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 {\textsf{SL{}_{\textsf{1G}}}}{[\mathcal{F}]}, we need the technical notion of concurrent multi-player parity game introduced in [55].

Definition 6.2**.**

A concurrent multi-player parity game (CMPG) is a tuple ${{\mathcal{P}}}=(\penalty 10000\Agt,\Act,\penalty-1000{\textsf{S}},\penalty-1000{\textsf{s}}_{\iota},\penalty-1000{{\mathsf{p}}},\Delta\penalty 10000)$, where $\Agt={0,\ldots,n}$ is a set of agents indexed with natural numbers, S is a set of states, ${\textsf{s}}_{\iota}$ is a designated initial state, ${{\mathsf{p}}}:{\textsf{S}}\to\mathbb{N}$ is a priority function, and $\Delta:{\textsf{S}}\times\Act^{\Agt}\to{\textsf{S}}$ is a transition function determining the evolution of the game according to the joint actions of the players.

A CMPG is a game played by players $\Agt={0,\ldots,n}$ for an infinite number of rounds. In each round, the players concurrently and independently choose moves, and the current state and the action chosen for each player determine the successor state. In details we have that each player $i$, with $i\mod 2=0$ is part of the existential (even) team; the other players are instead part of the universal (odd) team. Informally, the goal in a CMPG is to check whether there exists a strategy for [math] 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 [55, Theorem 4.1, Corollary 4.1], one can decide the winners of a CMPG ${{\mathcal{P}}}=(\penalty 10000\Agt,\Act,\penalty-1000{\textsf{S}},\penalty-1000{\textsf{s}}_{\iota},\penalty-1000{{\mathsf{p}}},\Delta\penalty 10000)$ in time polynomial w.r.t. ${{|{\textsf{S}}|}}$ and ${{|\Act|}}$, and exponential w.r.t. ${{|\Agt|}}$ and $k=\max{{\mathsf{p}}}$ (the maximal priority).

Theorem 6.3**.**

*The model-checking problem for closed formulas of {\textsf{SL{}_{\textsf{1G}}}}{[\mathcal{F}]} is decidable, and $2$-EXPTIME-complete. *

Proof 6.4**.**

*We let $\calG=(\penalty 10000\AP,\Agt,\penalty-1000\Act,\penalty-1000\textsf{V},\penalty-1000\textsf{v}_{\iota},\penalty-1000\Delta,\textsf{{w}}\penalty 10000)$ be a WCGS and we consider a formula of the form $\wp\flat\varphi$. We also assume, for simplicity, that \wp=\langle\!\langle x_{0}\rangle\!\rangle[\![x_{1}]\!],\ldots,\mbox{\langle!\langle}x_{k}\mbox{]>!!]}, that is, quantifiers perfectly alternate between existential and universal.333To reduce to this case, one can either collapse the agents occurring in the same quantification block, or interleave them with dummy agents quantified with the other modality. Note that the formula $\wp\flat\varphi$ is a sentence, therefore the choice of an assignment is useless. Moreover, recall that, by Lemma 5.1 and in particular Remark 5.2, the set $V(\wp\flat\varphi)$ of possible values is bounded by $2^{{{|\wp\flat\varphi|}}}$. We proceed by induction on the sentence nesting depth. As base case let ${{\mathsf{SntNest}}}(\wp\flat\varphi)=1$, i.e., there is no occurrence of neither quantifiers nor bindings in $\varphi$. Then, $\varphi$ can be regarded as an ${\textsf{LTL}}{[\mathcal{F}]}$ formula that can be interpreted over paths of the WKS $\mathcal{K}=(\penalty 10000\AP,\textsf{V},\penalty-1000\textsf{v}_{\iota},\penalty-1000R,\textsf{{w}}\penalty 10000)$ where $R=\{(\textsf{v}_{1},\textsf{v}_{2})\mid\exists\vec{c}\in\Act^{\Agt}.\ \textsf{v}_{2}=\Delta(\textsf{v}_{1},\vec{c})\}$. Now, thanks to [3, Theorem 3.1], for every value $v\in V(\wp\flat\varphi)$, there exists a nondeterministic generalised Büchi word automaton ${{\mathcal{B}}}_{{{\mathcal{K}}},\varphi,P_{v}}$, with $P_{v}=[v,1]$ that accepts all and only the infinite paths $\pi$ of $\mathcal{K}$ such that $\llbracket\varphi\rrbracket^{{\mathcal{K}}}(\pi)\in P_{v}$.

Following [60], we can convert ${{\mathcal{B}}}_{{{\mathcal{K}}},\varphi,P_{v}}$ into a deterministic parity word automaton ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,P_{v}}=(\penalty 10000\textsf{V},Q,\penalty-1000q_{\iota},\penalty-1000\delta,{{\mathsf{p}}}\penalty 10000)$ of size doubly-exponential in the size of $\varphi$ and index bounded by $2^{{{|\varphi|}}}$. At this point, define the following CMPG ${{\mathcal{P}}}=(\penalty 10000\Agt^{\prime},\Act,\penalty-1000{\textsf{S}},\penalty-1000{\textsf{s}}_{\iota},\penalty-1000{{\mathsf{p}}}^{\prime},\Delta^{\prime}\penalty 10000)$ such that*

• •

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

• •

$\Act$* is the set of actions in $\calG$;*

• •

${\textsf{S}}=\textsf{V}\times Q$* is the product of the states of $\calG$ and the automaton ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,P_{v}}$;*

• •

${\textsf{s}}_{\iota}=(\textsf{v}_{\iota},q_{\iota})$* is the pair given by the initial states of $\calG$ and ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,t}$, respectively;*

• •

${{\mathsf{p}}}^{\prime}(\textsf{v},q)={{\mathsf{p}}}(q)$* mimics the parity function of ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,P_{v}}$;*

• •

if $\vec{c}\in\Act^{\Agt^{\prime}}$, $\Delta^{\prime}((\textsf{v},q),\vec{c})=(\Delta(\textsf{v},\flat(\vec{c})),\delta(q,\textsf{v}))$ mimics the execution of both $\calG$ and ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,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 $\calG$. In the second, it emulates the execution of the automaton ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,P_{v}}$ when it reads the path $\pi$ generated in the first component. By construction, it results that every execution $(\pi,\eta)\in\textsf{V}^{\omega}\times Q^{\omega}$ in ${{\mathcal{P}}}$ satisfies the parity condition determined by ${{\mathsf{p}}}^{\prime}$ if, and only if, $\llbracket\varphi\rrbracket^{{\mathcal{K}}}(\pi)\in P_{v}$. Moreover, observe that, since ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,P_{v}}$ is deterministic, for every possible history $\rho$ in $\calG$, there is a unique partial run $\eta_{\rho}$ that makes the partial execution $(\rho,\eta_{\rho})$ possible in ${{\mathcal{P}}}$. This makes the sets of possible strategies ${{\mathrm{Str}}}_{\calG}(\textsf{v}_{\iota})$ and ${{\mathrm{Str}}}_{{{\mathcal{P}}}}({\textsf{s}}_{\iota})$ in perfect bijection. ${{\mathcal{P}}}$ has a winning strategy if and only if $\llbracket\wp\flat\varphi\rrbracket^{\calG}(\textsf{v}_{\iota})\in P_{v}$. In order to compute the exact value of $\llbracket\wp\flat\varphi\rrbracket^{\calG}(\textsf{v}_{\iota})$, we repeat the procedure described above for every $v\in V(\wp\flat\varphi)$ and take the maximum $v$ of those for which $\llbracket\wp\flat\varphi\rrbracket^{\calG}(\textsf{v}_{\iota})\in P_{v}$. For the induction case, assume we can compute the satisfaction value of every {\textsf{SL{}_{\textsf{1G}}}}{[\mathcal{F}]} formula with sentence nesting depth at most $n$, and let ${{\mathsf{SntNest}}}(\wp\flat\varphi)=n+1$. Observe that, for every subsentence $\wp^{\prime}\flat^{\prime}\varphi^{\prime}$ of $\wp\flat\varphi$, we have that ${{\mathsf{SntNest}}}(\wp^{\prime}\flat^{\prime}\varphi^{\prime})\leq n$ and so, by induction hypothesis, we can compute $\llbracket\wp^{\prime}\flat^{\prime}\varphi^{\prime}\rrbracket^{\calG}(\textsf{v})$ for every $\textsf{v}\in\textsf{V}$. Now, introduce a fresh atomic proposition $p_{(\wp^{\prime}\flat^{\prime}\varphi^{\prime})}$ whose weight in $\calG$ is defined as $\textsf{{w}}(v)(p_{(\wp^{\prime}\flat^{\prime}\varphi^{\prime})})=\llbracket\wp^{\prime}\flat^{\prime}\varphi^{\prime}\rrbracket^{\calG}(v)$ and a set of fresh atomic propositions $p_{\textsf{v}}$, one for every $\textsf{v}\in\textsf{V}$, whose weights in $\calG$ are defined as $\textsf{{w}}(\textsf{v})(p_{\textsf{v}})=1$ and $\textsf{{w}}(\textsf{v})(p_{\textsf{v}^{\prime}})=0$ if $\textsf{v}\neq\textsf{v}^{\prime}$. Now, consider the Boolean formula *

[TABLE]

Observe that every disjunct is a conjunction of the form $p_{\textsf{v}}\wedge p_{(\wp^{\prime}\flat^{\prime}\varphi^{\prime})}$, whose satisfaction value on a state $\textsf{v}^{\prime}$ is the minimum among the weights of $p_{\textsf{v}}$ and $p_{(\wp^{\prime}\flat^{\prime}\varphi^{\prime})}$. This can be either [math], if $\textsf{v}\neq\textsf{v}^{\prime}$ or $\llbracket\wp^{\prime}\flat^{\prime}\varphi^{\prime}\rrbracket^{\calG}(\textsf{v})$, if $\textsf{v}=\textsf{v}^{\prime}$. Now, the big disjunction takes the maximum among them. Therefore, we obtain that $\llbracket\Phi(\wp^{\prime}\flat^{\prime}\varphi^{\prime})\rrbracket^{\calG}(\textsf{v})=\llbracket\wp^{\prime}\flat^{\prime}\varphi^{\prime}\rrbracket^{\calG}(\textsf{v})$. This allows us to replace every occurrence of $\wp^{\prime}\flat^{\prime}\varphi^{\prime}$ in $\varphi$ with the Boolean combination $\Phi(\wp^{\prime}\flat^{\prime}\varphi^{\prime})$, making the resulting formula to be of sentence nesting depth $1$. Thus, we can apply the procedure described in the base case, to compute $\llbracket\wp\flat\varphi\rrbracket^{\calG}(\textsf{v})$. Regarding the complexity, note that the size of ${{\mathcal{P}}}$ is ${{|\textsf{V}|}}\cdot{{|Q|}}$ that is in turn linear with respect to the size of $\calG$ and doubly exponential in the size of $\varphi$. This is due to the fact that the automaton ${{\mathcal{A}}}_{{{\mathcal{K}}},\varphi,P_{v}}$ results from the construction of the NGBW ${{\mathcal{B}}}_{{{\mathcal{K}}},\varphi,P_{v}}$, of size singly exponential in ${{|\varphi|}}$ and the transformation to a DPW, that adds up another exponential to the construction. On the other hand, the number of priorities in ${{\mathcal{P}}}$ is only singly exponential in ${{|\varphi|}}$, and it is due to the fact that the transformation from NGBW to DPW requires a singly exponential number of priorities. Therefore, the CMPG ${{\mathcal{P}}}$ can be solved in time polynomial w.r.t. the size $\calG$ and double exponential in ${{|\varphi|}}$. Such $2$-EXPTIME procedure is executed a number of time exponential in $\varphi$, which is still $2$-EXPTIME. Hardness follows from that of SL${}_{\textsf{1G}}$ [56].

7 Future work

We introduced and studied ${\textsf{{SL}}}{[\mathcal{F}]}$, a formalism for specifying quality and fuzziness of strategic on-going behaviour. 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 modelling of the system and lack of exhaustiveness of the specification [30]. When applied to ${\textsf{{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 [45, 34] or tax increase [32], and more. Recall that our ${\textsf{{SL}}}{[\mathcal{F}]}$ model-checking algorithm reduces the problem to \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}}, where the quantified atomic propositions take Boolean values. It is interesting to extend \textsf{{BQCTL}}^{\star}\textsf{{[\mathcal{F}]}} to a logic in which the quantified atomic propositions are associated with different agents, which would enable easy specification of controllable events. Also, while in our application the quantified atomic propositions encode the strategies, and hence the restriction of their values to $\{0,1\}$ is natural, it is interesting to study \textsf{{QCTL}}^{\star}\textsf{{[\mathcal{F}]}}, where quantified atomic propositions may take values in $[0,1]$.