An Abstraction-Refinement Methodology for Reasoning about Network Games

1 Introduction

Network design is a fundamental and well-studied problem. A game-theoretic approach to the analysis of network design has become especially relevant with the emergence of the Internet, where different users share resources like software or communication channels [Fabrikant et al., 2003; Albers et al., 2014; Anshelevich et al., 2008]. Network games (NGs, for short) [Anshelevich et al., 2008; Rosenthal, 1973; Roughgarden and Tardos, 2002] constitute a well studied model of non-cooperative games. The game is played among selfish players on a network, which is a directed graph. NGs are used to model resources as edges in a network and the cost involved in sharing these resources. Each player has a source and a target vertex, and a strategy is a choice of a path that connects these two vertices. The cost a player pays is

∗The research leading to these results has received funding from the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013, ERC grant no 278410) and the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).

Orna Kupferman

The Hebrew University orna@cs.huji.ac.il

the sum of costs of the edges his path traverses, where a cost of an edge depends on the load on it, namely the number of players using the edge. We distinguish between two types of costs. In cost-sharing games [Anshelevich et al., 2008], each edge has a cost and the players that use it split the cost among them, thus increased load decreases the cost. For example, when the costs correspond to prices, users that share a resource also share its price. Then, in congestion games [Rosenthal, 1973], increased load increases the cost: each edge has a non-decreasing cost function that maps the load on the edge to its cost given this load. For example, when the network models a road system and costs correspond to the travel time, an increased load on an edge corresponds to a traffic jam, increasing the cost of the players that use it.

Since the players attempt to minimize their own costs, they selfishly select a path. The focus in game theory is on the stable outcomes of a given setting. The most prominent stability concept is that of a Nash equilibrium (NE): a profile (vector of strategies, one for each player) such that no player can decrease his cost by unilaterally deviating from his current strategy; i.e., assuming that the strategies of the other players do not change. 1 By [Rosenthal, 1973], there exists an NE in every NG. A social optimum (SO) is a profile that minimizes the sum of the players' costs; thus the one obtained if the players would have obeyed some centralized authority.

Finding SO and NE profiles is a complex and well studied problem. Finding an SO is NP-complete [Tardos and Wexler, 2007; Meyers, 2006], and finding an NE is PLS-complete [Fabrikant et al., 2004; Syrgkanis, 2010] (the complexity class PLS contains local search problems with polynomial time searchable neighborhoods [Johnson et al., 1988]). These high complexities become more acute if we recall that NGs often model huge networks.

The need to cope with very large models is a major research area in formal verification. There, we check that a system satisfies its specification by translating the system into some formal model, typically a labeled state-transition graph, and applying model-checking procedures on this model [Clarke et al., 1999]. One of the most successful methodologies for reasoning about the huge state space of systems is abstraction [Cousot and Cousot, 1977; Larsen, 1989], where we hide some of the information about the system. This enables us to reason about systems that are much smaller, yet it gives rise to approximated solutions. Indeed, hiding of information may result in an under-approximating system: one that has fewer behaviors than the original system, or in an over-approximating system: one that has more behaviors than the original system. Abstraction methodologies use both types of approximations [Dams et al., 1997; Bruns and Godefroid, 1999; Shoham and Grumberg, 2004].

1 Throughout this paper, we consider pure strategies, as is the case for the vast literature on NGs.

An important step in methodologies that are based on abstraction is refinement. Assume that we find an overapproximation of the system that does not satisfy a universal property. That is, the over-approximation has a forbidden behavior. It may be that this forbidden behavior exists also in the concrete system, in which case the verification algorithm terminates and reports a bug in the system. But it may also be that the forbidden behavior exists only in the overapproximation, thus the counterexample is spurious. Then, one can use the spurious counterexample to refine the overapproximation in a way that eliminates it, and repeat modelchecking until either a real counterexample is found, or the over-approximation satisfies the property. This methodology, of counterexample guided abstraction-refinement (CEGAR) has proven to be very effective [Clarke et al., 2003].

Abstraction has been studied in the context of extensiveform games. A strategy for a player in an extensive-form game prescribes which action to perform, given the histories of actions played so far. NGs, on the other hand, are "oneshot" games. The questions studied on NGs focus on stable outcome whereas in extensive-form games one often tries to find an optimal strategy for a player. The abstraction studied in [Gilpin and Sandholm, 2007b; Brown and Sandholm, 2015] tries to merge states in the game tree that are indistinguishable for the players. The idea of merging configurations due to hidden information is the key also in abstractions used in formal methods, yet the technical details are very different. Then, in action abstraction [Brown and Sandholm, 2015; Gilpin et al., 2008], some of the actions of the players are disabled, reducing the state space of reachable configurations in the game tree, which is again not similar to the approach taken here. Finally, formal methods often involves reasoning about multi-player games, and abstraction-refinement methodologies have been studied in this setting [Henzinger et al., 2000; de Alfaro et al., 2004; Ball and Kupferman, 2006]. Such games model on-going interactions between processes, say a system and its environment, and are infinite-duration games, thus they are again different from the NGs we study here.

In this paper we introduce and study an abstractionrefinement methodology for reasoning about network games. Given an NG N defined over a network 〈V,E〉, an abstraction function for N is a function α : V → A, for some set A of abstract vertices. We assume that A is smaller than V , thus the function α induces a partition of V . We define the under-approximation of N with respect to α, denoted N ↓ [α], and the over-approximation of N with respect to α, denoted N ↑ [α]. Both approximations are NGs that have A as their set of vertices. The under- and over-approximation is in the definition of the edges and the cost functions. Intuitively, N ↓ [α] is less appealing to the players than N: they have fewer possible profiles, and the profiles that are possible are at least as expensive as the ones that correspond to them in N. Accordingly, the edges under-approximate these in N: there is an edge from an abstract vertex a to an abstract vertex a′ if all the concrete vertices that are mapped by α to a have an edge to a concrete vertex that is mapped by α to a′ (a.k.a. must transitions [Larsen, 1989; Dams et al., 1997]). In addition, the cost of an abstract edge is essentially the maximal cost of a concrete edge that induces it. Dually, N ↑ [α] is more appealing to the players: they have more and cheaper profiles than in N. Accordingly, the edges in N ↑ [α] over-approximate these in N: there is an edge from a to a′ if some concrete vertex that is in a has an edge to some concrete vertex that is mapped to a′ (a.k.a. may transitions), and the cost of an abstract edge is essentially the minimal cost of a concrete edge that induces it. Traditional abstractionrefinement methodologies in formal verification focus on the transition relation. An extension that takes costs into account has been studied in [Avni and Kupferman, 2012], where the costs of a weighted automaton are also abstracted. Here, we take into account the cost functions as well as the load. Indeed, the merging of edges may lead to a spurious increased load in the abstraction.

We show how N ↓ [α] and N ↑ [α], which may be significantly smaller than N, can be used in order to reason about the SO and the NE profiles of N. Our methodology is based on the observation that each profile in N ↓ [α] can be mapped to at least one profile in N with a lower or equal cost, and that each profile in N can be mapped to a profile in N ↑ [α] with a lower or equal cost. Hence, for example, the cost of the SO in N is bounded from above and below by the costs of the SOs in N ↓ [α] and N ↑ [α], respectively. Moreover, refining α tightens these bounds, so the user can control the trade-off between preciseness and complexity.

A more technically-involved use of the under- and overapproximations is an algorithm we present for finding an NE in N. The algorithm, which can be viewed as the NGanalogue of CEGAR, is based on the notion of an abstract NE: we say that a profile P in N ↓ [α] is an abstract NE if no player has a beneficial deviation from P even in N ↑ [α]. Intuitively, an abstract NE has to face two challenges. First, the profile P has to exist in the under-approximation, where fewer strategies exist. In addition, deviations fromP are possible in the over-approximation, where more strategies exist, and their cost is lower. Consequently, as we shall formally prove, an abstract NE can direct the search for a concrete NE: once we find an abstract NE P in N ↓ [α], it is guaranteed that a concrete NE exists in N when restricted to profiles that agree with P. Our algorithm finds an abstract NE if one exists and then directs the search for a concrete NE in a much smaller state space. It is however not necessary that an abstract NE exists in every abstract game. When a candidate profile in N ↓ [α] is an NE in N ↓ [α] but is not an abstract NE in N, we use the spurious deviations of the players in N ↑ [α] in order to refine α, which narrows the search space.

Our experimental results demonstrate the efficiency of the methodology. The results show that the overhead required for abstraction becomes more negligible for larger systems.

This work belongs to a line of works that transfer concepts and ideas between the areas of formal verification and algorithmic game theory: logics for specifying multiagent systems [Alur et al., 2002; Chatterjee et al., 2007], studies of equilibria in games related to synthesis and repair problems [Chatterjee et al., 2006; Chatterjee, 2006; Fisman et al., 2010; Almagor et al., 2015], and of non-zerosum games in formal verification [Chatterjee et al., 2004; Brihaye et al., 2012]. Closest to this work are works that apply ideas from formal verification of NGs. This includes an extension of NGs to objectives that are richer than reachability [Avni et al., 2016b], NGs in which the players select their paths dynamically [Avni et al., 2016a], and efficient reasoning about NGs that are structures in a hierarchical manner [Kupferman and Tamir, 2017].

2 Preliminaries

2.1 Network Games

A network is a tuple 〈V,E〉, where V is a set of vertices and E ⊆ V × V is a set of directed edges. For an integer k ∈ IN, let [k] = {1, . . . , k}. A network game (NG) is N = 〈k, V, E, {le}e∈E, 〈si, ti〉i∈[k]〉, where k is the number of players; 〈V,E〉 is a network; for e ∈ E, the cost function le : [k] → IR≥0 maps the load on edge e, namely the number of players that use edge e, to the cost each of them pays for using e with this load; and for i ∈ [k], the pair 〈si, ti〉 ∈ V ×V describes the objective of Player i: traversing N from the source vertex si to the target vertex ti.

We distinguish between two types of cost functions. In uniform cost-sharing games (CS-NGs, for short) the players that use an edge share its cost equally. Formally, each edge e is associated with a weight we ∈ IR≥0, and for all x ∈ [k], we have le(x) = we x . Thus, increasing the load in uniform costsharing games decreases the cost of the players. In contrast, in congestion games (CON-NGs, for short), the cost functions are non-decreasing, thus increasing the load also increases the cost for each player.

A strategy of a player i ∈ [k] is a simple path π from si to ti. Thus, π = 〈v1, v2〉, 〈v2, v3〉, . . ., 〈vn-1, vn〉, with v1 = si, vn = ti, and (vj, vj+1) ∈ E for all 1 ≤ j < n. A profile is a tuple of strategies, one for each player. Consider a profile P = 〈π1, π2, . . . , πk〉 in the game. We sometimes refer to a path as the set of edges that it traverses, thus π ⊆ E. For an edge e ∈ E, we use loadP (e) to denote the number of players that traverse the edge e in P. Each player that uses e then pays le(loadP (e)), and the cost of Player i in P, denoted costi(P), is ∑e∈πi le(loadP (e)). The cost of the profile P, denoted cost(P), is the total cost incurred by all the players, i.e., cost(P) = ∑ki=1 costi(P). For a profile P and a strategy π of player i ∈ [k], let P[i ← π] denote the profile obtained from P by replacing the strategy for Player i by π. Given a profile P = 〈π1, . . . , πk〉, a best response (BR, for short) of a player, say Player k, in profile P is a strategy π′k such that for all strategies π of Player k, we have that cost k(P [k ← π′k ]) ≤ cost k(P [k ← π]).

Formally, a profile P is an NE iff for every Player i and every strategy π, we have costi(P[i ← π]) ≥ costi(P). A social optimum (SO) of a game N is a profile that attains the minimal cost over all profiles. We denote by SO(N) the cost of an SO profile; i.e., SO(N) = minP cost(P). An SO can be thought of as an optimal solution imposed by a centralized authority, and need not be an NE.

2.2 Abstraction and Refinement

Consider an NG N = 〈k, V, E, {le}e∈E, 〈si, ti〉i∈[k]〉. We refer to V as the set of concrete vertices. Let T = {t1, . . . , tk}. An abstraction function for N is a function α : V → A, for a set A of abstract vertices. We assume that T ⊆ A and that α is such that for all ti ∈ T , we have α(ti) = ti and α(v) ̸= ti for all v ̸= ti. We also assume that A is smaller than V , thus the function α induces a partition of V (with a singleton {ti} for each ti ∈ T ). Accordingly, we sometimes refer to abstract vertices as sets of concrete vertices. In particular, when α is clear from the context, we use v ∈ a, for v ∈ V and a ∈ A, to indicate that α(v) = a.

Consider the NG N and an abstraction function α. We define the under- and over-approximation of N formally. Given N, α, and b ∈ {↓, ↑}, we define N b [α] = 〈k, V,Eb , {lbe}e∈Eb, 〈α(si), α(ti)〉i∈[k]〉, where the underand over-approximating transition relations E↓ , E↑ ⊆ A×A, and the under- and over-approximating cost functions l↓ e and l↑ e are defined as follows.

Transition relations: Consider two abstract vertices a, a′ ∈ A. Then, E↓ (a, a′ ) iff for every concrete vertex v ∈ a, there is a concrete vertex v′ ∈ a′ such that E(v, v′ ). Also, E↑ (a, a′ ) iff there exist concrete vertices v ∈ a and v′ ∈ a′ such that E(v, v′ ). Note that E↓ ⊆ E↑ . For simplicity, we omit self-loops from E↓ and E↑ , as they are not going to be used anyway in strategies. We follow the common terminology in formal verification and refer to the under- and overapproximating edges as must and may edges, respectively. We extend α to edges in the expected way. Thus, α(h), for an edge h = 〈v, v′ 〉 ∈ E, is 〈α(v), α(v′ )〉. Note that α(h) is always in E↑ and may not be in E↓ .

Cost Functions: The definition of the under- and overapproximating cost functions depends on the type of N. We first describe the definition and then explain it.

• If N is a CON-NG, then
• for every e ∈ E↑ and x ∈ [k], we have l↑ e (x) = min{lh(1) : e = α(h)}.
• for every e ∈ E↓ and x ∈ [k], we have l↓ e (x) = max{lh(x) : e = α(h)}, and
• If N is a CS-NG, then
• for every e ∈ E↑ and x ∈ [k], we have l↑ e (x) = min{lh(x) : e = α(h)}.
• for every e ∈ E↓ and x ∈ [k], we have l↓ e (x) = max{lh(1) : e = α(h)}, and

The idea behind the definition is as follows. Recall that in the under-approximation N ↓ [α], we want the strategies to be more expensive. This is why we take, in l↓ e , the maximal cost of edges that induce e. In CON-NGs, the cost increases with load and hence the cost function l↓ e depends on x since we want more expensive profiles. In CS-NGs, we ignore x and assume that the load is 1. To see why, recall that an abstract edge e ∈ E↓ is obtained by merging several concrete edges. Consequently, the load on e is the sum of the loads on these concrete edges. This load is fake: it is only due to the merging of concrete edges and not due to an actual increased load. In CON-NGs, where the cost functions increase with an increased load, fake load goes well with generating more expensive profiles. In CS-NGs, however, increased load decreases the cost, and we have to cancel the fake load. This is done by dividing the load by itself, which bounds the fake load. Recall that in a CS-NGN, each edge h ∈ E has a weight wh such that lh(x) = wh x . Thus, as lh(1) = wh, the definition is equivalent to one with l↓ e (x) = max{wh : e = α(h)}.

Dually, the over-approximating cost function aims at providing cheaper strategies. Accordingly, l↑ e depends on the minimum cost function of edges that induce e. Here, we have to cancel fake load in CON-NGs, as fake load increases the cost and may cause the cost of an abstract edge to go beyond the cost of the concrete edges that induce it.

When α is clear from the context, we denote N b [α] by N b . When we refer to the cost of a profile P in N b , we use the notation cost b (P), to emphasize that the profile P is in N b . In Figure 1, we show an NG on the left and an abstraction to the right.

Let us emphasize the confusing fact that when we talk about an under-approximation, we take the maximum cost. This may seem counterintuitive. In order not to get confused, recall that the thing we are approximating is the range and attractiveness of possible profiles. In an under-approximation, we want both fewer and more expensive profiles. Dually, in an over-approximation, we take the minimum cost, as we want more and cheaper profiles. A similar intuition applies for the adjustment of the load.

Definition [Abstract NE] A profile P = 〈π1, . . . , πk〉 in N ↓ is an abstract NE if no player has a beneficial deviation from P even in N ↑ . Formally, for all i ∈ [k] and strategies π′i ̸= πi of Player i in N ↑ , we have cost ↓i (P) ≤ cost ↑i (P [i ← π′i ]).

Intuitively, an abstract NE has to face two challenges. First, the profile P has to exist in the under-approximation, where fewer strategies exist. Second, existence of deviations from P is checked in the over-approximation, where more strategies may exist, and their cost is lower. Consequently, as we formally prove in Theorem 3, an abstract NE directs the search for a concrete NE: once we find an abstract NE P in N ↓ , we know that a concrete NE exists in N when restricted to profiles that agree with P. Formally, given an NG N and a profile P in N ↓ , the restriction of N to P is the NG N|P = 〈k, V|P , E|P , {le}e∈E|P , 〈si, ti〉i∈[k]〉, where V|P = {v ∈ V : α(v) appears in a strategy in P} and E|P

= {〈v, v′ 〉 ∈ E : 〈α(v), α(v′ )〉 appears in a strategy in P}. The generation of N ↓ and N ↑ depends on the way N is given. When N is given in a succinct presentation, it is often possible to construct N ↓ and N ↑ on top of this succinct presentation. Of special interest, especially in the context of software-defined networks [Vissicchio et al., 2014], are NGs in which V = 2X for some set X of variables. Then, abstraction functions are based on predicates on the variables in X, and the construction of N ↓ and N ↑ is done on top of this succinct presentation N that is based on the variables in X.

Consider two abstraction functions α1 : V →A1 and α2 : V → A2. We say that α2 refines α1, denoted α2 ⪯ α1, if for all concrete vertices v and v′ , if α2(v) = α2(v′ ), then α1(v) = α1(v′ ). That is, the partition of V that is induced by α2 refines the partition induced by α1.

3 On Abstract SOs and NEs

In this section we study the theoretical properties of abstraction in NGs and show how reasoning about the (much smaller) under- and over-approximations of an NG N can be used for bounding the cost of an SO and for directing the search for an NE in N. We first relate strategies and profiles in N with strategies and profiles in its approximations.

Consider now a strategy π = 〈a1, a2〉, 〈a2, a3〉, . . ., 〈an-1, an〉 of Player i in N ↓ . By the definition of E↓ , for every concrete vertex v with α(v) = a1, and in particular for si - the source vertex of Player i, there is a path in N from v to some vertex v′ with α(v′ ) = an-1. Also, by the definition of N ↓ , we have that an = ti - the target vertex of Player i 2 , and for all the concrete vertices v′ with α(v′ ) = an-1, we have E(v′ , ti). Hence, the strategy π in N ↓ induces at least one path π′ = 〈v1, v2〉, 〈v2, v3〉, . . . , 〈vn-1, vn〉 in N such that v1 = si and vn = ti. Let α-1 (π) be the nonempty set of these paths. Finally, a profile P = 〈π1, . . . , πk〉 in N ↓ corresponds to the set α-1 (P) of profiles P ′ = 〈π′1 , . . . , π′k 〉 in N in which for all i ∈ [k], we have π′i ∈ α-1 (πi).

Consider a network N and a strategy π of Player i in N. The strategy α(π) that corresponds to π in N ↑ is obtained from π by replacing each concrete edge h by the abstract edge α(h), and removing cycles in the obtained path in N ↑ . Note that by the definition of E↑ , the edge α(h) exists in N ↑ . Formally, we define α(π) as follows. Let π = 〈v1, v2〉, 〈v2, v3〉, . . ., 〈vn-1, vn〉. We first define α′ (π) = 〈α(v1), α(v2)〉, 〈α(v2), α(v3)〉, . . . , 〈α(vn-1), α(vn)〉. Then, α(π) is obtained from α′ (π) by removing cycles; that is, by repeatedly removing subsequences 〈α(vj), α(vj+1)〉, . . ., 〈α(vj+m), α(vj+m+1)〉 with α(vj) = α(vj+m+1). A profile P = 〈π1, . . . , πk〉 in N corresponds to the profile α(P) = 〈α(π1), . . . , α(πk)〉 in N ↑ .

We now relate the costs of corresponding profiles in N, N ↓ , and N ↑ .

Lemma 1 Consider an NG N and an abstraction function α.

1. For every profile P in N, the profile α(P) in N ↑ is such that cost ↑ (α(P)) ≤ cost(P).

2 We note that this is the point where we use the fact that α(ti) is a singleton, for every i ∈ [k].

1. For every profile P in N ↓ and profile P ′ ∈ α-1 (P) in N, we have that cost(P ′ ) ≤ cost ↓ (P).

Theorem 1 For every NG N and abstraction function α, we have SO(N ↑ [α]) ≤ SO(N ) ≤ SO(N ↓ [α]).

Recall that given two abstraction functions α1 and α2, if α2 refines α1, then we can view N ↓ [α1] as an underapproximation of N ↓ [α2], and view N ↑ [α1] as an overapproximation of N ↑ [α2]. Accordingly, Theorem 1 can be viewed as a special case of Theorem 2 below, with α2 being the most refined abstraction function (that is, α2 : V → V , with α2(v) = v), and α1 being the refinement function α studied there.

Theorem 2 Consider an NG N and two abstraction functions α1 and α2. If α2 ⪯ α1, then SO(N ↑ [α1]) ≤ SO(N ↑ [α2]) and SO(N ↓ [α2]) ≤ SO(N ↓ [α1]).

Theorem 1 enables us to approximate the cost of an SO in N using the costs of the SO in the much smaller N ↓ and N ↑ . We now turn to study how N ↓ and N ↑ can be used in order to direct the search for an NE in N.

Note that profiles in α-1 (P) can be searched for in N|P . Thus, as we elaborate in Section 4, an NE in N can be found by a sequence of best response moves restricted to N|P .

Theorem 3 Consider an NG N, an abstraction function α for it, and an abstract NE P in N ↓ [α]. There exists a profile in α-1 (P) that is a concrete NE in N.

4 An Abstraction-Refinement Procedure for Finding an NE

In this section we describe an abstraction-refinement procedure for finding an NE in an NG . The input to the procedure is a concrete NG N and an abstraction function α for it. Experience in formal verification suggests that abstraction functions that are supplied by users familiar with the network, are the most successful ones. Alternatively, one can start with a coarse abstraction and refine it as we do in Section 5.

The output of the procedure is a concrete NE in N. Since the state space of N ↓ and N ↑ is much smaller than that of N , we would like to perform as many as possible computations on the approximating networks. Our procedure (see Fig. 2 for an overview) consists of two parts. The first, in which an abstract NE Pα is found, is done entirely in N ↓ and N ↑ , and it is the procedure we have implemented. The second, in which a concrete NE is found, is done in N, restricted to N|Pα . Thus, as is the case of the CEGAR methodology in formal verification, there is no way to avoid N entirely, yet we can significantly restrict the part of it in which the search proceeds. Moreover, it is possible to refine α and tighten N|Pα further. In Section 5, we show that the restriction indeed significantly reduces the size of the network.

There are many ways to refine an abstraction; one can work naively, choose an arbitrary abstract vertex and split it in some way, possibly by adding predicates that appear in the description of the network or the strategies. Even such a naive refinement is guaranteed to eventually lead to a solution. The challenge is to choose the refinements cleverly so that a concrete answer is obtained when the approximating networks are still much smaller than the concrete one. In CEGAR, the refinement is guided by a spurious counterexample. We follow this idea by always refining according to some path in the network that points to a spurious behavior of the approximations. We now describe the methodology in detail.

4.1 Part 1: AbsNE-Loop, Finding an Abstract NE

In the first part, our goal is to find, given N and α, an abstract NE. Recall that such a profile is an NE in N ↓ that is resistant to deviations of the players even in N ↑ . Since N ↓ is an NG, it has an NE. In Step 1 in Fig. 2, we find such an NE Pα. This is done by the user's favorite algorithm for finding an NE in NGs. The important point for us is that this is done in the (much smaller) under-approximation of N . Then, in Step 2, we check whether Pα is an abstract NE. Thus, we check whether players have beneficial deviations in N ↑ . Again, this is done in the (much smaller) over-approximation of N. If no player has a beneficial deviation in N ↑ , then Pα is an abstract NE, we conclude this part of the procedure, and move to Step 4. Otherwise, there is a player i ∈ [k] who can benefit from deviating to a strategy π′i .

We use π′i in order to guide the refinement. There are several reasons why Pα is an NE in N ↓ yet not an abstract NE in N. Step 3 consists of three possible refinement steps among which the user can choose, corresponding to the above different reasons. Let us start with Step 3a. Since π′i is a path in N ↑ , there might not be a concrete path in N that corresponds to it, thus π′i is a spurious path. Consider two adjacent abstract vertices a1 and a2 that π′i traverses. If the edge between a1 and a2 is in E↑ \E↓ , we can split a1 into a′1 and a′′ 1

such that a′1 contains exactly the vertices that have a neighbor in a2 (similarly we can split a2). Note that after refinement, there is a must edge from a′1 to a2 and there is not even a may edge between a′′ 1 to a2. Since π′i is spurious, such a candidate vertex is guaranteed to exist. (We note that disconnectivity in N ↓ can be treated in a similar way.)

We continue to Steps 3b and 3c. They have to do with under- and over-approximations of the cost functions that cause π′i to be a beneficial deviation in N ↑ . By the definition of l↓ and l↑ , we know that if cost ↓i (Pα[i ← π′i ]) > cost ↑i (Pα[i ← π′i ]), then the path π′i traverses an abstract edge e ∈ E↓ with load x for which l↓ e (x) > l↑ e (x). Assume that e = 〈a1, a2〉. In Step 3b, we split a1 or a2 in order to tighten this gap. Finally, it may be that the cost of the strategy of Player i in Pα is too big. In Step 3c, we use the strategy πi that Player i chooses in Pα in order to guide a similar refinement in order to tighten the gap in the costs between cost ↓i (Pα) and cost ↑i (Pα).

A refinement step can be a single refinement or a combination of the refinements that are described above. After completing such a step, we return to Step 1 and find a new NE in the new under-approximating N ↓ , and repeat the process.

4.2 Part 2: ConcNE-Loop, Finding a Concrete NE

The second part of the procedure gets an abstraction function α as well as an abstract NE Pα = 〈π1, . . . , πk〉. The goal is to find a concrete NE P in N such that P ∈ α-1 (Pα). By Theorem 3, such an NE exists. Recall the best-response dynamics (BRD) algorithm for finding an NE in NGs in which we start with an arbitrary profile, and iteratively allow the players to perform beneficial deviations. We follow this algorithm and start in Step 4 with an arbitrary profile P = 〈τ1, . . . , τk〉 in α-1 (Pα). If P is an NE, we are done. Otherwise, there is a concrete beneficial deviation τ ′ i for some Player i. Note that by Theorem 3, we can restrict the deviations of Player i to paths in α-1 (πi). If the size of N|Pα is small, the user can choose Step 6a and try and find an NE in α-1 (Pα) by performing a BRD step. However, when N|Pα is big, it makes sense to refine the abstraction by choosing Step 6b.

In Step 6b, we let the deviation τ ′ i guide the refinement. We look for a vertex v from which τi and τ ′ i differ, thus from v, one path continues with a vertex v′ while the other with v′′ , where v′ ̸= v′′ , yet α(v′ ) = α(v′′ ). We refine the abstraction function by splitting α(v′ ) so that v′ and v′′ are no longer in the same abstract vertex. We would like to have as many must edges as possible between the new vertices. One way to do it is to make v′′ a singleton abstract state, but it is also possible to split α(v′ ) as well as α(v) to achieve this. Once we conclude a refinement, we return to the first part of the procedure, and look for an abstract NE with the new abstraction.

5 Experimental Results

We have implemented our methodology and tested the performance of its AbsNE loop on randomly-generated cost-sharing games. We examined the benefit of the abstraction, namely we compared the size of the original game with the game that is truncated to the abstract-NE we find. We also examined the practicality of our approach, namely the number of CEGAR iterations until an abstract NE is found. We studied these questions for different parameters of the game; size of the graph, range of weights, and number of players. Our implementations are in Python, we use the library Networkx [Hagberg et al., 2008] for graph generation and graph algorithms, and we ran our experiments on a personal computer, Intel Core i5 quad core 1.75 GHz processor, with 8 GB memory. Our results are encouraging: we are able to find an abstract NE relatively easily and it significantly reduces the size of the network making it easier to find a concrete NE.

We generate a random game, given the parameters n, w, k ∈ IN and p ∈ [0, 1]. We use the Erd˝os-R´eyni G(n, p) model to generate the network. Then, for each edge in the graph, we choose at random a cost in a set {0, . . . ,w}. For each player i ∈ [k], we choose at random a source vertex si and a reachable target vertex ti. For the initial abstraction, we choose, for i ∈ [k], a shortest path πi between si and ti, and we let every vertex that πi traverses be a singleton abstract state. Thus, in the under approximation, we have at least one path from si to ti. All other concrete vertices are mapped to one abstract state.

We perform three types of experiments. We focus on the number |V | of vertices in the concrete network, the number k of players, and the range |W| of weights on the edges. The number of edges is approximately 1/2 · |V |2 . We fix two of the parameters and increase the third. In Fig. 3, we see how increasing one of the parameters affects the number of iterations of the CEGAR loop. In Fig. 4, we compare the sizes of the truncated network, namely, α-1 (Pα), and the original one; we show the ratio between the number of vertices in the two networks and the ratio between the number of edges.

We find the plots of the increasing number of vertices most encouraging. Since we fix the number of players, the part of the network that is being "used" becomes relatively smaller with increasing |V |, and an abstract NE has a good potential to shrink the network. Indeed, the ratios decrease. As further good news, the number of iterations reaches a ceiling and does not grow with |V |. Recall how we find an initial abstraction above. When k increases, there is a growing number of concrete vertices that are mapped to singleton abstract states in the initial abstraction. Thus, the abstraction is closer to the concrete network making it easier to find an abstract NE and increasing the ratios. For increasing |W|, we believe that at some point the large variance stops affecting the procedure.