Reasoning about Quality and Fuzziness of Strategic Behaviours

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 [Pnueli, 1981; Emerson and Halpern, 1986]. The need to reason about multiagent systems has led to the development of specification formalisms that enable the specification of on-going strategic behaviours in multi-agent systems. Essentially, these formalisms, most notably ATL, ATL⋆ [Alur et al., 2002] and Strategy Logic (SL) [Mogavero et al., 2014], include quantification over strategies of the different agents, making it possible to specify concepts that have been traditionally studied in game theory.

While SL, which subsumes ATL⋆ , enables the specification of rich strategic behaviours in on-going multi-agent systems, 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 LTL[F] is a multi-valued logic that augments LTL with quality operators [Almagor et al., 2016]. The satisfaction value of an LTL[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 F can prioritise different scenarios or reduce the satisfaction value of computations in which delays occur. For example, the set F may contain the min{x, y}, max{x, y}, and 1-x functions, which are the standard quantitative analogues of the ∧, ∨, and ¬ operators. The novelty of LTL[F] is the ability to manipulate values by arbitrary functions. For example, F may contain the weighted-average function ⊕λ. The satisfaction value of the formula ψ1 ⊕λ ψ2 is the weighted (according to λ) average between the satisfaction values of ψ1 and ψ2. This enables the specification of the quality of the system to interpolate different aspects of it.

LTL[F] with functions ∧, ∨ and ¬ also corresponds to Fuzzy Linear-time Temporal Logic (Fuzzy LTL) [Lamine and Kabanza, 2000; Frigeri et al., 2014]. Note that by equipping F with adequate functions, we can capture various classic fuzzy interpretations of Boolean operators, such as the Zadeh, G¨odel-Dummett or Łukasiewicz interpretations (see for instance [Frigeri et al., 2014]). However the interpretation of the temporal operators is always that of Fuzzy LTL.

We introduce and study SL[F], an analogous multi-valued extension of SL. In addition to the quantitative semantics that arises from the functions in F, another important aspect of SL[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 fuzziness. Thus, a model-checking procedure for SL[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, and whose objectives are to fly above and below all uncontrollable drones and perform certain actions when uncontrollable drones exhibit some disallowed behaviour. In SL[F] we can specify the quality of strategies for the drones: the different heights are specified with multi-valued atomic propositions, on-going behaviours are expressed with temporal operators and the functions in F may be used to refer to these behaviours in a quantitative manner, for example to compare heights and specify the satisfaction level of different possible scenarios. Note that the SL[F] formula does not merely specify the ability of the drones to behave in some desired manner, but rather it associates a satisfaction value in [0, 1] with each behaviour. For example (see 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. As a result we can express and generalise concepts such as ε-Nash Equilibria [Nisan et al., 2007].

We show that the quantification of strategies in SL[F] can be reduced to a Boolean quantification of atomic propositions, which enables us to reduce the model-checking problem of SL[F] to that of BQCTL⋆ [F], a logic that merges Quantified CTL⋆ [Laroussinie and Markey, 2014] (an extension of CTL⋆ with quantifiers on atomic propositions) with CTL⋆ [F] [Almagor et al., 2016]. A general technique for CTL⋆ 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 [Emerson and Lei, 1987]. This general technique is applied also to CTL⋆ [F], with the fresh atomic propositions being weighted [Almagor et al., 2016]. For BQCTL⋆ [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 CTL⋆ model-checking [Kupferman et al., 2000] to handle quantified propositions: given a BQCTL⋆ [F] formula ψ and predicate P ⊆ [0, 1], we construct an alternating parity tree automaton that accepts exactly all the weighted trees t such that the satisfaction value of ψ in t is in P. The translation, and hence the complexity of the model-checking problem, is nonelementary: we show that it is (k + 1)-EXPTIME-complete for formulas involving at most k nested quantifications on atomic propositions, and we show a similar complexity result for SL[F], in terms of nesting of strategy quantifiers.

1.1 RelatedWork

Various kinds of quantitative objectives have been studied in weighted games, both for two players (parity [Emerson and Jutla, 1991], mean-payoff [Ehrenfeucht and Mycielski, 1979] or energy [Bouyer et al., 2008]) and n-player games (see e.g. [Bruy`ere et al., 2014; Brenguier et al., 2016; Gutierrez et al., 2017]). Similarly, quantitative versions of LTL and CTL have been studied in different contexts, with discounting [Almagor et al., 2014], averaging [Bollig et al., 2012; Bouyer et al., 2014], or richer constructs [Boker et al., 2014; Almagor et al., 2016]. In contrast, the study of quantitative temporal logics for strategic reasoning has remained rather limited: works on LTL[F] include algorithms for synthesis and rational synthesis [Almagor et al., 2016; 2017; 2018], but no logics combine the quantitative aspect of LTL[F] with the strategic reasoning offered by SL.

A quantitative version of SL with Boolean goals over one-counter games has been considered in [Bouyer et al., 2015]; only a periodicity property was proven, and no modelchecking algorithm is known in that setting.

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 multi-valued ATL [Jamroga et al., 2016] and weighted versions of ATL [Laroussinie et al., 2006; Bulling and Goranko, 2013; Vester, 2015]. Finally, some works have considered non-quantitative ATL with quantitative constraints on the set of allowed strategies [Alechina et al., 2010; Della Monica and Murano, 2018], proving decidability of the model-checking problem.

A full version of the present paper with detailed proofs is available as [Bouyer et al., 2019].

2 Quantitative Strategy Logic

Let Σ be an alphabet. A finite (resp. infinite) word over Σ is an element of Σ∗ (resp. Σω ). The length of a finite word w = w0w1 . . .wn is |w| := n + 1, and last(w) := wn is its last letter. Given a finite (resp. infinite) word w and 0 ≤ i < |w| (resp. i ∈ N), the word w≤i = w0 . . .wi is the (non-empty) finite prefix of w that ends at position i and w≥i = wiwi+1 . . . is the suffix of w that starts at position i. We write Pref(w) for the set of non-empty prefixes of w. As usual, for any partial function f, we write dom(f) for the domain of f.

Strategy logic with functions, denoted SL[F], generalises both SL and LTL[F] by replacing the Boolean operators of SL with arbitrary functions over [0, 1]. The logic is actually a family of logics, each parameterised by a set F of functions.

2.1 Syntax

We build on the branching-time variant of SL [Fijalkow et al., 2018], which presents several benefits over classic SL, such as making the connection with Quantified CTL⋆ tighter. Let F ⊆ {f : [0, 1]m → [0, 1] | m ∈ N} be a set of functions.

Definition 1. The syntax of SL[F] is defined with respect to a finite set of atomic propositions AP, a finite set of agents Agt and a set of strategy variables Var. The set of SL[F] formulas is defined by the following grammar:

where p ∈ AP, x ∈ Var, a ∈ Agt, and f ∈ F.

Formulas of type ϕ are called state formulas, those of type ψ are called path formulas. Formulas 〈〈x〉〉ϕ are called strategy quantifications whereas formulas (a, x)ϕ are called bindings. Modalities X and U are temporal modalities, which take a specific quantitative semantics as we see below.

2.2 Semantics

While SL is evaluated on classic concurrent game structures with Boolean valuations for atomic propositions, SL[F] formulas are interpreted on weighted concurrent game structures, in which atomic propositions have values in [0, 1].

Definition 2. A weighted concurrent game structure (WCGS) is a tuple G = (AP, Agt, Act, V, vι, ∆, w) where AP is a finite set of atomic propositions, Agt is a finite set of agents, Act is a finite set of actions, V is a finite set of states, vι ∈ V is an initial state, ∆: V × Act Agt → V is the transition function, and w: V → [0, 1]AP is a weight function.

An element of Act Agt is a joint action. For v ∈ V, we let succ(v) be the set {v′ ∈ V | ∃⃗c ∈ Act Agt . v′ = ∆(v,⃗c)}.

A play in G is an infinite sequence π = (vi)i∈N of states such that v0 = vι and vi ∈ succ(vi-1) for all i > 0. We write PlayG for the set of plays in G, and PlayG (v) for the set of plays in G starting from v. Finite prefixes of plays are called histories, and we let HistG(v) = Pref(PlayG (v)) and HistG = ⋃v∈V HistG(v).

A strategy is a mapping σ : HistG → Act, and StrG is the set of strategies in G. An assignment is a partial function χ: Var ∪Agt ⇀ StrG, that assigns strategies to variables and agents. Assignment χ[a ↦→ σ] maps a to σ and is equal to χ otherwise. The set of outcomes of assignment χ from history ρ is the set Out(χ, ρ) of plays π = ρ · v1v2 . . . such that for every i ∈ N, there exists a joint action ⃗c ∈ Act Agt such that for each agent a ∈ dom(χ),⃗c(a) = χ(a)(π≤|ρ|+i-1) and vi+1 = ∆(vi, ⃗c), where v0 = last(ρ).

Definition 3. Let G be a WCGS over AP and Agt, and χ an assignment for Agt and Var. The satisfaction value of an SL[F] state formula ϕ in the last state of a history ρ with assignment χ, denoted JϕKGχ (ρ), and the satisfaction value of an SL[F] path formula ψ in a play π starting at point i ∈ N, denoted JϕKGχ (ρ), are defined inductively as follows:

That is, the satisfaction value of 〈〈x〉〉ϕ is the maximal value that a choice of strategy for variable x can give to ϕ. Binding (a, x)ϕ just assigns strategy given by x to agent a. In the semantics of ψ1Uψ2, while in the Boolean semantics we care about the first position in which ψ2 holds, in the quantitative setting we maximise over all positions along the play, the minimum between the value of ψ2 at that position and the minimal value of ψ1 before this position.

We may use ⊤, ∨, and ¬ to denote functions 1, max and 1 - x, respectively. We can then define the following classic abbreviations: ⊥:= ¬⊤, ϕ∧ϕ′ := ¬(¬ϕ∨¬ϕ′ ), ϕ→ϕ′ := ¬ϕ∨ϕ′ , Fψ := ⊤Uψ, Gψ := ¬F¬ψ and [[x]]ϕ := ¬〈〈x〉〉¬ϕ. When the values of the atomic propositions are in {0, 1}, one can then check that all standard notations take their usual Boolean meaning.

Remark 1. We will see that when the set of possible satisfaction values of atomic propositions is finite, as is the case when a model is chosen, then each formula has a finite set of possible satisfaction values. Therefore, the infima and suprema in the above definition are in fact minima and maxima.

For a state formula ϕ and a WCGS G, let JϕKG = JϕKG∅ (vι).

2.3 Model Checking

The problem we are interested in is the following generalisation of the model checking problem, which is solved in [Almagor et al., 2016] for LTL[F] and CTL⋆ [F].

Definition 4. Given an SL[F] state formula ϕ, a WCGS G and a predicate P ⊆ [0, 1], decide whether JϕKG ∈ P . 1

The precise complexity of the model-checking problem is stated in terms of nesting depth of formulas, which counts the maximal number nd(ϕ) of nested strategy quantifiers in a formula ϕ. We establish the following result in Section ??:

Theorem 1. The model-checking problem for SL[F] formulas of nesting depth at most k is (k + 1)-EXPTIME-complete.

2.4 What can SL[F] Express?

SL[F] naturally embeds SL. Indeed, if the values of the atomic propositions are in {0, 1} and F = {∨, ∧, ¬}, then the satisfaction value of every SL[F] formula ϕ is in {0, 1} and coincides with the semantics of ϕ seen as an SL formula. Also, the same way ATL⋆ [Alur et al., 2002] is embedded in SL, so is ATL∗ [F] embedded in SL[F], where ATL∗ [F] is the natural quantitative extension of ATL∗ .

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 ⃗γ = (γ1, γ2, γ3) ∈ [0, 1]3 . We use the triples of atomic propositions p⃗γ = (pγ1 , pγ2 , pγ3 ) and q⃗γ = (qγ1 , qγ2 , qγ3 ) to denote the coordinates of c and v, respectively. Write dist : [0, 1]3 × [0, 1]3 → [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 SL[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

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 LTL[F] specification is 0 if there is a path in which the artifact is never rescued.

Synthesis with Quantitative Objectives

In LTL reactive synthesis [Pnueli and Rosner, 1989], a controller and an environment operate on two disjoint sets of variables in the system. The problem consists in synthesising a strategy for the controller such that, no matter the behaviour of the environment, the resulting execution satisfies

1 Predicate P is finitely represented, typically as an interval.

ψ. Recently, this problem has been addressed in the context of LTL[F], where the controller aims at maximising the value of an LTL[F] formula ϕ, while the environment acts as minimiser. This problem can be expressed in SL[F] with the formula

where c and e are the controller and environment, and ψ is the specification in LTL[F].

We mention (but do not develop, by lack of space) that we can also express the variant of reactive synthesis called rational synthesis [Kupferman et al., 2016]. This problem considers an environment composed of several rational components, and aims at synthesising a strategy that ensures the specification against all (or some) rational behaviours of the environment, where rational is characterised by some game-theoretic concept such as Nash equilibrium of subgame-perfect equilibrium. Our expressive logic allows us to deal with richer objectives than in [Almagor et al., 2018].

Nash Equilibria in Weighted Games

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

A strategy profile (σi)ai∈Agt is a NE if all agents play one of their best responses against their opponents' strategies. Consider formula

where α ⪯ β is actually a function ⪯: [0, 1]2 → [0, 1] such that ⪯(α, β) = 1 if α ≤ β and ⪯(α, β) = 0 otherwise. Then JϕNEKGχ (v) = 1 if, and only if, (χ(xi))ai∈Agt form a NE from position v.

Adopting a more quantitative point of view, we can measure how much agent i can benefit from a selfish deviation using formula 〈〈yi〉〉diff((ai, yi)ϕi, ϕi), where diff(x, y) = max{0, x - y}. The maximal benefit that some agent may get is then captured by the following formula:

Formula ϕNE can be used to characterise ε-NE, by requiring that ϕNE has value less than or equal to ε; of course it also characterises classical NE as a special case.

Secure Equilibria in Weighted Games

Secure equilibria [Chatterjee et al., 2006] 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[F] as follows:

where (α1, α2) ⪯i (β1, β2) is equal to 1 when αi ≤ βi or both αi = βi and α3-i ≤ β3-i, and 0 otherwise.

Secure equilibria have also been studied in Q-weighted games [Bruy`ere et al., 2014]: 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 Gw is the infimum of the weights, while the value of FGw is the limit infimum. We can then characterise secure equilibria with (limit) infimum and supremum objectives by using those formulas as the objectives for the agents in formula ϕSE.

3 Booleanly Quantified CTL⋆ [F]

In this section we introduce Booleanly Quantified CTL⋆ [F] (BQCTL⋆ [F], for short) which extends both CTL⋆ [F] and QCTL⋆ [Laroussinie and Markey, 2014].

3.1 Syntax

Let F ⊆ {f : [0, 1]m → [0, 1] | m ∈ N} be a set of functions.

Definition 5. The syntax of BQCTL⋆ [F] is defined with respect to a finite set AP of atomic propositions, using the following grammar:

where p ranges over AP and f over F.

Formulas of type ϕ are called state formulas, those of type ψ are called path formulas, and BQCTL⋆ [F] consists of all state formulas. We again use ⊤, ∨, and ¬ to denote functions 1, max and 1 - x, as well as classic abbreviations already introduced for SL[F], plus Aψ := ¬E¬ψ.

3.2 Semantics

While BQCTL⋆ [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, hence the name of the logic.

Definition 6. A weighted Kripke structure (WKS) is a tuple K = (AP, S, sι,R,w) where AP is a finite set of atomic propositions, S is a finite set of states, sι ∈ S is an initial state, R ⊆ S × S is a left-total transition relation, and w: S → [0, 1]AP is a weight function.

A path in K is an infinite word π = π0π1 . . . over S such that π0 = sι and (πi, πi+1) ∈ R for all i. We call finite prefixes of paths histories, and HistK is the set of all histories in K. We also let VK = {w(s)(p) | s ∈ S and p ∈ AP} be the finite set of values appearing in K.

Given finite sets D of directions, AP of atomic propositions, and V ⊆ [0, 1] of possible values, an (AP, V )-labelled D-tree, (or tree for short when the parameters are understood), is a pair t = (τ,w) where τ ⊆ D+ is closed under non-empty prefixes, all nodes u ∈ τ start with the same direction r, called the root, and have at least one child u·d ∈ τ , and w : τ → V AP is a weight function. A branch λ = u0u1 . . . is an infinite sequence of nodes such that for all i ≥ 0, we have that ui+1 is a child of ui. We let Br(u) be the set of branches that start in node u. We say that a tree t = (τ,w) is Boolean in p, written Bool(t, p), if for all u ∈ τ we have w(u)(p) ∈ {0, 1}. As with weighted Kripke structures, we let Vt = {w(u)(p) | u ∈ τ and p ∈ AP}.

Given two (AP, V )-labelled D-trees t, t′ and p ∈ AP, we write t ≡p t′ if t and t′ differ only in assignments to p, which must be Boolean in t′ : formally, t = (τ,w), t′ = (τ,w′ ), for the same domain τ , Bool(t′ , p), and for all p′ ∈ AP such that p′ ̸= p and all u ∈ τ , we have w(u)(p′ ) = w′ (u)(p′ ).

Finally, the tree unfolding of a WKS K over atomic propositions AP and states S is the (AP, VK)-labelled S-tree tK = (HistK, w′ ), where w′ (u) = w(last(u)) for every u ∈ HistK.

Definition 7. Given a tree t, the satisfaction value JϕKt (u) of a BQCTL⋆ [F] state formula ϕ in node u of t, and the satisfaction value JψKt (λ) of a BQCTL⋆ [F] path formula ψ along a path λ of t, are defined inductively as follows:

Remark 2. As with SL[F], the suprema in the above definition can be replaced with maxima (see Lemma 3 below).

First, note that if F = {⊤, ∨, ¬}, then BQCTL⋆ [F] evaluated on Boolean Kripke structures corresponds to classic QCTL⋆ . Note also that the quantifier on propositions does not range over arbitrary values in [0, 1]. Instead, as in QCTL⋆ , it quantifies only on Boolean valuations. It is still quantitative though, in the sense that instead of merely stating the existence of a valuation, ∃p. ϕ maximises the value of ϕ over all possible (Boolean) valuations of p.

For a tree t with root r we write JϕKt for JϕKt (r), and for a WKS K we write JϕKK for JϕKtK . Note that this semantics is an extension of the tree semantics of QCTL⋆ , 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 SL based on strategies with perfect recall, where moves can depend on the history, as opposed to the memoryless semantics, where strategies can only depend on the current state (see [Laroussinie and Markey, 2014] for more details).

We study the following model-checking problem:

Definition 8. Given a BQCTL⋆ [F] state formula ϕ, a WKS K and a predicate P ⊆ [0, 1], decide whether JϕKK ∈ P .

Similarly to SL[F], the precise complexity of the modelchecking problem will be stated in terms of nesting depth of formulas, which counts the maximal number of nested propositional quantifiers in a formula ϕ, and is written nd(ϕ).

In the next section we establish our main technical contribution, which is the following:

Theorem 2. The model-checking problem for BQCTL⋆ [F] formulas of nesting depth k is (k + 1)-EXPTIME-complete.

This result, together with a reduction from SL[F] to BQCTL⋆ [F] that we present in Section ??, entails the decidability of model checking SL[F] announced in Theorem 1.

4 Model Checking

We start by proving that, as for LTL[F], when the set of possible values of atomic propositions is finite, so is the set of possible satisfaction values of each BQCTL⋆ [F] formula. This property allows to use max instead of sup in Definition 7.

Lemma 3. Let V ⊂ [0, 1] be a finite set of values with {0, 1} ⊆ V and ϕ a BQCTL⋆ [F] state formula. Define

be the set of values taken by ϕ in nodes of (AP, V )-labelled trees. Then, |Vϕ| ≤ |V||ϕ| , and one can compute ˜ Vϕ of size at most |V||ϕ| such that Vϕ ⊆ ˜ Vϕ.

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 A and A′ we denote A∧A′ (resp. A∨A′ ) the APT of size linear in |A| and |A′ | that accepts the intersection (resp. union) of the languages of A and A′ , and we call index of an automaton the number of priorities in its parity condition. We refer the reader to [Kupferman and Vardi, 2005] for a detailed exposition of alternating parity tree automata.

We extend the automata construction from [Kupferman et al., 2000] to handle quantification on atomic propositions and the quantitative aspect of our model-checking problem.

Proposition 4. Let V ⊂ [0, 1] be a finite set of values such that {0, 1} ⊆ V, and let D be a finite set of directions. For every BQCTL⋆ [F] state formula ϕ and predicate P ⊆ [0, 1], one can construct an APT AV,P ϕ such that for every (AP, V )- labelled D-tree t, AV,P ϕ accepts t if and only if JϕKt ∈ P.

The APT AV,P ϕ has at most (nd(ϕ)+1)-exponentiallymany states, and its index is at most nd(ϕ)-exponential.

Proof sketch. We sketch how the two interesting inductive cases are dealt with.

When ϕ is of the form ∃p. ϕ′ , the automaton has to check that the maximal satisfaction value of ϕ′ for all possible Boolean valuations of p is in P. First, compute finite set ˜ Vϕ′ from Lemma 3. Then for each possible v ∈ ˜ Vϕ′ ∩P , we build an automaton for checking that the value of ϕ′ is less than v for all p-valuations, and that value v is reached for some pvaluation. Inductively build the APTs AV,{v} ϕ′ andAV,[0,v]∩P ϕ′ .

Turn the first one into a NPT N=v and the second one into a UPT U≤v. Project N=v existentially on p, and call the result N ′=v . Project U≤v universally on p, call the result U ′≤v . Finally, define the APT AV,P ∃p. ϕ′ := ∨v∈˜ Vϕ′∩P N ′=v ∧ U ′≤v . 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 ϕ′ for all p-valuations.

When ϕ is of the form Eψ, first let atoms(ψ) be the set of maximal state sub-formulas of ψ (called atoms). In a first step we see ψ as an LTL[F] formula over atoms(ψ). For each ϕ′ ∈ atoms(ψ), compute the set ˜ Vϕ′ from Lemma 3, and let ˜ V = ⋃ϕ′∈atoms(ψ) ˜ Vϕ′ . Build a non-deterministic parity automaton Wψ P that accepts the set of words w ∈ (˜ V atoms(ψ) )ω such that JψK(w) ∈ P [Almagor et al., 2016]. Then compute ˜ VEψ (again using Lemma 3), and for each v ∈ ˜ VEψ ∩ P , construct an NPT N E=v that guesses a branch in its input and simulates Wψ {v} on it. Dually, build a universal word automaton Wψ [0,v] and then a UPT U A≤v that executes Wψ [0,v] on all branches of its input. Finally, define the APT AP on ˜ V atoms(ψ) -trees as AP = ∨v∈˜ VEψ∩P N E=v ∧ U A≤v .

To go from atoms to atomic propositions, define an APT AV,P Eψ that, in each state and each node of its input, guesses a value vi in ˜ Vϕi for each ϕi ∈ atoms(ψ), simulates AP on the resulting label, and launches a copy of AV,{vi} ϕi for each ϕi ∈ atoms(ψ). Note that the automaton is alternating and thus may have to guess several times the satisfaction value of a formula ϕi in a same node, but launching the AV,{vi} ϕi forces it to always guess the same, correct value.

To check whether JϕKK ∈ P, where atomic propositions in K take values in V, it is enough to build AV,P ϕ as in Proposition 4, take its product with a deterministic tree automaton that accepts only tK, and check for emptiness of the product automaton. The formula complexity is (nd(ϕ) + 1)- exponential, but the structure complexity is polynomial. The time complexity is (nd(ϕ) + 1)-exponential in the size of ϕ, but it is polynomial in the size of the game structure.

The lower bounds are obtained by reduction from the model-checking problem for EQkCTL⋆ , a fragment of QCTL⋆ that consists in formulas in prenex normal formwith at most k alternations between existential and universal quantifiers. This problem is (k + 1)-EXPTIME-hard [Laroussinie and Markey, 2014], and clearly, EQkCTL⋆ can be translated in BQCTL⋆ [F] with formulas of linear size and nesting depth at most k (alternation is simply coded by inserting function ¬ between quantifiers).

The usual reduction for qualitative variants of SL (see e.g. [Laroussinie and Markey, 2015; Berthon et al., 2017; Fijalkow et al., 2018]) can be lifted to the quantitative setting in a straightforward manner: for each instance (G, ϕ, P) of the model-checking problem for SL[F], we build a WKS KG and a BQCTL⋆ [F] formula ϕ′ such that JϕKG = Jϕ′ KKG .

The model-checking problem for (G, φ, P) is then solved by deciding whether Jϕ′ KKG ∈ P , which can be done by Theorem 2. This establishes the upper-bounds in Theorem 1.

As in the case of BQCTL⋆ [F], the lower-bounds are obtained by reduction from the model-checking problem for EQkCTL⋆ . This reduction is an adaptation of the one from QCTL⋆ to ATL with strategy context in [Laroussinie and Markey, 2015], and that preserves nesting depth.

Remark 3. This reduction and Lemma 3 imply that when we fix possible values for atomic propositions, then possible values for an SL[F] formula are at most exponentially many.

We now consider the fragment SL1G[F] of SL[F], in which all formulas have the form ℘ ♭ ψ where ℘ only contains strategy quantifiers, ♭ binds strategies to all agents, and ψ is an LTL[F] formula (possibly involving closed SL1G[F] subformulas as subformulas). It is the quantitative extension of SL1G, the one-goal fragment of SL [Mogavero et al., 2014].

As in the Boolean case, where SL1G strictly subsumes ATL⋆ while enjoying the same elementary complexity for the model-checking problem, in the quantitative setting also SL1G[F] strictly subsumes ATL⋆ [F], and we have:

Theorem5. The model-checking problem for SL1G[F] is decidable, and 2-EXPTIME-complete.

5 Discussion

We introduced and studied SL[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 [Chockler et al., 2006]. When applied to SL[F], these algorithms can set the basis to a formal reasoning about classical notions in game theory, like the sensitivity of utilities to price changes, the effectiveness of burning money [Hartline and Roughgarden, 2008; Souza and Rego, 2016] or tax increase [Cole et al., 2006], and more. Recall that our SL[F] model-checking algorithm reduces the problem to BQCTL⋆ [F], where the quantified atomic propositions take Boolean values. It is interesting to extend BQCTL⋆ [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 QCTL⋆ [F], where quantified atomic propositions may take values in [0, 1].

Acknowledgements

Perelli thanks the support of the project "dSynMA", funded by the ERC under the European Union's Horizon 2020 research and innovation programme (grant agreement No 772459). Bouyer and Markey thank the support of the ERC Project EQualIS (308087).