Abstract Interpretation of Supermodular Games
Francesco Ranzato
Dipartimento di Matematica, University of Padova, Italy

arXiv:1507.01423v1 [cs.GT] 6 Jul 2015

Abstract
Supermodular games find significant applications in a variety of models, especially in operations
research and economic applications of noncooperative game theory, and feature pure strategy Nash equilibria characterized as fixed points of multivalued functions on complete lattices. Pure strategy Nash equilibria of supermodular games are here approximated by resorting to the theory of abstract interpretation,
a well established and known framework used for designing static analyses of programming languages.
This is obtained by extending the theory of abstract interpretation in order to handle approximations
of multivalued functions and by providing some methods for abstracting supermodular games, in order
to obtain approximate Nash equilibria which are shown to be correct within the abstract interpretation
framework.

1 Introduction
Motivations. Games may have strategic complementarities, which means, roughly speaking, that best
responses of players have monotonic reactions, reflecting a complementarity relationship between own
actions and rivals’ actions. Games with strategic complementarities occur in a large array of models, especially in operations research and economic applications of noncooperative game theory, a significant sample
of them is described by Topkis’ book [17]. Pionereed by Topkis [16], this class of games is formalized by
supermodular games, where the payoff functions of each player have the lattice-theoretical properties of
supermodularity and increasing differences. In a supermodular game, the strategy space of every player
is partially ordered and is assumed to be a complete lattice, while the utility in playing a higher strategy
increases when the opponents also play higher strategies. It turns out that pure strategy Nash equilibria
of supermodular games exist and form a complete lattice w.r.t. the ordering relation of the strategy space,
thus exhibiting the least and greatest Nash equilibria. Furthermore, since the best response correspondence
of a supermodular game satisfies a monotonicity hypothesis, its least and greatest equilibria can be characterized and, under some assumptions of finiteness, calculated as least and greatest fixed points by the
well-known lattice-theoretical Knaster-Tarski fixed point theorem, which provides the theoretical basis for
the Robinson-Topkis algorithm [17].
Since the breakthrough on the PPAD-completeness of finding mixed Nash equilibria [7], the question
of approximating Nash equilibria emerged as a key problem in algorithmic game theory [8, 11]. In this
context, approximate equilibrium refers to ǫ-approximation, with ǫ > 0, meaning that, for each player, all
the strategies have a payoff which is at most ǫ more (or less) than the precise payoff of the given strategy.
It is well known that the notion of correct (a.k.a. sound) approximation is fundamental in static program
analysis, one major research area in programming language theory and design. Static program analysis
derives some partial but correct information of the run-time program behavior without actually executing
programs. Prominent examples of static analysis include dataflow analysis used in program compilers, type
systems for inferring program types, model checking for program verification, and abstract interpretation
used to design abstract interpreters of programs. In particular, the abstract interpretation approach to static
analysis [2, 3] relies on a lattice-theoretical model of the notion of approximation. Program properties are
modelled by a domain C endowed with a partial order ≤ which plays the role of approximation relation,
where x ≤ y intuitively means that the property y is an approximation of the property x, or, equivalently,
that the property x is logically stronger than y. The key principle in static analysis by abstract interpretation is to provide an approximate interpretation, a.k.a. an abstract interpretation, of a program for a given
abstraction of the properties of its concrete semantics. This leads to the idea of abstract domain, which is an
1

ordered collection of abstract program properties which can be inferred by static analysis, where approximation is again modeled by the ordering relation. The classical introductory example of program abstract
interpretation is sign analysis. Given an arithmetic integer expression e, one tries to bound its sign—
negative, zero or positive—without actually computing e. The idea is that one can prove that e ≡ 3 × −2 is
negative without actually computing that e evaluates to −6. If S = {−, 0, +} then abstract integers in A are
defined as subsets of these signs in S, i.e., A , ℘(S). Here, A is ordered by inclusion which encodes the
approximation relation: for example, {+} ⊆ {0, +} encodes that being positive is a stronger property than
being nonnegative, so that nonnegative is an approximation of positive. Then, any set of integer numbers
S ∈ ℘(Z) can be abstractly represented by its most precise abstraction in A through an abstraction function
α : ℘(Z) → A. Hence, a set of integers S is correctly approximated by an abstract integer a ∈ A precisely
when α(S) ⊆ a holds. In turn, one can define abstract addition ⊕ and multiplication ⊗ on abstract integers
in A: for example, {−, 0} ⊕ {−} = {−} and {−} ⊕ {+} = {−, 0, +}, while {−} ⊗ {+, 0} = {−, 0} and
{−, +} ⊗ {0} = {0}. Hence, in order to analyze the expression 3 × −2 we convert it to α({3}) ⊗ α({−2})
to infer {−}. Of course, it may well happen that the abstract domain does not carry enough precision to
compute the most precise information theoretically available in A: for the expression −2 + 2, we have that
α({−2}) ⊕ α({2}) = {−, 0, +} although α({−2 + 2}) = {0} ( α({−2}) ⊕ α({2}). In such cases, the
output of the static analysis is “I don’t know”. In the terminology of abstract interpretation, ⊕ and ⊗ are
correct approximations of concrete integer addition and multiplication. Program semantics are typically
formalized using fixed points of functions for modelling loops and recursive procedures. A basic result of
abstract interpretation tells us that correctness is preserved for least and greatest fixed points: if a concrete
monotone function f : C → C is correctly approximated by an abstract monotone function f ♯ : A → A
on an abstraction A of C then the least (or greatest) fixed point lfp(f ) ∈ C of f is correctly approximated
by the least (or greatest) fixed point lfp(f ♯ ) ∈ A of f ♯ , i.e., α(lfp(f )) ≤A lfp(f ♯ ). For example, the
concrete output of the program P ≡ x := 3; while (x < 13) do x := 2 ∗ x is {24}, while its abstract
interpretation is derived as the least fixed point which is greater than or equal to the initial abstract value
α({3}) = {+} for the function f ♯ : A → A defined by f ♯ (a) = α({2}) ⊗ a, so that this least fixed point
is lfp≥{+} (f ♯ ) = {+}, and in this case we have that α({24}) = lfp≥{+} (f ♯ ).
Goal. The similarities between supermodular games and formal program semantics should be therefore
clear, since they both rely on order-theoretical models and on computing extremal fixed points of suitable
functions on lattices. However, while the order theory-based approximation of program semantics by static
analysis is a traditional and well-established area in computer science since forty years, to the best of
our knowledge, no attempt has been made to apply some techniques used in static program analysis for
defining a corresponding notion of approximation in supermodular games. The overall goal of this paper
is to investigate whether and how abstract interpretation can be used to define and calculate approximate
Nash equilibria of supermodular games, where the key notion of approximation will be modeled by a
partial ordering relation similarly to what happens in static program analysis. This appears to be the first
contribution to make use of an order-theoretical notion of approximation for equilibria of supermodular
games, in particular by resorting to the abstract interpretation technique ordinarily used in static program
analysis.
Contributions. As sketched above, abstract interpretation essentially relies on: (1) abstract domains A
which encode approximate properties; (2) abstract functions f ♯ which must correctly approximate on A
the behavior of some concrete operations f ; (3) results of correctness for the abstract interpreter using A
and f ♯ , for example the correctness of extremal fixed points of abstract functions, e.g. lfp(f ♯ ) correctly
approximates lfp(f ); (4) so-called widening/narrowing operators tailored for the abstract domains A to
ensure and/or accelerate the convergence in iterative fixed point computations of abstract functions f ♯ . We
contribute to set up a general framework for designing abstract interpretations of supermodular games which
basically encompasses the above points (1)-(3), while widening/narrowing operators are not taken into
account since their definition is closely related to some individual abstract domain. Our main contributions
can be summarized as follows.
• In supermodular games, a strategy space Si for the player i is assumed to be a complete lattice and
best response correspondences are (multivalued) functions defined over a product S1 × · · · × SN of
complete lattices which plays the role of concrete domain. Thus, as a preliminary step, we show how
abstractions of strategy spaces can be composed in order to define an abstract domain of the product
2

S1 ×· · ·×SN , and, on the other hand, an abstraction of the product S1 ×· · ·×SN can be decomposed
into abstract domains of the individual Si ’s.
• Abstract interpretation is commonly used for approximating single-valued functions on complete
lattices. For supermodular games, best responses are indeed multivalued functions B : S1 × · · · ×
SN → ℘(S1 × · · · × SN ) that we expect to approximate. Thus, we first provide short and direct
constructive proofs ensuring the existence of fixed points for multivalued functions. Then, we show
how abstract interpretation can be generalized to handle multivalued functions, first by defining a
parametric notion of correct approximation for multivalued functions, and then by proving that these
correct abstract multivalued functions preserve their correctness for their fixed points.
• We investigate how to define an “abstract interpreter” of a supermodular game. The first approach
consists in defining a supermodular game on an abstract strategy space. Given a game Γ with strategy
spaces Si and utility functions ui : S1 × · · · × SN → R, this means that we assume a family of
abstractions Ai , one for each Si , that gives rise to an abstract strategy space A = A1 × · · · × AN , and
a suitable abstract restriction of the utility functions uA
i : A1 × · · · × AN → R. This defines what
we call an abstract game ΓA , which, under some conditions, has abstract equilibria which correctly
approximate the equilibria of Γ. Obviously, the fixed point computations over A for the abstract
game ΓA should be more efficient than in Γ. This abstraction technique provides a generalization
of the efficient algorithm by Echenique [9] for finding all equilibria in a finite game with strategic
complementarities.
• On the other hand, we put forward a second notion of abstract game where the strategy spaces are
subject to a kind of partial approximation, meaning that, for any utility function, we consider approximations of the strategy spaces of the “other players”, i.e., correct approximations over abstract
domains Ai of the functions ui (si , ·) : S1 × · · · Si−1 × Si+1 × · · · × SN → R, for any given strategy
si ∈ Si . This abstraction technique gives rise to games having an abstract best response correspondence. This approach is inspired and somehow generalizes the implicit methodology of approximate
computation of equilibria considered by Carl and Heikkilä [1, Chapter 8].
Our results are illustrated on some examples of supermodular games, in particular a couple of examples of
Bertrand oligopoly models are taken from Carl and Heikkilä’s book [1].

2 Background
2.1 Order-Theoretical Notions
Given a function f : X → Y and a subset S ⊆ X then f (S) , {f (s) ∈ Y | s ∈ S} denotes the image of
f on S and f s : ℘(X) → ℘(Y ) denotes the corresponding standard powerset lifting of f , that is, f s (S) ,
N
f (S). Given a family of N > 0 sets (Si )N
i=1 , ×i=1 Si denotes their Cartesian product. If i ∈ [1, N ] and
N
s ∈ ×i=1 Si then S−i , S1 × · · ·× Si−1 × Si+1 × · · · SN , while s−i , (s1 , . . . , si−1 , si+1 , . . . , sN ) ∈ S−i .
Also, hRN , ≤i denotes the standard product poset of real numbers, where for s, t ∈ RN , s ≤ t iff for any
i ∈ [1, N ], si ≤ ti , while s + t = (si + ti )N
i=1 . A multivalued function, also called correspondence, is a
mapping f : X → ℘(X). An element x ∈ X is a fixed point of f when x ∈ f (x), where Fix(f ) , {x ∈
X | x ∈ f (x)}.
Let hC, ≤, ∧, ∨, ⊥, ⊤i be a complete lattice, compactly denoted by hC, ≤i. A nonempty subset S ⊆ C
is a subcomplete sublattice of C if for all its nonempty subsets X ⊆ S, ∧X ∈ S and ∨X ∈ S. Let us recall
the following relations on the powerset ℘(C): for any X, Y ∈ ℘(C),
△

(Smyth preorder)

X S Y ⇐⇒ ∀y ∈ Y.∃x ∈ X. x ≤ y

(Hoare preorder)

X H Y ⇐⇒ ∀x ∈ X.∃y ∈ Y. x ≤ y

(Egli-Milner preorder)
(Veinott relation)

△

△

X EM Y ⇐⇒ X S Y & X H Y
△

X V Y ⇐⇒ ∀x ∈ X.∀y ∈ Y. x ∧ y ∈ X & x ∨ y ∈ Y

Smyth, Hoare and Egli-Milner relations are preorders (i.e., reflexive and transitive), while Veinott relation
(also called strong set relation) is transitive and antisymmetric. A multivalued function f : C → ℘(C) is
3

S-monotone if for any x, y ∈ C, x ≤ y implies f (x) S f (y). H-, EM - and V -monotonicity are defined
analogously. We also use the following notations:
℘∧ (C) , {X ∈ ℘(C) | ∧X ∈ X}
℘⋄ (C) , ℘∧ (C) ∩ ℘∨ (C)

℘∨ (C) , {X ∈ ℘(C) | ∨X ∈ X}

SL(C) , {X ∈ ℘(C) | X 6= ∅, X subcomplete sublattice of C}

Observe that if X, Y ∈ ℘∧ (C) then X S Y ⇔ ∧X ≤ ∧Y . Similarly, if X, Y ∈ ℘∨ (C) then
X H Y ⇔ ∨X ≤ ∨Y and if X, Y ∈ ℘⋄ (C) then X EM Y ⇔ ∧X ≤ ∧Y & ∨X ≤ ∨Y .
The pointwise ordering relation ⊑ between two functions f, g : X → C whose range C is a complete
lattice, is defined by f ⊑ g if for any x ∈ X, f (x) ≤C g(x). A function f : C → D between complete
lattices is additive (co-additive) when f preserves arbitrary lub’s (glb’s). Given a function f : C → C on
a complete lattice C, Fix(f ) , {x ∈ C | x = f (x)} denotes the set of fixed points of f , while lfp(f )
and gfp(f ) denote, respectively, the least and greatest fixed points of f , when they exist. Let us recall that
least and greatest fixed points always exist for monotone functions. If f : C → C then for any ordinal
α ∈ O, the α-power f α : C → C is defined by transfinite induction as follows: for any x ∈ C, (1) if
0
β+1
α = 0 then
(x) , f (f β (x)); (3) if α = ∨{β ∈ O | β < α} then
W f (x)β, x; (2) if α = β + 1 then f
α
f (x) , β<α f (x).
A map ρ : C → C, with C complete lattice, is a (topological) closure operator when: (i) x ≤ y ⇒
ρ(x) ≤ ρ(y); (ii) x ≤ ρ(x); (iii) ρ(ρ(x)) = ρ(x). We denote by uco(hC, ≤i) the set of all closure operators
on the complete lattice C. A closure operator ρ ∈ uco(C) is uniquely determined by its image ρ(C), which
coincides with its set of fixed points Fix(ρ), as follows: for any c ∈ C, ρ(c) = ∧C {x ∈ ρ(C) | c ≤ x}.
Also, a subset S ⊆ C is the image of a closure operator ρS ∈ uco(C) iff S is meet-closed, i.e., S =
{∧C X ∈ C | X ⊆ S}; in this case, ρS (c) = ∧C {x ∈ S | c ≤ x}.
Supermodularity. Given a complete lattice C, a function u : C → RN is a supermodular if for any
c1 , c2 ∈ C, u(c1 ∨ c2 ) + u(c1 ∧ c2 ) ≥ u(c1 ) + u(c2 ), while u is quasisupermodular if for any c1 , c2 ∈ C,
u(c1 ∧ c2 ) ≤ u(c1 ) ⇒ u(c2 ) ≤ u(c1 ∨ c2 ) and u(c1 ∧ c2 ) < u(c1 ) ⇒ u(c2 ) < u(c1 ∨ c2 ). Clearly,
supermodularity implies quasisupermodularity (while the converse is not true). Recall that if u : C → RN
is quasisupermodular then argmax(f ) , {x ∈ C | ∀y ∈ C. f (y) ≤ f (x)} is a sublattice of C.
A function u : C1 × C2 → RN has increasing differences when for any (x, y) ≤ (x′ , y ′ ), u(x′ , y) −
u(x, y) ≤ u(x′ , y ′ ) − u(x, y ′ ), or, equivalently, the functions u(x′ , ·) − u(x, ·) and u(·, y ′ ) − u(·, y) are
monotone. A function u : C1 × C2 → RN has the single crossing property when for any (x, y) ≤ (x′ , y ′ ),
u(x, y) ≤ u(x′ , y) ⇒ u(x, y ′ ) ≤ u(x′ , y ′ ) and u(x, y) < u(x′ , y) ⇒ u(x, y ′ ) < u(x′ , y ′ ). Clearly, if u
has increasing differences then u has the single crossing property, while the converse does not hold.
Supermodularity on product complete lattices and increasing differences are related as follows: a function u : C1 × C2 → RN is supermodular if and only if u has increasing differences and, for any ci ∈ Ci ,
u(c1 , ·) : C2 → RN and u(·, c2 ) : C1 → RN are supermodular.

2.2 Noncooperative Games
In our model, a noncooperative game Γ = hSi , ui ini=1 for players i = 1, ..., n consists of a family of
feasible strategy spaces (Si , ≤i )ni=1 which are assumed to be complete lattices, so that the strategy space
S , ×ni=1 Si is a complete lattice for the componentwise order ≤, and of a family of utility (or payoff)
functions ui : S → RNi , with Ni ≥ 1. The i-th best response correspondence Bi : S−i → ℘(Si ) is defined
as Bi (s−i ) , {xi ∈ Si | ∀si ∈ Si . ui (si , s−i ) ≤ ui (xi , s−i )}, while the best response correspondence
B : S → ℘(S) is defined by B(s1 , ..., sn ) , ×ni=1 Bi (s−i ). A strategy s ∈ S is a pure Nash equilibrium
for Γ when s is a fixed point of B, i.e., s ∈ B(s), meaning that in s there is no feasible way for any
player to strictly improve its utility if the strategies of all the other players remain unchanged. We denote
by Eq(Γ) ∈ ℘(S) the set of Nash equilibria for Γ, so that Eq(Γ) = Fix(B).
2.2.1 (Quasi)Supermodular Games
A noncooperative Γ = hSi , ui ini=1 is supermodular when:
(1) for any i, for any s−i ∈ S−i , ui (·, s−i ) : Si → RNi is supermodular;
(2) for any i, ui (·, ·) : Si × S−i → RNi has increasing differences.

4

hs1 , ..., sn i := h⊥1 , ..., ⊥n i; //hs1 , ..., sn i := h⊤1 , ..., ⊤n i;

do ht1 , ..., tn i := hs1 , ..., sn i;
s1 := ∧1 B1 (s−1 );
...

//s1 := ∨1 B1 (s−1 );

sn := ∧n Bn (s−n );

//s1 := ∨n Bn (s−n );

while ¬(hs1 , ..., sn i = ht1 , ..., tn i)
Figure 1: Robinson-Topkis (RT) algorithm.
On the other hand, Γ is quasisupermodular (or, with strategic complementarities) when:
(1) for any i, for any s−i ∈ S−i , ui (·, s−i ) : Si → RNi is quasisupermodular;
(2) for any i, ui (·, ·) : Si × S−i → RNi has the single crossing property.
In these cases, it turns out (cf. [17, Theorems 2.8.1 and 2.8.6]) that the i-th best response correspondence
Bi : S−i → ℘(Si ) is EM -monotone, as well as the best response correspondence B : S → ℘(S).
Let us recall that, given a complete lattice C, a function f : C → RN is order upper semicontinuous if
for any chain Y ⊆ C,
lim sup f (x) ≤ f (∨C)

and

x∈Y,x→∨Y

lim sup f (x) ≤ f (∧C).
x∈Y,x→∧Y

It turns out (cf. [17, Lemma 4.2.2]) that if each ui (·, s−i ) : Si → RNi is order upper semicontinuous
then, for each s ∈ S, Bi (s−i ) ∈ SL(Si ), i.e., Bi (s−i ) is a nonempty subcomplete sublattice of Si , so
that B(s) ∈ SL(S) also holds. In particular, we have that ∧i Bi (s−i ), ∨i Bi (s−i ) ∈ Bi (s−i ) as well as
∧B(s), ∨B(s) ∈ B(s), namely, Bi (s−i ) ∈ ℘⋄ (Si ) and B(s) ∈ ℘⋄ (S). It also turns out [18, Theorem 2]
that hEq(Γ), ≤i is a complete lattice—although, in general, it is not a subcomplete sublattice of S—and
therefore Γ admits the least and greatest Nash equilibria, which are denoted, respectively, by leq(Γ) and
geq(Γ). It should be remarked that the hypothesis of upper semicontinuity for ui (·, s−i ) holds for any
finite-strategy game, namely for those games where each strategy space Si is finite. In the following, we
will consider (quasi)supermodular games which satisfy this hypothesis of upper semicontinuity.
If, given any si ∈ Si , the function ui (si , ·) : S−i → RNi is monotone then it turns out [1, Propositions 8.23 and 8.51] that geq(Γ) majorizes all equilibria, i.e., for all i and s ∈ Eq(Γ), ui (geq(Γ)) ≥ ui (s),
while leq(Γ) minimizes all equilibria.

2.3 Computing Game Equilibria
Consider a (quasi)supermodular game Γ = hSi , ui ini=1 and define the functions B∧ , B∨ : S → S as follows: B∧ (s) , ∧B(s) and B∨ (s) , ∨B(s). As recalled in Section 2.2.1, we have that B∧ (s), B∨ (s) ∈
B(s). When the image of the strategy space S for B∧ turns out to be finite, the standard algorithm [17,
Algorithm 4.3.2] for computing leq(Γ) consists
fixed point theW in applying the constructive Knaster-Tarski V
orem to the function B∧ so that leq(Γ) = k≥0 B∧k (⊥S ). Dually, we have that geq(Γ) = k≥0 B∨k (⊤S ).
In particular, this procedure can be always used for finite games. The application of the so-called chaotic
iteration in this fixed point computation provides the Robinson-Topkis (RT) algorithm [17, Algorithm 4.3.1]
in Figure 2.3, also called round-robin optimization, which is presented in its version for least fixed points,
while the statements in comments provide the version for calculating greatest fixed points.
Let us provide a running example of supermodular finite game.
Example 2.1. Consider a two players finite game Γ represented in normal form by the following doubleentry payoff matrix:

5

6
5
4
3
2
1

1
-1, -3
0, 0
3, 1
2, 2
6, 4
6, 4

2
-1, -1
0, 2
3, 3
2, 4
6, 6
5, 6

3
2, 4
3, 4
3, 5
2, 6
6, 7
5, 6

4
5, 6
6, 6
5, 6
4, 5
6, 4
4, 2

5
6, 5
7, 5
5, 5
4, 4
5, 2
3, 0

6
6, 5
6, 5
4, 4
3, 2
4, -1
2, -3

Here, S1 and S2 are both the finite chain of integers C = h{1, 2, 3, 4, 5, 6}, ≤i and u1 (x, y), u2 (x, y) :
S1 × S2 → R are, respectively, the first and second entry in the matrix element determined by row x and
column y. It turns out that both u1 and u2 have increasing differences, so that, since S1 and S2 are finite
chains, Γ is a finite supermodular game. The two best response correspondences B1 , B2 : C → SL(C) are
as follows:
B1 (1) = {1, 2}, B1 (2) = {2}, B1 (3) = {2}, B1 (4) = {2, 5}, B1 (5) = {5}, B1 (6) = {5, 6};
B2 (1) = {2, 3}, B2 (2) = {3}, B2 (3) = {3}, B2 (4) = {4},
B2 (5) = {4}, B2 (6) = {4}.
Thus, Eq(Γ) = {(2, 3), (5, 4)}, since this is the set Fix(B) of fixed points of the best response correspondence B = B1 × B2 . We also notice that u1 (·, s2 ), u2 (s1 , ·) : C → R are neither monotone nor
antimonotone. The fixed point computations of the least and greatest equilibria through the above RT
algorithm proceed as follows:


(1, 1) 7→ ∧B1 (1, 1), 1 = (1, 1) 7→ 1, ∧B2 (1, 1) = (1, 2) 7→ (2, 2) 7→ (2, 3) 7→ (2, 3) 7→ (2, 3) (lfp)
(6, 6) 7→ (∨B1 (6, 6), 6) = (6, 6) 7→ (6, ∨B2 (6, 6)) = (6, 4) 7→ (5, 4) 7→ (5, 4) 7→ (5, 4) (gfp)

2.4 Abstract Interpretation
Static program analysis relies on correct (a.k.a. sound) and computable semantic approximations. A program P is modeled by some semantics SemJP K and a static analysis of P is designed as an approximate
semantics Sem♯ JP K which must be correct w.r.t. SemJP K. This may be called global correctness of static
analysis. Any (finite) program P is a suitable composition of a number of constituents subprograms ci
and this is reflected on its global semantics SemJP K which is commonly defined by some combinations of
the semantics SemJci K of its components. Thus, global correctness of a static analysis of P is typically
derived from local correctness of static analyses for its components ci . This global vs. local picture of static
analysis correctness is very common, independently of the kind of programs (imperative, functional, reactive, etc.), of static analysis techniques (model checking, abstract interpretation, logical deductive systems,
type systems, etc.), of program properties under analysis (safety, liveness, numerical properties, pointer
aliasing, type safety, etc.). A basic and rough proof principle in static analysis is that global correctness is
derived from local correctness. In particular this applies to static program analyses that are designed using
some form of abstract interpretation. Let us consider a simplified but recurrent scenario, where SemJP K is
defined as least (or greatest) fixed point lfp(f ) of a monotone function f on some domain C of program
properties, which is endowed with a partial order that encodes the relative precision of properties. In abstract interpretation, a static analysis is then specified as an abstract fixed point computation which must
be correct for lfp(f ). This is routinely defined through an ordered abstract domain A of properties and an
abstract semantic function f ♯ : A → A that give rise to a fixed point-based static analysis lfp(f ♯ ) (whose
decidability and/or practical scalability is usually ensured by chain conditions on A, widenings/narrowings
operators, interpolations, etc.). Correctness relies on encoding approximation through a concretization map
γ : A → C and/or an abstraction map α : C → A: the approximation of some value c through an abstract
property a is encoded as α(c) ≤A a or — equivalently, when α/γ form a Galois connection — c ≤C γ(a).
Hence, global correctness translates to α(lfp(f )) ≤ lfp(f ♯ ), local correctness means α ◦ f ⊑ f ♯ ◦ α, and
the well-known “fixed point approximation lemma” [2, 3] tells us that local implies global correctness.
In standard abstract interpretation [2, 3], abstract domains, also called abstractions, are specified by
Galois connections/insertions (GCs/GIs for short). Concrete and abstract domains, hC, ≤C i and hA, ≤A i,
are assumed to be complete lattices which are related by abstraction and concretization maps α : C → A
and γ : A → C that give rise to a GC (α, C, A, γ), that is, for all a ∈ A and c ∈ C, α(c) ≤A a ⇔ c ≤C
γ(a). A GC is a GI when α ◦ γ = id. A GC is (finitely) disjunctive when γ preserves all (finite) lubs. We
6

use Abs(C) to denote all the possible abstractions of C, where A ∈ Abs(C) means that A is an abstract
domain of C specified by some GC/GI. Let us recall some well known properties of a GC (α, C, A, γ):
(1) α is additive; (2) γ is co-additive; (3) γ ◦ α : C → C is a closure operator; (4) if ρ : C → C is a closure
operator then (ρ, C, ρ(C), id) is a GI; (5) (α, C, A, γ) is a GC iff γ(A) is the image of a closure operator
on C; (6) a GC (α, C, A, γ) is (finitely) disjunctive iff γ(A) is (finitely) meet- and join-closed.
Example 2.2. Let us consider a concrete domain hC, ≤i which is a finite chain. Then, it turns out that
(α, C, A, γ) is a GC iff γ(A) is the image of a closure operator on C iff γ(A) is a any subset of C which
contains ⊤C . As an example, for the game Γ in Example 2.1, where Si is the chain of integers [1, 6], we
have that A1 = {3, 5, 6} and A2 = {2, 6} are two abstractions of C.
Example 2.3. Let us consider the ceil function on real numbers ⌈·⌉ : R → R, that is, ⌈x⌉ is the smallest
integer not less than x. Let us observe that ⌈·⌉ is a closure operator on hR, ≤i because: (1) x ≤ y ⇒ ⌈x⌉ ≤
⌈y⌉; (2) x ≤ ⌈x⌉; (3) ⌈⌈x⌉⌉ = ⌈x⌉. Therefore, the ceil function allows us to view integer numbers Z = ⌈R⌉
as an abstraction of real numbers. The ceil function can be generalized to any finite fractional part of real
N
x⌉
numbers: given any integer number N ≥ 0, clN : R → R is defined as follows: clN (x) = ⌈10
10N . For
N = 0, clN (x) = ⌈x⌉, while for N > 0, clN (x) is the smallest rational number with at most N fractional
digits not less than x. For example, if x ∈ R and 1 < x ≤ 1.01 then cl2 (x) = 1.01. Clearly, it turns out
that clN is a closure operator which permits to cast rational numbers with at most N fractional digits as an
abstraction of real numbers.
Let f : C → C be some concrete monotone function—to keep notation simple, we consider 1-ary
functions—and let f ♯ : A → A be a corresponding monotone abstract function defined on some abstraction A specified by a GC (α, C, A, γ). Then, f ♯ is a correct (or sound) approximation of f on A when
f ◦ γ ⊑ γ ◦ f ♯ holds. If f ♯ is a correct approximation of f then we also have fixed point correctness, that
is, lfp(f ) ≤C γ(lfp(f ♯ )) and gfp(f ) ≤C γ(gfp(f ♯ )). The abstract function f A , α ◦ f ◦ γ : A → A is
called the best correct approximation of f on A, because any abstract function f ♯ is correct iff f A ⊑ f ♯ .
Hence, f A plays the role of the best possible approximation of f on the abstraction A.

3 Abstractions on Product Domains
Let us show how abstractions of different concrete domains Ci can be composed in order to define an
abstract domain of the product domain ×i Ci , and, on the other hand, an abstraction of a product ×i Ci can
be decomposed into abstract domains of the component domains Ci . In the following, we consider a finite
family of complete lattices hCi , ≤i ini=1 , while product domains are considered with the componentwise
ordering relation.
Product Composition of Abstractions. This method has been introduced by Cousot and Cousot in [6,
Section 4.4]. Given a family of GCs (αi , Ci , Ai , γi )ni=1 , one can easily define a componentwise abstraction (α, ×ni=1 Ci , ×ni=1 Ai , γ) of the product complete lattice ×ni=1 Ci , where ×ni=1 Ci and ×ni=1 Ai are both
complete lattices w.r.t. the componentwise partial order and for any c ∈ ×ni=1 Ci and a ∈ ×ni=1 Ai ,
α(c) , (αi (ci ))ni=1 ,

γ(a) , (γi (ai ))ni=1 .

For any i, we also use the function γ−i : A−i → C−i to denote γ−i (a−i ) = γ(a)−i = (γj (aj ))j6=i .
Lemma 3.1. (α, ×ni=1 Ci , ×ni=1 Ai , γ) is a GC. Moreover, if each (αi , Ci , Ai , γi ) is a (finitely) disjunctive
GC then (α, ×ni=1 Ci , ×ni=1 Ai , γ) is a (finitely) disjunctive GC.
In static program analysis, (α, ×ni=1 Ci , ×ni=1 Ai , γ) is called a nonrelational abstraction since, intuitively,
the product abstraction ×ni=1 Ai does not take into account any relationship between the different concrete
domains Ci .
Decomposition of Product Abstractions. Let us show that any GC (α, ×ni=1 Ci , A, γ) for the concrete
product domain ×ni=1 Ci induces corresponding abstractions (αi , Ci , Ai , γi ) of Ci as follows:
– Ai , {ci ∈ Ci | ∃a ∈ A.γ(a)i = ci } ⊆ Ci , endowed with the partial order ≤i of Ci ;
7

– for any ci ∈ Ci , αi (ci ) , γ(α(ci , ⊥−i ))i ;
– for any xi ∈ Ai , γi (xi ) , xi .
Lemma 3.2. (αi , Ci , Ai , γi ) is a GC. Moreover, this GC is (finitely) disjunctive when (α, ×ni=1 Ci , A, γ) is
(finitely) disjunctive.
Proof. Let us show that Ai ⊆ Ci is meet-closed. If X ⊆ Ai then for any x ∈ X there exists some
ax ∈ A such that γ(ax )i = x. Then, let a , ∧A {ax ∈ A | x ∈ X} ∈ A. Since γ preserves arbitrary
meets, we have that γ(a) = ∧C {γ(ax ) ∈ C | x ∈ X}, so that γ(a)i = ∧Ci X, that is, ∧Ci X ∈ Ai .
Hence, since Ai is a Moore-family of Ci , we have that γi = id : Ai → Ci preserves arbitrary meets and
therefore is a concretization function. Let us check that αi is the left adjoint of γi , i.e., for any ci ∈ Ci ,
αi (ci ) = γ(α(ci , ⊥−i ))i = ∧Ci {xi ∈ Ai | ci ≤i xi }. On the one hand, since (ci , ⊥−i ) ≤ γ(α(ci , ⊥−i )),
we have that ci ≤ γ(α(ci , ⊥−i ))i , so that since γ(α(ci , ⊥−i ))i ∈ Ai , we conclude that ∧Ci {xi ∈ Ai | ci ≤i
xi } ≤i γ(α(ci , ⊥−i ))i . On the other hand, if xi ∈ Ai and ci ≤i xi then xi = γ(a)i for some a ∈ A,
so that we have that (ci , ⊥−i ) ≤ γ(a), therefore γ(α(ci , ⊥−i )) ≤ γ(α(γ(a))) = γ(a), and, in turn,
γ(α(ci , ⊥−i ))i ≤i γ(a)i = xi , which implies that γ(α(ci , ⊥−i ))i ≤i ∧Ci {xi ∈ Ai | ci ≤i xi }. Finally,
let us observe that if γ is (finitely) additive and X ⊆ Ai so that for any x ∈ X there exists some ax ∈ A
such that γ(ax )i = x then γ(∨A {ax ∈ A | x ∈ X}) = ∨{γ(ax ) ∈ ×ni=1 Ci | x ∈ X}, so that γ(∨A {ax ∈
A | x ∈ X})i = ∨i γ(ax )i = ∨i X, namely, ∨i X ∈ Ai , meaning that γi = id is (finitely) additive.
A GC (α, ×ni=1 Ci , A, γ) is called nonrelational when it is isomorphic to the product composition, according to Lemma 3.1, of its components obtained by Lemma 3.2. Of course, the product composition by
Lemma 3.1 of abstract domains is trivially nonrelational. Otherwise, (α, ×ni=1 Ci , A, γ) is called relational.
It is worth remarking that if A is relational then A cannot be obtained as a product of abstractions of C.
As a consequence, the relationality of an abstraction A prevents the definition of a standard noncooperative
game over the strategy space A since A cannot be obtained as a product domain.
Example 3.3. Let us consider the game Γ in Example 2.1 whose finite strategy space is C × C, where
C = {1, 2, 3, 4, 5, 6} is a chain. Consider the subset A ⊆ C × C as depicted by the following diagram
where the ordering is induced from C × C:
(6, 6)
(4, 5)
(4, 4)

(3, 5)
(3, 4)
(2, 2)

Since A is meet- and join-closed and includes the greatest element (6, 6) of C × C, we have that A is
a disjunctive abstraction of C × C, where α : C × C → A is the closure operator induced by A and
γ : A → C × C is the identity. Observe that A is relational since its decomposition by Lemma 3.2 provides
A1 = {2, 3, 4, 6} and A2 = {2, 4, 5, 6}, and the product composition A1 × A2 by Lemma 3.1 yields a more
expressive abstraction than A, for example (2, 4) ∈ (A1 × A2 ) r A.
On the other hand, for the abstractions A1 = {3, 5, 6} and A2 = {2, 6} of Example 2.2, by Lemma 3.1,
the product domain A1 × A2 is a nonrelational abstraction of C × C.

4 Approximation of Multivalued Functions
Let us show how abstract interpretation can be applied to approximate least and greatest fixed points of
multivalued functions.

8

4.1 Constructive Results for Fixed Points of Multivalued Functions
Let C be a complete lattice, f : C → ℘(C) be a multivalued function and f∧ , f∨ : C → C be the functions
defined as: f∧ (c) , ∧f (c) and f∨ (c) , ∨f (c). The following constructive result ensuring the existence
of least fixed points for a multivalued function is given in [15, Propositions 3.10 and 3.24]. We provide
here a shorter and more direct constructive proof than in [15] which is based on the constructive version of
Tarski’s fixed point theorem given by Cousot and Cousot [4].
Lemma
4.1. If f : C → ℘∧ (C) is S-monotone then f has the least fixed point lfp(f ). Moreover, lfp(f ) =
W
α
α∈O f∧ (⊥).
Proof. By hypothesis, f (x) ∈ ℘∧ (C), so that f∧ (x) ∈ f (x). If x, y ∈ C and x ≤ y then, by hypothesis,
f (x) S f (y), therefore, since f∧ (y) ∈ f (y), there exists some z ∈ f (x) such that z ≤ f∧ (y), and,
in turn, f∧ (x) ≤ z ≤ f∧ (y). Hence, since f∧ is a monotone function on a complete lattice, by Tarski’s
theorem, its least fixed point lfp(f∧ ) ∈
W C exists. Furthermore, by the constructive version of Tarski’s
theorem [4, Theorem 5.1], lfp(f∧ ) = α∈O f∧α (⊥). We have that lfp(f∧ ) = f∧ (lfp(f∧ )) ∈ f (lfp(f∧ )),
hence lfp(f∧ ) ∈ Fix(f ). Consider any z ∈ Fix(f ). We prove by transfinite induction that for any α ∈ O,
f∧α (⊥) ≤ z. If α = 0 then f∧0 (⊥) = ⊥ ≤ z. If α = β + 1 then f∧α (⊥) = f∧ (f∧β (⊥)), and, since, by
inductive hypothesis, f∧β (⊥) ≤ z, then, by monotonicity ofWf∧ , f∧ (f∧β (⊥)) ≤ f∧ (z) = ∧f (z) ≤ z. If
α = ∨{β ∈ O | β < α} is a limit ordinal then f∧α (⊥) = β<α f∧β (⊥); since, by inductive hypothesis,
f∧β (⊥) ≤ z for any β < α, we obtain that f∧α (⊥) ≤ z. This therefore shows that f has the least fixed point
lfp(f ) = lfp(f∧ ).
By duality, as consequences of the above result, we obtain the following characterizations, where
point (3) coincides with Zhou’s theorem (see [18, Theorem 1] and [15, Proposition 3.15]), which is used
for showing that pure Nash equilibria of a supermodular game form a complete lattice.
Corollary 4.2.
V
(1) If f : C → ℘∨ (C) is H-monotone then f has the greatest fixed point gfp(f ) = α∈O f∨α (⊤).
(2) If f : C → ℘⋄ (C) is EM
then f has the least and greatest fixed points, where lfp(f ) =
V -monotone
W
α
α
f
(⊤).
f
(⊥)
and
gfp(f
)
=
α∈O ∨
α∈O ∧
(3) If f : C → SL(C) is EM -monotone then hFix(f ), ≤i is a complete lattice.
(4) If f, g : C → SL(C) are EM -monotone and, for any c ∈ C, f (c) EM g(c) then Fix(f ) EM Fix(g).
Proof. Let us prove point (4). By Point (3), both Fix(f ) and Fix(g) are complete lattices for ≤. Thus,
Fix(f ) EM Fix(g) holds iff ∧ Fix(f ) = lfp(f ) ≤ lfp(g) = ∧ Fix(g) and ∨ Fix(f ) = gfp(f ) ≤
gfp(g) = ∨ Fix(g). Moreover, since, for any c ∈ C, f (c) EM g(c), we also have that f∧ (c) = ∧f (c) ≤
∧f (c) = g∧ (c), thus, as a consequence, lfp(f∧ ) ≤ lfp(g∧ ). The proof of Lemma 4.1 shows that lfp(f ) =
lfp(f∧ ) and lfp(g) = lfp(g∧ ), so that we obtain lfp(f ) ≤ lfp(g). The proof for gfp(f ) ≤ gfp(g) is dual.

4.2 Concretization-based Approximations
As discussed in [5], a minimal requirement for defining an abstract domain consists in specifying the meaning of its abstract values through a concretization map. Let hA, ≤A i be an abstraction of a concrete domain
C specified by a monotone concretization map γ : A → C. Let us observe that the powerset lifting
γ s : ℘(A) → ℘(C) is S-monotone, meaning that if Y1 S Y2 then γ s (Y1 ) S γ s (Y2 ): if γ(y2 ) ∈ γ s (Y2 )
then there exists y1 ∈ Y1 such that y1 ≤A y2 , so that γ(y1 ) ∈ γ s (Y1 ) and γ(y1 ) ≤C γ(y2 ), i.e.,
γ s (Y1 ) S γ s (Y2 ). Analogously, γ s is H- and EM -monotone. Consider a concrete S-monotone multivalued function f : C → ℘∧ (C), whose least fixed point exists by Lemma 4.1.
Definition 4.3 (Correct Approximation of Multivalued Functions). An abstract multivalued function
f ♯ : A → ℘(A) over A is a S-correct approximation of f when:
(1) f ♯ : A → ℘∧ (A) and f ♯ is S-monotone

(fixed point condition)

(2) for any a ∈ A, f (γ(a)) S γ s (f ♯ (a))

(soundness condition)

H- and EM -correct approximations are defined by replacing in this definition S- with, respectively, H- and
EM -, and ℘∧ with, respectively, ℘∨ and ℘⋄ .

9

Let us point out that the soundness condition (2) is the standard correctness requirement used in abstract
interpretation, as recalled in Section 2.4. The difference here is that C2 and A2 are mere preorders rather
than partial orders. However, this is enough for guaranteeing a correct approximation of least fixed points.
Theorem 4.4 (Correct Least Fixed Point Approximation). If f ♯ is a S-correct approximation of f then
lfp(f ) ≤C γ(lfp(f ♯ )).
Proof. Let us consider f∧ : C → C and f∧♯ : A → A. By Lemma 4.1, lfp(f ) = lfp(f∧ ) and lfp(f ♯ ) =
lfp(f∧♯ ). Let us check that f∧♯ is a standard correct approximation of f∧ . For any a ∈ A, γ(f∧♯ (a)) ∈
γ s (f ♯ (a)), hence, since f (γ(a)) S γ s (f ♯ (a)), we have that there exists some z ∈ f (γ(a)) such that
z ≤ γ(f∧♯ (a)), so that f∧ (γ(a) = ∧f (γ(a)) ≤ z ≤ γ(f∧♯ (a)). Hence, by the concretization-based fixed
point transfer (see [13, Theorem 2.2.4]), it turns out that lfp(f∧ ) ≤C γ(lfp(f∧♯ )), therefore showing that
lfp(f ) ≤ γ(lfp(f ♯ )).
Dual results hold for H- and EM -correct approximations.
Corollary 4.5.
(1) If f ♯ is a H-correct approximation of f then gfp(f ) ≤C γ(gfp(f ♯ )).
(2) If f ♯ is a EM -correct approximation of f then Fix(f ) EM γ s (Fix(f ♯ )), in particular, lfp(f ) ≤C
γ(lfp(f ♯ )) and gfp(f ) ≤C γ(gfp(f ♯ )).
Proof. By duality from Theorem 4.4. In particular, point (2) follows because, by Corollary 4.2, Fix(f ) ∈
℘⋄ (C), Fix(f ♯ ) ∈ ℘⋄ (A) and therefore γ s (Fix(f ♯ )) ∈ ℘⋄ (C), so that Fix(f ) EM γ s (Fix(f ♯ )) iff
lfp(f ) ≤ γ(lfp(f ♯ )) and gfp(f ) ≤ γ(gfp(f ♯ )).
The approximation of least/greatest fixed points of multivalued functions can also be easily given for an
abstraction map α : C → A. In this case, a S-monotone map f ♯ : A → ℘∧ (A) is a correct approximation
of a concrete S-monotone map f : C → ℘∧ (C) when, for any c ∈ C, αs (f (c)) S f ♯ (α(c)), where
αs : ℘(C) → ℘(A). Here, fixed point approximation states that α(lfp(f )) ≤A lfp(f ♯ ).

4.3 Galois Connection-based Approximations
Let us now consider the ideal case of abstract interpretation where the best approximations in an abstract
domain A of concrete objects always exist, that is, A is specified by a GC (α, C, A, γ). However, recall
that here h℘∧ (C), S i and h℘∧ (A), S i are mere preorders, and not posets. Then, given two preorders
hX, X i and hY, Y i, we say that two functions β : X → Y and δ : Y → X specify a preorder-GC
(β, X, Y, δ) when δ and β are monotone (meaning, e.g. for β, that x X x′ ⇒ β(x) Y β(x′ )) and the
equivalence β(x) Y y ⇔ x X δ(y) holds. As expected, it turns out that GCs induce preorder-GCs for
Smyth, Hoare and Egli-Milner preorders.

Lemma 4.6. Let (α, C, A, γ) be
a Galois connection. Then, αs , h℘∧ (C), S i, h℘∧ (A), S i, γ s , αs ,

h℘∨ (C), H i,h℘∨ (A), H i, γ s , and αs , h℘⋄ (C), EM i, h℘⋄ (A), EM i, γ s are preorder-Galois connections.
Proof. Let us check that αs is S-monotone: if X S Y and α(y) ∈ αs (Y ) then there exists x ∈ X such
that x ≤C y, so that, by monotonicity of α, α(x) ≤A α(y), and therefore αs (X) S αs (Y ). Analogously,
γ s is S-monotone. Let us check that αs (X) S Y ⇒ X S γ s (Y ): if γ(y) ∈ γ s (Y ) then there exists
α(x) ∈ αs (X) such that α(x) ≤A y, and, since (α, C, A, γ) is a GC, this implies that x ≤C γ(y), so that
s
s
X S γ s (Y ). Analogously, it turns
 out that X S γ (Y ) ⇒ α (X) S Y . Hence, this shows that
s
∧
∧
s
α , h℘ (C), S i, h℘ (A), S i, γ is a preorder-GC. The proofs for Hoare and Egli-Milner preorders are
analogous.
The ideal Galois connection-based framework allows us to define best correct approximations of multivalued functions. If f : C → ℘(C) and (α, C, A, γ) is a GC then its best correct approximation on the
abstract domain A is the multifunction f A : A → ℘(A) defined as follows: f A (a) , αs (f (γ(a))). In particular, if f : C → ℘∧ (C) is S-monotone then f A : A → ℘∧ (A) turns out to be S-monotone. Analogously
for Hoare and Egli-Milner preorders. Similarly to standard abstract interpretation [3], it turns out that f A is
the best among the S-correct approximations of f , as formalized by the following result.

10

Lemma 4.7. A S-monotone correspondence f ♯ : A → ℘∧ (A) is a S-correct approximation of f iff for any
a ∈ A, f A (a) S f ♯ (a). Also, analogous characterizations hold for H- and EM -correct approximations.
Proof. An easy consequence of Lemma 4.6, since for any a ∈ A, f A (a) = αs (f (γ(a)) S f ♯ (a) iff for
any a ∈ A, f (γ(a)) S γ s (f ♯ (a)).
Hence, it turns out that the fixed point approximations given by Theorem 4.4 and Corollary 4.5 apply to
the best correct approximations f A .
Completeness. In abstract interpretation, completeness [3, 10] formalizes an ideal situation where the
abstract function f ♯ on A is capable of not losing information w.r.t. the abstraction in A of the concrete
function f , that is, the equality α(f (c)) = f ♯ (α(c)) always holds. As a key consequence, completeness
lifts to fixed points, meaning that α(lfp(f )) = lfp(f ♯ ) holds. Let us show that this also holds for multivalued
functions. An abstract S-monotone function f ♯ : A → ℘∧ (A) is a complete approximation of a S-monotone
function f : C → ℘∧ (C) when for any c ∈ C, αs (f (c)) = f ♯ (α(c)).
Lemma 4.8 (Complete Least Fixed Point Approximation). If f ♯ is a complete approximation of f then
α(lfp(f )) = lfp(f ♯ ).
Proof. By Lemma 4.1, lfp(f ) = lfp(f∧ ) and lfp(f ♯ ) = lfp(f∧♯ ). Since f∧ (c) ∈ f (c), we have that
α(f∧ (c)) ∈ αs (f (c)), so that α(f∧ (c)) = ∧αs (f (c)). By hypothesis, ∧αs (f (c)) = ∧f ♯ (α(c)) = f∧♯ (α(c)),
so that α ◦ f∧ = f∧♯ ◦ α holds. Thus, by complete fixed point transfer [3, Theorem 7.1.0.4], α(lfp(f∧ )) =
lfp(f∧♯ ).

4.4 Approximations of Best Response Correspondences
The above abstract interpretation-based approach for multivalued functions can be applied to (quasi)supermodular games by approximating their best response correspondences. In particular, one can abstract both
the i-th best response correspondences Bi : S−i → SL(Si ) and the overall best response B : S → SL(S).
Example 4.9. Let us consider the game Γ in Example 2.1 and the abstraction A of its strategy space C × C
defined in Example 3.3. Then, one can define the best correct approximation B A in A of the best response
function B : C × C → SL(C × C), that is, B A : A → ℘(A) is defined as B A (a) , αs (B(γ(a)) =
αs (B(a)) = {α(s1 , s2 ) ∈ A | (s1 , s2 ) ∈ B(a)}. We therefore have that:
B A (2, 2) = αs ({(2, 3)}) = {(3, 4)}, B A (3, 4) = αs ({(2, 3), (5, 3)}) = {(3, 4), (6, 6)},
B A (4, 4) = αs ({(2, 4), (5, 4)}) = {(3, 4), (6, 6)}, B A (3, 5) = αs ({(5, 3)}) = {(6, 6)},
B A (4, 5) = αs ({((5, 4)}) = {(6, 6)}, B A (6, 6) = αs ({(5, 4), (6, 4)}) = {(6, 6)}.
Hence, Fix(B A ) = {(3, 4), (6, 6)}. Therefore, by Theorem 4.4 and Corollary 4.5, here we have that
leq(Γ) = lfp(B) = (2, 3) ≤ (3, 4) = lfp(B A ) and geq(Γ) = gfp(B) = (5, 4) ≤ (6, 6) = gfp(B A ).

5 Games with Abstract Strategy Spaces
Let us consider a game Γ = hSi , ui ini=1 and a corresponding family G = (αi , Si , Ai , γi )ni=1 of GCs of the
strategy spaces Si . By Lemma 3.1, (α, ×ni=1 Si , ×ni=1 Ai , γ) specifies a nonrelational product abstraction of
the whole strategy space ×ni=1 Si . We define the i-th utility function uGi : ×ni=1 Ai → RNi on the abstract
strategy space ×ni=1 Ai simply by restricting ui on γ(×ni=1 Ai ) as follows: uGi (a) , ui (γ(a)). We point
out that this definition is a form of generalization of the restricted games considered by Echenique [9,
Section 2.3].
Lemma 5.1. If ui (·, s−i ) is (quasi)supermodular and all the GCs in G are finitely disjunctive then uGi (·, a−i ) :
Ai → RNi is (quasi)supermodular. Also, if ui (si , ·) is monotone then uGi (ai , ·) : A−i → RNi is monotone.

11

Proof. Let us check that uGi (·, a−i ) is supermodular:
uGi (ai ∨Ai bi , a−i ) + uGi (ai ∧Ai bi , a−i ) =
ui (γi (ai ∨Ai bi ), γ−i (a−i )) + ui (γi (ai ∧Ai bi ), γ−i (a−i )) =
ui (γi (ai ) ∨i γi (bi ), γ−i (a−i )) + ui (γi (ai ) ∧i γi (bi ), γ−i (a−i )) ≥
ui (γi (ai ), γ−i (a−i )) + ui (γi (bi ), γ−i (a−i )) =

[by definition]
[G are finitely disjunctive GCs]
[by supermodularity of ui ]
[by definition]

uGi (ai , a−i ) + uGi (bi , a−i )
The proof of quasisupermodularity is analogous. Let us also check that uGi (ai , ·) is monotone. Consider
a−i ≤ b−i , so that, by monotonicity of γ−i , we have that γ−i (a−i ) ≤ γ−i (b−i ). Hence, by monotonicity of
ui (γi (ai ), ·), we obtain: uGi (ai , a−i ) = ui (γi (ai ), γ−i (a−i )) ≤ ui (γi (ai ), γ−i (b−i )) = uGi (ai , b−i ).
Let us also observe that if ui (si , s−i ) has increasing differences (the single crossing property), X ⊆
×ni=1 Si is any subset of the strategy space and ui/X : X → RNi is the mere restriction of ui to the subset
X then ui/X still has increasing differences (the single crossing property). Hence, in particular, this holds
for uGi : ×ni=1 Ai → R. As a consequence of this and of Lemma 5.1, we obtain the following abstract
(quasi)supermodular games.
Corollary 5.2. If Γ = hSi , ui ini=1 is a (quasi)supermodular game and G = (αi , Si , Ai , γi )ni=1 is a family
of finitely disjunctive GCs then ΓG , hAi , uGi ini=1 is a (quasi)supermodular game.
Let us see an array of examples of abstract games.
Example 5.3. Consider the game Γ in Example 2.1 and the product abstraction A1 × A2 ∈ Abs(S1 × S2 )
defined in Example 3.3. The restricted game Γ♯ of Lemma 5.1 on the abstract strategy space {3, 5, 6} ×
{2, 6} is therefore specified by the following payoff matrix:

6
5
3

2
-1, -1
0, 2
2, 4

6
6, 5
6, 5
3, 2

Since both A1 and A2 are trivially disjunctive abstractions, by Corollary 5.2, it turns out that Γ♯ is supermodular. The best response correspondences Bi♯ : A−i → SL(Ai ) for the supermodular game Γ♯ are
therefore as follows:
B1♯ (2) = {3}, B1♯ (6) = {5, 6}, B2♯ (3) = {2}; B2♯ (5) = {6}, B2♯ (6) = {6}.
We observe that B2♯ is not a S-correct approximation of B2 because: B2 (3) = {3} 6 S {2} = B2♯ (3).
Indeed, it turns out that Eq(Γ♯ ) = {(3, 2), (5, 6), (6, 6)}, so that leq(Γ) = (2, 3) 6≤ (3, 2) = leq(Γ♯ ). Thus,
in this case, the solutions of the abstract game Γ♯ do not correctly approximate the solutions of Γ.
Instead, following Section 4.4 and analogously to Example 4.9, one can define the best correct approximation B A : A → SL(A) in A , A1 × A2 of the best response correspondence B of Γ, that is,
B A (a1 , a2 ) = {(α1 (s1 ), α2 (s2 )) ∈ A | (s1 , s2 ) ∈ B(a1 , a2 )} acts as follows:
B A (3, 2) = {(3, 6)}, B A (3, 6) = {(5, 6), (6, 6)}, B A (5, 2) = {(3, 6)},
B A (5, 6) = {(5, 6), (6, 6)}, B A (6, 2) = {(3, 6)}, B A (6, 6) = {(5, 6), (6, 6)}.
Hence, Fix(B A ) = {(5, 6), (6, 6)}, so that leq(Γ) = lfp(B) = (2, 3) ≤ (5, 6) = lfp(B A ) and geq(Γ) =
gfp(B) = (5, 4) ≤ (6, 6) = gfp(B A ).
Example 5.4. In Example 5.3, let us consider the abstraction A2 = {4, 6} ∈ Abs(S2 ), so that the supermodular game Γ♯ is given by the following payoff matrix:
6
5
3

4
5, 6
6, 6
4, 5
12

6
6, 5
6, 5
3, 2

while the best response correspondences Bi♯ become:
B1♯ (4) = {5}, B1♯ (6) = {5, 6}, B2♯ (3) = {4}; B2♯ (5) = {4}, B2♯ (6) = {4}.
Thus, here we have that Eq(Γ♯ ) = {(5, 4)}. In this case, it turns out that Bi♯ is a EM -correct approximation
of Bi , so that, by Corollary 4.5 (2), Eq(Γ) = Fix(B) = {(2, 3), (5, 4)} EM {(5, 4)} = Fix(B ♯ ) =
Eq(Γ♯ ) holds.
Example 5.5. Here, we consider the disjunctive abstractions A1 = {4, 5, 6} ∈ Abs(S1 ) and A2 =
{3, 4, 5, 6} ∈ Abs(S2 ). In this case, we have the following supermodular abstract game Γ♯ over A1 × A2 :

6
5
4

3
2, 4
3, 4
3, 5

4
5, 6
6, 6
5, 6

5
6, 5
7, 5
5, 5

6
6, 5
6, 5
4, 4

where the best response functions Bi♯ are therefore as follows:
B1♯ (3) = {4, 5}, B1♯ (4) = {5}, B1♯ (5) = {5}, B1♯ (6) = {5, 6};
B2♯ (4) = {4},
B2♯ (5) = {4}, B2♯ (6) = {4}.
Here, it turns out that Bi♯ is a EM -correct approximation of Bi , so that the abstract best response B ♯ :
A1 × A2 → SL(A1 × A2 ) is a EM -correct approximation of B. Then, by Corollary 4.5 (2), we have that
Eq(Γ) = Fix(B) = {(2, 3), (5, 4)} EM {(5, 4)} = Fix(B ♯ ) = Eq(Γ♯ ).
Thus, for the concrete supermodular game Γ of Example 2.1, while the abstract games of Examples 5.4
and 5.5 can be viewed as correct approximations of Γ, this instead does not hold for the abstract game in
Example 5.3. The following results provide conditions that justify these different behaviors.
Theorem 5.6 (Correctness of Games with Abstract Strategy Spaces). Let G = (αi , Si , Ai , γi )ni=1 be
a family of finitely disjunctive GIs, S = ×ni=1 Si , A = ×ni=1 Ai and (α, S, A, γ) be the nonrelational
product composition of G. Let Γ = hSi , ui ini=1 be a (quasi)supermodular game, with best response B,
and ΓG = hAi , uGi ini=1 be the
(quasi)supermodular game, with best response B G .
V
W corresponding abstract
Assume that for any a ∈ A, S B(γ(a)) ∨S γ( A B G (a)) ∈ γ(A). Then, Eq(Γ) EM γ s (Eq(ΓG )) and,
in particular, leq(Γ) ≤ γ s (leq(ΓG )) and geq(Γ) ≤ γ s (geq(ΓG )).
Proof. We have that Eq(Γ) = Fix(B) and Eq(ΓG ) = Fix(B G ), where B : S → ℘⋄ (S) and B G : A →
s
G
℘⋄ (A) are EM -monotone. Thus, by Corollary 4.5 (2), in order to prove that Eq(Γ)
W EM γ (Eq(Γ ))
s
G
it is enough to prove that for any a ∈ A, B(γ(a)) EM γ (B (a)). Let h , S B(γ(a)) ∈ S, so
V
that h ∈ B(γ(a)), and k , A B G (a) ∈ A, so that, by Corollary 5.2, k ∈ B G (a). By hypothesis, we
have that h ∨S γ(k) ∈ γ(A). Let us consider some i ∈ [1, n]. Therefore, hi ∨i γi (ki ) ∈ γi (Ai ), that is,
hi ∨i γi (ki ) = γi (bi ), for some bi ∈ Ai . Hence, since ki ∈ BiG (a−i ), we have that
ui (hi ∨i γi (ki ), γ−i (a−i )) = ui (γi (bi ), γ−i (a−i )) = uGi (bi , a−i ) ≤ uGi (ki , a−i ) = ui (γi (ki ), γ−i (a−i )).
On the other hand, since hi ∈ Bi (γ(a)−i ) = Bi (γ−i (a−i )), we have that ui (hi ∧i γi (ki ), γ−i (a−i )) ≤
ui (hi , γ−i (a−i )). Furthermore, since ui is supermodular, we also have that
ui (hi ∧i γi (ki ), γ−i (a−i )) + ui (hi ∨i γi (ki ), γ−i (a−i )) ≥ ui (hi , γ−i (a−i )) + ui (γi (ki ), γ−i (a−i )).
We therefore obtain:
ui (hi , γ−i (a−i )) + ui (γi (ki ), γ−i (a−i )) ≥ ui (hi ∧i γi (ki ), γ−i (a−i )) + ui (hi ∨i γi (ki ), γ−i (a−i ))
≥ ui (hi , γ−i (a−i )) + ui (γi (ki ), γ−i (a−i ))
so that
ui (hi , γ−i (a−i )) + ui (γi (ki ), γ−i (a−i )) = ui (hi ∧i γi (ki ), γ−i (a−i )) + ui (hi ∨i γi (ki ), γ−i (a−i ))
13

and, in turn, ui (hi ∧i γi (ki ), γ−i (a−i )) = ui (hi , γ−i (a−i )) and uGi (bi , a−i ) = ui (hi ∨i γi (ki ), γ−i (a−i )) =
ui (γi (ki ), γ−i (a−i )) = uGi (ki , a−i ). Thus, hi ∧i γi (ki ) ∈ Bi (γ−i (a−i )) and hi ∨i γi (ki ) ∈ γi (BiG (a−i )).
Therefore, it turns out that h∧γ(k) ∈ B(γ(a)) and h∨γ(k) ∈ γ s (B G (a)). Hence, if s ∈ B(γ(a)) then s ≤
h ≤ h ∨ γ(k) ∈ γ s (B G (a)), while if t ∈ γ s (B G (a)) then t = γ s (d), for some d ∈ B G (a), so that k ≤A d
and, in turn, t = γ s (d) ≥ γ(k) ≥ h ∧ γ(k) ∈ B(γ(a)), thus showing that B(γ(a)) EM γ s (B G (a)). The
proof for quasisupermodular games is analogous.
As a consequence of the above result, we obtain a generalization of [9, Lemma 4], which is the basis
for designing the efficient algorithm in [9, Section 4] that computes all the Nash equilibria in a finite game
with strategic complementarities. A GC (α, C, A, γ) is called a principal filter GC when the image γ(A) is
the principal filter at γ(⊥A ), that is, γ(A) = {c ∈ C | γ(⊥A ) ≤ c}.
Corollary 5.7. Let G = (αi , Si , Ai , γi )ni=1 be principal filter GCs. Then, Eq(Γ) EM γ s (Eq(ΓG )).
Proof. Observe that the product (α,W
×ni=1 Si , ×ni=1 Ai , γ)
Then, this is a straight
V GC.
V is a Gprincipal filter
G
B
(a))
≥ γ((⊥Ai )ni=1 ), so
B
(a))
≥
γ(
B(γ(a))
∨
γ(
consequence
of
Theorem
5.6,
since
S
A
A
S
V
W
G
that S B(γ(a)) ∨S γ( A B (a)) ∈ γ(A) holds.
Example 5.8. Let us consider the following finite supermodular game ∆ taken from [1, Example 8.11],
which is an example of the well known Bertrand oligopoly model [17]. Players i ∈ {1, 2, 3} stand for firms
which sell substitute products pi (e.g., a can of beer), whose feasible selling prices (e.g., in euros) si range
in Si , [a, b], where the smallest price shift is 5 cents. The payoff function ui : S1 × S2 × S3 → R models
the profit of firm i:
ui (s1 , s2 , s3 ) , di (s1 , s2 , s3 )(si − ci )
where di (s1 , s2 , s3 ) gives the demand of pi , i.e., how many units of pi the firm i sells in a given time frame,
while ci is the unit cost of pi so that (si − ci ) is the profit per unit. Following [1, Example 8.11], let us
assume that:
u1 (s1 , s2 , s3 ) = (370 + 213(s2 + s3 ) + 60s1 − 230s21)(s1 − 1.10)
u2 (s1 , s2 , s3 ) = (360 + 233(s1 + s3 ) + 55s2 − 220s22)(s2 − 1.20)
u3 (s1 , s2 , s3 ) = (375 + 226(s1 + s2 ) + 50s3 − 200s23)(s3 − 1.25)
As shown in general in [1, Corollary 8.9], it turns out that each payoff function ui has increasing differences
and ui (si , ·) is monotone, so that the game ∆ has the least and greatest price equilibria leq(∆) and geq(∆),
and geq(∆) (leq(∆)) provides the best (least) profits among all equilibria. It should be noted that [1, Example 8.11] considers as payoff functions the integer part of ui , namely, ⌊ui (s1 , s2 , s3 )⌋, however we notice
that that this definition of payoff function does not have increasing differences, so that [1, Corollary 8.9],
which assumes the hypothesis of increasing differences, cannot be applied: for example, [1, Example 8.11]
considers Si = {x/20 | x ∈ [26, 42]Z} and with (1.3, 1.3, 1.8) ≤ (1.35, 1.3, 1.85), we would have that
⌊u1 (1.35, 1.3, 1.8)⌋ − ⌊u1 (1.3, 1.3, 1.8)⌋ = ⌊173.03125⌋ − ⌊143.92⌋ = 30 >
⌊u1 (1.35, 1.3, 1.85)⌋ − ⌊u1 (1.3, 1.3, 1.85)⌋ = ⌊175.69375⌋ − ⌊146.05⌋ = 29
Instead, we consider here Si , {x/20 | x ∈ [20, 46]Z}, namely the feasible prices range from 1 to 2.3 euros
with 0.05 shift. Using the standard RT algorithm in Figure 2.3 (we made a simple C++ implementation of
RT), one obtains:
leq(∆) = (1.80, 1.90, 1.95) = geq(∆)
namely, ∆ admits a unique Nash equilibrium. It turns
V out that the algorithm RT calculates leq(∆) starting
from the bottom (1.0, 1.0, 1.0) through 12 calls to Bi (s−i ), while
W it may output the same equilibrium as
geq(∆) beginning from the top (2.3, 2.3, 2.3) through 9 calls to Bi (s−i ).
Let us consider the following abstractions Ai ∈ Abs(Si ):
A1 , {x/20 | x ∈ [35, 38]Z ∪ [42, 46]Z},

A2 , {x/20 | x ∈ [36, 46]Z},

14

A3 , {x/20 | x ∈ [38, 46]Z}.

Notice that A2 and A3 are principal filter abstractions, while this is not the case for A1 , so that Corollary 5.7
cannot be applied. We observe that:
W
{ 1 B1 (a−1 ) ∈ S1 | a−1 ∈ A2 × A3 } = {36/20, 37/20, 38/20},
W
{ 2 B2 (a−2 ) ∈ S2 | a−2 ∈ A1 × A3 } = {38/20, 39/20, 40/20},
W
{ 3 B3 (a−3 ) ∈ S3 | a−3 ∈ A1 × A2 } = {39/20, 40/20, 41/20, 42/20}.
W
The hypothesis of Theorem 5.6 is therefore satisfied, because for any a−i ∈ A−i , we have that Bi (a−i ) ∈
Ai . Hence, by Corollary 5.2, we consider the supermodular abstract game ∆A on the abstract strategy
spaces Ai . By exploiting the standard RT algorithm in Figure 2.3 for ∆A , we still obtain a unique equilibrium leq(∆A ) = (1.80, 1.90, 1.95) = geq(∆A ), so that in this case no approximation of equilibria occurs.
A
Here, RT calculates leq(∆V
) starting from the bottom (1.8, 1.8, 1.9) of A1 × A2 × A3 through 6 calls to
V
A
Bi (a−i ) and any call BiA (a−i ) scans the smaller abstract strategy space Ai instead of Si . On the
other
W hand, (1.80, 1.90, 1.95) = geq(∆) can be also calculated from the top (2.3, 2.3, 2.3) still with 9 calls
to BiA (a−i ), each scanning the reduced abstract strategy spaces Ai .

6 Games with Abstract Best Response
In the following, we put forward a notion of abstract game where the strategy spaces are subject to a form of
partial approximation by abstract interpretation, meaning that we consider approximations of the strategy
spaces of the “other players” for any utility function, i.e., correct approximations of the functions ui (si , ·),
for any given si . This approach gives rise to games having an abstract best response correspondence.
Here, we aim at providing a systematic abstraction framework for the implicit methodology of approximate
computation of equilibria considered by Carl and Heikkilä [1] in their Examples 8.58, 8.63 and 8.64.
Given a game Γ = hSi , ui ini=1 , we consider a family G = (αi , Si , Ai , γi )ni=1 of GCs and, by Lemma 3.1,
their nonrelational product (α, ×ni=1 Si , ×ni=1 Ai , γ), where we denote by ρ , γ ◦ α ∈ uco(×ni=1 Si ) the
corresponding closure operator and, for any i, by ρ−i ∈ uco(S−i ) the closure operator corresponding to
the (n − i)-th nonrelational product (α−i , ×j6=i Sj , ×j6=i Aj , γ−i ). The utility function ui,G : ×ni=1 Si → R
is then defined as follows: for any s ∈ ×ni=1 Si , ui,G (si , s−i ) , ui (si , ρ−i (s−i )).
Lemma 6.1. If ui (si , s−i ) has increasing differences (the single crossing property) then ui,G (si , s−i )
has increasing differences (the single crossing property). Also, if ui (si , ·) is monotone then ui,G (si , ·) is
monotone.
Proof. Assume that (si , s−i ) ≤ (ti , t−i ). Hence, s−i ≤−i t−i , so that, by monotonicity of ρ−i , ρ−i (s−i ) ≤−i
ρ−i (t−i ), and, in turn, (si , ρ−i (s−i )) ≤ (ti , ρ−i (t−i )). Then:
ui,G (ti , s−i ) − ui,G (si , s−i ) =
ui (ti , ρ−i (s−i )) − ui (si , ρ−i (s−i )) ≤
ui (ti , ρ−i (t−i )) − ui (si , ρ−i (t−i )) =

[by definition]
[since ui has increasing differences]
[by definition]

ui,G (ti , t−i ) − ui,G (si , t−i ).
The single crossing property for ui,G (si , s−i ) can be proved similarly. Let s−i ≤−i t−i , so that, by monotonicity of ρ−i , ρ−i (s−i ) ≤−i ρ−i (t−i ). Then, by monotonicity of ui (si , ·), we obtain: ui,G (si , s−i ) =
ui (si , ρ−i (s−i )) = ui (si , ρ−i (t−i )) = ui,G (si , t−i ), thus proving the monotonicity of ui,G (si , ·).
Moreover, let us point out that if ui (·, s−i ) is (quasi)supermodular then, obviously, ui,G (·, s−i ) remains
(quasi)supermodular as well, so that by defining the game ΓG , hSi , ui,G ini=1 we obtain the following
consequence.
Corollary 6.2. If Γ is (quasi)supermodular then ΓG is (quasi)supermodular.
We call ΓG a game with abstract best response because the i-th best response correspondence Bi,G :
S−i → SL(Si ) is such that Bi,G (s−i ) = {si ∈ Si | ∀xi ∈ Si .ui (xi , ρ−i (s−i )) ≤ ui (xi , ρ−i (s−i ))} =
Bi (ρ−i (s−i )), so that the best response correspondence satisfies BG (s) = BG (ρ(s)) = B(ρ(s)), namely,
BG can be viewed as the restriction of B to the abstract strategy space ρ(S).

15

Corollary 6.3 (Correctness of Games with Abstract Best Response). Let G = (αi , Si , Ai , γi )ni=1 be a
family of GCs. Then, Eq(Γ) EM Eq(ΓG ) and, in particular, leq(Γ) ≤ leq(ΓG ) and geq(Γ) ≤ geq(ΓG ).
Proof. Since, by Corollary 6.2, ΓG is (quasi)supermodular, we have that Eq(Γ) = Fix(B) and Eq(ΓG ) =
Fix(BG ). We have that for any s ∈ ×ni=1 Si , by extensiveness of ρ, s ≤ ρ(s), so that, since B is monotone,
we obtain B(s) EM B(ρ(s)) = BG (s). Hence, by Corollary 4.2 (4), we obtain that Fix(B) EM
Fix(BG ).
Example 6.4. Let us consider the two-player game Γ = hSi , ui i2i=1 in [1, Example 8.53], which is a further
example of Bertrand oligopoly, where S1 = S2 = [ 23 , 25 ]×[ 23 , 52 ] and the utility functions ui : S1 ×S2 → R2
are defined by ui ((si1 , si2 ), s−i ) = (ui1 (si1 , s−i ), ui2 (si2 , s−i )) ∈ R2 with

u11 (s11 , s21 , s22 ) , 52 − 21s11 + s21 + 4s22 + 8 sgn(s21 s22 − 4) (s11 − 1)

11
11
u12 (s12 , s21 , s22 ) , 51 − 21s12 − sgn(s12 − ) + 2s21 + 3s22 + 4 sgn(s21 + s22 − 4) (s12 − )
5
10

11
11
u21 (s21 , s11 , s12 ) , 50 − 20s21 − sgn(s21 − ) + 3s11 + 2s12 + 2 sgn(s11 + s12 − 4) (s21 − )
5
10

u22 (s22 , s11 , s12 ) , 49 − 20s22 + 4s11 + s12 + sgn(s11 s12 − 4) (s22 − 1)
Since any utility function uij (sij , s−i ) does not depend on si,−j , let us observe that ui (·, s−i ) : Si → R2
is supermodular. Moreover, by [1, Propositions 8.56, 8.57], we also have that ui (s1 , s2 ) has the single
crossing property, so that Γ is indeed quasisupermodular. Also, since Si is a compact (for the standard
topology) complete sublattice of R2 , we also have that ui (·, s−i ) is order upper semicontinuous, so that,
for any s ∈ S1 × S2 , the best response correspondence B satisfies B(s) ∈ SL(S1 × S2 ). Indeed, as
observed in [1, Example 8.53], it turns out that the utility functions uij (·, s−i ) : [ 32 , 25 ] → R have unique
d
maximum points denoted by fij (s−i ) which are the solutions of the equations ds
uij (s, s−i ) = 0. An easy
computation then provides:
73
1
2
4
+ s21 + s22 +
sgn(s21 s22 − 4)
42 42
21
21
247
1
1
2
f12 (s21 , s22 ) ,
+ s21 + s22 +
sgn(s21 + s22 − 4)
140 42
14
21
3
1
1
9
sgn(s11 + s12 − 4)
f21 (s11 , s12 ) , + s11 + s12 +
5 40
20
20
69
1
1
1
f22 (s11 , s12 ) ,
+ s11 + s12 +
sgn(s11 s12 − 4)
40 10
40
40

f11 (s21 , s22 ) ,

so that the best response B can be simplified as follows:


B(s11 , s12 , s21 , s22 ) = f11 (s21 , s22 ), f12 (s21 , s22 ), f21 (s11 , s12 ), f22 (s11 , s12 ) .
As shown in [1, Example 8.53], direct solutions of Γ can be obtained by solving a linear system of four
equations with four real variables and this yields the following least and greatest equilibria:
 4940854 5281784 5497457 10699993 
leq(Γ) =
,
,
,
2778745 2778745 2778745 5557490
 6033654 5848294 5885617 11224753 
,
,
,
geq(Γ) =
2778745 2778745 2778745 5557490
Carl and Heikkilä [1, Example 8.58] describe how to derive algorithmically approximate solutions of Γ by
approximating the fractional part of real numbers through the floor function, namely, the greatest rational
number with N fractional digits which is not more than a given real number. In this section we gave an
abstract interpretation-based methodology for systematically designing this kind of approximate solutions
which generalizes the approach in [1, Example 8.58]. Here, we use the ceil abstraction of real numbers
already described in Example 2.3. Thus, we consider the closure operator cl3 : [ 32 , 52 ] → [ 23 , 52 ], that is,
cl3 (x) is the smallest rational number with at most 3 fractional digits not less than x. With a slight abuse
of notation, cl3 is also used to denote the corresponding componentwise function cl3 : [ 32 , 52 ]2 → [ 23 , 52 ]2 ,
namely, cl3 (si1 , si2 ) = (cl3 (si1 ), cl3 (si1 )). Let Acl3 , { 10y3 ∈ Q | y ∈ [1500, 2500]Z} = {cl3 (x) | x ∈
[ 23 , 52 ]} (and this is a finite domain) and A , Acl3 × Acl3 . Then, (cl3 , [ 32 , 52 ], Acl3 , id) is a GC, so that, by
16

Lemma 3.1, G3 = (cl3 , Si , A, id)2i=1 is a pair of GCs. Let us denote by ΓG3 the corresponding game with
abstract best response defined in Corollary 6.2, so that ui,G3 (si , s−i ) = ui (si , cl3 (s−i )). Thus, it turns out
that the abstract best response correspondence BG3 is defined as follows:


B(s1 , s2 ) = f11 (cl3 (s2 )), f12 (cl3 (s2 )), f21 (cl3 (s1 )), f22 (cl3 (s1 ))
so that, BG3 can be restricted to the finite domain A × A and therefore has a finite range. This allows us
to compute the least and greatest equilibria of ΓG3 by the standard RT algorithm in Figure 2.3. Through a
simple C++ program, we obtain the following solutions:
 10669 6653 79139 77017 
,
,
,
leq(ΓG3 ) =
6000 3500 40000 40000
 91199 14733 42363 80793 
geq(ΓG3 ) =
,
,
,
42000 7000 20000 40000
By Corollary 6.3, we know that these are correct approximations, i.e., leq(Γ) ≤ leq(ΓG3 ) and geq(Γ) ≤
geq(ΓG3 ). Both fixed point calculations leq(ΓG3 ) and geq(ΓG3 ) need 16 calls to the abstract functions
fij (a−i ), for some a−i ∈ A−i , which provide the unique maximum points for uij (·, a−i ). It is worth
noting that, even with the precision of 3 fractional digits of cl3 , the maximum approximation for these
2148733
abstract solutions turns out to be leq(ΓG3 )22 − leq(Γ)22 = 22229960000
= 0.00009665932822.

7 Further Work
We investigated how the abstract interpretation technique, which is widely used for static program analysis,
can be applied to define and calculate approximate Nash equilibria of supermodular games, thus showing
how a notion of approximation of equilibria can be modeled by an ordering relation analogously to what
happens in the standard approaches to static analysis of the run-time behaviors of programs. To our knowledge, this is the first contribution towards the goal of approximating solutions of supermodular games by
relying on a lattice-theoretical approach. We see a number of interesting avenues for further work on this
subject. First, our notion of correct approximation of a multivalued function relies on a naive pointwise
lifting of an abstract domain, as specified by a Galois connection, to Smyth, Hoare, Egli-Milner and Veinott
preorder relations on the powerset, which is the range of best response correspondences in supermodular
games. It is worth investigating whether abstract domains can be lifted in different and more sophisticated
ways to this class of preordered powersets, in particular by taking into account that, for a certain class of
complete lattices, the Veinott ordering gives rise to complete lattices [14]. Secondly, it could be interesting
to investigate some further conditions which can guarantee the correctness of games with abstract strategy
spaces (cf. Theorem 5.6). The goal here is that of devising a notion of simulation between games whose
strategy spaces are related by some form of abstraction, in order to prove that if Γ′ simulates Γ then the
equilibria of Γ are approximated by the equilibria of Γ′ . Finally, while this paper set up the abstraction
framework by using very simple abstract domains, the general task of designing useful and expressive
abstract domains, possibly endowed with widening operators for efficient fixed point computations, for
specific classes of supermodular games is left as an open issue.
Acknowledgements. The author has been partially supported by the Microsoft Research Software Engineering Innovation Foundation 2013 Award (SEIF 2013) and by the University of Padova under the 2014
PRAT project “ANCORE”.

References
[1] S. Carl and S. Heikkilä. Fixed Point Theory in Ordered Sets and Applications. Springer, 2011.
[2] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixed points. In Proc. 4th ACM Symposium on Principles
of Programming Languages (POPL’77), pp. 238-252, ACM Press, 1977.
[3] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th ACM
Symposium on Principles of Programming Languages (POPL’79), pp. 269-282, ACM Press, 1979.
17

[4] P. Cousot and R. Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific J. Math.,
82(1):43-57, 1979.
[5] P. Cousot and R. Cousot. Abstract interpretation frameworks. J. Log. Comput., 2(4):511-547, 1992.
[6] P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages) (Invited
Paper). In Proc. of the IEEE Int. Conf. on Computer Languages (ICCL’94), pp. 95-112. IEEE Computer Society Press, 1994.
[7] C. Daskalakis, P.W. Goldberg, and C.H. Papadimitriou. The complexity of computing a Nash equilibrium. SIAM Journal on Computing, 39(1):195-259, 2009.
[8] C. Daskalakis, A. Mehta, and C.H. Papadimitriou. Progress in approximate Nash equilibria. In
Proceedings of the 8th ACM Conference on Electronic Commerce (EC’07), pp. 355-358, ACM Press,
2007.
[9] F. Echenique. Finding all equilibria in games of strategic complements. J. Economic Theory,
135(1):514-532, 2007.
[10] R. Giacobazzi, F. Ranzato and F. Scozzari. Making abstract interpretations complete. J. ACM,
47(2):361-416, 2000.
[11] E. Hazan and R. Krauthgamer. How hard is it to approximate the best Nash equilibrium? SIAM
Journal on Computing, 40(1):79-91, 2011.
[12] P. Milgrom and C. Shannon. Monotone comparative statics. Econometrica, 62(1):157?180, 1994.
[13] A. Miné. Weakly Relational Numerical Abstract Domains. PhD thesis, École Polytechnique, France,
2004.
[14] F. Ranzato. A new characterization of complete Heyting and co-Heyting algebras.
arXiv:1504.03919v1, 2015.

Preprint

[15] U. Straccia, M. Ojeda-Aciego, and C.V. Damásio. On fixed-points of multivalued functions on complete lattices and their application to generalized logic programs. SIAM Journal on Computing,
38(5):1881-1911, 2008.
[16] D.M. Topkis. Minimizing a submodular function on a lattice. Operations Research, 26(2):305–321,
1978.
[17] D.M. Topkis. Supermodularity and Complementarity. Princeton University Press, 1998.
[18] L. Zhou. The set of Nash equilibria of a supermodular game is a complete lattice. Games and
Economic Behavior, 7(2):295-300, 1994.

18

