Discounting in Strategy Logic

1 Introduction

The goal of this paper is to advance the research on strategic reasoning and formal verification by considering a discounting effect: the utility of agents decreases over time. Boolean state-transition models have been widely used to define the semantics of temporal and strategic logics, including Linear Temporal Logic (LTL) [Pnueli, 1977], Alternating-time Temporal Logic (ATL) [Alur et al., 2002], Strategy Logic (SL) [Mogavero et al., 2014; Chatterjee et al., 2010]. In conjunction with model checking techniques [Clarke et al., 2018], these formal frameworks are useful for the representation and verification of hardware and software systems. Given a strategic logic specification, the correctness of a system is a yes/no matter: either the system satisfies the specification or it does not. Complex systems that interact with a physical environment or that are composed of multiple autonomous agents may have quantitative aspects described by real numbers (e.g. utilities, time and costs). Evaluating the quality of such systems through the Boolean satisfaction of the specifications is often inadequate. Different levels of quality may exist, and this should be reflected in the output of the verification procedure [Almagor et al., 2014].

In this work, we are interested in verifying Multi-Agent Systems (MAS) whose quality assessment needs to take into account that satisfying the goal sooner is different from satisfying it after a long wait. To illustrate this setting, consider an agent whose task is to organize a trip and who is facing the problem of booking a flight. An early booking is more susceptible to becoming unfeasible in the case of unforeseen changes in the travel plans. On the other hand, waiting to book may result in more important costs for the agent. Moreover, the trip-organizing agent may be a part of a system composed of other, self-interested, agents. In this case, the agents' interactions can also influence their ability to find reasonable flight options and price tags. On one side, there is a competitive aspect when agents dispute the last available tickets. Cooperation could also take place as some companies offer discounts for group booking. To address this problem for (single-agent) systems, researchers have suggested to augment Linear Temporal Logic with future discounting [De Alfaro et al., 2005; Almagor et al., 2014]. In the discounted setting, the satisfaction value of specifications is a numerical value, and it depends, according to some discounting function, on the time waited for eventualities to get satisfied.

Discounting is a key dimension in Economics and has been studied in Markov decision processes [Filar and Vrieze, 1996] as well as game theory [Shapley, 1953] and system theory [De Alfaro et al., 2003] to capture the intuition that the far-away future is not as important as the near future. The multi-agent setting has also been widely investigated, including repeated games [Abreu, 1988; Fudenberg and Maskin, 2009; P˛eski, 2014], the prisoner's dilemma game [Harris and Madden, 2002; Locey et al., 2013], and negotiation protocols [Weg et al., 1990; Fatima et al., 2006], to name a few. Previous work [Jamroga, 2008b; Chen et al., 2013] have initiated to study logics inspired on ATL and Markov chains for reasoning about discounting in stochastic MAS. Likewise ATL, these logics are unable to capture complex solution concepts in MAS (such as Nash equilibria), which are important when evaluating the possible outcomes of such systems.

Contribution. In this work, we augment Strategy Logic with future discounting, denoted SL disc [D], and study its complexity for model-checking. The main advantage of this logic is that it allows us to express and verify (i) the strategic abilities of agents to achieve certain goals while considering temporal discounts, and (ii) complex strategy concepts such as Nash equilibrium of discounted games. Different from previous work, we focus on deterministic games and consider temporal discounting alongside a logic that quantifies over strategies. This enables an unbounded number of alternations from strategic operators which is necessary to capture complex solution concepts. In relation to technical results, we also studied the complexity of the model-checking problem under memoryless and perfect recall strategies, which was not established in [Jamroga, 2008b].

SL disc [D] represents a family of logics, each one parameterized by a set of discounting functions. Considering a set of functions allows us to model games in which each agent, or a coalition of them, is affected differently by how long in the future events occur (e.g., patient vs hurried agents). We also provide complexity results for model-checking and motivate the approach with classical examples from Game Theory.

This is the first work to consider a Strategy Logic with discounting for strategic reasoning in MAS. We aim at paving the way for a new line of research that applies the formal techniques developed for verification and reasoning in MAS to game-theoretic problems involving future discounts.

Outline. We first discuss related work in Section 2. Then, we define SL disc [D] in Section 3. We proceed by illustrating the use of SL disc [D] in multi-agent games (Section 4). Next, we study the complexity results for model checking (Section 5). Finally, we conclude the paper in Section 6.

2 RelatedWork

Weighted games have been studied in the literature in relation to various kinds of objectives, including parity [Emerson and Jutla, 1991], mean-payoff [Ehrenfeucht and Mycielski, 1979; Zwick and Paterson, 1996], energy [Chakrabarti et al., 2003; Bouyer et al., 2008], and combining qualitative and quantitative objectives in equilibrium [Gutierrez et al., 2021]. SL[F] [Bouyer et al., 2019; Bouyer et al., 2023] was recently introduced as a quantitative extension of SL defined over weighted concurrent game structures. It extends LTL[F] [Almagor et al., 2016], a multi-valued logic that augments LTL with quality operators. SL[F] subsumes both SL and LTL[F] and is expressive enough to express complex solution concepts such as Nash equilibrium and properties about quantities. An extension of SL[F] with imperfect information and epistemic operators was recently proposed [Maubert et al., 2021]. Other quantitative extensions of LTL have been explored in the context of averaging [Bouyer et al., 2014], discounting [Almagor et al., 2014; Mandrali, 2012], and mean-payoff objectives [Bohy et al., 2013]. Quantitative extensions of ATL have also been investigated, such as timed ATL [Henzinger and Prabhu, 2006; Brihaye et al., 2007], multi-valued ATL [Jamroga et al., 2020], ATL with resource bounds [Alechina et al., 2017; Alechina et al., 2018], and weighted versions of ATL [Laroussinie et al., 2006; Bulling and Goranko, 2022; Vester, 2015]. Another related problem is prompt requirements (see, for instance, [Aminof et al., 2016; Fijalkow et al., 2020]), which consider a bound on the number of steps to satisfy the specification.

To encode the notion that the importance of events should be discounted according to how late they occur, De Alfaro et al. (2005) proposed an extension of the Computational Tree Logic with quantitative semantics. In this logic, path operators are discounted by a parameter that can be chosen to give more weight to states that are closer to the beginning of the path. Later, Almagor et al. (2014) proposed LTL augmented with an arbitrary set of discounting functions, denoted LTL disc [D]; and further explored with unary propositional quality operators and average-operator. Bozzone and Naumov (2021) proposes a logical system for reasoning about strategic abilities under budget constraints and discounting.

In the context of stochastic systems, Jamroga (2008a) proposed an extension of the Branching-Time Temporal Logic and captures discounted goals. Later, this approach was extended to the multi-agent setting [Jamroga, 2008b]. Finally, Chen et al. (2013) considered a probabilistic extension of ATL, alongside discounted rewards.

3 Strategy Logic with Discounting

Strategy Logic with Discount (SL disc [D]) generalizes SL by adding discounting temporal operators. The logic is actually a family of logics, each parameterized by a set D of discounting functions. A function d : N → [0, 1] is a discounting function if limi→∞d(i) = 0, and d is non-increasing. Examples of discounting functions include d(i) = λi , for some λ ∈ (0, 1), and d(i) = 1 i+1 .

For the remainder of the paper, we fix a set of discounting functions D, a set of atomic propositions AP, a set of agents Ag, and a set of strategy variables Var, except when stated otherwise.

The syntax of SL disc [D] adds to SL the operator φUdψ (discounting-Until), for every function d ∈ D. The logic is defined SL disc [D] as follows:

Definition 1. The syntax of SL disc [D] is defined by the grammar

The intuitive reading of the operators is as follows: ∃s. φ means that there exists a strategy such that φ holds; (a, s)φ means that when strategy s is assigned (or "bound") to agent a, φ holds; X and U are the usual temporal operators "next" and "until". The intuition of the operator Ud is that events that happen in the future have a lower influence, and the rate by which this influence decreases depends on the function d.

A variable is free in a formula φ if it is bound to an agent without being quantified upon, and an agent a is free in φ if φ contains a temporal operator (X, U, Ud) not in the scope of any binding for a. The set of free variables and agents in φ is written free(φ), and a formula φ is a sentence if free(φ) = ∅.

A state-transition model is a labeled directed graph, in which the vertices represent the system states, the edges the state changes (e.g., according to environment or agents' actions), and the labels the Boolean characteristics of the state (i.e., the truth values of state atomic propositions). In this paper, we consider state-transition models in which there are multiple agents that act simultaneously and independently. These models are called concurrent game structures (CGS).

Definition 2. A concurrent game structure (CGS) is a tuple G = (Ac, V, vι, δ, ℓ) where (i) Ac is a finite set of actions; (ii) V is a finite set of positions; (iii) vι ∈ V is an initial position; (iv) δ : V ×Ac Ag → V is a transition function; (v) ℓ : V → 2AP is a labeling function.

In a position v ∈ V , each player a chooses an action ca ∈ Ac, and the game proceeds to position δ(v, c) where c ∈ Ac Ag is an action profile (ca)a∈Ag.

We write o for a tuple of objects (oa)a∈Ag, one for each agent, and such tuples are called profiles. Given a profile o and a ∈ Ag, we let oa be agent a's component, and o-a is (ob)b̸=a. Similarly, we let Ag-a = Ag \ {a}. For a group of n agents A = {a1, ..., an} and strategy profile σ = σ1, ..., σn we write (A, σ) as a shortcut for (a1, σ1)...(an, σn).

A play π = v0v1... in G is an infinite sequence of positions such that v0 = vι and for every i ≥ 0 there exists an action profile c such that δ(vi, c) = vi+1. We write πi = vi for the position at index i in play π. A history h is a finite prefix of a play, last(h) is the last position of history h, |h| is the length of h and Hist is the set of histories.

A (perfect recall) strategy is a function σ : Hist → Ac that maps each history to an action. A (memoryless) strategy is a function σ : V → Ac that maps each position to an action. We let Str R (similarly Str r ) be the set of perfect recall strategies (resp. memoryless strategies). For the remainder of the paper, we use r and R to denote memoryless and perfect recall, respectively, and we let ρ = {r, R}.

An assignment χ : Ag ∪ Var → Str is a function from players and variables to strategies. For an assignment χ, an agent a and a strategy σ for a, χ[a ↦→ σ] is the assignment that maps a to σ and is otherwise equal to χ, and χ[s ↦→ σ] is defined similarly, where s is a variable.

For an assignment χ and a state v, we let Out(χ, v) be the unique play that continues v following the strategies assigned by χ. Formally, Out(χ, v) is the play vv0v1... such that for all i ≥ 0, vi = δ(vi-1, c) where for all a ∈ Ag, ca = χ(a)(vv1...vi-1).

Definition 3. Let G = (Ac, V, vι, δ, ℓ) be a CGS, χ be an assignment, and ρ ∈ {R, r}. The satisfaction value �φ�G, ρ χ (v) ∈ [0, 1] of an SL disc [D] formula φ in a state v is defined as follows, where π denotes Out(χ, v):

If φ is a sentence, its satisfaction value does not depend on the assignment, and we write �φ�G, ρ (v) for �φ�G, ρ χ (v) where χ is any assignment. We also let �φ�G, ρ = �φ�G, ρ (vι).

Classical abbreviations are defined as follows: ⊥:= ¬⊤, φ∧φ′ := ¬(¬φ∨¬φ′ ), φ→φ′ := ¬φ∨φ′ , Fψ := ⊤Uψ, Gψ := ¬F¬ψ and ∀s. φ := ¬∃s. ¬φ. The quantitative counterparts of G and F, denoted Gd and Fd, are defined analogously.

Relation with LTL disc [D], SL and SL[F]. LTL disc [D] [Almagor et al., 2014] is the fragment of SL disc [D] without strategy quantification and bindings. Considering that the satisfactions values 1 and 0 represent true and false (resp.), SL [Mogavero et al., 2014] is a syntactical restriction of SL disc [D] (without the discounted-Until). SL cannot express that the value of a formula decays over time. To notice the difference, assume a CGS G, an assignment χ and states v, v′ such that and Out(χ, v′ ) = π0π and π = Out(χ, v), that is, the outcome from v′ is the outcome from v with the first state repeated. Assuming that p ∈ ℓ(πi) and d(i) ̸= d(i - 1), for some i ≥ 1 and p ∈ AP, we have that �Fd p�G, ρ χ (v) ̸= �Fd p�G, ρ χ (π′ ). However, using the classical until, we have that �Fp�G, ρ χ (v) = �Fp�G, ρ χ (π′ ). As for SL[F] [Bouyer et al., 2019], notice it is interpreted over different classes of models from SL disc [D], namely weighted CGS, which uses weight functions for atomic propositions in place of propositional labeling of states. SL[F] is defined over a set of functions F over [0, 1], but its semantics does not enable to use these functions to capture the effect of future discounts. This is because functions are applied over the satisfaction value of formulas in a given state, independent from how far in the play they are being evaluated w.r.t. the initial state.

4 Discounting inMulti-Agent Games

We now introduce problems and concepts from Game Theory that motivated reasoning about discounts in MAS.

4.1 Nash Equilibrium for SL disc [D] Goals

Nash equilibrium (NE) is a central solution concept in game theory that captures the notion of a stable solution, that is a solution from which no single player can individually improve his or her welfare by deviating [Nisan et al., 2007]. Deterministic concurrent multi-player Nash equilibrium can be expressed using SL (or its extensions) for Boolean valued goals [Mogavero et al., 2014] and quantitative goals [Bouyer et al., 2019]. With SL disc [D], we can express that agent's goals are affected by how long in the future they are achieved.

Let the LTL disc [D]-formula ψa (i.e., an SL disc [D] formula without bindings and strategy quantification) denote the goal of agent a. We can express whether a strategy profile σ = (σa)a∈Ag is a Nash equilibrium through the SL disc [D] formula

The existence of a Nash equilibrium is captured by the formula ˆ φNE := ∃σ(φNE(σ)). This is a classical problem in game theory and, more precisely when studying games with future discounting [Fudenberg and Maskin, 1990].

As we shall see in the next sections, the goal ψa of an agent a may involve temporal discounts. In the booking agent example, for instance, the discounted goal

specifies that the flight ticket is affordable (that is, below a threshold ϑ) until agent a booked her ticket. The value obtained from achieving the goal later is reduced according to the discounted function d.

4.2 Secretary Problem

The classical secretary problem studies the problem of an agent selecting online an element (called a "secretary") the maximum value from a known number of candidates to be presented one by one in random order. As each item is presented she must either accept it, in which case the game ends, or reject it. In the second case, the next item in the sequence is presented and the agent faces the same choice as before [Freeman, 1983]. Applications of this problem include agents' facing the decision of buying a house or hiring employees. Several variants and extensions of the secretary problem are considered in the literature, including using time-dependent discount factors to reduce the benefit derived from selecting a secretary at a later time [Babaioff et al., 2009]. The discounted setting captures the cost of rejecting elements. For instance, when seeking to purchase a house, an agent may prefer to chose a suboptimal house at the beginning of the game than wait longer to pick her most desirable house. Recently, Do et al. (2022) investigated the selection of k secretaries by a multi-agent selection committee. The hiring decision is made by a group of voting agents that specify whether they consider acceptable to hire the current candidate or not.

With CGS, we can represent deterministic perfect information instances of the secretary problem. Let us consider the selection of k secretaries by multiple voting agents. For each candidate j from a finite set of candidates C, we let the atomic propositions presentj denote whether she was presented and hiredj denote whether she was hired. Proposition k-hired specifies whether k secretaries were already selected 1 .

The SL disc [D] formula Fd k-hired represents the goal of having enough candidates hired in the future. The satisfaction value of this goal decreases according to d, denoting that it is preferable to hire k candidates as soon as possible. The discounted goal

represents that the voter a has a strategy to ensure that, no matter the strategies of the other agents, there are candidates still not presented until enough secretaries were hired.

1 The formalization of the game as a CGS is left to the reader. Examples on how to model similar problems using CGS can be found in [Mittelmann and Perrussel, 2020; Maubert et al., 2021].

In Figure 1, we exemplify the CGS Gsec representing an instance of the secretary problem with two voting agents, Ann and Bob, and three candidates, a, b, and c. In the initial state (q0), the agents vote on whether they want to hire candidate a by performing the action y or n. Candidate a is hired only if both agents play y, in which case the game moves to state q2. Otherwise, the game proceeds to state q1 in which they can vote for candidate b (and similarly, for candidate c in state q3. The game ends when one secretary is hired (states q2, q4, and q6) or all candidates have been presented (state q5).

We let the following SL disc [D] formulas denote agent a's and agent b's goals, resp.:

and we assume the discount functions dAnn(i) = 1 i+1 and dBob(i) = ( 12 )i . In other words, Ann's goal is to hire candidate b in the future or to hire any candidate (with a discount according to dAnn), while Bob's goal is to hire a candidate in the future (with a discount given by dBob). Notice that without the discount functions, hiring a secretary earlier would be similar to hiring later. The two discount functions stress that Bob is more eager to hire a secretary than Ann. Table 1 shows the value of the functions in each time i.

The satisfaction value of the agents' goals is only different from 0 in the states in which a candidate were hired. Let σabc denote the strategy of playing y for each candidate (that is, σabc(q0) = σabc(q1) = σabc(q3) = y), σbc denote the strategy of playing y only for candidates b and c, and σc denote the strategy of playing y only for c. Table 2 shows the satisfaction value of agents goals' from the initial state q0 for different assignments of strategies.

As illustrated on Table 2, the strategy profile (σbc, σabc) is a Nash equilibrium and thus � ˆ φNE�Gs,r ̸= 0 (note memoryless strategies are enough for this problem).

4.3 Negotiation with Time Constraints

Let us consider a second context where discounting is a key issue. Negotiation is a type of interaction in MAS in which disputing agents decide how to divide a resource. Time constraints, which may be in the form of both deadlines and discount factors, are an essential element of negotiation because the interaction cannot go on indefinitely and must end within a reasonable time limit [Livne, 1979]. Here we consider the problem of negotiation with time constraints studied in [Rubinstein, 1982; Fatima et al., 2006], and generalize to the multiple agent case. In this problem, agents want to determine how to divide (single or multiple) issues, called "pies", of size 1 among themselves. The negotiation must end in at most n ∈ N+ rounds. This deadline can be represented with an arbitrary discounting function dn such that dn(n) = 0. In this case, a goal in the form Fdn ψ motivates agents to achieve ψ before the n-th stage of the negotiation.

The negotiation process is made by alternating offers from the agents. Initially, a starts by making an offer on how to divide a pie to the other agents Ag-a . Agents in Ag-a can either accept or reject this offer. If agents in Ag-a accept, the negotiation ends in an agreement with the proposed share. Otherwise, an agent b ̸= a makes a counteroffer in the next round. The negotiation proceeds until there is an agreement on accepting an offer. The key feature of this problem is that the pie is assumed to shrink (i.e., to lose value) with time [Rubinstein, 1982]. This represents the situation in which the pie perishes with time or is affected by inflation. The pie shrinkage is represented with by a discount function dpie. At time i = 1, the size of the pie is 1, but in all subsequent time periods i > 1, the pie shrinks to dpie(i).

Figure 2 shows the CGS Gngt, which illustrates an instance of the negotiation problem with a single-issue and two agents, Alice and Beth. The game starts in state q0, where Alice can make an offer to split the pie either so as to take half or two thirds of it for herself (while the remaining of the pie is left for Beth). In the next state (either q1 or q2, according to Alice's action), Beth can perform the action acc to accept the offer or she can make a counteroffer and pass the turn to Alice. As soon as an agent accepts an offer, the negotiation ends and the pie is divided (e.g., states q3, q6, q9, ans q12).

Let us use the atomic propositions twothirda, halfa, and onethirda to denote whether agent a ∈ {Alice, Beth} has received two thirds, half, or one-third of the pie. Agents may have different preferences for how much of the pie they receive. Discounting functions can be used to capture the share they are more eager to receive. For instance, let

be the goal of agents a ∈ {Alice,Beth}, with the discounting functions defined as dn/m := nm dpie(i) for n,m ∈ {1, 2, 3}. This goal stresses that agent a prefers to get twothirds of the pie over half or one-third, and half of the pie over one-third. Note that for the sake of simplicity of this example, deadlines are not considered in ψa.

To continue the example, consider that the discounting function dpie is defined as follows

This represents that the pie starts shrinking only after the 2nd game stage (states q9, q10, q11 and so on). After that, the pie shrinks by half in each successive state. In this case, the rate in which the pie shrinks motivates agents to accept the first proposed division.

Given the discount function dpie(i) and the goals ψAlice and ψBeth, a Nash equilibrium from the game is the strategy profile (σAlice, σBeth), where σAlice and σBeth are strategies such that σAlice(q0) = [ 23 , 13 ] and σBeth(q) = acc for any state q. Thus, we have that � ˆ φNE�Gn,r ̸= 0.

5 Model Checking SL with Discounting

In this section, we study the quantitative model checking problem for SL disc [D]. Let us first define it formally.

Definition 4. The threshold model-checking problem for SL disc [D] consists in deciding, given a formula φ, a CGS G, ρ ∈ {R, r}, and a threshold ϑ ∈ [0, 1], whether �φ�G, ρ ≥ ϑ.

5.1 Memoryless Strategies

Model-checking SL disc [D] with memoryless agents is no harder than model-checking LTL or classical SL with memoryless agents.

Theorem 1. Assuming that functions in D can be computed in polynomial space, model checking SL disc [D] with memoryless agents is PSPACE-complete.

Proof. The lower bound is inherited fromSL [Cermák et al., 2018] 2 , which is captured by SL disc [D]. For the upper bound, we first show that each recursive call only needs at most polynomial space. Most cases are treated analogously to the proof of Theorem 2 in [Maubert et al., 2021]. We focus on the case �φ1Udφ2�G, r χ (v). Let π = Out(v, χ). When evaluating a discounted operator on π, one can restrict attention to two cases: either the satisfaction value of the formula goes below ϑ, in which case this happens after a bounded prefix (with index m ≥ 0), or the satisfaction value always remains above ϑ, in which case we can replace the discounted operator with a Boolean one. This allows us to look only at a finite number of stages. In the first case, let m ≥ 0 denote the first index in which the satisfaction value of the formula goes below ϑ. Let φ = φ1Udφ2, it follows that

This can be computed by a while loop that increments i, computes �φ2�G, r χ (πi), min0≤j<i�φ1�G, r χ (πj) and their minimum, records the result if it is bigger than the previous maximum, and stops upon reaching a position that has already been visited. This requires storing the current value of min0≤j<i�φ1�G, r χ (πj), the current maximum, and the list of positions already visited, which are at most |V |. The second case is treated as for Boolean until (see Appendix ?? for more details).

Next, the number of nested recursive calls is at most |φ|, so the total space needed is bounded by |φ| times a polynomial in the size of the input, and is thus polynomial.

5.2 Perfect Recall

Our solution to the problem of SL disc [D] model checking for perfect recall applies the automata-theoretic approach [Thomas, 1990; Vardi and Wolper, 1986]. The solution opportunely combines the techniques used for model-checking in [Almagor et al., 2014; Mogavero et al., 2014]. Let us recall relevant definitions from automata theory (see [Kupferman et al., 2000] for details).

Alternating tree automata. An alternating tree automaton (ATA) is a tuple A = ⟨Σ,∆,Q, δ, q0, ℵ⟩, where Σ, ∆, and Q are, respectively, non-empty finite sets of input symbols, directions, and states, q0 ∈ Q is an initial state, ℵ is an acceptance condition, and δ : Q× Σ → B+(∆×Q) is an alternating transition function that maps each pair of states and input symbols to a positive Boolean combination on the set of propositions of the form (d, q) ∈ ∆×Q, called moves.

2 The proof provided in [Cermák et al., 2018] (Thm. 1) considers SL with epistemic operators, but by carefully reading the proof one can notice removing the operators and restricting to perfect information do not affect the complexity results.

A Σ-labeled tree is a pair ⟨T, v⟩ where T is a tree and V : T → Σ maps each node of T to a letter in Σ.

Run. A run of an ATA A = ⟨Σ,∆,Q, δ, q0, ℵ⟩ on a Σlabeled ∆-tree τ = ⟨T, v⟩ is a (∆×Q)-tree R such that for all nodes x ∈ R, where x = ∏ni=1 (di, qi) and y = ∏ni=1 di with n ∈ [0, ω[, it holds that (i) y ∈ T and (ii) there is a set of moves S ⊆ ∆ × Q with S |= δ(qn, v(y)) such that x · (d, q) ∈ R for all (d, q) ∈ S.

Alternating parity tree automata (APT) are alternating tree automata along with a parity acceptance condition [Grädel et al., 2002]. We consider ATAs along with the parity acceptance condition (APT) ℵ = (F1, ..., Fk) ∈ (2Q)+ with F1 ⊆ ... ⊆ Fk = Q. A nondeterministic parity tree automaton (NPT) is a special case of APT in which each conjunction in the transition function δ has exactly one move (d, q) associated with each direction d.

APTAcceptance. AnAPTA = ⟨Σ,∆,Q, δ, q0, ℵ⟩ accepts a Σ-labeled ∆-tree τ if and only if is there exists a run R of A on τ such that all its infinite branches satisfy the acceptance condition ℵ. By L(A) we denote the language accepted by the APT A, that is, the set of trees τ accepted by A. The emptiness problem for A is to decide whether L(A) = ∅.

We reuse the structure of the model-checking approach for SL [Mogavero et al., 2014]. Precisely, given a CGS G, a state v, and an SL-sentence φ, the procedure consists of building an NPT that is non-empty if φ is satisfied in G at state v (Thm 5.8 [Mogavero et al., 2014]). As an intermediate step to obtain the NPT, the construction builds an APT A that accepts a tree encoding of G containing the information on an assignment χ iff the CGS satisfies the formula of interest for χ. The NPT N is obtained by using an APT direction projection with distinguished direction v to the APT A (Thm 5.4 [Mogavero et al., 2014]). The size of the APT A is polynomial in the size of G and exponential in the number k of alternations of strategy quantifiers. Then, building the NPT N and checking its emptiness requires an additional exponent on top of the number of alternations k, which leads to a final complexity (k+1)-EXPTIME-complete (and PTIME in the size of the G). For adapting this procedure to model checking of SL disc [D] with perfect recall, we need to unpack and extend the construction of the APT shown in Lemma 5.6 in [Mogavero et

al., 2014], which we do here in the rest of this section.

We define a translation for each SL disc [D] formula φ to an APT A that recognizes a tree encoding τ of a CGS G, containing the information on the assignment χ iff �ψ�G, R χ (vι) ≥ ϑ.

Defining the appropriate transition function for the A follows the semantics of SL disc [D] in the expected manner. The transitions involving the discounting operators need a careful treatment, as discounting formulas can take infinitely many satisfaction values. As for LTL disc [D] [Almagor et al., 2014], given a threshold ϑ and a computation π, when evaluating a discounted operator on π, one can restrict attention to two cases: either the satisfaction value of the formula goes below ϑ, in which case this happens after a bounded prefix, or the satisfaction value always remains above ϑ, in which case we can replace the discounted operator with a Boolean one.

As for [Mogavero et al., 2014], we use the concept of encoding for a CGS assignment. First, let Valφ :=free(φ)→Ac. Assignment-State Encoding. Let G be a CGS, v ∈ V be a state, and χ be an assignment. Then, the assignmentencoding for χ is the (Valφ × V )-labeled V -tree τ, ⟨T, u⟩, such that T is the set of histories h of G given χ starting in v and u(h) := (f, q), where q is the last state in h and f : free(φ) → Ac is defined by f(s) := χ(s)(h) for each free variable s ∈ free(ψ).

Lemma 1. Let G be a CGS, φ an SL disc [D] formula, and ϑ ∈ [0, 1] be a threshold. Then, there exists an Aφ,ϑ = ⟨Valφ × V, V, Q, δ, q0, ℵ⟩ such that, for all states q ∈ Q, and assignments χ, it holds that �φ�G, R χ (v) > ϑ iff τ ∈ L(Aφ,ϑ), where τ is the assignment-state encoding for χ.

Proof sketch. The construction of the APT Aφ,ϑ is done recursively on the structure of the formula φ. Let xcl(φ) be the extended closure of φ defined analogously to [Almagor et al., 2014]. The state space Q consists of two types of states. Type-1 states are assertions of the form (ψ > t) or (ψ < t), where ψ ∈ xcl(φ) is not an SL formula and t ∈ [0, 1]. Type2 states correspond to SL formulas. The precise definition of xcl(φ), Type 1 and Type 2 states is analogously to [Almagor et al., 2014] and can be found in Appendix ??. Let S be the set of Type-1 and Type-2 states for all ψ ∈ xcl(φ) and thresholds t ∈ [0, 1]. Then, Q is the subset of S constructed on-the-fly according to the transition function defined below.

The transition function δ : (Valφ × V ) → B+(V × Q) is defined as follows. For Type-2 states, the transitions are as in the standard translation from SL to APT [Mogavero et al., 2014]. For the other states, we define the transitions as follows. Let (f, v) ∈ (Valφ × V ) and ⊕ ∈ {<, >}.

• δ((∃sψ) ⊕ t), (f, v)) = ∨c∈Ac δ′ (ψ ⊕ t, (f[s ↦→ c], v)) where δ′ψ is obtained by nondeterminizing the APT Aψ,t, by applying the classic transformation [Muller and Schupp, 1987] which gives the equivalent NPT Nψ,t = ⟨Valψ × V, V, Q′ , δ′ , q′0 , ℵ′ ⟩.
• δ(((s, a)ψ⊕t), (f, v)) = δ′ ((ψ⊕t), (f ′ , v)) where f ′ = f[t ↦→ f(s)] if t ∈ free(ψ), and f ′ = f otherwise.

The remaining cases are a simple adaptation of the proof in [Almagor et al., 2014] (Thm 1) to the input symbols Valφ×V . We provide more details of the proof in Appendix ??.

The initial state of Aφ,ϑ is (φ > ϑ). The accepting states are these of the form (ψ1Uψ2 < t) for Type-1 states, as well as accepting states that arise in the standard translation of Boolean SL to APT for Type-2 states. While the construction as described above is infinite only finitely many states are reachable from the initial state, and we can compute these states in advance.

Using the threshold and the discounting behavior of the discounted-Until, we can restrict attention to a finite resolution of satisfaction values, enabling the construction of a finite automaton. Its size depends on the functions inD. Intuitively, the faster the discounting tends to 0, the fewer states there will be. Thus, the exact complexity of model checking SL disc [D] (which relies on the size of the APT) depends on two aspects. First, the alternation of quantifiers in the formula and, second, the type of discounting functions considered. In the specific setting where D is composed of exponential-discounting functions, (i.e., D ⊆ {d(j) = λj : j ∈ (0, 1) ∩Q}), the overall complexity remains as it is for SL. Exponential discounting functions are perhaps the most common class of discounting functions, as they describe many natural processes (e.g., temperature change and effective interest rate [Shapley, 1953; De Alfaro et al., 2003]).

Theorem 2. Assuming that functions in D are exponentialdiscounting, model checking SL disc [D] with memoryfull agents is (k+1)-EXPTIME and k-EXPSPACE w.r.t the number k of quantifiers alternations in the specification.

Proof sketch. The model checking procedure from [Mogavero et al., 2014] is (k + 1)-EXPTIME-complete and kEXPSPACE w.r.t the number k of quantifiers alternations in the specification. Let ϑ ∈ (0, 1) be a threshold. When discounting by an exponential-discounting function d(j) = λj ∈ D, the number of states in the APT constructed as per Lemma 1 is proportional to the maximal number j such that λj < ϑ, which is polynomial in the description length of ϑ and λ [Almagor et al., 2014].

6 Conclusion and Discussion

In this paper, we proposed Strategy Logic with discounting (SL disc [D]), which contains an operator that captures the idea that the longer it takes to fulfill a requirement, the smaller the satisfaction value is. This work extends the research on temporal and strategic reasoning in Game Theory. As advocated by Pauly and Wooldridge (2003), logics for strategic reasoning can have an important role in the specification and verification of game-theoretical problems and, in particular, related to Automated Mechanism Design (AMD). Indeed, recent works have proposed a new approach for AMD based on model-checking and synthesis from specifications in SL[F] [Maubert et al., 2021; Mittelmann et al., 2022]. Remarkably, SL disc [D] provides less complicated machinery in relation to SL[F], as it is defined over classical concurrent game structures. More importantly, it brings a new dimension for reasoning about mechanisms that take into consideration how events are affected by how long in the future they occur.

There are several interesting directions for future work, including considering synthesis from SL disc [D]-specifications as well as the setting of imperfect information. With SL already, imperfect information yields undecidability, but known tractable fragments exist [Berthon et al., 2021; Belardinelli et al., 2020]. We will investigate them in the case of SL disc [D].

Acknowledgments

We thank the ANR project AGAPE ANR-18-CE23-0013, the PNRR MUR project PE0000013-FAIR, the InDAM project "Strategic Reasoning in Mechanism Design", the PRIN 2020

Project RIPER, and the EU ICT-48 2020 project TAILOR (No. 952215).