ifaamas [AAMAS ’22]Proc. of the 21st International Conference on Autonomous
Agents and Multiagent Systems (AAMAS 2022)May 9–13, 2022 OnlineP. Faliszewski,
V. Mascardi, C. Pelachaud, M.E. Taylor (eds.) 2022 2022 654 Université d’Evry
Évry France University of Luxembourg Esch-sur-Alzette Luxemburg Télécom Paris
Paris France Université de Toulouse - IRIT Toulouse France University of
Naples Federico II Naples Italy Université de Toulouse - IRIT Toulouse France

# Reasoning about Human-Friendly Strategies in Repeated Keyword Auctions

Francesco Belardinelli<EMAIL_ADDRESS>,  Wojtek Jamroga
<EMAIL_ADDRESS>,  Vadim Malvone<EMAIL_ADDRESS>,
Munyque Mittelmann<EMAIL_ADDRESS>,  Aniello Murano
<EMAIL_ADDRESS>and  Laurent Perrussel<EMAIL_ADDRESS>
###### Abstract.

In online advertising, search engines sell ad placements for keywords
continuously through auctions. This problem can be seen as an infinitely
repeated game since the auction is executed whenever a user performs a query
with the keyword. As advertisers may frequently change their bids, the game
will have a large set of equilibria with potentially complex strategies. In
this paper, we propose the use of natural strategies for reasoning in such
setting as they are processable by artificial agents with limited memory
and/or computational power as well as understandable by human users. To reach
this goal, we introduce a quantitative version of Strategy Logic with natural
strategies in the setting of imperfect information. In a first step, we show
how to model strategies for repeated keyword auctions and take advantage of
the model for proving properties evaluating this game. In a second step, we
study the logic in relation to the distinguishing power, expressivity, and
model-checking complexity for strategies with and without recall.

###### Key words and phrases:

Mechanism Design; Auctions; Strategic Reasoning

##  1\. Introduction

In recent years a wealth of logic-based languages have been introduced to
reason about the strategic abilities of autonomous agents in multi-agent
systems (MAS), including Alternating-time Temporal Logic (ATL) Alur et al.,
(2002), Strategy Logic (SL) Mogavero et al., (2014); Chatterjee et al.,
(2010), and Game Logic Pauly and Parikh, (2003), just to name a few. In
conjunction with model checking techniques Baier and Katoen, (2008), these
formal languages have allowed for the development of efficient verification
tools Lomuscio et al., (2015); Gammie and van der Meyden, (2004); Cermák et
al., (2014), which have been successfully applied to the certification of MAS
as different as voting protocols Belardinelli et al., (2017); Jamroga et al.,
(2020), robot swarms Dixon et al., (2012); Kouvaros and Lomuscio, (2015), and
business processes Deutsch et al., (2009); Gonzalez et al., (2015).

Still, verification tools and techniques are comparatively less developed for
data-driven and data-intensive systems111“[Model checking] is mainly
appropriate to control-intensive applications and less suited for data-
intensive applications” (Baier and Katoen,, 2008, p. 15), that is, contexts
where the data content of processes, or agents, is key to model and account
for the evolution of the system Belardinelli et al., (2014); Montali et al.,
(2014). This is the case also for online advertising, where search engines
sell ad placements for keywords continuously through auctions. This problem
can be seen as an infinitely repeated game since the auction is executed
whenever a user performs a query with the keyword. As advertisers may
frequently change their bids, the game will have a large set of equilibria
with potentially complex strategies, thus making the specification and
verification of keyword auctions a complex problem to solve for current model
checking methods222“In principle, the sets of equilibria in such repeated
games can be very large, with players potentially punishing each other for
deviations. The strategies required to support such equilibria are usually
quite complex, however, requiring precise knowledge of the environment and
careful implementation. In theory, advertisers could implement such strategies
via automated robots, but in practice they may not be able to: bidding
software must first be authorized by the search engines, and search engines
are unlikely to permit strategies that would allow advertisers to collude and
substantially reduce revenues.” Edelman et al., (2007).

In this paper, we propose the use of _natural strategies_ Jamroga et al.,
2019a ; Jamroga et al., 2019b  for reasoning about equilibria in keyword
auctions. Strategies in MAS are typically defined as functions from (sequences
of) states to actions. The authors of Jamroga et al., 2019a ; Jamroga et al.,
2019b  argued that such “combinatorial” strategies might be appropriate to
model the strategic abilities of a machine (robot, computer program) with
extensive computational power. However, they do not provide good models of
behaviour for agents with limited memory and computing capacity, such as
humans. As a remedy, they proposed to model “human-friendly” strategies by
lists of condition-action pairs with bounded complexity. This is consistent
with the empirical research on human concept learning Bourne, (1970); Feldman,
(2000) and social norms Santos et al., (2018); Santos, (2018), as well as some
works on usability Nielsen, (1994) and psychology of planning Morris and Ward,
(2014). Natural strategies have been already used to redefine some security
requirements for voting protocols in Jamroga et al., (2020).

In our case, the bidding strategy in an auction should be executable for a
_simple_ artificial agent, as well as reasonably transparent to the human
user, which makes natural strategies a good match. Moreover, natural
strategies provide a way to define complexity (and hence also “simplicity”)
metrics for various functionality, security, and usability properties in MAS.
By focusing on simple strategies, one can make the verification of equilibrium
properties decidable, or even tractable, despite the prohibitive complexity of
the general problem. This is especially evident for strategies with memory,
which normally make the synthesis and model checking problems undecidable Dima
and Tiplea, (2011); Vester, (2013).

Contribution By leveraging on natural strategies, we introduce a quantitative
semantics for SL with natural strategies and imperfect information. As a first
contribution, we show how to represent popular strategies for repeated keyword
auctions in the proposed framework, as well as prove properties pertaining to
this game. Second, we analyse our novel variant of SL in relation with its
distinguishing power, expressivity, and complexity of the model checking
problem, for natural strategies with and without recall.

###  1.1. Related work

Recently, there have been efforts to apply formal methods to the
(semi-)automatic verification of some decision-making mechanisms, including
auctions and voting protocols. A number of works Caminati et al., (2015);
Barthe et al., (2016); Kerber et al., (2016) expresses these mechanisms in
high-level specification languages. However, in contrast with standard model
checking techniques Baier and Katoen, (2008), their verification is not fully
automated, but only assisted by a reasoner. Troquard et al., (2011) introduce
a framework for fully-automated verification of voting protocols. Still, their
approach can only model one-shot mechanisms and thus does not capture multi-
stage protocols and repeated auctions. In preliminary works, Pauly and
Wooldridge, (2003) and Wooldridge et al., (2007) advocate the use of ATL Alur
et al., (2002) to reason about decision-making mechanisms. As ATL lacks the
expressivity to reason about quantitative aspects such as valuations and
payments, and solution concepts such as equilibria, Maubert et al., (2021)
introduce ${\textnormal{{SLK}}}{[\mathcal{F}]}$, a quantitative and epistemic
version of SL Chatterjee et al., (2010); Mogavero et al., (2014), and show how
it can be used for reasoning about notions such as Nash equilibrium and
strategyproofness. Still, their approach considers strategies as functions
from states to actions and cannot handle strategies with recall.

A key assumption of the present contribution is that agents have only partial
observability of the global state of the system, as it is often the case in
real-life applications. Contexts of imperfect information have been
extensively considered in the literature on formal verification Dima and
Tiplea, (2011); Kupferman and Vardi, (2000); Jamroga and Ågotnes, (2007);
Reif, (1984); Bulling and Jamroga, (2014). Generally speaking, imperfect
information immediately entails higher complexity of game solving. In multi-
player games, the complexity can go up to being non-elementary Pnueli and
Rosner, (1989), or even undecidability when considered in the context of
memoryful strategies Dima and Tiplea, (2011). Hence, it is of interest to
analyse imperfect information systems where agents have finite or bounded
memory, in order to retrieve a decidable model checking problem. Works that
are closest in spirit to our contribution concern modeling, specification, and
reasoning about strategies of bounded-memory agents. We directly build on the
research by Jamroga, Malvone, and Murano on natural strategies Jamroga et al.,
2019a ; Jamroga et al., 2019b . We generalize the approach by considering
quantitative semantics for both natural strategies and the logic, which is
more suitable for reasoning about mechanisms with monetary transfer (e.g.,
auctions). We also consider SL instead of ATL, due to its expressive power. In
a related vein, Ågotnes and Walther, (2009) investigate strategic abilities of
agents with bounded memory, while Belardinelli et al., (2018) consider bounded
memory as an approximation of perfect recall. On a related direction, temporal
and strategic logics have been extended to handle agents with bounded
resources Alechina et al., (2009, 2010); Bulling and Farwer, 2010a ; Bulling
and Farwer, 2010b . Issues related to bounded rationality are also
investigated in Barlo et al., (2008); Hörner and Olszewski, (2009); Gupta et
al., (2015).

Also relevant for the present contribution are papers that study explicit
representations of strategies. This category is much richer and includes
extensions of $\textnormal{{ATL}}^{*}$ with explicit reasoning about actions
and strategies van der Hoek et al., (2005); Ågotnes, (2006); Walther et al.,
(2007); Herzig et al., (2014), as well as logics that combine features of
temporal and dynamic logic Harel and Kozen, (1982); Novák and Jamroga, (2009).
Duijf and Broersen, (2016) present a variant of STIT logic, that enables
reasoning about strategies and their performance in the object language. Also,
plans in agent-oriented programming are in fact rule-based descriptions of
strategies. In particular, reasoning about agent programs using strategic
logics was investigated in Bordini et al., (2006); Alechina et al., (2007,
2008); Dastani and Jamroga, (2010); Yadav and Sardiña, (2012).

Outline In Sec. 2, we recall basic definitions. In Sec. 3, we define Natural
Strategy Logic, denoted ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$. In Sec. 4
we focus on the problem of repeated keyword auctions. In Sec. 5, we
investigate the expressivity and distinguishing power of
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$. Sec. 6 establishes the complexity
of model checking, and Sec. 7 concludes the paper.

##  2\. Preliminaries

We first recall basic notions. For the remainder of the paper, we fix a set of
atomic propositions AP, a set of agents Ag and a set of strategy variables
Var. We let $\mathsf{n}$ be the number of agents in Ag. Finally, let
$\mathcal{F}\subseteq\\{f\colon[-1,1]^{m}\to[-1,1]\mid m\in\mathbb{N}\\}$ be a
set of functions over $[-1,1]$ of possibly different arities.

###  2.1. Weighted Concurrent Game Structures

The semantics of natural strategies and
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ are interpreted over weighted
concurrent game structures (wCGS ). A difference from classical structures is
that the labelling of atomic propositions is replaced by a weight function. We
consider weighted propositions for easily handling quantitative aspects (such
as prices).

######  Definition 0.

A _weighted concurrent game structure with imperfect information_ (wCGS ) is a
tuple
$\mathcal{G}=(\textnormal{Ac},V,L,\delta,\ell,V_{\iota},\\{\sim_{a}\\}_{a\in\textnormal{Ag}})$
where: (i) Ac is a finite set of _actions_ ; (ii) $V$ is a finite set of
_states_ ; (iii) $L:\textnormal{Ag}\times V\to 2^{\textnormal{Ac}}$ is a
_legality function_ , defining the availability of actions; (iv) $\delta$ is a
transition function assigning a successor state
$v^{\prime}=\delta(v,(c_{a})_{a\in\textnormal{Ag}})$ to each state $v\in V$
and any tuple of actions $(c_{a})_{a\in\textnormal{Ag}}$, where $c_{a}\in
L(a,v)$; (v) $\ell:V\times\textnormal{AP}\to[-1,1]$ is a _weight function_ ;
(vi) $V_{\iota}\subseteq V$ is a set of _initial states_ ; and (vii)
$\sim_{a}\;\subseteq V\times V$ is an equivalence relation called the
_observation relation_ of agent $a$.

We require that the wCGS is uniform, that is $v\sim_{a}v^{\prime}$ implies
$L(a,v)=L(a,v^{\prime})$. We write $\bm{o}$ for a tuple of objects
$(o_{a})_{a\in\textnormal{Ag}}$, one for each agent, and such tuples are
called _profiles_. Given a profile $\bm{o}$ and $a\in\textnormal{Ag}$, we let
$o_{a}$ be agent $a$’s component, and $o_{-a}$ is
$(o_{i})_{i\in\textnormal{Ag}\setminus\\{a\\}}$. Similarly, we let
$\textnormal{Ag}_{-a}=\textnormal{Ag}\setminus\\{a\\}$.

In a state $v\in V$, each player $a$ chooses an available action $c_{a}\in
L(a,v)$, and the game proceeds to state $\delta(v,\bm{c})$ where $\bm{c}$ is
the _action profile_ $(c_{a})_{a\in\textnormal{Ag}}$. A _play_
$\pi=v_{0}v_{1}v_{2}...$ is an infinite sequence of states such that for every
$i\geq 0$ there exists an action profile $\bm{c}$ such that
$\delta(v_{i},\bm{c})=v_{i+1}$. We write $\pi_{i}=v_{i}$ for the state at
index $i$ in play $\pi$. A history $h=v_{0}v_{1}v_{2}...v_{n}$ is a finite
sequence of states. The last element of a history is denoted by
$last(h)=v_{n}$. $H_{\mathcal{G}}$ denotes the set of all histories in the
wCGS $\mathcal{G}$.

###  2.2. Natural Strategies

In this section we recall the notion of uniform natural strategies from
Jamroga et al., 2019b . Natural strategies are conditional plans, represented
through an ordered list of condition-action rules Jamroga et al., 2019b . The
intuition is that the first rule whose condition holds in the history of the
game is selected, and the corresponding action is executed. As we are
considering the setting of imperfect information, the conditions are regular
expressions over weighted epistemic (WE) formulas. Given an agent $a$, the WE
formulas over AP, denoted ${\mathit{WE}}(\textnormal{AP})$, are conditions on
$a$’s knowledge and are expressed by the following Backus-Naur Form grammar:

$\psi::=\top\mid K_{a}\varphi\mid f(\psi,...,\psi)$ $\varphi::=p\mid
f(\varphi,...,\varphi)\mid K_{i}\varphi$

where $f\in\mathcal{F}$ is a function, $p\in\textnormal{AP}$ is an atomic
proposition and $i\in\textnormal{Ag}$ is an agent.

Given a wCGS $\mathcal{G}$, a state $v\in V$ and a
${\mathit{WE}}(\textnormal{AP})$ formula $\varphi$, we inductively define the
satisfaction value of $\varphi$ in $v$, denoted
$\llbracket\varphi\rrbracket(v)$:

$\displaystyle\llbracket p\rrbracket(v)$ $\displaystyle=\ell(v,p)$
$\displaystyle\llbracket K_{a}\varphi\rrbracket(v)$
$\displaystyle=\min_{v^{\prime}\sim_{a}v}\llbracket\varphi\rrbracket(v^{\prime})$
$\displaystyle\llbracket f(\varphi_{1},\\!...,\varphi_{m})\rrbracket(v)$
$\displaystyle=f(\llbracket\varphi_{1}\rrbracket(v),...,\llbracket\varphi_{m}\rrbracket(v))$

The semantics for the knowledge modality is the standard in the literature on
fuzzy epistemic logic (e.g. Maruyama, (2021)). Let
$Reg({\mathit{WE}}(\textnormal{AP}))$ be the set of regular expressions over
the weighted epistemic conditions ${\mathit{WE}}(\textnormal{AP})$, defined
with the constructors $\cdot,\cup,\text{*}$ representing concatenation,
nondeterministic choice, and finite iteration, respectively. Given a regular
expression $r$ and the language $\mathcal{L}(r)$ on words generated by $r$, a
history $h$ is consistent with $r$ iff there exists $b\in\mathcal{L}(r)$ such
that $|h|=|b|$ and $\llbracket b[i]\rrbracket(h[i])=1$, for all $0\leq
i\leq|h|$. Intuitively, a history $h$ is consistent with a regular expression
$r$ if the $i$-th weighted epistemic condition in $r$ “holds” in the $i$-th
state of $h$ (for any position $i$ in $h$).

A uniform natural strategy with recall $\sigma_{a}$ for agent $a$ is a
sequence of pairs $(r,c)$, where $r\in Reg({\mathit{WE}}(\textnormal{AP}))$ is
a regular expression, and $c$ is an action available in $\mbox{last}(h)$, for
all histories $h\in H_{\mathcal{G}}$ consistent with $r$. The last pair on the
sequence is required to be $(\top\text{*},c)$, with $c\in L(a,v)$ for every
$v\in V$ and some $c\in\textnormal{Ac}$.

A uniform memoryless natural strategy is a special case of natural strategy in
which each condition is a weighted epistemic formula (i.e., no regular
operators are allowed).

Natural strategies are uniform in the sense they specify the same actions in
indistinguishable states (see Jamroga et al., 2019b ). We define
$\mbox{\emph{Str}}_{a}^{\rho}$ to be the set of uniform natural strategies for
agent $a$ and
$\mbox{\emph{Str}}^{\rho}=\cup_{a\in\textnormal{Ag}}\mbox{\emph{Str}}_{a}^{\rho}$,
where $\rho\in\\{ir,iR\\}$333As usual in the verification process, we denote
imperfect recall with r, perfect recall with R, imperfect information with i,
and perfect information with I.. Let $size(\sigma_{a})$ denote the number of
guarded actions in $\sigma_{a}$, $cond_{i}(\sigma_{a})$ be the $i$-th guarded
condition on $\sigma_{a}$, $cond_{i}(\sigma_{a})[j]$ be the $j$-th WE formula
of the guarded condition $\sigma_{a}$, and $act_{i}(\sigma_{a})$ be the
corresponding action. Finally, $match(h,\sigma_{a})$ is the smallest index
$i\leq size(\sigma_{a})$ such that for all $0\leq j\leq|last(h)|$, $\llbracket
cond_{i}(\sigma_{a})[j]\rrbracket(h[j])=1$444Note that, we considered the case
in which the condition have the same length of the history. There is also the
case in which the condition is shorter than the history. This is due to the
usage of the finite iteration operator. In the latter case, we need to check a
finite number of times the same weighted epistemic formula in different states
of the history. For more details on this aspect see Jamroga et al., 2019a ;
Jamroga et al., 2019b . and $act_{i}(\sigma_{a})\in L(a,last(h))$. In other
words, $match(h,\sigma_{a})$ matches the state $last(h)$ with the first
condition in $\sigma_{a}$ that holds in $h$, and action available in
$last(h)$.

Measurement of Natural Strategies. The complexity of the strategy $\sigma$ is
the total size of its representation and is denoted as follows:
$compl(\sigma):=\sum_{(r,c)\in\sigma}|r|$, where $|r|$ is the number of
symbols in $r$, except by parentheses. If $r$ is a $n$-ary function in
$\mathcal{F}$, then $|r|=n+1$.

##  3\. Natural Strategy Logic

${\textnormal{{SL}}}{[\mathcal{F}]}$ Bouyer et al., (2019) proposes a
quantitative semantics for Strategy Logic, in which strategies are functions
mapping histories to actions. For reasoning about intuitive and simple
strategies, we introduce ${\textnormal{{SL}}}{[\mathcal{F}]}$ with natural
strategies and imperfect information, denoted
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$. Throughout this section, let
$\rho\in\\{ir,iR\\}$ denote whether the semantics considers memoryless or
recall strategies.

An _assignment_
$\chi:\textnormal{Ag}\cup\textnormal{Var}\to\mbox{\emph{Str}}^{\rho}$ is a
function from players and variables to strategies. For an assignment $\chi$,
an agent $a$ and a strategy $\sigma$ for $a$, $\chi[a\mapsto\sigma]$ is the
assignment that maps $a$ to $\sigma$ and is otherwise equal to $\chi$, and
$\chi[s\mapsto\sigma]$ is defined similarly, where $s$ is a variable. For an
assignment $\chi$ and a state $v$ we let $\textnormal{Out}(\chi,v)$ be the
unique play that starts in $v$ and follows the strategies assigned by $\chi$.
Formally, $\textnormal{Out}(\chi,v)$ is the play $v_{0}v_{1}...$ such that
$v_{0}=v$ and for all $i\geq 0$, $v_{i+1}=\delta(v_{i},\bm{c})$ where for all
$a\in\textnormal{Ag}$, $\bm{c}_{a}=act_{match(v_{i},\chi(a))}(\chi(a))$.

###  3.1. ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ Syntax

######  Definition 0.

The syntax of ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ is defined as follows:

$\displaystyle\varphi::=p\mid\exists s_{a}^{\leq
k}.\,\varphi\mid(a,s_{a})\varphi\mid f(\varphi,...,\varphi)\mid{\bf
X}\varphi\mid\varphi{\bf U}\varphi$

where $p\in\textnormal{AP}$, $s_{a}\in\textnormal{Var}\ \cup\
\mbox{\emph{Str}}^{\rho}_{a}$, $a\in\textnormal{Ag}$, and $f\in\mathcal{F}$.

The intuitive reading of the operators is as follows: $\exists s_{a}^{\leq
k}.\,\varphi$ means that there exists a strategy with complexity less or equal
than $k$ for agent $a$ such that $\varphi$ holds; $(a,s_{a})\varphi$ means
that when strategy $s_{a}$ is assigned to agent $a$, $\varphi$ holds; ${\bf
X}$ and ${\bf U}$ are the usual temporal operators “next” and “until”. The
meaning of $f(\varphi_{1},...,\varphi_{n})$ depends on the function $f$. We
use $\top$, $\vee$, and $\neg$ to denote, respectively, function $1$, function
$x,y\mapsto\max(x,y)$ and function $x\mapsto-x$.

A variable is _free_ in formula $\varphi$ if it is bound to an agent without
being quantified upon, and an agent $a$ is free in $\varphi$ if $\varphi$
contains a temporal operator (${\bf X}$ or ${\bf U}$) that is not in the scope
of any binding for $a$. The set of free variables and agents in $\varphi$ is
written $\text{free}(\varphi)$, and a formula $\varphi$ is a _sentence_ if
$\text{free}(\varphi)=\emptyset$. The strategy quantifier $\exists s_{a}^{\leq
k}.\,\varphi$ quantifies on strategies _for agent $a$_.

###  3.2. ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ Semantics

######  Definition 0.

Let
$\mathcal{G}=(\textnormal{Ac},V,\delta,\ell,V_{\iota},\\{\sim_{a}\\}_{a\in\textnormal{Ag}})$
be a wCGS , and $\chi$ an assignment. The satisfaction value
$\llbracket\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)\in[-1,1]$ of a
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ formula $\varphi$ in a state $v$ is
defined as follows, where $\pi$ denotes $\textnormal{Out}(v,\chi)$:

$\displaystyle\llbracket p\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=\ell(v,p)$ $\displaystyle\llbracket\exists s_{a}^{\leq
k}.\,\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=\max_{\sigma\in\\{\alpha\in\mbox{\emph{Str}}_{a}^{\rho}:compl(\alpha)\leq
k\\}}\llbracket\varphi\rrbracket^{\mathcal{G},\rho}_{\chi[s_{a}\mapsto\sigma]}(v)$
$\displaystyle\llbracket(a,s_{a})\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=\llbracket\varphi\rrbracket^{\mathcal{G},\rho}_{\chi[a\mapsto\chi(s_{a})]}(v)\text{
if }s_{a}\in\textnormal{Var}$
$\displaystyle\llbracket(a,\sigma_{a})\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=\llbracket\varphi\rrbracket^{\mathcal{G},\rho}_{\chi[a\mapsto\sigma_{a}]}(v)\text{
if }\sigma_{a}\not\in\textnormal{Var}$ $\displaystyle\llbracket
f(\varphi_{1},\\!...,\varphi_{m})\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=f(\llbracket\varphi_{1}\rrbracket^{\mathcal{G},\rho}_{\chi}(v),...,\llbracket\varphi_{m}\rrbracket^{\mathcal{G},\rho}_{\chi}(v))$
$\displaystyle\llbracket{\bf X}\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=\llbracket\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{1})$
$\displaystyle\llbracket\varphi_{1}{\bf
U}\varphi_{2}\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=\sup_{i\geq
0}\min\Big{(}\llbracket\varphi_{2}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{i}),\\!\min_{0\leq
j<i}\llbracket\varphi_{1}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{j})\Big{)}$

If $\varphi$ is a sentence, its satisfaction value does not depend on the
assignment, and we write $\llbracket\varphi\rrbracket^{\mathcal{G},\rho}(v)$
for $\llbracket\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$ where $\chi$ is
any assignment. We also let
$\llbracket\varphi\rrbracket^{\mathcal{G},\rho}=\min_{v_{\iota}\in
V_{\iota}}\llbracket\varphi\rrbracket^{\mathcal{G},\rho}(v_{\iota})$.

######  Remark 0.

When propositions only take values in $\\{-1,1\\}$ and
$\mathcal{F}=\\{\top,\lor,\neg\\}$, ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$
corresponds to a Boolean-valuated extension of SL with Natural Strategies.

We define the classic abbreviations: ${\perp:=\neg\top}$,
${\varphi\rightarrow\varphi^{\prime}:=\neg\varphi\vee\varphi^{\prime}}$,
${\varphi\wedge\varphi^{\prime}:=\neg(\neg\varphi\vee\neg\varphi^{\prime})}$,
${{\bf F}\psi:=\top{\bf U}\psi}$, ${{\bf G}\psi:=\neg{\bf F}\neg\psi}$ and
$\forall s^{\leq k}.\,\varphi:=$ $\neg\exists s^{\leq k}.\,\neg\varphi$, and
check that they correspond to the intuition. For instance, $\wedge$
corresponds to $\min$, ${\bf F}\psi$ computes the supremum of the satisfaction
value of $\psi$ over all future points in time, ${\bf G}\psi$ computes the
infimum of these values, and $\forall s^{\leq k}.\,\varphi$ minimizes the
value of $\varphi$ over all possible strategies $s$.

##  4\. Repeated Keyword Auctions

Modeling mechanisms with monetary transfer and private valuations require
handling quantitative features and imperfect information. Memoryless
strategies are enough for mechanisms in which all relevant information is
encoded in the current state (e.g. English auction). In repeated auctions,
agents may, as well, use information from the previous states for choosing
their strategies.

We now focus on using ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ to model and
verify repeated keyword auctions and related strategies. Repeated keyword
auctions are used by online search engines for selling advertising slots when
users perform a search with a keyword Cary et al., (2007). For a keyword of
interest, the advertisers (bidders) submit a bid stating the maximum amount
she is willing to pay for a click on her sponsored link. When a user submits a
query, an auction is run to determinate the slot allocation among the
advertisers bidding on the keyword of interest. The most common mechanism for
keyword auctions is the Generalized Second Price (GSP) Cary et al., (2007), in
which the agents are allocated slots in decreasing order of bids and the
payment for the slot $s$ is the bid of the agent allocated to the slot $s+1$.

We assume that $\mathcal{F}$ contains the function $\leq\,:(x,y)\mapsto 1$ if
$x\leq y$ and $\leq\,:(x,y)\mapsto-1$ otherwise; and for readability we use
the infix notation $x\leq y$ in the formula. We also assume that $\mathcal{F}$
contains the equality $=$ and comparison functions $<$, $>$, $\geq$ (defined
similarly). Finally, we assume $\mathcal{F}$ contains functions $-$, $\sum$,
$\times$, $\backslash$, $min$, $max$ and $argmax$ with the standard meaning
(for details, see Maubert et al., (2021)).

Let us fix a price increment $\mathsf{inc}\in(0,1]$, a set of slots
$S=\\{1,...,\mathsf{m}\\}$, where $\mathsf{m}\in\mathbb{N}\setminus\\{0\\}$.
Each slot has a click-through rate $\theta_{1}>...>\theta_{\mathsf{m}}$, where
$\theta_{s}\in[0,1]$ is the probability that the user will click on the
advertisement in slot $s$. The agents in Ag are the advertisers, each one
having a private valuation ${\mathsf{v}}_{a}\in{\mathsf{V}}_{a}$ for a click,
where ${\mathsf{V}}_{a}\subset[0,1]$ is a finite set of possible valuations.
We assume the valuations are distinct, that is, if $a\neq a^{\prime}$, then
${\mathsf{v}}_{a}\neq{\mathsf{v}}_{a^{\prime}}$. We denote by $\prec$ an
arbitrary order among the agents in Ag, used in case of ties. The atomic
propositional set is
$\textnormal{AP}=\\{\text{all}_{a,s},\text{p}_{s},\vartheta_{a}:a\in\textnormal{Ag},s\in
S\\}$, where $\text{all}_{a,s}$ represents whether agent $a$ is allocated to
slot $s$, $\text{p}_{s}$ denotes the price of slot $s$ and $\vartheta_{a}$
denotes $a$’s valuation. Define
$\mathcal{G}_{GSP}=(\textnormal{Ac},V,L,\delta,\ell,V_{\iota},\\{\sim_{a}\\}_{a\in\textnormal{Ag}})$,
where:

  * •

$\textnormal{Ac}=\\{0+x\times\mathsf{inc}:0\leq
x\leq\frac{1}{\mathsf{inc}}\\}$, where $b\in\textnormal{Ac}$ denotes a bid
with price $b$ for a click; given $\bm{c}=(c_{a})_{a\in\textnormal{Ag}}$, let
$rank_{\bm{c}}=(a_{1},...,a_{\mathsf{n}})$ be the sequence of distinct agents
in Ag ordered by their bid, that is, $i<j$ if $c_{a_{i}}>c_{a_{j}}$ or
$c_{a_{i}}=c_{a_{j}}$ and $a_{i}\prec a_{j}$ for
$i,j\in\\{1,...,\mathsf{n}\\}$ with $i\neq j$. In case of draws, the sequence
is determined with respect to $\prec$. We let $rank_{\bm{c}}(i)$ denote the
agent in the $i$-th position of the sequence $rank_{\bm{c}}$.

  * •

$V=\\{\langle al_{1},\allowbreak...,\allowbreak al_{\mathsf{m}},\allowbreak
pr_{1},\allowbreak...,\allowbreak
pr_{\mathsf{m}},\allowbreak(vl_{a})_{a\in\textnormal{Ag}}\rangle:al_{s}\in\textnormal{Ag}\cup\\{none\\}$
& $pr_{s}\in\textnormal{Ac}$ & $vl_{a}\in{\mathsf{V}}_{a}$ &
$a\in\textnormal{Ag}$ & $1\leq s\leq\mathsf{m}\\}$, where each state
represents the current slot allocation and prices, with $al_{s}$, $pr_{s}$,
and $vl_{a}$ denoting the winner of slot $s$, the price per click of $s$ and
$a$’s valuation, resp.;

  * •

For each $a\in\textnormal{Ag}$ and $v\in V$, $L(a,v)=\textnormal{Ac}$;

  * •

For each $v\in V$ and $\bm{c}=(c_{a})_{a\in\textnormal{Ag}}$ such that
$c_{a}\in L(a,v)$, the transition function uses the agent’s bids to chose the
next allocations and prices and is defined as follows:
$\delta(v,(c_{a})_{a\in\textnormal{Ag}})=\langle
al_{1}^{\prime},\allowbreak...,\allowbreak
al_{\mathsf{m}}^{\prime},\allowbreak
pr_{1}^{\prime},\allowbreak...,\allowbreak
pr_{\mathsf{m}}^{\prime},\allowbreak(vl_{a})_{a\in\textnormal{Ag}}\rangle$,
where for each agent $a$ and slot $s$, (i) $al_{s}=rank_{\bm{c}}(s)$ if
$s\leq\mathsf{n}$, and $al_{s}=none$ otherwise; (ii)
$pr_{s}=c_{rank_{\bm{c}}(s+1)}$ if $s+1\leq\mathsf{n}$, and $pr_{s}=0$
otherwise.

  * •

For each agent $a$, slot $s\in S$ and state $v=\langle
al_{1},\allowbreak...,\allowbreak al_{\mathsf{m}},\allowbreak
pr_{1},\allowbreak...,\allowbreak
pr_{\mathsf{m}},\allowbreak(vl_{a})_{a\in\textnormal{Ag}}\rangle$, the weight
function is defined as follows: (i) $\ell(v,\text{all}_{a,s})=1$ if
$al_{s}=a$, and $\ell(v,\text{all}_{a,s})=0$ otherwise; (ii)
$\ell(v,\text{p}_{s})=pr_{s}$; and (iii) $\ell(v,\vartheta_{a})=vl_{a}$.

  * •

In an initial state, the prices are 0 and the slots are allocated to $none$,
that is, $V_{\iota}=\\{\langle none,\allowbreak...,\allowbreak
none,\allowbreak 0,\allowbreak...,\allowbreak 0,\allowbreak
vl_{1},\allowbreak...,\allowbreak vl_{\mathsf{n}}\rangle\in V\\}$;

  * •

For each agent $a$ and two states $v=\langle al_{1},\allowbreak...,\allowbreak
al_{\mathsf{m}},\allowbreak pr_{1},\allowbreak...,\allowbreak
pr_{\mathsf{m}},\allowbreak(vl_{a})_{a\in\textnormal{Ag}}\rangle$ and
$v^{\prime}=\langle al_{1}^{\prime},\allowbreak...,\allowbreak
al_{\mathsf{m}}^{\prime},\allowbreak
pr_{1}^{\prime},\allowbreak...,\allowbreak
pr_{\mathsf{m}}^{\prime},\allowbreak(vl_{a}^{\prime})_{a\in\textnormal{Ag}}\rangle$
in $V$, the observation relation $\sim_{a}$ is such that if
$v\sim_{a}v^{\prime}$ then (i) $al_{s}=al_{s^{\prime}}$, for each $1\leq
s\leq\mathsf{m}$; (ii) $p_{s}=p_{s^{\prime}}$, for each $1\leq
s\leq\mathsf{m}$; (iii) $vl_{a}=vl_{a}^{\prime}$.

Notice there is exactly one initial state for each possible valuation profile
in $(\prod_{a\in\textnormal{Ag}}{\mathsf{V}}_{a})$. Additionally, valuations
remain unchanged after the initial state. We use the formula
$s^{-1}:=1\backslash s$ when it is convenient to obtain a value in $[-1,1]$
for representing a slot $s$. The utility of agent $a$ when she is assigned to
slot $s$ is denoted by the formula
$\text{ut}_{a,s}:=\theta_{s}\times(\vartheta_{a}-\text{p}_{s})$. The expected
utility for agent $a$ depends on her actual allocation, that is,
$\text{ut}_{a}:=\sum_{s\in S}\text{all}_{a,s}\times\text{ut}_{a,s}$.

###  4.1. Solution concepts for $\mathcal{G}_{GSP}$

In this section, we show how ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ can be
used for the verification of mechanisms with natural strategies. In sight of
our motivating example, we aim at rephrasing conditions and properties usually
considered in the analysis of keyword auctions Cary et al., (2007); Edelman et
al., (2007); Varian, (2007).

Nash equilibrium Since auctions are noncooperative, the solution concept in
the pure strategy setting usually considered is the Nash equilibrium (NE). The
NE captures the notion of stable solution: a strategy profile is NE if no
player can improve her utility through an unilateral change of strategy
Roughgarden, (2010). With ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$, we
restrict the range of strategies to simple ones, as it enables us to reason
about artificial agents with limited capabilities and human-friendly
strategies. Let $\bm{\sigma}=(\sigma_{a})_{a\in\textnormal{Ag}}$ be a profile
of strategies and $k>0$ and define the formula

$\displaystyle\text{N}\text{E}(\bm{\sigma},k):=\bigwedge_{a\in\textnormal{Ag}}\forall
t^{\leq k}.\,\big{[}(\textnormal{Ag}_{-a},\sigma_{-a})$
$\displaystyle(a,t){\bf X}\text{ut}_{a}\leq(\textnormal{Ag},\bm{\sigma}){\bf
X}\text{ut}_{a}\big{]}$

The formula $\text{N}\text{E}(\bm{\sigma},k)$ means that, for every agent and
alternative strategy $t$ of complexity at most $k$, binding to $t$ when
everyone else binds to their strategies in $\bm{\sigma}$ leads to at most the
same utility as when she also binds to her strategy in $\bm{\sigma}$. In
relation to strategies with complexity at most $k$, the strategy profile
$\bm{\sigma}$ leads to a NE in the next state of $v$ if
$\llbracket\text{N}\text{E}(\bm{\sigma},k)\rrbracket^{\mathcal{G},\rho}_{\chi}(v)=1$.

Predicting outcomes of a keyword auction is a difficult task given the
infinite nature of NE continuum Yuan et al., (2017). For this reason, refined
solution concepts have been proposed to reduce the NE continuum to subsets.
Edelman et al.  Edelman et al., (2007) studied the subset called locally envy-
free equilibrium (LEFE), in which no advertiser can improve her utility by
exchanging her current slot to the one ranked one position above, given the
current prices.

Locally envy free equilibrium Let
$\bm{\sigma}=(\sigma_{a})_{a\in\textnormal{Ag}}$ be a profile of strategies,
we define the formula

$\displaystyle\text{LEF}\text{E}(\bm{\sigma}):=\bigwedge_{a\in\textnormal{Ag}}(\textnormal{Ag},\bm{\sigma}){\bf
X}\big{[}\text{LEF}_{wins}^{a}\land\text{LEF}_{loses}^{a}]$

where
$\text{LEF}_{wins}^{a}:=\bigwedge_{1<s\leq\mathsf{m}}(\text{all}_{a,s}=1\to\text{ut}_{a,s}\geq\text{ut}_{a,s-1})$
indicates that when an agent is allocated to a slot, she does not prefer to
switch to the slot right above and $\text{LEF}_{loses}^{a}:=(\bigwedge_{s\in
S}\text{all}_{a,s}=0)\to 0\geq\text{ut}_{a,\mathsf{m}}$ denotes that agents
who were not assigned to any slot do not prefer to get the last slot.

$\text{LEF}\text{E}(\bm{\sigma})$ means that, for any agent, when everyone
follows the strategies in $\bm{\sigma}$, it holds that (i) if she wins $s$,
her utility for $s$ is greater than for slot $s-1$ (at current prices) and
(ii) if she does not get any slot, then her utility for the last slot is at
most zero. Strategy profile $\bm{\sigma}$ leads to LEFE in the next state of
$v$ if
$\llbracket\text{LEF}\text{E}(\bm{\sigma})\rrbracket^{\mathcal{G},\rho}_{\chi}(v)=1$.
Based on Edelman et al., (2007); Varian, (2007), we have that any LEFE is also
a NE:

######  Proposition 0.

For any complexity $k\geq 0$, state $v\in V$, $\rho\in\\{iR,ir\\}$ and
strategy profile $\bm{\sigma}=(\sigma_{a})_{a\in\textnormal{Ag}}$ with
$\sigma_{a}\in\mbox{\emph{Str}}^{\rho}_{a}$ for each agent
$a\in\textnormal{Ag}$,
$\llbracket\text{LEF}\text{E}(\bm{\sigma})\to\text{N}\text{E}(\bm{\sigma},k)\rrbracket^{\mathcal{G}_{GSP},\rho}(v)=1$.

###### Proof sketch.

Let $\chi$ be an assignment, $k\geq 0$ be a complexity bound for strategies,
$v\in V$ be a state, $\rho\in\\{iR,ir\\}$, and
$\bm{\sigma}=(\sigma_{a})_{a\in\textnormal{Ag}}$ be a profile of
$\rho$-strategies. Assume
$\llbracket\text{LEF}\text{E}(\bm{\sigma})\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v)=1$.
Let $v_{\bm{\sigma}}=\delta(v,\bm{b})$ where
$\bm{b}=(b_{i})_{i\in\textnormal{Ag}}$ and $b_{i}=act_{match(v,\sigma_{i})}$
denotes the action performed by $i$ in $v$ if she follows $\sigma_{i}$. By
definition, $\ell(v_{\bm{\sigma}},\text{all}_{i,s})=1$ iff
$i=rank_{\bm{b}}(s)$ is the winner of slot $s$ and her payment is
$\ell(v_{\bm{\sigma}},\text{p}_{s})=b_{rank_{\bm{b}}}(s+1)$. For each slot
$s\in\\{1,...,min(\mathsf{m},\mathsf{n})\\}$, we consider whether its winner
$a=rank_{\bm{b}}(s)$ could improve her utility by deviating to strategy
$t\in\\{\alpha\in\mbox{\emph{Str}}_{a}^{\rho}:compl_{\rho}(\alpha)\leq k\\}$.
The case for agents who were not assigned any slot is proved similarly. Denote
by $\bar{b}=match(v,t)\in\textnormal{Ac}$ the action that $a$ would take if
she followed $t$ and $v_{(\sigma_{-a},t)}=\delta(v,(b_{-a},\bar{b}))$ the next
reached state from $v$ when she follows $t$ and others play according to
$\sigma$.

If $s=1$, any $\bar{b}\geq\ell(v_{\bm{\sigma}},\text{p}_{s})$ does not change
the outcome of the auction and
$\llbracket(\textnormal{Ag}_{-a},\sigma_{-a}^{\rho})(a,t){\bf
X}\text{ut}_{a}=(\textnormal{Ag},\bm{\sigma}){\bf
X}\text{ut}_{a}\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v)=1$. The same
holds when $1<s<m$ for
$\bar{b}\in[\ell(v_{\bm{\sigma}},\text{p}_{s}),\ell(v_{\bm{\sigma}},\text{p}_{s-1})]$
and when $s=\mathsf{m}$ for
$\bar{b}\leq\ell(v_{\bm{\sigma}},\text{p}_{\mathsf{m}})$. In the remaining
cases, $a$ would change her position in $rank_{\bm{b}}$ with other agent. By
the results of Edelman et al., (2007) (see Lemma 1), the outcome given by bids
$\bm{b}$ is a stable assignment, that is, no advertiser can profitably rematch
by changing her position with any other advertiser. Thus,
$\llbracket(\textnormal{Ag}_{-a},\sigma_{-a})(a,t){\bf
X}\text{ut}_{a}\leq(\textnormal{Ag},\bm{\sigma}){\bf
X}\text{ut}_{a}\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v)=1$. ∎

As LEFE is still an equilibrium continuum, Edelman et al.  Edelman et al.,
(2007) characterize an equilibrium in which the slot allocation and payments
coincide with the ones in the dominant-strategy equilibrium (DSE) of the
Vickrey–Clarke–Groves (VCG) mechanism.

Let $\bm{{\mathsf{v}}}=({\mathsf{v}}_{a})_{a\in\textnormal{Ag}}$ be a
valuation profile. Truthfully reporting $\bm{{\mathsf{v}}}$ is the DSE of VCG
Roughgarden, (2010). For each slot $s$ and agent $a$, the allocation rule for
VCG in the keyword auction is the same as under GSP Edelman et al., (2007):
$\text{all}^{*}_{a,s}(\bm{{\mathsf{v}}})=1\text{ if
}rank_{\bm{{\mathsf{v}}}}(s)=a\text{ and }s\leq\mathsf{n}$. Otherwise,
$\text{all}^{*}_{a,s}(\bm{{\mathsf{v}}})=0$. The payment for the last slot
$\mathsf{m}$ is
$\text{p}^{*}_{\mathsf{m}}(\bm{{\mathsf{v}}})=\theta_{\mathsf{m}}\cdot{\mathsf{v}}_{rank_{\bm{{\mathsf{v}}}}(\mathsf{m}+1)}$
if $\mathsf{m}+1\leq\mathsf{n}$ and $\text{p}^{*}_{\mathsf{m}}=0$ otherwise.
For the remaining slots $1\leq s<\mathsf{m}$,
$\text{p}^{*}_{s}(\bm{{\mathsf{v}}})=(\theta_{s}-\theta_{s+1})\cdot{\mathsf{v}}_{rank_{\bm{{\mathsf{v}}}}(s+1)}+\text{p}^{*}_{s+1}(\bm{{\mathsf{v}}})$.
We assume $\text{p}^{*}_{s}(\bm{{\mathsf{v}}})$ and
$\text{all}^{*}_{s,a}(\bm{{\mathsf{v}}})$ are functions in $\mathcal{F}$.

VCG outcome The following formula denotes whether the allocation and payments
in the next state are the same as the ones for the VCG when agents bid
truthfully:

$\varphi_{\text{VCG}}(\bm{\sigma}):=(\textnormal{Ag},\sigma){\bf
X}\big{[}\bigwedge_{s\in
S}(\text{p}_{s}=\text{p}^{*}_{s}(\bm{\vartheta})\land\bigwedge_{a\in\textnormal{Ag}}\text{all}_{s,a}=\text{all}^{*}_{s,a}(\bm{\vartheta}))\big{]}$

If a strategy profile leads to the VCG outcome, then it is a LEFE:

######  Proposition 0.

For any state $v\in V$, $\rho\in\\{iR,ir\\}$ and strategy profile
$\bm{\sigma}=(\sigma_{a})_{a\in\textnormal{Ag}}$ with
$\sigma_{a}\in\mbox{\emph{Str}}^{\rho}_{a}$ for each $a$,
$\llbracket\varphi_{\text{VCG}}(\bm{\sigma})\to\text{LEF}\text{E}(\bm{\sigma})\rrbracket^{\mathcal{G}_{GSP},\rho}(v)=1$.

###### Proof sketch.

Let $\chi$ be an assignment, $v\in V$ be a state, $\rho\in\\{iR,ir\\}$ and
$\bm{\sigma}=(\sigma_{a})_{a\in\textnormal{Ag}}$ be a profile of
$\rho$-strategies. We denote
$\bm{{\mathsf{v}}}=({\mathsf{v}}_{a})_{a\in\textnormal{Ag}}$ where
${\mathsf{v}}_{a}=\ell(v,\vartheta_{a})$. Assume
$\llbracket\varphi_{\text{VCG}}(\bm{\sigma})\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v)=1$,
then we have $\llbracket(\textnormal{Ag},\bm{\sigma}){\bf
X}\big{[}\bigwedge_{s\in
S}(\text{p}_{s}=\text{p}^{*}_{s}(\bm{\vartheta})\land\bigwedge_{a\in\textnormal{Ag}}\text{all}_{s,a}=\text{all}^{*}_{s,a}(\bm{\vartheta}))\big{]}\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v)=1$.
We denote by $v_{\bm{\sigma}}=\delta(v,\bm{b})$ the state succeeding $v$ when
agents follow $\bm{\sigma}$, where $\bm{b}=(b_{i})_{i\in\textnormal{Ag}}$ and
$b_{i}=act_{match(v,\sigma_{i})}$. Let $s>1$ be a slot and $a$ be an agent. By
the definition of $\varphi_{\text{VCG}}$,
$\ell(v_{\bm{\sigma}},\text{all}_{s,a})=1$ if $rank_{\bm{{\mathsf{v}}}}(s)=a$
and $s\leq\mathsf{n}$. Otherwise, $\text{all}^{*}_{a,s}=0$.

Given that allocations in $v_{\bm{\sigma}}$ are the same as in the (truthful)
outcome of VCG, it must be the case that
$rank_{\bm{b}}(s)=rank_{\bm{{\mathsf{v}}}}(s)$. Thus, agents were allocated by
descending order of their valuations (recall the valuations are distinct).

According to the weight function, each agent is allocated to at most one slot.
We consider first the case in which $a$ is not allocated to any slot, i.e.
$max_{s^{\prime}\in S}(\ell(v_{\bm{\sigma}},\text{all}_{a,s^{\prime}}))=0$.
This case happens when $\mathsf{m}<\mathsf{n}$, that is, there are no enough
slots for all agents. The utility of $a$ for the slot $\mathsf{m}$ is
$\text{ut}_{a,\mathsf{m}}=\theta_{\mathsf{m}}({\mathsf{v}}_{a}-\ell(v_{\bm{\sigma}},\text{p}_{\mathsf{m}}))$.
By the definition of $\text{p}^{*}_{\mathsf{m}}$,
$\text{ut}_{a,\mathsf{m}}=\theta_{\mathsf{m}}({\mathsf{v}}_{a}-\theta_{\mathsf{m}}{\mathsf{v}}_{rank_{\bm{{\mathsf{v}}}(\mathsf{m}+1)}})$.
That is,
$\text{ut}_{a,\mathsf{m}}=\theta_{\mathsf{m}}{\mathsf{v}}_{a}-\theta_{\mathsf{m}}^{2}{\mathsf{v}}_{rank_{\bm{{\mathsf{v}}}(\mathsf{m}+1)}}$.
Since ${\mathsf{v}}_{a}<{\mathsf{v}}_{rank_{\bm{b}}(\mathsf{m}+1)}$, we have
that $\text{ut}_{a,\mathsf{m}}<0$. Thus, $\llbracket
0>\text{ut}_{a,\mathsf{m}}\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v_{\bm{\sigma}})=1$
and
$\llbracket\text{LEF}_{loses}\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v_{\bm{\sigma}})=1$.

Now we verify the case $a$ was assigned to a slot $1<s\leq\mathsf{m}$. Assume
for the sake of contradiction, that
$\llbracket\text{ut}_{a,s-1}>\text{ut}_{a,s}\rrbracket^{\mathcal{G}_{GSP},\rho}_{\chi}(v_{\bm{\sigma}})=1$.
Then, in the game induced by VCG, $a$ would have an incentive to switch her
bid with the agent in slot $s-1$, which is a contradiction since the bidding
${\mathsf{v}}_{a}$ is the dominant strategy for $a$ in VCG. ∎

In fact, from Edelman et al., (2007); Varian, (2007) the VCG payments are the
lower bound of locally envy-free equilibrium. Thus, in any other locally envy-
free equilibrium the total revenue obtained by GSP is at least as high as the
one obtained by VCG in equilibrium.

######  Corollary 0.

For any state $v\in V$, $\rho\in\\{iR,ir\\}$ and strategy profile
$\bm{\sigma}=(\sigma_{a})_{a\in\textnormal{Ag}}$ with
$\sigma_{a}\in\mbox{\emph{Str}}^{\rho}_{a}$ for each agent $a$,
$\llbracket\text{LEF}\text{E}(\bm{\sigma})\to\sum_{s\in
S}(\text{p}_{s})\geq\sum_{s\in
S}(\text{p}^{*}_{s})\rrbracket^{\mathcal{G}_{GSP},\rho}(v)=1$.

The solution concepts characterized in the previous section are considered in
a single stage of the game. Since the auction is repeated, advertisers can
change their bids very frequently and one may investigate whether the prices
stabilize and at what values Edelman et al., (2007). Stable bids must be best
responses to each other, that is, the bids form an (one-shot) equilibrium.
Cary et al. Cary et al., (2007) raises the problem on whether there exists a
“natural bidding strategy” for the advertisers that would lead to equilibrium.

Convergence The concept of convergence or stabilization can be easily encoded
in ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$: we say a wCGS $\mathcal{G}$
converge to a property $\varphi$ if the initial states lead to $\varphi$ being
eventually always the case. Formally, a wCGS converge to a condition $\varphi$
if $\llbracket{\bf F}{\bf
G}(\varphi)\rrbracket^{\mathcal{G},\rho}_{\chi}(v_{\iota})=1$ for each initial
state $v_{\iota}\in V_{\iota}$.

###  4.2. Natural Strategies for $\mathcal{G}_{GSP}$

Given agent $a$ and the wCGS $\mathcal{G}_{GSP}$, we exemplify strategies for
$a$ in a repeated keyword auction. For readability, we omit the epistemic
operator $K_{a}$ from an epistemic condition $K_{a}\varphi$ when the
satisfaction value of $\varphi$ is known by $a$ in all states. A common
approach for an advertiser is to assume that all the other bids will remain
fixed in the next round and target the slot that maximizes her utility at
current prices. This mechanism allows a range of bids that will result in the
same outcome from $a$’s perspective, so a number of strategies are
distinguished by the bid choice within this range.

Balanced bidding In the balanced bidding strategy (BB) Cary et al., (2007),
the agent bids so as to be indifferent between successfully winning the
targeted slot at its current price, or winning a slightly more desirable slot
at her bid price. The natural strategy representing balanced bidding for agent
$a$ is denoted $BB_{a}$ and is constructed in three parts. First, include the
guarded actions $(BB_{a,1}(b),b)$ for each action $b\in\textnormal{Ac}$.
Second, include $(BB_{a,2}(b,s),b)$ for each $b\in\textnormal{Ac}$ and
$1<s\leq\mathsf{m}$. Third, the last guarded action is $(\top,0)$. The
condition $BB_{a,1}(b)$ refers to the case in which the slot maximizing $a$’s
utility is the top slot and $b$ is $(\vartheta_{a}+\text{p}_{1})/2$:

$BB_{a,1}(b):=b=\frac{\vartheta_{a}+\text{p}_{1}}{2}\land(argmax_{s\in
S(\text{ut}_{a,s})})^{-1}=1$

Condition $BB_{a,2}(b,s)$ denotes the case in which the slot $s\neq 1$
maximizes $a$’s utility and $b$ is the bid value that is high enough to force
the prices paid by her competitors to rise, but not so high that she would
mind getting a higher slot at a price just below $b$.

$\displaystyle
BB_{a,2}(b,s):=\text{ut}_{a,s}=\theta_{s-1}\times(\vartheta_{a}-b)\land(argmax_{s^{\prime}\in
S}(\text{ut}_{a,s^{\prime}}))^{-1}=s^{-1}$

Notice the guarded action $BB_{a,2}(b,s)$ is defined for $s>1$ since it
compares the utility with the one for $s-1$. The case $s=1$ is treated by the
guarded action $BB_{a,1}(b)$.

Given a valuation profile
$\bm{{\mathsf{v}}}=({\mathsf{v}}_{a})_{a\in\textnormal{Ag}}$, let $\eta_{x}$
be the agent in the $x$-th position of $rank_{\bm{{\mathsf{v}}}}$ (that is,
$\eta_{x}$ is the agent with $x$-th highest valuation). We let
$b_{\eta_{x}}(\bm{{\mathsf{v}}})$ be a function in $\mathcal{F}$ defined as
follows:

$b_{\eta_{x}}(\bm{{\mathsf{v}}})=\begin{dcases}\frac{\theta_{x}}{\theta_{x-1}}\cdot
b_{rank_{\bm{{\mathsf{v}}}}(x+1)}(\bm{{\mathsf{v}}})+(1-\frac{\theta_{x}}{\theta_{x-1}}){\mathsf{v}}_{\eta_{x}}&\text{
if }x\geq\mathsf{m}+1\\\ {\mathsf{v}}_{\eta_{x}}&\text{ if }2\leq
x\leq\mathsf{m}\end{dcases}$

If $\bm{BB}=(BB_{a})_{a\in\textnormal{Ag}}$ converges to the equilibrium with
VCG outcomes, the agent with the highest valuation bids any value above
$b_{\eta_{2}}(\bm{{\mathsf{v}}})$. The equilibrium bid for $a\neq\eta_{1}$ is
$b_{a}(\bm{{\mathsf{v}}})$ Cary et al., (2007). When there are two slots and
all players update their bids according to BB, the game converges to the
equilibrium with VCG outcome. However, this is not the case for more than two
slots Cary et al., (2007).

######  Proposition 0.

For any initial state $v_{\iota}\in V_{\iota}$, state $v\in V$, and
$1<x\leq\mathsf{n}$, the following holds, where
$\bm{{\mathsf{v}}}=(\ell(v,\vartheta_{a}))_{a\in\textnormal{Ag}}$:

  1. (1)

If
$\llbracket\varphi_{\text{VCG}}(\bm{BB})\rrbracket^{\mathcal{G}_{GSP},ir}(v)=1$,
then $act_{match(v,BB_{\eta_{x}})}=b_{\eta_{x}}(\bm{{\mathsf{v}}})$ and
$act_{match(v,BB_{\eta_{1}})}>b_{\eta_{2}}(\bm{{\mathsf{v}}})$;

  2. (2)

If $\mathsf{m}=2$, then $\llbracket{\bf F}{\bf
G}(\varphi_{\text{VCG}}(\bm{BB}))\rrbracket^{\mathcal{G}_{GSP},ir}(v_{\iota})=1$;

  3. (3)

If $\mathsf{m}\geq 3$, then $\llbracket{\bf F}{\bf
G}(\varphi_{\text{VCG}}(\bm{BB}))\rrbracket^{\mathcal{G}_{GSP},ir}(v_{\iota})\neq
1$.

###### Proof sketch.

Statement (1) is derived in Cary et al., (2007) from the results of Edelman
et. al Edelman et al., (2007). Notice that when each agent $a$ is bound to the
natural strategy $\text{BB}_{a}$, they will update their bids simultaneously
in every state reachable form $v$. Thus, it corresponds to the synchronous
setting described by Cary et al., (2007). The proof for Statements (2) and (3)
are very similar to the one provided in the analysis of the synchronous
setting by Cary et. al Cary et al., (2007). ∎

Restricted BB The restricted balanced bidding strategy (RBB) Cary et al.,
(2007) is a variation of BB in which the agent only targets slots that are no
better than her current slot. The natural strategy representing RBB for agent
$a$ is denoted $RBB_{a}$ and is constructed as follows. First, include the
guarded actions $(RBB_{a,1}(b),b)$ for each action $b\in\textnormal{Ac}$.
Second, include $(RBB_{a,2}(b,s),b)$ for each $b\in\textnormal{Ac}$ and
$1<s\leq\mathsf{m}$. Finally, the last guarded action is $(\top,0)$. Let
$s_{a}=min(\mathsf{m},\sum_{s^{\prime}\in
S}s^{\prime}\times\text{all}_{a,s^{\prime}})$ be the slot assigned to agent
$a$ or the last slot if there is no such slot. Define $RBB_{a,1}(b)$ and
$RBB_{a,2}(b,s)$:

$RBB_{a,1}(b):=b=\frac{\vartheta_{a}+\text{p}_{1}}{2}\land argmax_{s\in
S\&s\geq s_{a}}(\text{ut}_{a,s})=1$ $\displaystyle
RBB_{a,2}(b,s):=\text{ut}_{a,s}=\theta_{s-1}\times(\vartheta_{a}-b)$
$\displaystyle\land(argmax_{s^{\prime}\in S\&s^{\prime}\geq
s_{a}}(\text{ut}_{a,s^{\prime}}))^{-1}=s^{-1}$

Similar to the results in Cary et al., (2007), we have that if all agents
follow the restricted balanced-bidding strategy, the auction converge to the
VCG equilibrium outcome. RBB always converge:

######  Proposition 0.

For any initial state $v_{\iota}\in V_{\iota}$, state $v\in V$, and
$1<x\leq\mathsf{n}$, the following holds, where
$\bm{{\mathsf{v}}}=(\ell(v,\vartheta_{a}))_{a\in\textnormal{Ag}}$:

  1. (1)

If
$\llbracket\varphi_{\text{VCG}}(\bm{RBB})\rrbracket^{\mathcal{G}_{GSP},ir}(v)=1$,
then $act_{match(v,RBB_{\eta_{x}})}=b_{\eta_{x}}(\bm{{\mathsf{v}}})$ and
$act_{match(v,RBB_{\eta_{1}})}>b_{\eta_{2}}(\bm{{\mathsf{v}}})$;

  2. (2)

$\llbracket{\bf F}{\bf
G}(\varphi_{\text{VCG}}(\bm{RBB}))\rrbracket^{\mathcal{G}_{GSP},ir}(v_{\iota})=1$.

###### Proof sketch.

Statement (1) is a derivation from the results presented in Edelman et al.,
(2007). For Statement (2), the proof is similar to the one provided in Cary et
al., (2007). The proof idea is the following. First bound the number of steps
until convergence of the price of slot $\mathsf{m}$ and the set of players who
will not be allocated slots. After this step, no losing player can afford a
slot and their bids do not interfere with the convergence of the top
$\mathsf{m}$ agents. The second stage of the proof is to show that the
allocation of the top $\mathsf{m}$ players converges to a fixed point (in
which they are sorted by their valuations). Then, for $1\leq i\leq\mathsf{m}$,
the proof inductively considers the allocation of slots $[i+1,\mathsf{m}]$. A
subset of slots is called stable if the allocation is in order of decreasing
values and if agent $\eta_{j}$ is the player currently allocated slot $j$,
then her last bid is in accordance with $b_{\eta_{j}}(\bm{\vartheta})$ for
every $j\in[i+1,\mathsf{m}]$. While the current setting is not a fixed point
of RBB, the proof proceeds by characterizing the number of rounds taken for
increasing the size of the maximal stable set. ∎

Knowledge grounded RBB The knowledge grounded RBB strategy (KBB) is a
variation of RBB in which the agent uses her knowledge about the valuation of
the player currently at her target slot to ground her bid value. The idea is
to avoid bidding more than what she knows her opponent valuates the slot. The
natural strategy representing KBB for agent $a$ is denoted $KBB_{a}$ is
constructed in three steps. First, include the guarded actions
$(KBB_{a,1}(b,c,i),c)$ for each $b,c\in\textnormal{Ac}$ and agent $i\neq a$.
Second, include $(KBB_{a,2}(b,s,c,i),c)$ for each $b,c\in\textnormal{Ac}$,
slot $1<s\leq\mathsf{m}$ and agent $i\neq a$. Finally, include the guarded
actions from $RBB_{a}$. The conditions $KBB_{a,1}(b,c,i)$ and
$KBB_{a,2}(b,s,c,i)$ are defined as follows:

$\displaystyle
KBB_{a,1}(b,c,i):=K_{a}\big{(}RBB_{a,1}(b)\land\text{all}_{i,1}=1\land
c=min(\vartheta_{i},b)\big{)}$ $\displaystyle
KBB_{a,2}(b,s,c,i):=K_{a}\big{(}RBB_{a,2}(b,s)\land\text{all}_{i,s}=1\land
c=min(\vartheta_{i},b)\big{)}$

The prices under KBB are at most the same as under RBB:

######  Proposition 0.

For any state $v\in V$, slot $s\in S$ and agent $a\in\textnormal{Ag}$,
$\llbracket(\textnormal{Ag},\bm{KBB})\text{p}_{s}\leq(\textnormal{Ag},\bm{RBB})\text{p}_{s}\rrbracket^{\mathcal{G}_{GSP},ir}(v)=1$.

###### Proof.

Consequence from the construction of $\bm{KBB}$. ∎

######  Remark 0.

With natural strategies, we can easily construct an strategy in which agent
$\eta_{x}$ plays according to $b_{\eta_{x}}(\bm{{\mathsf{v}}})$ (for
$1<x\leq\mathsf{n}$) and agent $\eta_{1}$ bids $b_{\eta_{2}}+\mathsf{inc}$
when she knows others’ valuations.

BB with recall Since BB may not converge to the VCG equilibrium outcome due to
loops on the slot allocation and prices, we construct a strategy that behaves
according to BB while there is no repetition in the outcome and follows RBB
otherwise. Hereafter, we show that this strategy with recall prevents the
loops that hinder the convergence of BB. Define the set of weighted conditions
$\Psi=\\{\bigwedge_{s\in
S}(\text{p}_{s}=pr_{s}\land\bigwedge_{a\in\textnormal{Ag}}\text{all}_{a,s}=al_{a,s}):pr_{s}\in\textnormal{Ac}$
& $al_{a,s}\in\\{0,1\\}\\}$. The natural strategy representing balanced
bidding with recall for agent $a$ is denoted $BBR_{a}$ and is constructed as
follows. First, include the guarded actions $(BBR_{a,1}(\psi,b),b)$ for each
action $b\in\textnormal{Ac}$ and condition $\psi\in\Psi$. Second, include
$(BBR_{a,2}(\psi,b,s),b)$ for each $\psi\in\Psi$, $b\in\textnormal{Ac}$ and
$1<s\leq\mathsf{m}$. Third, include $(BBR_{a,3}(\psi,b),b)$ for each action
$b\in\textnormal{Ac}$. Fourth, include $(BBR_{a,4}(b,s),b)$ for each
$b\in\textnormal{Ac}$ and $1<s\leq\mathsf{m}$. Finally, the last guarded
action is $(\top\text{*},0)$.

Now we define each guarded condition in $BBR_{a}$. If the current allocation
and payments have already happen in the past, $a$ plays according to the
restricted bidding strategy:

$BBR_{a,1}(\psi,b):=\top\text{*}\cdot\psi\cdot\top\text{*}\cdot(\psi\land
RBB_{a,1}(b))$
$BBR_{a,2}(\psi,b,s):=\top\text{*}\cdot\psi\cdot\top\text{*}\cdot(\psi\land
RBB_{a,2}(b,s))$

If there was no repetition on the payments and slot allocation, she plays
according to the balanced bidding strategy:

$BBR_{a,3}(\psi,b):=\top\text{*}\cdot BB_{a,1}(b)$
$BBR_{a,4}(\psi,b,s):=\top\text{*}\cdot BB_{a,2}(b,s)$

When all agents follow the strategy profile
$\bm{BBR}=(BBR_{a})_{a\in\textnormal{Ag}}$, the game converges to the VCG
equilibrium outcome.

######  Proposition 0.

For any initial state $v_{\iota}\in V_{\iota}$, state $v\in V$, and
$1<x\leq\mathsf{n}$, the following holds, where
$\bm{{\mathsf{v}}}=(\ell(v,\vartheta_{a}))_{a\in\textnormal{Ag}}$:

  1. (1)

If
$\llbracket\varphi_{\text{VCG}}(\bm{BBR})\rrbracket^{\mathcal{G}_{GSP},iR}(v)=1$,
then $act_{match(v,BBR_{\eta_{x}})}=b_{\eta_{x}}(\bm{{\mathsf{v}}})$ and
$act_{match(v,BBR_{\eta_{1}})}>b_{\eta_{2}}(\bm{{\mathsf{v}}})$;

  2. (2)

$\llbracket{\bf F}{\bf
G}(\varphi_{\text{VCG}}(\bm{BBR}))\rrbracket^{\mathcal{G}_{GSP},iR}(v_{\iota})=1$.

###### Proof sketch.

Statement (1) follows from Propositions 8 and 9. Statement (2) is proven by
contradiction. Assume the game does not converge to the VCG equilibrium
outcome. Let $\chi$ be an assignment and
$\pi=\textnormal{Out}(v_{\iota},\chi)$ be the play starting in $v_{\iota}$ and
follows the strategies assigned by $\chi$. Since $\mathcal{G}_{GSP}$ has
finitely many states, there exist two indices $g<l$ such that
$\pi_{g}=\pi_{l}$. Thus, for every $\psi\in\Psi$,
$\llbracket\psi\rrbracket^{\mathcal{G}_{GSP},iR}(\pi_{g})=\llbracket\psi\rrbracket^{\mathcal{G}_{GSP},iR}(\pi_{l})$.
Then, the game proceeds according to RBB strategy. That is, for any index
$j\geq l$ and agent $a$,
$act_{match(\pi_{l},BBR_{a})}=act_{match(\pi_{l},RBB_{a})}$. From Proposition
9, it follows that $\llbracket{\bf F}{\bf
G}(\varphi_{\text{VCG}}(\bm{BBR}))\rrbracket^{\mathcal{G}_{GSP},iR}_{\chi}(v_{\iota})=1$.
∎

When other agents are inactive (i.e. they repeat their last action), if
$BBR_{a}$ selects a different bid from the one assigned by $RBB_{a}$, the
utility of $a$ in the next state is greater under $BBR_{a}$.

######  Proposition 0.

Let $\rho\in\\{ir,iR\\}$ and $v=\delta(v^{\prime},\bm{c})$, for some state
$v^{\prime}\in V$ and action profile $\bm{c}=(c)_{a\in\textnormal{Ag}}$. Given
an agent $a\in\textnormal{Ag}$, let
${\sigma^{\rho}_{-a}}=(\sigma_{i}^{\rho})_{i\in\textnormal{Ag}_{-a}}$ be a
$\rho$-strategy profile, where the strategy $\sigma_{i}^{\rho}$ of agent $i$
is such that $act_{match(v,\sigma_{i}^{\rho})}=c_{i}$. If
$act_{match(v,BBR_{a})}\neq act_{match(v,RBB_{a})}$, then
$\llbracket(\textnormal{Ag}_{-a},{\sigma^{iR}_{-a}})\allowbreak(a,\allowbreak
BBR_{a}){\bf X}\text{ut}_{a}\rrbracket^{\mathcal{G}_{GSP},iR}(v)$ $>$
$\llbracket(\textnormal{Ag}_{-a},\allowbreak{\sigma^{ir}_{-a}})\allowbreak(a,\allowbreak
RBB_{a})\allowbreak{\bf X}\text{ut}_{a}\rrbracket^{\mathcal{G}_{GSP},ir}(v)$.

###### Proof sketch.

Assume the actions assigned by $BBR_{a}$ and $RBB_{a}$ are different, that is,
$act_{match(v,BBR_{a})}\neq act_{match(v,RBB_{a})}$, then it must be the case
that $act_{match(v,BBR_{a})}=b$ such that
$\llbracket\text{ut}_{a,s}=\theta_{s-1}\times(\vartheta_{a}-b)\land(argmax_{s^{\prime}\in
S}(\text{ut}_{a,s^{\prime}}))^{-1}=s^{-1}\rrbracket^{\mathcal{G}_{GSP},ir}_{\chi}(v)=1$
for some slot $s>1$. Notice that $RBB_{a}$ selected the action
$act_{match(v,RBB_{a})}$ that maximizes the utility among slots that are
better or equal to $a$’s current slot. By the other hand, the condition
followed by $BBR_{a}$ in $v$ chose the action $b$ that maximizes among all
slots. Thus, since the actions are different, $b$ has the greatest estimated
utility assuming the others repeat their previous bids. As it is in fact the
case, by the definition of $\sigma_{-a}^{iR}$ and $\sigma_{-a}^{ir}$, $a$’s is
assigned to $s$ in the next state and her utility is the one estimated, that
is $\llbracket{\bf
X}\text{ut}_{a}\rrbracket^{\mathcal{G}_{GSP},iR}_{\chi}(v)=\llbracket\text{ut}_{a,s}\rrbracket^{\mathcal{G}_{GSP},iR}_{\chi}(v)$.
Thus, $\llbracket(\textnormal{Ag}_{-a},\sigma_{-a}^{iR})(a,\allowbreak
BBR_{a}){\bf X}\text{ut}_{a}\rrbracket^{\mathcal{G}_{GSP},iR}(v)$ $>$
$\llbracket(\textnormal{Ag}_{-a},\sigma_{-a}^{ir})\allowbreak(a,RBB_{a}){\bf
X}\text{ut}_{a}\rrbracket^{\mathcal{G}_{GSP},ir}_{\chi}(v)$. ∎

######  Remark 0.

In vindictive bidding Zhou and Lukose, (2007), the agent bids as high as
possible to raise the payment of the advisor in the slot right below hers.
Since there is the risk that a change in other agents’ bids could result in
paying a higher price than expected, the player could use memory to balance
the use of aggressive bids.

##  5\. Expressivity

In relation to ${\textnormal{{SL}}}{[\mathcal{F}]}$with combinatorial
strategies, ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ introduces a new,
broader class of human-friendly strategies _and_ a language for expressing
properties of agents that use such strategies. Clearly, strategies with
quantitative conditions can be used to obtain goals that would not be
achievable otherwise. On the other hand, bounded natural strategies of
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ may not achieve some goals that can
be enforced with combinatorial strategies of
${\textnormal{{SL}}}{[\mathcal{F}]}$. In this section, we show that the
expressive power of ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ is incomparable
to that of ${\textnormal{{SL}}}{[\mathcal{F}]}$. In other words, there are
properties of quantitative games with natural strategies that cannot be
equivalently translated to properties based on combinatorial strategies, and
vice versa. From this, we conclude that reasoning about human-friendly
strategies offers an inherently different view of a multi-agent system from
the “standard” one.

###  5.1. Expressive and Distinguishing Power

We first adapt the notions of distinguishing power and expressive power to the
quantitative case as follows555 Cf., e.g., Wang and Dechesne, (2009) for a
detailed discussion of standard notions of expressivity. .

######  Definition 0 (Distinguishing power of real-valued logics).

Let $\mathcal{L}_{1}=(L_{1},{\llbracket\cdot\rrbracket}_{1})$ and
$\mathcal{L}_{2}=(L_{2},{\llbracket\cdot\rrbracket}_{2})$ be two logical
systems with syntax $L_{1},L_{2}$ and real-valued semantics
${\llbracket\cdot\rrbracket}_{1},{\llbracket\cdot\rrbracket}_{2}$ over the
same class of models $\mathcal{M}$. We say that $\mathcal{L}_{2}$ is _at least
as distinguishing_ as $\mathcal{L}_{1}$ (written:
$\mathcal{L}_{1}\preceq_{d}\mathcal{L}_{2}$) iff for every pair of models
$M,M^{\prime}\in\mathcal{M}$, if there exists a formula
$\varphi_{1}\in{L}_{1}$ such that
${\llbracket\varphi_{1}\rrbracket}^{M}_{1}\neq{\llbracket\varphi_{1}\rrbracket}^{M^{\prime}}_{1}$,
then there is also $\varphi_{2}\in{L}_{2}$ with
${\llbracket\varphi_{2}\rrbracket}^{M}_{2}\neq{\llbracket\varphi_{2}\rrbracket}^{M^{\prime}}_{2}$.
In other words, if there is a formula of $\mathcal{L}_{1}$ discerning $M$ from
$M^{\prime}$, then there must be also a formula of $\mathcal{L}_{2}$ doing the
same.

######  Definition 0 (Expressive power of real-valued logics).

$\mathcal{L}_{2}$ is _at least as expressive_ as $\mathcal{L}_{1}$ (written:
$\mathcal{L}_{1}\preceq_{e}\mathcal{L}_{2}$) iff for every
$\varphi_{1}\in{L}_{1}$ there exists $\varphi_{2}\in{L}_{2}$ such that, for
every model $M\in\mathcal{M}$, we have
${\llbracket\varphi_{1}\rrbracket}^{M}_{1}={\llbracket\varphi_{2}\rrbracket}^{M}_{2}$.
In other words, every formula of $\mathcal{L}_{1}$ has a translation in
$\mathcal{L}_{2}$ that produces exactly the same truth values on models in
$\mathcal{M}$.

It is easy to see that $\mathcal{L}_{1}\preceq_{e}\mathcal{L}_{2}$ implies
$\mathcal{L}_{1}\preceq_{d}\mathcal{L}_{2}$. Thus, by transposition, we also
get that $\mathcal{L}_{1}\not\preceq_{d}\mathcal{L}_{2}$ implies
$\mathcal{L}_{1}\not\preceq_{e}\mathcal{L}_{2}$.

In the remainder, $\mathcal{M}$ is the class of pointed weighted games, i.e.,
pairs $(\mathcal{G},v)$ where $\mathcal{G}$ is a wCGS and $v$ is a state in
$\mathcal{G}$.

###  5.2. Expressivity of ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ vs.
${\textnormal{{SL}}}{[\mathcal{F}]}$

${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ and
${\textnormal{{SL}}}{[\mathcal{F}]}$ are based on different notions of
strategic ability. The former refers to “natural” strategies, represented as
mappings from regular expressions over atomic propositions to actions. The
latter uses ”combinatorial” strategies, represented by mappings from sequences
of states to actions. Each natural strategy can be translated to a
combinatorial one, but not vice versa. Consequently,
${\textnormal{{SL}}}{[\mathcal{F}]}$ can express that a given coalition has a
combinatorial strategy to achieve their goal (which is not expressible in
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$). On the other hand,
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ allows expressing that a winning
natural strategy does not exist (which cannot be captured in
${\textnormal{{SL}}}{[\mathcal{F}]}$). Now we show that
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ allows to express properties that
cannot be captured in ${\textnormal{{SL}}}{[\mathcal{F}]}$, and vice versa.

$q_{0}$$q_{1}$$\mathsf{{p}}$$q_{1}^{\prime}$$\mathsf{{p}}$$q_{1}^{\prime\prime}$$\mathsf{{p}}$$q_{2}^{\prime}$$q_{2}$$q_{3}$$\mathsf{{win}}$$q_{4}$$(a_{1},\\_)$$(b_{1},\\_)$$(c_{1},\\_)$$(d_{1},\\_)$$(e_{1},\\_)$$(\\_,a_{2})$$(\\_,b_{2})$$(\\_,a_{2})$$(\\_,b_{2})$
Figure 1. Model $\mathcal{G}_{1}$. Its counterpart $\mathcal{G}_{1}^{\prime}$
is obtained by fixing $\mathsf{{p}}$ to hold only in $q_{1},q_{1}^{\prime}$.
Underscore fits any action label

######  Proposition 0.

${\textnormal{{{NatSL}}}}{[\mathcal{F}]}\not\preceq_{d}{\textnormal{{SL}}}{[\mathcal{F}]}$
in both $ir$ and $iR$ semantics.

###### Proof sketch.

Consider model $\mathcal{G}_{1}$ in Figure 1, with agents
$\textnormal{Ag}=\\{1,2\\}$, actions
$\textnormal{Ac}_{1}=\\{a_{1},b_{1},c_{1},d_{1},e_{1}\\}$ and
$\textnormal{Ac}_{2}=\\{a_{2},b_{2}\\}$ available at all positions, and
propositions $\textnormal{AP}=\\{\mathsf{{p}},\mathsf{{win}}\\}$. Both
propositions are qualitative (that is, the propositions have only values in
{-1,1}). For each proposition, the states where it evaluates to $1$ are
indicated; otherwise its truth value is assumed to be $-1$. The outgoing
transitions in $q_{1}^{\prime},q_{1}^{\prime\prime}$ (resp. $q_{2}^{\prime}$)
are exact copies of those at $q_{1}$ (resp. $q_{2}$). Moreover, model
$\mathcal{G}_{1}^{\prime}$ is obtained by fixing proposition $\mathsf{{left}}$
to hold in both $q_{1},q_{1}^{\prime}$, instead of only $q_{1}$. As all the
propositions are qualitative, formulas of
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ and
${\textnormal{{SL}}}{[\mathcal{F}]}$ evaluate to $-1$ or $1$. Note also that
the sets of $ir$ and $iR$ strategies in each model coincide, so we can
concentrate on the $ir$ case w.l.o.g.

Let $\mathcal{G}\\!\dagger\\!\sigma$ denote the model obtained by fixing the
(memoryless) strategy $\sigma$ in $\mathcal{G}$. In order to prove that
$(\mathcal{G}_{1},q_{0})$ and $(\mathcal{G}_{1}^{\prime},q_{0})$ satisfy the
same formulas of ${\textnormal{{SL}}}{[\mathcal{F}]}$, it suffices to observe
that:

  1. (1)

For every strategy $\sigma_{1}$ of agent $1$ in $\mathcal{G}_{1}$, there is
$\sigma_{1}^{\prime}$ in $\mathcal{G}_{1}^{\prime}$ such that agent $2$ has
the same strategic abilities in
$(\mathcal{G}^{\prime}_{1}\\!\dagger\\!\sigma_{1},q_{0})$ and
$(\mathcal{G}_{1}^{\prime}\\!\dagger\\!\sigma_{1},q_{0})$ (and vice versa).
For instance, playing $c_{1}$ in $\mathcal{G}$ obtains the same abilities of
$1$ as playing $a_{1}$ in $\mathcal{G}^{\prime}$.

  2. (2)

Analogously for strategies of agent $2$, e.g., strategy
$a_{2}a_{2}a_{2}b_{2}b_{2}$ in $\mathcal{G}_{1}$ can be simulated by strategy
$a_{2}a_{2}b_{2}b_{2}b_{2}$ in $\mathcal{G}_{1}^{\prime}$.

On the other hand, the formula $\exists s_{2}^{\leq 2}\forall s_{1}^{\leq
1}(1,s_{1})(2,s_{2}){\bf F}\mathsf{{win}}$ of
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ holds in $(\mathcal{G}_{1},q_{0})$,
but not in $(\mathcal{G}_{1}^{\prime},q_{0})$. The winning natural strategy
for agent $2$ in $\mathcal{G}_{1}$ is $\big{(}(\top^{*}\mathsf{{p}},a_{2}),\
(\top^{*},b_{2})\big{)}$; clearly, it does not succeed in
$\mathcal{G}_{1}^{\prime}$. ∎

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\mathsf{{win}}$$q_{4}$$(a_{1},\\_)$$(b_{1},\\_)$$(\\_,a_{2})$$(\\_,b_{2})$$(\\_,a_{2})$$(\\_,b_{2})$

$q_{0}$$q_{1}$$q_{2}$$q_{3}$$\mathsf{{win}}$$q_{4}$$(a_{1},\\_)$$(b_{1},\\_)$$(\\_,a_{2})$$(\\_,b_{2})$$(\\_,a_{2})$$(\\_,b_{2})$$1$

Figure 2. Models $\mathcal{G}_{2}$ (left) and $\mathcal{G}_{2}^{\prime}$
(right)

######  Proposition 0.

${\textnormal{{SL}}}{[\mathcal{F}]}\not\preceq_{d}{\textnormal{{{NatSL}}}}{[\mathcal{F}]}$
in both $ir$ and $iR$ semantics.

###### Proof sketch.

Consider models $\mathcal{G}_{2}$ and $\mathcal{G}_{2}^{\prime}$ in Figure 2.
They have isomorphic action/transition structures, the only difference being
the indistinguishability of states $q_{1},q_{2}$ in $\mathcal{G}_{2}^{\prime}$
(but not in $\mathcal{G}_{2}$). Since the two states have the same valuations
of propositions, each natural strategy must specify the same decision in
$q_{1},q_{2}$. Thus, both players have exactly the same available natural
strategies in $\mathcal{G}_{2}$ and $\mathcal{G}_{2}^{\prime}$, and hence
$(\mathcal{G}_{2},q_{0})$ and $(\mathcal{G}_{2}^{\prime},q_{0})$ produce the
same valuations of ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ formulas.

On the other hand, we have that $\exists s_{2}\forall
s_{1}(1,s_{1})(2,s_{2}){\bf F}\mathsf{{win}}$ of
${\textnormal{{SL}}}{[\mathcal{F}]}$ holds in $(\mathcal{G}_{2},q_{0})$, but
not in $(\mathcal{G}_{2}^{\prime},q_{0})$. ∎

The following is an immediate consequence.

######  Theorem 19.

${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ and
${\textnormal{{SL}}}{[\mathcal{F}]}$ have incomparable distinguishing power
over the class of pointed wCGS (in both $ir$ and $iR$ semantics).

######  Corollary 0.

${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ and
${\textnormal{{SL}}}{[\mathcal{F}]}$ have incomparable expressive power over
the class of pointed wCGS (in both $ir$ and $iR$ semantics).

##  6\. Model Checking

In this section we show that the model checking problem for
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ with imperfect information is no
harder than model checking LTL or classic SL with memoryless agents. First of
all, we define the quantitative model-checking problem for
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$.

######  Definition 0.

Given $\rho\in\\{ir,iR\\}$, the model-checking problem for
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ consists in deciding, for a given
sentence $\varphi$, wCGS $\mathcal{G}$, state $v\in V$ and predicate
$P\subseteq[-1;1]$, whether
$\llbracket\varphi\rrbracket^{\mathcal{G},\rho}(v)\in P$.

Now, we have all the ingredients to prove the following result.

######  Theorem 22.

Assuming that functions in $\mathcal{F}$ can be computed in polynomial space,
model checking ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ with imperfect
information, natural strategies with recall, and $k$ as parameter of the
problem is Pspace -complete.

###### Proof.

For the lower-bound we recall that ${\textnormal{LTL}}{[\mathcal{F}]}$ model
checking is Pspace -complete Almagor et al., (2016). For the upper-bound, to
verify that a given ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ formula
$\varphi$ is satisfied over a wCGS $\mathcal{G}$ at a state $v\in V$ under
assignments $\chi$ over uniform natural strategies with recall, we make use of
a recursive function as is done in Cermák et al., (2018). We start by showing
that each recursive call only needs at most polynomial space. First, observe
that each assignment $\chi$ has a strategy $s_{a}$ for each agent $a\in Ag$
666Note that, as defined in Section 3, we consider only complete assignments.
Thus, we can assume that a strategy is assigned for each agent.. We know that
each strategy $s_{a}$ that can be assigned to agent $a$ is bounded, and we
have that $compl(s_{a})\leq k$. Thus, each strategy can be stored in
$O(k\cdot|Act|)$ and, by consequence, any assignment can be stored in space
$O((|Ag|\cdot|\text{free}(\varphi)|)\cdot(k\cdot|Act|))$. Now, we can analyse
the recursive function. For the base case, $\llbracket
p\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$ can be computed in constant space
via the weight function. For strategy quantification $\llbracket\exists
s_{a}^{\leq k}.\,\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$, besides the
recursive call to
$\llbracket\varphi\rrbracket^{\mathcal{G},\rho}_{\chi[s\mapsto\sigma]}(v)$ we
need space $O(|k|\cdot|\textnormal{Ac}|)$ to store the current strategy and
the current maximum value computed. For $\llbracket
f(\varphi_{1},...,\varphi_{m})\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$, by
assumption $f$ is computed in polynomial space. For $\llbracket{\bf
X}\varphi\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$, we only need to observe
that the next state in $\textnormal{Out}(v,\chi)$ is computed in constant
space. Finally, we detail how $\llbracket\varphi_{1}{\bf
U}\varphi_{2}\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$ is computed. Let
$\pi=\textnormal{Out}(v,\chi)$. Since $\mathcal{G}$ has finitely many states,
there exist two indices $g<l$ such that $\pi_{g}=\pi_{l}$, and since
strategies are bounded by $k$, the suffix of $\pi$ starting at index $l$ is
equal to the suffix starting at index $g$. So there exist
$\rho_{1}=v_{0}...v_{g-1}$ and $\rho_{2}=v_{g}...v_{l-1}$ such that
$\pi=\rho_{1}\cdot\rho_{2}^{\omega}$. It follows that

$\displaystyle\llbracket\varphi_{1}{\bf
U}\varphi_{2}\rrbracket^{\mathcal{G},\rho}_{\chi}(v)$
$\displaystyle=\sup_{i\geq
0}\min\Big{(}\llbracket\varphi_{2}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{i}),\min_{0\leq
j<i}\llbracket\varphi_{1}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{j})\Big{)}$
$\displaystyle=\max_{0\leq
i<l}\min\Big{(}\llbracket\varphi_{2}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{i}),\min_{0\leq
j<i}\llbracket\varphi_{1}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{j})\Big{)}$

This can be computed by a while loop that increases $i$, computes
$\llbracket\varphi_{2}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{i})$ and
$\min_{0\leq
j<i}\llbracket\varphi_{1}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{j})$, their
minimum, and records the result if it is bigger than the previous maximum.
This requires to store the current value of $\min_{0\leq
j<i}\llbracket\varphi_{1}\rrbracket^{\mathcal{G},\rho}_{\chi}(\pi_{i})$, the
current maximum, and the list of states already visited, which are at most
$k\cdot|V|$. Finally, the number of nested recursive calls is at most
$|\varphi|$, so the total space needed is bounded by $|\varphi|$ times a
polynomial in the size of the input, and is thus polynomial. ∎

Since memoryless natural strategies are a special case of natural strategies
with recall, we obtain the following result.

######  Corollary 0.

Assuming that functions in $\mathcal{F}$ can be computed in polynomial space,
model checking ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ with imperfect
information, memoryless natural strategies, and $k$ as parameter of the
problem is Pspace -complete.

##  7\. Conclusion

In this work we have introduced Natural Strategy Logic with quantitative
semantics and imperfect information
(${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$) for reasoning about strategic
ability in auctions. ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ provides a tool
for mechanism design and offers a new perspective for formal verification and
design of novel mechanisms and strategies. We demonstrated the usefulness of
our approach by modelling and evaluating strategies for repeated keyword
auctions.

In terms of technical results, we proved that the model checking problem for
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ is Pspace -complete, that is, no
harder than model checking for the much less expressive language of
quantitative LTL (${\textnormal{LTL}}{[\mathcal{F}]}$). We also showed that
${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ has incomparable distinguishing and
expressive power to ${\textnormal{{SL}}}{[\mathcal{F}]}$. This means that the
characterizations based on simple bounded strategies offer an inherently
different view of auctions and mechanism design from characterizations using
combinatorial strategies of arbitrary complexity. Amazingly, this aspect has
never been studied for natural strategies, not even for the original proposal
of NatATL Jamroga et al., 2019a .

We consider several directions for future work. First, a probabilistic
extension of Strategy Logic Aminof et al., (2019) would allow handling
mechanisms in stochastic settings with mixed strategies. Another direction is
to investigate the use of strategies with recall for learning other players’
valuations based on their behaviour. Finally, the implementation of a model
checker for ${\textnormal{{{NatSL}}}}{[\mathcal{F}]}$ will enable the
empirical evaluation of auctions with natural strategies.

This research is supported by the ANR project AGAPE ANR-18-CE23-0013.

## References

  * Ågotnes, (2006) Ågotnes, T. (2006).  Action and knowledge in alternating-time temporal logic.  Synthese, 149(2):377–409.
  * Ågotnes and Walther, (2009) Ågotnes, T. and Walther, D. (2009).  A logic of strategic ability under bounded memory.  Journal of Logic, Language and Information, 18(1):55–77.
  * Alechina et al., (2007) Alechina, N., Dastani, M., Logan, B., and Meyer, J.-J. C. (2007).  A logic of agent programs.  In Proceedings of AAAI, pages 795–800.
  * Alechina et al., (2008) Alechina, N., Logan, B., Dastani, M., and Meyer, J.-J. C. (2008).  Reasoning about agent execution strategies.  In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 1455–1458.
  * Alechina et al., (2009) Alechina, N., Logan, B., Nga, N., and Rakib, A. (2009).  A logic for coalitions with bounded resources.  In Proc. of International Joint Conference on Artificial Intelligence (IJCAI), pages 659–664.
  * Alechina et al., (2010) Alechina, N., Logan, B., Nguyen, H., and Rakib, A. (2010).  Resource-bounded alternating-time temporal logic.  In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 481–488.
  * Almagor et al., (2016) Almagor, S., Boker, U., and Kupferman, O. (2016).  Formally reasoning about quality.  Journal of the ACM, 63(3):24:1–24:56.
  * Alur et al., (2002) Alur, R., Henzinger, T. A., and Kupferman, O. (2002).  Alternating-time temporal logic.  Journal of the ACM, 49(5):672–713.
  * Aminof et al., (2019) Aminof, B., Kwiatkowska, M., Maubert, B., Murano, A., and Rubin, S. (2019).  Probabilistic strategy logic.  In Kraus, S., editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI.
  * Baier and Katoen, (2008) Baier, C. and Katoen, J.-P. (2008).  Principles of Model Checking (Representation and Mind Series).  The MIT Press.
  * Barlo et al., (2008) Barlo, M., Carmona, G., and Sabourian, H. (2008).  Bounded memory with finite action spaces.  Sabanci University, Universidade Nova de Lisboa and University of Cambridge.
  * Barthe et al., (2016) Barthe, G., Gaboardi, M., Arias, E., Hsu, J., Roth, A., and Strub, P.-Y. (2016).  Computer-aided verification for mechanism design.  In Conference on Web and Internet Economics (WINE).
  * Belardinelli et al., (2017) Belardinelli, F., Condurache, R., Dima, C., Jamroga, W., and Jones, A. V. (2017).  Bisimulations for verifying strategic abilities with an application to threeballot.  In Proc. of AAMAS 17, pages 1286–1295.
  * Belardinelli et al., (2018) Belardinelli, F., Lomuscio, A., and Malvone, V. (2018).  Approximating perfect recall when model checking strategic abilities.  In Proc. of KR, pages 435–444.
  * Belardinelli et al., (2014) Belardinelli, F., Lomuscio, A., and Patrizi, F. (2014).  Verification of agent-based artifact systems.  Journal of Artificial Intelligence Research, 51:333–376.
  * Bordini et al., (2006) Bordini, R., Fisher, M., Visser, W., and Wooldridge, M. (2006).  Verifying multi-agent programs by model checking.  Autonomous Agents and Multi-Agent Systems, 12(2):239–256.
  * Bourne, (1970) Bourne, L. E. (1970).  Knowing and using concepts.  Psychol. Rev., 77:546–556.
  * Bouyer et al., (2019) Bouyer, P., Kupferman, O., Markey, N., Maubert, B., Murano, A., and Perelli, G. (2019).  Reasoning about Quality and Fuzziness of Strategic Behaviours.  In Proc. of IJCAI.
  * (19) Bulling, N. and Farwer, B. (2010a).  Expressing properties of resource-bounded systems: The logics RTL* and RTL.  In Proceedings of Computational Logic in Multi-Agent Systems (CLIMA).
  * (20) Bulling, N. and Farwer, B. (2010b).  On the (un-)decidability of model checking resource-bounded agents.  In Proceedings of ECAI, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 567–572. IOS Press.
  * Bulling and Jamroga, (2014) Bulling, N. and Jamroga, W. (2014).  Comparing variants of strategic ability: how uncertainty and memory influence general properties of games.  Journal of Autonomous Agents and Multi-Agent Systems, 28(3):474–518.
  * Caminati et al., (2015) Caminati, M., Kerber, M., Lange, C., and Rowat, C. (2015).  Sound auction specification and implementation.  In ACM Conference on Economics and Computation (EC).
  * Cary et al., (2007) Cary, M., Das, A., Edelman, B., Giotis, I., Heimerl, K., Karlin, A. R., Mathieu, C., and Schwarz, M. (2007).  Greedy bidding strategies for keyword auctions.  EC 2007 - Proceedings of the Eighth Annual Conference on Electronic Commerce, pages 262–271.
  * Cermák et al., (2014) Cermák, P., Lomuscio, A., Mogavero, F., and Murano, A. (2014).  MCMAS-SLK: A model checker for the verification of strategy logic specifications.  In Proc. of the Int. Conf. on Computer Aided Verification (CAV), volume 8559 of Lecture Notes in Computer Science, pages 525–532. Springer.
  * Cermák et al., (2018) Cermák, P., Lomuscio, A., Mogavero, F., and Murano, A. (2018).  Practical verification of multi-agent systems against SLK specifications.  Inf. Comput., 261:588–614.
  * Chatterjee et al., (2010) Chatterjee, K., Henzinger, T. A., and Piterman, N. (2010).  Strategy logic.  Information and Computation, 208(6):677–693.
  * Dastani and Jamroga, (2010) Dastani, M. and Jamroga, W. (2010).  Reasoning about strategies of multi-agent programs.  In Proceedings of AAMAS, pages 625–632.
  * Deutsch et al., (2009) Deutsch, A., Hull, R., Patrizi, F., and Vianu, V. (2009).  Automatic verification of data-centric business processes.  In Proceedings of the 12th International Conference on Database Theory (ICDT09), pages 252–267. ACM.
  * Dima and Tiplea, (2011) Dima, C. and Tiplea, F. (2011).  Model-checking ATL under imperfect information and perfect recall semantics is undecidable.  CoRR, abs/1102.4225.
  * Dixon et al., (2012) Dixon, C., Winfield, A., Fisher, M., and Zeng, C. (2012).  Towards temporal verification of swarm robotic systems.  Robotics and Autonomous Systems, 60(11):1429–1441.
  * Duijf and Broersen, (2016) Duijf, H. and Broersen, J. (2016).  Representing strategies.  In Proc. of Int. Workshop on Strategic Reasoning (SR), pages 15–26.
  * Edelman et al., (2007) Edelman, B., Ostrovsky, M., and Schwarz, M. (2007).  Internet advertising and the generalized second-price auction: Selling billions of dollars worth of keywords.  American economic review, 97(1):242–259.
  * Feldman, (2000) Feldman, J. (2000).  Minimization of Boolean complexity in human concept learning.  Nature, 407:630–3.
  * Gammie and van der Meyden, (2004) Gammie, P. and van der Meyden, R. (2004).  MCK: Model checking the logic of knowledge.  In Proc. of 16th Int. Conf. on Computer Aided Verification (CAV), volume 3114 of Lecture Notes in Computer Science, pages 479–483. Springer.
  * Gonzalez et al., (2015) Gonzalez, P., Griesmayer, A., and Lomuscio, A. (2015).  Verification of GSM-based artifact-centric systems by predicate abstraction.  In Proceedings of the 13th International Conference on Service Oriented Computing (ICSOC15), volume 9435 of Lecture Notes in Computer Science, pages 253–268. Springer.
  * Gupta et al., (2015) Gupta, A., Schewe, S., and Wojtczak, D. (2015).  Making the best of limited memory in multi-player discounted sum games.  In Esparza, J. and Tronci, E., editors, Proc. of the Int. Symposium on Games, Automata, Logics and Formal Verification (GandALF 2015), volume 193 of EPTCS, pages 16–30.
  * Harel and Kozen, (1982) Harel, D. and Kozen, D. (1982).  Process logic: Expressiveness, decidability, completeness.  Journal of Computer and System Sciences, 25(2):144–170.
  * Herzig et al., (2014) Herzig, A., Lorini, E., Maffre, F., and Walther, D. (2014).  Alternating-time temporal logic with explicit programs.  In Proceedings of Workshop on Logical Aspects of Multi-Agent Systems (LAMAS).
  * Hörner and Olszewski, (2009) Hörner, J. and Olszewski, W. (2009).  How robust is the folk theorem?  The Quarterly Journal of Economics, pages 1773–1814.
  * Jamroga and Ågotnes, (2007) Jamroga, W. and Ågotnes, T. (2007).  Constructive knowledge: what agents can achieve under imperfect information.  J. Applied Non-Classical Logics, 17(4):423–475.
  * Jamroga et al., (2020) Jamroga, W., Kurpiewski, D., and Malvone, V. (2020).  Natural strategic abilities in voting protocols.  In Groß, T. and Viganò, L., editors, Socio-Technical Aspects in Security and Trust - 10th International Workshop, STAST 2020, Virtual Event, September 14, 2020, volume 12812 of Lecture Notes in Computer Science, pages 45–62. Springer.
  * (42) Jamroga, W., Malvone, V., and Murano, A. (2019a).  Natural strategic ability.  Artificial Intelligence, 277:103170.
  * (43) Jamroga, W., Malvone, V., and Murano, A. (2019b).  Natural strategic ability under imperfect information.  In Proceedings of the International Conference on Autonomous Agents and MultiAgent Systems (AAMAS).
  * Kerber et al., (2016) Kerber, M., Lange, C., and Rowat, C. (2016).  An introduction to mechanized reasoning.  Journal of Mathematical Economics, 66:26 – 39.
  * Kouvaros and Lomuscio, (2015) Kouvaros, P. and Lomuscio, A. (2015).  A counter abstraction technique for the verification of robot swarms.  In Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI15), pages 2081–2088. AAAI Press.
  * Kupferman and Vardi, (2000) Kupferman, O. and Vardi, M. Y. (2000).  Synthesis with incomplete informatio.  In Advances in Temporal Logic, pages 109–127. Springer.
  * Lomuscio et al., (2015) Lomuscio, A., Qu, H., and Raimondi, F. (2015).  MCMAS: A model checker for the verification of multi-agent systems.  Software Tools for Technology Transfer.  http://dx.doi.org/10.1007/s10009-015-0378-x.
  * Maruyama, (2021) Maruyama, Y. (2021).  A reasoning system for fuzzy distributed knowledge representation in multi-agent systems.  In 2021 IEEE International Conference on Fuzzy Systems (FUZZ-IEEE), pages 1–6. IEEE.
  * Maubert et al., (2021) Maubert, B., Mittelmann, M., Murano, A., and Perrussel, L. (2021).  Strategic reasoning in automated mechanism design.  In Proc. of the Eighteen Conference on Principles of Knowledge Representation and Reasoning.
  * Mogavero et al., (2014) Mogavero, F., Murano, A., Perelli, G., and Vardi, M. (2014).  Reasoning about strategies: On the model-checking problem.  ACM Trans. Comput. Log., 15(4).
  * Montali et al., (2014) Montali, M., Calvanese, D., and De Giacomo, G. (2014).  Verification of data-aware commitment-based multiagent system.  In Proc. of the 14th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS14), pages 157–164. IFAAMAS.
  * Morris and Ward, (2014) Morris, R. and Ward, G. (2014).  The Cognitive Psychology of Planning.  Psychology Press.
  * Nielsen, (1994) Nielsen, J. (1994).  Usability Engineering.  Morgan Kaufmann.
  * Novák and Jamroga, (2009) Novák, P. and Jamroga, W. (2009).  Code patterns for agent oriented programming.  In Proceedings of AAMAS’09, pages 105–112.
  * Pauly and Parikh, (2003) Pauly, M. and Parikh, R. (2003).  Game logic-an overview.  Studia Logica, 75(2):165–182.
  * Pauly and Wooldridge, (2003) Pauly, M. and Wooldridge, M. (2003).  Logic for mechanism design–a manifesto.  In Proc. of the 2003 Workshop on Game Theory and Decision Theory in Agent Systems.
  * Pnueli and Rosner, (1989) Pnueli, A. and Rosner, R. (1989).  On the Synthesis of a Reactive Module.  In Symposium on the Principles of Programming Languages (POPL 89), pages 179–190. ACM.
  * Reif, (1984) Reif, J. H. (1984).  The complexity of two-player games of incomplete information.  J. Comput. Syst. Sci., 29(2):274–301.
  * Roughgarden, (2010) Roughgarden, T. (2010).  Algorithmic game theory.  Communications of the ACM, 53(7):78–86.
  * Santos, (2018) Santos, F. (2018).  Dynamics of Reputation and the Self-organization of Cooperation.  PhD thesis, University of Lisbon.
  * Santos et al., (2018) Santos, F., Santos, F., and Pacheco, J. (2018).  Social norm complexity and past reputations in the evolution of cooperation.  Nature, 555:242–245.
  * Troquard et al., (2011) Troquard, N., van der Hoek, W., and Wooldridge, M. (2011).  Reasoning about Social Choice Functions.  Journal of Philosophical Logic, 40(4):473––498.
  * van der Hoek et al., (2005) van der Hoek, W., Jamroga, W., and Wooldridge, M. (2005).  A logic for strategic reasoning.  In Proceedings of AAMAS’05, pages 157–164.
  * Varian, (2007) Varian, H. R. (2007).  Position auctions.  international Journal of industrial Organization, 25(6):1163–1178.
  * Vester, (2013) Vester, S. (2013).  Alternating-time temporal logic with finite-memory strategies.  In Proceedings of GandALF, EPTCS, pages 194–207.
  * Walther et al., (2007) Walther, D., van der Hoek, W., and Wooldridge, M. (2007).  Alternating-time temporal logic with explicit strategies.  In Proceedings TARK XI, pages 269–278. Presses Universitaires de Louvain.
  * Wang and Dechesne, (2009) Wang, Y. and Dechesne, F. (2009).  On expressive power and class invariance.  CoRR, abs/0905.4332.
  * Wooldridge et al., (2007) Wooldridge, M., Agotnes, T., Dunne, P., and Van der Hoek, W. (2007).  Logic for automated mechanism design-a progress report.  In Proc. of AAAI.
  * Yadav and Sardiña, (2012) Yadav, N. and Sardiña, S. (2012).  Reasoning about agent programs using ATL-like logics.  In Proceedings of JELIA, pages 437–449.
  * Yuan et al., (2017) Yuan, Y., Wang, F.-Y., and Zeng, D. (2017).  Competitive analysis of bidding behavior on sponsored search advertising markets.  IEEE Transactions on Computational Social Systems, 4(3):179–190.
  * Zhou and Lukose, (2007) Zhou, Y. and Lukose, R. (2007).  Vindictive bidding in keyword auctions.  ACM International Conference Proceeding Series, 258:141–146.