{'fraction_non_alphanumeric': 0.06996713124570031, 'fraction_numerical': 0.011389405559660611, 'mean_word_length': 3.873711660250838, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 24, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Abstract Interpretation of Supermodular Games

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.


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 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 signnegative, 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 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 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 S i for the player i is assumed to be a complete lattice and best response correspondences are (multivalued) functions defined over a product S 1 × · · · × S N 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 S 1 ×· · ·×S N , and, on the other hand, an abstraction of the product S 1 ×· · ·×S N can be decomposed into abstract domains of the individual S i 's.
• Abstract interpretation is commonly used for approximating single-valued functions on complete lattices. For supermodular games, best responses are indeed multivalued functions B : S 1 × · · · × S N → ℘(S 1 × · · · × S N ) 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 S i and utility functions u i : S 1 × · · · × S N → R, this means that we assume a family of abstractions A i , one for each S i , that gives rise to an abstract strategy space A = A 1 × · · · × A N , and a suitable abstract restriction of the utility functions u A i : 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

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) f (S). Given a family of N > 0 sets ( Let C, ≤, ∧, ∨, ⊥, ⊤ be a complete lattice, compactly denoted by C, ≤ . 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, 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 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: 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 : } 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 . We denote by uco( C, ≤ ) 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) Supermodularity. Given a complete lattice C, a function u : C → R N is a supermodular if for any . Clearly, supermodularity implies quasisupermodularity (while the converse is not true). Recall that if u : C → R N is quasisupermodular then argmax(f ) {x ∈ C | ∀y ∈ C. f (y) ≤ f (x)} is a sublattice of C.
A function u : C 1 × C 2 → R N 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 : C 1 × C 2 → R N has the single crossing property when for any (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 : C 1 × C 2 → R N is supermodular if and only if u has increasing differences and, for any c i ∈ C i , u(c 1 , ·) : C 2 → R N and u(·, c 2 ) : C 1 → R N are supermodular.

Noncooperative Games
In our model, a noncooperative game Γ = S i , u i n i=1 for players i = 1, ..., n consists of a family of feasible strategy spaces (S i , ≤ i ) n i=1 which are assumed to be complete lattices, so that the strategy space S × n i=1 S i is a complete lattice for the componentwise order ≤, and of a family of utility (or payoff) . 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).

(Quasi)Supermodular Games
s 1 , ..., s n := ⊥ 1 , ..., ⊥ n ; // s 1 , ..., s n := ⊤ 1 , ..., ⊤ n ; do t 1 , ..., t n := s 1 , ..., s n ; while ¬( s 1 , ..., s n = t 1 , ..., t n ) On the other hand, Γ is quasisupermodular (or, with strategic complementarities) when: (1) for any i, for any 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 : . It also turns out [18,Theorem 2] that Eq(Γ), ≤ 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 u i (·, s −i ) holds for any finite-strategy game, namely for those games where each strategy space S i is finite. In the following, we will consider (quasi)supermodular games which satisfy this hypothesis of upper semicontinuity. If, given any s i ∈ S i , the function u i (s i , ·) : S −i → R Ni 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(Γ), u i (geq(Γ)) ≥ u i (s), while leq(Γ) minimizes all equilibria.

Computing Game Equilibria
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. Here, S 1 and S 2 are both the finite chain of integers C = {1, 2, 3, 4, 5, 6}, ≤ and u 1 (x, y), u 2 (x, y) : S 1 × S 2 → R are, respectively, the first and second entry in the matrix element determined by row x and column y. It turns out that both u 1 and u 2 have increasing differences, so that, since S 1 and S 2 are finite chains, Γ is a finite supermodular game. The two best response correspondences B 1 , B 2 : C → SL(C) are as follows: Thus, Eq(Γ) = {(2, 3), (5, 4)}, since this is the set Fix(B) of fixed points of the best response corre- We also notice that u 1 (·, s 2 ), u 2 (s 1 , ·) : 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:

Abstract Interpretation
Static program analysis relies on correct (a.k.a. sound) and computable semantic approximations. A program P is modeled by some semantics Sem P and a static analysis of P is designed as an approximate semantics Sem ♯ P which must be correct w.r.t. Sem P . This may be called global correctness of static analysis. Any (finite) program P is a suitable composition of a number of constituents subprograms c i and this is reflected on its global semantics Sem P which is commonly defined by some combinations of the semantics Sem c i of its components. Thus, global correctness of a static analysis of P is typically derived from local correctness of static analyses for its components c i . 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 Sem P 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).
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, C, ≤ C and A, ≤ A , 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 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, γ): 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 C, ≤ 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 S i is the chain of integers [1, 6], we have that A 1 = {3, 5, 6} and A 2 = {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 R, ≤ 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 numbers: given any integer number N ≥ 0, cl N : R → R is defined as follows: cl N (x) = ⌈10 N x⌉ 10 N . For N = 0, cl N (x) = ⌈x⌉, while for N > 0, cl N (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 cl 2 (x) = 1.01. Clearly, it turns out that cl N 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, γ).
Hence, f A plays the role of the best possible approximation of f on the abstraction A.

Abstractions on Product Domains
Let us show how abstractions of different concrete domains C i can be composed in order to define an abstract domain of the product domain × i C i , and, on the other hand, an abstraction of a product × i C i can be decomposed into abstract domains of the component domains C i . In the following, we consider a finite family of complete lattices C i , ≤ i n i=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 , C i , A i , γ i ) n i=1 , one can easily define a componentwise abstrac- A i are both complete lattices w.r.t. the componentwise partial order and for any c For any i, we also use the function γ −i : In static program analysis, (α, is called a nonrelational abstraction since, intuitively, the product abstraction × n i=1 A i does not take into account any relationship between the different concrete domains C i . Decomposition of Product Abstractions. Let us show that any GC (α, × n i=1 C i , A, γ) for the concrete product domain × n i=1 C i induces corresponding abstractions (α i , C i , A i , γ i ) of C i as follows: Since γ preserves arbitrary meets, we have that γ(a) = ∧ C {γ(a x ) ∈ C | x ∈ X}, so that γ(a) i = ∧ Ci X, that is, ∧ Ci X ∈ A i . Hence, since A i is a Moore-family of C i , we have that γ i = id : A i → C i preserves arbitrary meets and therefore is a concretization function. Let us check that α i is the left adjoint of γ i , i.e., for any γ(a))) = γ(a), and, in turn, Finally, let us observe that if γ is (finitely) additive and X ⊆ A i so that for any x ∈ X there exists some 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, (α, × n i=1 C i , 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: 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 A 1 = {2, 3, 4, 6} and A 2 = {2, 4, 5, 6}, and the product composition A 1 × A 2 by Lemma 3.1 yields a more expressive abstraction than A, for example (2, 4) ∈ (A 1 × A 2 ) A.
On the other hand, for the abstractions A 1 = {3, 5, 6} and A 2 = {2, 6} of Example 2.2, by Lemma 3.1, the product domain A 1 × A 2 is a nonrelational abstraction of C × C.

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

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].
. 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 ∧ ) ∈ C exists. Furthermore, by the constructive version of Tarski's theorem [4,Theorem 5 Consider any z ∈ Fix(f ). We prove by transfinite induction that for any α ∈ O, 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.

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 A, ≤ A be an abstraction of a concrete domain C specified by a monotone concretization map γ : A → C. Let us observe that the powerset lifting then there exists y 1 ∈ Y 1 such that y 1 ≤ A y 2 , so that γ(y 1 ) ∈ γ s (Y 1 ) and γ(y 1 ) ≤ C γ(y 2 ), i.e., γ s (Y 1 ) S γ s (Y 2 ). Analogously, γ s is Hand 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) Hand EM -correct approximations are defined by replacing in this definition Swith, respectively, Hand EM -, and ℘ ∧ with, respectively, ℘ ∨ and ℘ ⋄ .
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 C 2 and A 2 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
Proof. Let us consider f ∧ : . Hence, by the concretization-based fixed point transfer (see [13,Theorem 2.2.4] Dual results hold for Hand EM -correct approximations.

Corollary 4.5.
( Proof. By duality from Theorem 4.4. In particular, point (2) follows because, by Corollary 4.2, 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 ♯ : Here, fixed point approximation states that α(lfp(f )) ≤ A lfp(f ♯ ).

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 ℘ ∧ (C), S and ℘ ∧ (A), S are mere preorders, and not posets. Then, given two preorders X, X and Y, Y , 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. 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 X S γ s (Y ). Analogously, it turns out that X S γ s (Y ) ⇒ α s (X) S Y . Hence, this shows that α s , ℘ ∧ (C), S , ℘ ∧ (A), S , γ s 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. 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)).

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 B i : S −i → SL(S i ) and the overall best response B : S → SL(S).

Games with Abstract Strategy Spaces
Let us consider a game Γ = S i , u i n i=1 and a corresponding family specifies a nonrelational product abstraction of the whole strategy space × n i=1 S i . We define the i-th utility function u G i : γ(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 u i (·, s −i ) is (quasi)supermodular and all the GCs in G are finitely disjunctive then u G i (·, a −i ) : Proof. Let us check that u G i (·, a −i ) is supermodular: The proof of quasisupermodularity is analogous. Let us also check that Let us also observe that if u i (s i , s −i ) has increasing differences (the single crossing property), X ⊆ × n i=1 S i is any subset of the strategy space and u i /X : X → R Ni is the mere restriction of u i to the subset X then u i /X still has increasing differences (the single crossing property). Hence, in particular, this holds for As a consequence of this and of Lemma 5.1, we obtain the following abstract (quasi)supermodular games. Since both A 1 and A 2 are trivially disjunctive abstractions, by Corollary 5.2, it turns out that Γ ♯ is supermodular. The best response correspondences B ♯ i : A −i → SL(A i ) for the supermodular game Γ ♯ are therefore as follows: We observe that B ♯ 2 is not a S-correct approximation of B 2 because: . Indeed, it turns out that Eq(Γ ♯ ) = {(3, 2), (5, 6), (6, 6)}, so that leq(Γ) = (2, 3) ≤ (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 approx-  while the best response correspondences B ♯ i become: Thus, here we have that Eq(Γ ♯ ) = {(5, 4)}. In this case, it turns out that B ♯ i is a EM -correct approximation of B i , so that, by Example 5.5. Here, we consider the disjunctive abstractions A 1 = {4, 5, 6} ∈ Abs(S 1 ) and A 2 = {3, 4, 5, 6} ∈ Abs(S 2 ). In this case, we have the following supermodular abstract game Γ ♯ over A 1 × A 2 : 2, 4 5, 6 6, 5 6, 5 5 3, 4 6, 6 7, 5 6, 5 4 3, 5 5, 6 5, 5 4, 4 where the best response functions B ♯ i are therefore as follows: Here, it turns out that B ♯ i is a EM -correct approximation of B i , so that the abstract best response B ♯ : be the corresponding abstract (quasi)supermodular game, with best response B G . 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 )).
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}.
Proof. Observe that the product (α, is a principal filter GC. Then, this is a straight consequence of Theorem 5.6, since S B(γ(a)) 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 p i (e.g., a can of beer), whose feasible selling prices (e.g., in euros) s i range in S i [a, b], where the smallest price shift is 5 cents. The payoff function u i : S 1 × S 2 × S 3 → R models the profit of firm i: As shown in general in [1, Corollary 8.9], it turns out that each payoff function u i has increasing differences and u i (s i , ·) 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. Notice that A 2 and A 3 are principal filter abstractions, while this is not the case for A 1 , so that Corollary 5.7 cannot be applied. We observe that: /20, 39/20, 40/20}, The hypothesis of Theorem 5.6 is therefore satisfied, because for any a −i ∈ A −i , we have that B i (a −i ) ∈ A i . Hence, by Corollary 5.2, we consider the supermodular abstract game ∆ A on the abstract strategy spaces A i . 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.
Here, RT calculates leq(∆ A ) starting from the bottom (1.8, 1.8, 1.9) of A 1 × A 2 × A 3 through 6 calls to B A i (a −i ) and any call B A i (a −i ) scans the smaller abstract strategy space A i instead of S i . On the other 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 B A i (a −i ), each scanning the reduced abstract strategy spaces A i .

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 u i (s i , ·), for any given s i . 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 Heikkilä [1] in their Examples 8.58, 8.63 and 8.64. Given a game Γ = S i , u i n i=1 , we consider a family G = (α i , S i , A i , γ i ) n i=1 of GCs and, by Lemma 3.1, their nonrelational product (α, × n i=1 S i , × n i=1 A i , γ), where we denote by ρ γ • α ∈ uco(× n i=1 S i ) 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 , × j =i S j , × j =i A j , γ −i ). The utility function u i,G : × n i=1 S i → R is then defined as follows: for any s ∈ × n i=1 S i , u i,G (s i , s −i ) u i (s i , ρ −i (s −i )).
Lemma 6.1. If u i (s i , s −i ) has increasing differences (the single crossing property) then u i,G (s i , s −i ) has increasing differences (the single crossing property). Also, if u i (s i , ·) is monotone then u i,G (s i , ·) is monotone.
Proof. Assume that (s i , s −i ) ≤ (t i , t −i ). Hence, s −i ≤ −i t −i , so that, by monotonicity of ρ −i , ρ −i (s −i ) ≤ −i ρ −i (t −i ), and, in turn, (s i , ρ −i (s −i )) ≤ (t i , ρ −i (t −i )). Then: The single crossing property for u i,G (s i , s −i ) can be proved similarly. Let s −i ≤ −i t −i , so that, by mono- Then, by monotonicity of u i (s i , ·), we obtain: u i,G (s i , s −i ) = u i (s i , ρ −i (s −i )) = u i (s i , ρ −i (t −i )) = u i,G (s i , t −i ), thus proving the monotonicity of u i,G (s i , ·).
Moreover, let us point out that if u i (·, s −i ) is (quasi)supermodular then, obviously, u i,G (·, s −i ) remains (quasi)supermodular as well, so that by defining the game Γ G S i , u i,G n i=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 B i,G : S −i → SL(S i ) is such that B i,G (s −i ) = {s i ∈ S i | ∀x i ∈ S i .u i (x i , ρ −i (s −i )) ≤ u i (x i , ρ −i (s −i ))} = B i (ρ −i (s −i )), so that the best response correspondence satisfies B G (s) = B G (ρ(s)) = B(ρ(s)), namely, B G can be viewed as the restriction of B to the abstract strategy space ρ(S).