2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science Improved Algorithms for One-Pair and k-Pair Streett Objectives Krishnendu Chatterjee Monika Henzinger Veronika Loitzenbauer 1ST Austria University of Vienna University of Vienna krishnendu.chatterjee@ist.ac.at Faculty of Computer Science Faculty of Computer Science monika.henzinger @ univie. ac. at veronika. loitzenbauer @ univie. ac .at Abstract—The computation of the winning set for one-pair Streett objectives and for k-pair Streett objectives in (standard) graphs as well as in game graphs are central problems in computer-aided verification, with application to the verification of closed systems with strong fairness conditions, the verification of open systems, checking interface compatibility, well-formedness of specifications, and the synthesis of reactive systems. We give faster algorithms for the computation of the winning set for (1) one-pair Streett objectives (aka parity-3 problem) in game graphs and (2) for k-pair Streett objectives in graphs. For both problems this represents the first improvement in asymptotic running time in 15 years. Index Terms—Computer-aided verification; Synthesis; Graph games; Parity games; Streett automata; Graph algorithms. I. Introduction Game graphs and graphs. Consider a directed graph (V, E) with a partition (Vi, V2) of V, which is called a game graph. Let n = \V\ and m = \E\. Two players play the following alternating game on the graph that forms an infinite path. They start by placing a token on an initial vertex and then take turns indefinitely in moving the token: At a vertex v 6 V\ player 1 moves the token along one of the outedges of v, at a vertex u 6 V2 player 2 moves the token along one of the outedges of u. If V2 = 0, then we simply have a standard graph. Objectives and winning sets. Objectives are subsets of infinite paths that specify the desired set of paths for player 1, and the objective for player 2 is the complement of the player-1 objective (i.e., we consider zero-sum games). Given an objective $, an infinite path satisfies the objective if it belongs to $. Given a starting vertex x €V and an objective $, if player 1 can guarantee that the infinite path starting at x satisfies $, no matter what choices player 2 makes, then player 1 can win from x and x belongs to the winning set of player 1. Since the winning sets partition the game graph [33], the complement of the winning set for player 1 is the winning set for player 2. In case the game graph is a standard graph (i.e., V2 = 0), the winning set consists of those vertices x such that there exists an infinite path starting at x that satisfies $. The winning set computation for game graphs is more involved than for standard graphs due to the presence of the adversarial player 2. Relevant objectives. The most basic objective is reachability where, given a set U C V of vertices, an infinite path satisfies the objective if the path visits a vertex in U at least once. The next interesting objective is the Biichi objective that requires an infinite path to visit some vertex in U infinitely often. The next and a very central objective in formal verification and automata theory is the one-pair Streett objective that consists of a pair (Li, U\) of sets of vertices (i.e., L\ C V and U\ C V), and an infinite path satisfies the objective iff the following condition holds: if some vertex in L\ is visited infinitely often, then some vertex in U\ is visited infinitely often (intuitively the objective specifies that if one Buchi objective holds, then another Buchi objective must also hold). A generalization of one-pair Streett objectives is the k-pair Streett objective (aka general Streett objective) that consists of fc-Streett pairs (Li, Ui), (L2, U2), • • •, {Lk, Uk), and an infinite path satisfies the objective iff the condition for every Streett pair is satisfied (in other words the objective is the conjunction of k one-pair Streett objectives). We study (1) game graphs with one-pair Streett objectives and (2) graphs with general Streett objectives. Significance in verification. Two-player games on graphs are useful in many problems in computer science, specially in verification and synthesis of systems such as the synthesis of reactive systems [12], [36], [37], verification of open systems [2], checking interface compatibility [15], well-formedness of specifications [16], and many others. General and one-pair Streett objectives are central in verification as most commonly used specifications can be expressed as Streett automata [38], [42]. Game graphs with one-pair Streett objectives arise in many applications in verification. We sketch a few of them. (A) Timed automaton games are a model for real-time systems. The analysis of such games with reachability objectives and safety objectives (which are the dual of reachability objectives) reduces to game graphs with one-pair Streett objectives [9], [11], [13], [14]. (B) The synthesis of Generalized Reactivity(l) (aka GR(1)) specifications exactly require the solution of game graphs with one-pair Streett objectives [4]; GR(1) specifications are standard for hardware synthesis [35] and even used in synthesis of industrial protocols [5], [23](C) Finally, the 'A gr(1) specification expresses that if a conjunction of Buchi objectives holds, then another conjunction of Biichi objectives must also hold, and since conjunction of Biichi objectives can be reduced in linear time to a single Biichi objective, a gr(1) specification reduces to implication between two Biichi objectives, which is an one-pair Streett objective. 1043-6871/15 $31.00 ©2015 ieee doi 10.1109/lics.2015.34 269 --, IEEE ®COmfÄy problem of fair simulation [26] between two systems also reduces to game graphs with one-pair Streett objectives [6]. General Streett objectives in standard graphs arise, for example, in the verification of closed systems with strong fairness conditions [17], [22], [31]. In program verification, a scheduler is strongly fair if every event that is enabled infinitely often is scheduled infinitely often. Thus, verification of systems with strong fairness conditions directly corresponds to checking the non-emptiness of Streett automata, which in turn corresponds to determining the winning set in standard graphs with Streett objectives. Note, however, that a Streett objective can either specify desired behaviors of the system or erroneous ones, and for erroneous specifications, it is useful to have a certificate (as defined below) to identify an error trace of the system [17], [18], [31]. Note that standard graphs are relevant for the verification of closed systems or open systems with demonic non-determinism (e.g., all inputs are from the environment that are not controllable); while game graphs are relevant for the synthesis and verification of open systems with both angelic and demonic non-determinism (e.g., certain inputs are controllable, and certain inputs are not controllable). Previous results. We summarize the previous results for game graphs and graphs with Streett objectives. Game graphs. We consider the computation of the winning set for player 1 in game graphs. For reachability objectives, the problem is PTIME-complete, and the computation can be achieved in time linear in the size of the graph [3], [27]. For Bilchi objectives, the current best known algorithm requires 0(n2) time [7], [8]. For general Streett objectives, the problem is coNP-complete [19], and for one-pair Streett objectives the current best known algorithm requires 0(nm) time [29]. One-pair Streett objectives also corresponds to the well-known parity games problem with three priorities (the parity games problem in general is in UP n coUP [28]; it is one of the rare and intriguing combinatorial problems that lie in UP n coUP, but not known to be in PTIME). Despite the importance of game graphs with one-pair Streett objectives in numerous applications and several algorithmic ideas to improve the running time for general parity games [30], [39], [43] or Biichi games [7], [8], [10], there has been no algorithmic improvement since 2000 [29] for one-pair Streett games. Graphs. In standard graphs we study the computation of the winning set for general Streett objectives. If x belongs to the winning set, it is often useful to output a certificate for x. Let S be a (not necessarily maximal) strongly connected component (sec) that is reachable from x such that for all 1 < j < k we have either S(~)Lj = 0 or SCiUj 0 (i.e., if S contains a vertex from Lj then it also contains a vertex from Uj). A certificate is a "lasso-shaped" path that reaches S and then visits all vertices in S infinitely often to satisfy the general Streett objective. The basic algorithm [21], [32] for the winning set problem has an asymptotic running time of 0((m + b) min(ra, k)) with b = X!j=i(l^jl + Wj\) < Ink. Within the same time bound Latvala and Heljanko [31] additionally compute a certificate of size at most nmin(n, 2k). Duret-Lutz et al. [17] presented a space-saving "on-the-fly" algorithm with the same time complexity for the slightly different transition-based Streett automata. The current fastest algorithm for the problem by Henzinger and Telle [25] from 1996 has a running time of 0(mmin(-^/mlogra, + &min(logra, k)); however, given a start vertex x, to report the certificate for x adds an additive term of 0(ramin(ra, k)) to the running time bound. Our contributions. In this work our contributions are two-fold. Game graphs. We show that the winning set computation for game graphs with one-pair Streett objectives can be achieved in 0{n2-5) time. Our algorithm is faster for m > n15, and breaks the long-standing 0(nm) barrier for dense graphs. We also discuss the implications of our algorithm for general parity games in Remark 1. Graphs. We present an algorithm with 0(n2 + &logra) running time for the winning set computation in graphs with general Streett objectives, which is faster for m > max(ra4/3log~1/3ra, &2/3log1/3ra) and k > n2/m. We additionally give an algorithm that computes a certificate for a vertex x in the winning set in time 0(m + nmin(n, k)). We also provide an example where the smallest certificate has size 0(ramin(ra, k)), showing that no algorithm can compute and output a certificate faster. In contrast to [25] the running time of our algorithm for the winning set computation does not change with certificate reporting. Thus when certificates need to be reported and k = f2(ra), our algorithm is optimal up to a factor of log n as the size of the input is at least & and the size of the output is Q.(n2). Technical contributions. Both of our algorithms use a hierarchical (game) graph decomposition technique that was developed by Henzinger et al. [24] to handle edge deletions in undirected graphs. In [7], [8] it was extended to deal with vertex deletions in directed and game graphs. We combine and extend this technique in two ways. Game graphs. The classical algorithm for one-pair Streett objectives repeatedly solves Biichi games such that the union of the winning sets of player 1 in the Biichi games is exactly the winning set for the one-pair Streett objective. Schewe [39] showed that an algorithm for parity games by Jurdzinski [29] can be used to compute small subsets of the winning set of player 1, called dominions, and thereby improved the running time for general parity games. However his ideas do not improve the running time for one-pair Streett (aka parity-3) games. With this algorithm dominions with at most h vertices in Biichi games can be found in time 0(mh). We extend this approach by using the hierarchical game graph decomposition technique to find small dominions quickly and call the 0(n2) Biichi game algorithm of [7], [8] for large dominions. This extension is possible as we are able to show that, rather surprisingly, it is sufficient to consider game graphs with O (nh) edges to detect dominions of size h (see Lemma 2). Graphs. In prior work that used the hierarchical graph decomposition technique the runtime analysis relied on the fact that identified vertex sets that fulfilled a certain desired 270 condition were removed from the (game) graph after their detection. The work for identifying the vertex set was then charged in an amortization argument to the removed vertex set. This is not possible for general Streett objectives on graphs, where sees are identified and some but not all of its vertices might be removed. As a consequence a vertex might belong to an identified sec multiple times. We show how to overcome this difficulty by identifying, when an see S splits into multiple sees, an sec IcS whose size is at most half of the size of S. We identify X by using Tarjan's sec algorithm [41] on the graph and its reverse graph, thereby finding the smallest top (i.e. with no incoming edges) or bottom (i.e. with no outgoing edges) sec contained in S. The smallest such sec X has size at most (S11/2 and the algorithm takes time 0{\X\n) to find it, i.e., 0(n) time per vertex in X. This will allow us to bound the total running time for this part of the algorithm with 0(n2) In Section II we present our algorithm for one-pair Streett objectives in game graphs, in Section III the algorithm for general Streett objectives in graphs. II. One-Pair Streett Objectives in Game Graphs A. Preliminaries Parity games. A parity game P = (G, a) consists of a game graph G = ((V, E), (Ve>, Vg)) and a priority function a : V —> Z that assigns an integer value to each vertex. We denote the two players with O (for odd) and £ (for even). Player O (resp. player £) wins a play if the lowest priority occurring in the play infinitely often is odd (resp. even). We say that the vertices in Vq are O-vertices and the vertices in Vs are ^-vertices. We use p to denote one of the players {O, £} and p to denote his opponent. We will specifically consider parity-3 games with a : V —> {—1, 0,1} and Biichi games with a : V —> {0,1}, where the vertices in the set B = {v a(v) = 0} are called Biichi vertices. Biichi games are denoted as (G,B). One-pair Streett and parity-3 games. A one-pair Streett objective with pair (Li,C/i) is equivalent to a parity game with three priorities. Let the vertices in U\ have priority — 1, let the vertices va.L\\U\ have priority 0 and let the remaining vertices have priority 1. Then player 1 wins the game with the one-pair Streett objective if and only if player O wins the parity-3 game. As the known algorithms for parity-3 games are special cases of algorithms for general parity games, we will use the notion of parity games (i.e., player O and player E instead of player 1 and player 2). Plays. For technical convenience we consider that every vertex in the game graph G has at least one outgoing edge. A game is initialized by placing a token on a vertex. Then the two players form an infinite path called play in the game graph by moving the token along the edges. Whenever the token is on a vertex in Vp, player p moves the token along one of the outgoing edges of the vertex. Formally, a play is an infinite sequence (vq, vi, t>2,...) of vertices such that (vj,vj+i) € E for all j>0. For a vertex u 6 V, we write Out(u) = {v 6 V \ (u, v) 6 E} for the set of successor vertices of u and In(u) = {v 6 V | (v, u) 6 E} for the set of predecessor vertices of u. We denote by Outdeg(u) = \ Out(u) \ the number of outgoing edges from u, and by Indeg(u) = \ In(u)\ the number of incoming edges. Strategies. A strategy of a player p 6 {O, £} is a function that, given a finite prefix of a play ending at v 6 Vp, selects a vertex from Out(v) to extend the play. Memoryless strategies do not depend on the history of a play but only on the current vertex. That is, a memoryless strategy of player p is a function t '. Vp —y V such that for all v 6 Vp we have t(v) 6 Out(v). It is well-known that for parity games it is sufficient to consider memoryless strategies (see Theorem 1 below). Therefore we will only consider memoryless strategies from now on. A start vertex v together with a strategy a for E and a strategy it for O defines a unique play ui(v, a, it) = (vq,vi,V2, ■ ■ •), which is defined as follows: v0 = v and for all j > 0, if Vj 6 Vs, then u(vj) = Vj+i, and if vj 6 Vo, then it(vj) = Vj+i. Winning strategies and sets. A strategy t is winning for player p at start vertex v if the resulting play is winning for player p irrespective of the strategy of player p. A vertex v belongs to the winning set Wp of player p if player p has a winning strategy from v. By the following theorem every vertex is winning for exactly one of the two players. When required for explicit reference of a specific game graph G or specific parity game P we use WP(G) and WP(P) to refer to the winning sets. Theorem 1 ([20], [34]): For every parity game the vertices V can be partitioned into the winning set Ws of £ and the winning set Wq of O. There exists a memoryless winning strategy for E (resp. O) for all vertices in Ws (resp. Wq). The algorithmic question for parity games is to compute the set Ws. We will use the following algorithm for Biichi games as a subroutine in our algorithm. Theorem 2 ([7], [8]): Let (G,B) be a Biichi game with game graph G and Biichi vertices B. There is an algorithm Buchi(G, B) that computes W£ in time 0(n2). For the analysis of our algorithm we further introduce the notions of closed sets, attractors, and dominions. Closed sets and attractors. A set U C V is p-closed if for all p-vertices u in U we have Out(u) C U and for all p-vertices v in U there exists a vertex w 6 Out(v) n U. Note that player p can ensure that a play that currently ends in a p-closed set never leaves the p-closed set against any strategy of player p by choosing an edge (v,w) with w 6 Out(v) n U whenever the current vertex v is in U (~)VP (see also [8, Proposition 2.2]). Given a game graph G and a p-closed set X, we will denote by G[X] the game graph induced by the set X of vertices. In a game graph G, a p-attractor Attrp(U,G) of a set U C V is the set of vertices from which player p has a strategy to reach U against all strategies of player p. We have that U C Attrp(U, G). A p-attractor can be constructed inductively as follows: Let R0 = U; and for alii > 0 let Rl+1 =RlU{veVp | Out(v) n Rt 0} U{veVp\ Out(v) C Rt}. 271 Then Attrp(U, G) = {Ji>0 Ri- The lemma below summarizes some well-known facts about closed sets, attractors, and winning sets. Lemma 1: Let p 6 {€),£} and let U C V. The following assertions hold for parity games. 1) The set V \ Attrp{U, G) is p-closed in G [44, Lemma 4]. 2) Let U be p-closed. Then Attrp{U, G) is p-closed [44, Lemma 5]. 3) The attractor Attrp(U,G) can be computed in 0(E^«,pWG)I^HI)time[3], [27]. 4) Let U be a subset of the winning set WP(G) of player p and let A be its p-attractor Attrp (U,G). Then the winning set WP(G) of the player p is the union of A and the winning set WP(G[V \A]) in the game graph induced by V \ A, and the winning set WP(G) of the opponent p is equal to WP(G[V \ A}) [30, Lemma 4.5]. Dominions. A set of vertices D C V is a p-dominion if D ^ 0, player y> has a winning strategy from every vertex in D that also ensures only vertices in D are visited, and D is a p-closed set. We will only consider ^-dominions in this paper and therefore usually omit the reference to the player. Dominions of size \D\ < h can be computed by running the small-progress measure algorithm of Jurdzifiski [29] with a reduced codomain [39]. A description of the small-progress measure algorithm for Buchi games is given in [8, Section 2.4.1]. We will use the following algorithm as a subroutine. Theorem 3 ([8], [29], [39]): Let (G, B) be a Buchi game with game graph G and Buchi vertices B. There is an algorithm BuchiProgress(G, B, h) that returns the set of all dominions of size at most h in time O(mh). B. Algorithm In this section we present our new algorithm to compute the winning set of player E in a parity-3 game P = (G, a) in time 0(n2-5). Its complement is the winning set of player O. Initialization (Steps 1-4 of Algorithm 1). First the algorithm constructs the modified game graph G' = ((V, E'), (Vq, Ve)) from G. Let Z be the vertices in V with priority —1. In G' the vertices in Z are made absorbing, that is, the outgoing edges of the vertices in Z are replaced with self-loops. Otherwise G' contains the same edges as G. We will consider a Buchi game on G' where the vertices in Z have priority 1, and thus in the Buchi game there are only two priorities (priority 0 and 1). The construction of G' ensures that dominions in the Buchi game are also dominions in the parity-3 game P (see Lemma 5). Iterated vertex deletions (Steps 5-11 of Algorithm 1). The algorithm will repeatedly remove vertices from the graphs G and G'. Initially the set V is the set of vertices in the input game graph G. During the algorithm, we denote with V the set of remaining vertices after vertex deletions and we denote with G[V] and G'[V] the subgraphs induced by the vertices remaining in V. The set of Buchi vertices B maintains the set of priority-0 vertices in V. The vertex set removal is achieved by identifying dominions and removing their attractors. Input a game graph G = ((V,E), (Ve>, V^)) and a priority function a : V —> {— 1, 0,1} Output the winning set Ws of player E 1: Z = {v eV \ a(v) = -1} 2: E' = {{u,u) u e z} u {(u,v) e E I u e V \ z} 3: G' = (V, E') t> vertices with a = —1 are absorbing in G' 4: W <- 0, B <- {v e V a(v) = 0} 5: repeat 6: D <— BuCHlDOM(G'[y], B, \Jn) 1: if D = 0 then 8: D <- BUCHI(G'[V],B) 9: A^ Attr£(D,G[V});W ^WUA 10: V <-V\A; B^B\A 11: until D = 0 12: return W 13: procedure BuchiDom(G'[V],B, hmm) 14: for i <- 1,..., riog(frmax)] do 15: construct G\ 16: Bk <-{veV0\ Outdeg(v) > 21} 17: Yii-AtbroiBluG'A 18: T>i <- BUCHlPROGRESS(G^[y \y2],B\y2,2J) 19: if T>i ± 0 then 20: return union of dominions in T>i 21: return 0 Fig. 1. New Algorithm for Parity-3 aka One-Pair Streett Objective Dominion find and attractor removal. The algorithm repeatedly finds dominions in the Buchi game (G' [V], B). After a dominion in the Buchi game G'[V] is found, its 5-attractor in G[V] is removed from V and B. Then the search for dominions is continued on the remaining vertices. If all vertices in the Buchi game are winning for O, i.e., no dominion exists in the Buchi game, then Algorithm 1 terminates. The winning set of player £ is the union of the E-attractors of all found dominions. The remaining vertices are winning for player O. We now describe the steps to find dominions. Steps of dominion find. For the search for dominions in the Buchi game (G' [V], B) we use two different algorithms, Buchi and BuchiDom. We first search for "small" dominions with up to 0{hmta) vertices with /imax = y/n with Procedure BuchiDom. If no dominion is found, we can conclude that either all dominions contain more than ^fn vertices or the winning set of £ on the current game graph is empty (in this case the algorithm terminates). The former case occurs at most ^/n times and in such a case we use the 0(n2) algorithm buchi (Theorem 2) to obtain a dominion. Below we describe the details of BuchiDom. Graph decomposition for BuchiDom. In the Procedure BuchiDom we use the following graph decomposition. For a game graph G' = ((V, E'), (Vq, V^)) we denote its decomposition with {G'{}. We consider the incoming edges of each vertex in E' in a fixed order: First the edges from 272 vertices in V£, then the remaining edges. We define [logra] graphs G\ = (V, e'{), 1 < i < [logra], where the set of edges e[ contains for each vertex v € V with Outdeg(v) < 2J all its outgoing edges in e' and in addition for each vertex v €v its first t incoming edges in e'. Note that (1) e[ C e'i+1, (2) \e[\ < 2t+1n, and (3) G'riognl = G'. We color O-vertices v with Outdeg(v) > 2J blue in G'{ and denote the set of blue vertices with Bli. We call vertices with Outdeg(v) < 2J white. Procedure BUCHIDOM {Steps 13-21 of Algorithm 1). The Procedure BuchiDom searches for dominions in the subgraphs G\, starting at i = 1. The index i is increased one by one up to at most i = [log(/imax)] (with /imax = •s/n) as long as no dominion was found. Let Yi be the O-attractor of blue vertices in G\, i.e., of O-vertices that are missing outgoing edges in G\. To ensure that dominions found in the subgraph G'{ are also dominions in G', only the vertices in V \ Yi are considered. The BuchiProgress algorithm (Theorem 3) is used to find dominions of size at most 0(2J) in G'{[V \ Yi]. The following key lemma describes the central connection between dominions of a certain size and our graph decomposition. Namely, if a dominion D is found in G\ but not in G'i_x, then Attr£(D,G') contains more than 2J_1 vertices. This has the remarkable consequence, detailed in Corollary 1, that every dominion of size h can be found by searching for a dominion in G'i with i = |~log(/i)]. This will be crucial for our runtime analysis. Lemma 2: Let G' = ((V, e'), {Vq, V£)) be a game graph and {G'{} its graph decomposition. For 1 < i < [logra] we define the following sets: the set of blue vertices Bli = {v 6 Vq Outdeg(v) > 22}, the attractor of blue vertices Yi = Attro(Bli,G'i), and the set of dominions T>i = BuchiProgress [G't[V \Yt],B\ Yt, 2J). If a dominion D is contained in T>i but not in X>i_i, then Attr£(D,G') contains more than 2J_1 vertices. Proof: We distinguish three cases: Case 1: The dominion D contains more than 2«-i vertices. This situation might arise as Procedure BuchiProgress (G^_ 1 [V \ Y2_i], B \ Y2_i, 2J"1) only guarantees to detect dominions of size at most 2J_1. In this case the lemma is satisfied trivially. Case 2: The dominion D contains a vertex v 6 Vq that is blue in G'i_1, i.e., an O-vertex with more than 2J_1 outgoing edges. Since D is O-closed, we have Out(v) C D. Thus \Attr£(D,G')\ > \D\ > 2i_1 in this case. Case 3: All vertices v 6 Vq in D are white in G'i_1 and thus the outgoing edges of the O-vertices in D are the same in G'i_1 and G\. There are two subcases. Case 3a: All edges (w, v) from vertices u 6 Vs l~l D to vertices v 6 D that are present in G\ are also present in G'i_1. Let a be the winning strategy of E for the vertices in D found in G'i- This implies that (i) D is O-closed in G'i_1 and (ii) all edges (w, v) with u 6 D n Vs and v = a(u) are contained in G'i_1. Thus a is also a winning strategy of E for the vertices in D in G'i_1. Hence the set D is a dominion in G'i_1. Thus either Case 1 applies or the dominion would already have been detected in iteration i — 1, a contradiction. Case 3b: There exists a vertex u 6 Vs l~l D that has an outgoing edge (w, v) to a vertex v 6 D in G\ but not in G'i_1. This implies Indeg(v) > 2J_1. By the ordering of the incoming edges and the fact that u e 1^, at least 2J_1 edges in In(v) emanate from vertices in Vs. By the definition of an attractor, all these vertices are contained in Attr^D, G'). Thus we have \Attr£(D,G')\ > 2i_1 as required. ■ Corollary 1: Let G", {G'{}, Bli, Yi, and T>i be defined as in Lemma 2. Let D be a dominion in G" with D = Attr£(D, G") and h = \D\. Then for i = [log(/i)] the set of dominions T>i contains D. Proof: By the definition of i we have 2J_1 < h < 2\ Assume by contradiction that T>i does not contain D. Since and Ypiogn] = 0> by Theorem 3 there exists some with i < i' < [logra], such that XV contains D. Let i* be the smallest i' such that XV contains D. Note that i* > i+ 1. We have that D ^ XV-i- By Lemma 2 this implies \Attr£(D, G")| > 2i*-1 > 2% a contradiction to h < 2\ ■ Corollary 2: Either the Procedure BuCHlDOM(G"[y], B, /imax) returns a dominion or every dominion L> in G'[V] with D = .4ttr£(D,G'[y]) has size greater than /imax. In the runtime analysis we will additionally use the following lemma, which follows from the inductive construction of attractors. Lemma 3: Let the game graphs G and G' and the vertex set V be defined as in Algorithm 1. Then for a player p 6 {£, O} and every set U C V it holds that Attrp(U, G'[V]) C ^ttrp(C/,G[y]). Proof: Let us consider the attractor computation Attrp(U,G'[V]) and Attrp(U, G[V]) as defined in (J), and let us call the respective sequences as R'{ and Ri respectively. By the definition of G' for every vertex v in V either (1) Out'(v) = Out(v) or (2) Out'(v) = {v}. It is straightforward to prove by induction that R'{ C R{ and the desired result follows. ■ Lemma 4 (Runtime): Algorithm 1 can be implemented in 0(n2-5) time. Proof: Algorithm 1 can be initialized in 0(m) time as the graph G' and the set B can be constructed from G in linear time. Note that the number of edges m! in G' is at most the number of edges m in G. For the operations in the repeat-until loop we analyze the total running time over all iterations of the loop. The runtime analysis relies on the fact that when a dominion D is identified, the vertices in Attr£(D, G) and their incident edges are removed from G and G'. In combination with Corollary 2, this ensures that BUCHI is called at most 0{n/hmta) times. By Theorem 2 one call to BUCHI takes time 0(n2). With /imaj = y/n we obtain a total time spent in BUCHI of 0(n2-5). To analyze the total time spent in BuchiDom, we first show how to efficiently construct the graph decomposition {G'i} of G'. We maintain the following data structure for G' over all iterations of Algorithm 1. At each vertex v of G' we maintain (a) a sorted list of inedges In(v), and (b) a list of outedges Out(v). Additionally we maintain for each edge 273 (u, v) a pointer to its position in the inlist of v and in the outlist of u. This allows us to update the data structure in time proportional to the degree of v when a vertex v is removed. As each vertex can be deleted at most once, the total time to update this data structure is bounded by 0(m). We next analyze the time needed per iteration i of the for-loop in BtJCHlDOM. Given the above data structure, the graph G[, the set of blue vertices Bli, and the attractor Y{ = Attro(Bli,G'i) can be constructed in time 0(n ■ 2J). By Theorem 3 the time for one call of the subroutine BuchiProgress(., .,2j) on graph G[, is 0(n- 2J • 2J) = 0{n-22t). Let i* be the iteration at which Procedure BuchiDom stops after it is called by Algorithm 1. The runtime for this call to Procedure BuchiDom from i = 1 to i* forms a geometric series that is bounded by 0{n-22t ). By Lemmata 2 and 3 and Corollary 2 either (1) a dominion D with \Attr£(D1G)\ > 2« -i vertices was found by BuchiDom or (2) all dominions in G' have more than /imax vertices or there are no more dominions in G'. Thus either (2a) a dominion D with more than /imax vertices is detected in the subsequent call to BUCHI or (2b) there is no dominion in G' and this is the last iteration of Algorithm 1. Case (2b) can happen at most once and its runtime is bounded by 0(ra-221ogClm™)) = 0(n2). In the cases (1) and (2a) more than 2J _1 vertices are removed from the graph in this iteration, as /imax > 2J _1. We charge each such vertex 0(n ■ 2l ) = 0(n ■ /imax) time. Hence the total runtime for these cases is 0(n2 ■ /imax) = 0(n2-5). It remains to consider the total time needed to compute A = Attr£(D, G[V]). By Lemma 1. (3) the attractor A can be computed in time 0(^2veA\In(v)\). Since the edges adjacent to vertices in A are removed from G after the iteration in which D was found, this attractor computation can be done in total time O (m). We conclude that the runtime of Algorithm 1 is 0(n2-5). m We will show the correctness of Algorithm 1 by first proving that every dominion found in the Biichi game on G' is indeed a dominion in the parity-3 game on G. Together with Lemma 1. (4) this implies that the computed set W is indeed a part of the winning set of player E in the parity-3 game. We then provide a winning strategy for player O for all remaining vertices. Lemma 5: Let the game graphs G and G' and the vertex sets V and B be defined as in Algorithm 1. If D is a dominion in the Biichi game (G'[V], B), then D is a dominion in the parity-3 game P = (G[V], a). Proof: Let Z be the vertices in V with priority a equal to —1. The vertices in Z have priority 1 in the Biichi game, i.e., Z n B = 0. Whenever a play in G'[V] reaches a vertex u in Z, only u will be visited in the subsequent play since Out(u) = {«}. Thus no vertex in Z is winning for E in (G'[V],B), i.e., D n Z = 0. Hence for all vertices in D the outgoing edges are the same in G[V] and G'[V]. Thus D is O-closed in G[V] and the winning strategy of player £ for D in the Biichi game (G' [V], B) is also winning for player E for all vertices in D in the parity-3 game P. ■ Lemma 6 (Correctness): Given a parity-3 game P, let W be the output of Algorithm 1. We have: (1) (Soundness). W C W£(P); and (2) (Completeness). W£{P) C W. Proof: The first part on soundness follows from Lemmata 5 and 1. (4). We now prove the completeness result. Given the output W, let W denote the complement set. When Algorithm 1 terminates, the winning set of player £ in the Biichi game (G' [W], B) is empty (otherwise the algorithm would not have terminated). Also note that since the algorithm removes attractors for £, the set W is closed for E (by Lemma 1. (1)). Consider the set Z = {v 6 W a(v) = —1}, its attractor X = Attro(Z,G[W]), and the subgame induced by U = W \ X. Note that in U the game graphs G and G' coincide. Thus all vertices in U must be winning for player O in the Biichi game (G[f7], B) as otherwise W£ would have been non-empty for (G'fW7], B). We prove the lemma by describing a winning strategy for player O in P for all vertices in W. Since W is 5-closed, for vertices in Z n Vq, the winning strategy chooses an edge in W. For vertices in X player O follows his attractor strategy to Z. In the subgame induced by U = W \ X player O follows his winning strategy in the Biichi game (G[f7], B). Then in a play either (i) X is visited infinitely often; or (ii) from some point on only vertices in U are visited. In the former case, the attractor strategy ensures that then some vertex in Z with priority —1 is visited infinitely often; and in the later case, the subgame winning strategy ensures that only vertices with priority 1 and no vertices with priority 0 are visited infinitely often. It follows that W C Wo{P), i.e., W£ (P) C W, and the desired result follows. ■ Lemmata 4 and 6 yield the following result. Theorem 4: Algorithm 1 correctly computes the winning sets in parity-3 games in 0(n25) time. Computation of winning strategies. In parity-3 games the previous results for computing winning strategies for the players in their respective winning sets are as follows: The small-progress measure algorithm of [29] requires 0{nm) time to compute the winning strategy of the player whose parity is equal to the parity of the lowest priority and 0{n2m) time to compute the respective winning strategies for both players; Schewe [40] shows how to modify the small-progress measure algorithm to compute the respective winning strategies of both players in O(nm) time. We show that our algorithm also computes the respective winning strategies in 0(n25) time. We first observe that the algorithm of [7], [8] that solves Biichi games in 0(n2) time also computes the respective winning strategies of both players (the algorithm is based on identifying traps and attractors, and the corresponding winning strategies are identified immediately with the computation). In Lemma 6 we describe the strategy computation for a winning strategy for player O which involves an attractor strategy and the sub-game strategy for Biichi games, each of which can be computed in 0(n2) time. A winning strategy for player E is obtained in the iterations of the algorithm, i.e., whenever we obtain a dominion by solving Biichi games we also obtain a corresponding winning strategy, and similarly for the attractor computation. Thus the winning strategy for player £ can be 274 computed in 0(n25) time. Corollary 3: Winning strategies for player E and player O in parity-3 games in their respective winning sets can be computed in 0(n2-5) time. Remark 1: (discussion on general parity games). We now discuss the implication of our result for general parity games (we do not discuss general Streett games where the problem is coNP-complete [19]). The current best known algorithm for parity games with dependence on the number of priorities d is from [39], and the algorithm is referred as the Big-step algorithm. The (simplified) running time of the Big-step algorithm for d = o(y/n) is 0(ra7(d) • m), where 7(d) is approximately d/3 for large d. More precisely, 7(d) = d/3 + 1/2 - l/([0.5d]L0.5dJ) for odd d, and 7(d) = d/3 + 1/2 - l/(3d) - l/([0.5d] [0.5dJ) for even d. Our algorithm for parity-3 games also extends to parity games as a recursive algorithm as follows: we apply our initialization step and iterated vertex deletions, and to find dominions we replace buchi by our recursive algorithm that handles games that have one less priority and replace BuchiDom by a procedure to find dominions with small-progress measure of [29] with our graph decomposition and codomain bounded by /imax (where /imax is chosen to balance the running time of the two dominion find procedures). Note that, in contrast to the Big-step algorithm, we apply the small-progress measure algorithm on a game with one less priority; this does not influence the correctness as we find (possibly different) dominions for the same player as in the recursion of the Big-step algorithm but slightly changes the running time analysis. For the sake of simplicity of presentation we present the analysis for the case of constantly many priorities, extending the analysis of [39] in combination with our approach (the extension for the general case follows from a similar extension of the analysis of the general case of [39]). Similar to the analysis and notation of [39], let /3(d) = 7(d)/([0.5dJ + 1). With hmm = -nP^ we obtain that the running time of our algorithm is 0(ra1+T(d+1)) = 0(n2+7(d)-/3(d)) for parity games with d priorities, i.e., it replaces m of [39] by n2~l3<-d\ We present the details of the calculation. We show by induction that our algorithm solves parity games with d — 1 priorities in 0(n1+1<-d*>) time. The base case of d — 1 = 3 follows from our algorithm for parity-3 games. The inductive case is as follows: To solve a parity game with d priorities, our algorithm calls the progress measure algorithm (on the graph decomposition) for d — 1 priorities and recursively calls the algorithm for d — 1 priorities at most 0(ra1-,3(d)) times. The total time for the progress measure algorithm is bounded by 0(n2 ■ (/w)L°-MJ) = 0(n2 ■ nmi0-5d\^ and me tQtal time for all calls to the algorithm for d — 1 priorities is bounded by 0((ra//w) • n1+7(d)) = 0(n1_/9^ • ra1+7^). We obtain the recurrence j(d + 1) = 1 + 7(d) — /3(d), which yields 7(d) as defined above and a running time of 0(n1+1<-d+1*>) for d priorities. In the limit /3(d) approaches 2/3. For small d we compare our running times with the Big-step algorithm in Table I. We have presented the details for parity-3 games for the following reasons: (1) All the key ideas and conceptual details are easily demonstrated for the simpler case of parity-3 games and (2) while all previous ideas for general parity games (such as [30], [39]) and for Buchi games (such as [7], [8], [10]) fail to improve the running time for parity-3 games, our approach succeeds to break the long-standing O(nm) barrier for dense graphs. III. K-Pair Streett Objectives in Graphs A. Preliminaries Let G[S] denote the subgraph of a graph G = (V, E) induced by the set of vertices S C V. RevG denotes the graph with vertices V and all edges of G reversed. Let Reach(S, G) be the set of vertices in G that can reach a vertex in S C V. A strongly connected component (sec) of a directed graph G = (V, E) is a subgraph G[S] induced by a subset of vertices S C V such that there is a path in G[S] between every pair of vertices in S. We call an sec trivial if it only contains a single vertex and no edges. All other sees are non-trivial. The set Reach(S, G) and the maximal sees of a graph G can be found in linear time [3], [27], [41]. Algorithm streett and good component detection. The input is a directed graph G = (V, E) and k Streett pairs [Lj,Uj), j = 1,..., k. The size of the input is measured in terms of m = \E\, n = \V\, k, and b = X!j=i(l-^jl + \Uj\) < nk. Consider a maximal sec C; the good component detection problem asks to (a) output a non-trivial sec G[X] C C induced by some set of vertices X such that for all 1 < j < k either no vertex in Lj or at least one vertex in Uj is contained in the sec (i.e., L3; n X = 0 or U3; n X ± 0), or (b) detect that no such sec exists. In the former case, there exists an infinite path that visits X infinitely often and satisfies the Streett objective, while in the later case there exists no infinite path that visits vertices in C infinitely often and satisfies the Streett objective. It follows from the results of [1] that the following algorithm, called Algorithm streett, suffices for the winning set computation: (1) Compute the maximal see decomposition of the graph; (2) for each maximal sec C for which the good component detection returns an sec, label the maximal sec C as satisfying; (3) output the set of vertices that can reach a satisfying maximal sec as the winning set. Since the first and last step are linear time, the runtime of Algorithm Streett is dominated by the detection of good components in maximal sees. In the following we assume that the input graph is strongly connected and focus on good component detection. B. Certificate computation In this section we present our results for the certificate computation. Given a start vertex x that belongs to the winning set, a certificate is an example of an accepting run, i.e., an infinite path from x that satisfies the objective. The output of Algorithm streett can be used to construct such an accepting run. Given a start vertex x and a good component G[X] induced by some set of vertices X that is reachable from x, we generate the accepting run as follows. A path from x to X can be found 275 TABLE I Comparison of Running Times for Few Priorities. Algorithm # priorities 3 4 5 6 7 Big-step [39] O(rnn) 0(mn3/2) 0(mn2) 0(mn7/3) 0(mnn/4) Big-step [39] with rn — &(n2) 0(n3) 0(n7/2) 0(n4) 0(n13/3) 0(n19/4) Our algorithm 0(n2-5) 0(n3) 0(n10/3) 0(n15/4) 0(n65/16) in linear time by a depth-first search. Let v be the vertex in X where this path ends. We call v the root of the see G[X]. We show next how to obtain, in 0(m + nmin(n, k)) time, from the sec G[X] a cycle starting and ending at the root v such that the resulting certificate is indeed an accepting ran. For this it is sufficient that the cycle in G[X] contains for each Lj with Lj n X 0 a vertex of Uj D X, i.e., we do not have to include all vertices in X. We can use Tarjan's depth-first search based sec algorithm [41] to traverse the subgraph G[X] in linear O(m) time, starting from root v. Tarjan's algorithm constructs a graph called jungle with 0(\X\) edges that for an sec G[X] consists of a spanning tree and at most one backedge per vertex in X. The vertices are assigned pre-order numbers in the order they are traversed. We say an edge of G[X] is a backedge if it leads from a vertex with a higher number to a vertex with a lower number. Spanning tree edges always lead from lower numbered vertices to higher numbered vertices. In Tarjan's algorithm a lowlink is determined for each vertex u which refers to the lowest numbered vertex w that u can reach by a sequence of tree edges followed by at most one backedge. We additionally store at each vertex u v a backlink that is the first edge on the path from u to its lowlink. The backlinks can be determined and stored during the depth-first search without increasing its running time. With this data structure we can find within G[X] a path from root v to a vertex u 6 X, u v, and back by first searching for u in the spanning tree and then following the backlinks back to v. Since no vertex will appear more than twice on this path, its size and the time to compute it is 0{\X\). As it suffices to find such paths for one vertex per non-empty set UjDX, we can generate a certificate from G[X] in 0(m + \X\ min(|X|, \{j [/jfll/ 0}|)) time, which can be bounded with 0(m + nmin(n, k)). This certificate has a size of 0(nmin(n, k)). Example 1 (Illustration of Tarjan's jungle graph.): Figure 2 shows the types of edges and the values at the vertices as assigned by Tarjan's sec algorithm for a small example graph. Example 2 (Lower bound.): Figure 3 shows that the smallest existing certificate can be as large as 0(ramin(ra, k)). C. Algorithm In this section we present the algorithm for good component detection. First we introduce the different concepts used in the algorithm for good component detection. We start with Fig. 2. An example for a "jungle" constructed by Tarjan's sec algorithm for an scc. Backedges are dotted, spanning tree edges are solid. Backlinks are marked with a dot. The numbers of the vertices represent the order in which the vertices are visited, the numbers in brackets are the lowlinks. Fig. 3. Let the only path between s and t be of length 0(n/2) — O(n), not containing any of the vertices Vj for 1 < j < k. Let the Streett pairs (Lj, Uj) be given by Lj — {s} and Uj — {vj} for 1 < j < k. Then the size of the smallest certificate is O(nk), where k can be of order O(n). describing the hierarchical graph decomposition technique for this setting, which will be crucial for the runtime analysis. Graph decomposition. In our algorithm we decompose a graph G in the following way. For i 6 {1,..., [logra]}, let Gi = (V, Ei) be a subgraph of G with Ei = {(u,v) \ Outdeg(u) < 22}, i.e., the edges of Gi are the outedges of the vertices with outdegree at most 2\ Note that for i = [logra] we have that Gi = G. We say vertices in G with Outdeg(v) > 2J are colored blue in Gi and denote the set of blue vertices in Gi by Bli. All other vertices are white. Note that all vertices in G = Gfi0gn] are white and that all vertices in Bli have outdegree zero in Gi. Top and bottom strongly connected components. The algorithm will repeatedly find a top or a bottom SCC in the remaining graph G. A bottom SCC G[S] in a directed graph G, induced by some set of vertices S, is an SCC with no edges from vertices in S to vertices in V \ S, i.e., no outgoing edges. A top SCC is a bottom SCC of RevG, i.e., an SCC without incoming edges. Top and bottom sees are by definition maximal sees. Note that every graph has at least one bottom and at least one top SCC. If they are not the same, then they are disjoint and thus one of them contains at most half of the vertices of G. Bad vertices. In contrast to good components we also define 276 bad vertices. The basic idea behind the algorithms for good component detection, described for example in [25], is to repeatedly delete bad vertices until either a good component is found or it can be concluded that no such component exists. A vertex is bad if for some index j with 1 < j < k the vertex is in Lj but it is not strongly connected to any vertex in Uj. All other vertices are good. Note that good vertices can become bad if some vertex deletion disconnects an see or a vertex of a set Uj is deleted. A good component is a non-trivial sec that only contains good vertices. Data structure. The algorithm maintains for the current graph G = (V, E) (some vertices of the input graph might have been deleted) a decomposition into vertex sets S C V such that every sec of G is completely contained in G[S] for one of the sets S. For all the sets S a data structure D(S) is saved in a list Q. The data structure D(S) supports the following operations: (1) Construct(S) initializes the data structure for the set S, (2) Remove(S1 D(S), B) removes a set B C V from S and updates the data structure of S accordingly, and (3) Bad(D(S)) returns the set {v e S 3j with v e Lj and Uj; n S = 0}. In [25] an implementation of this data structure was given that achieves the following running times. For a set of vertices S C V let bits(S) be defined as £*=1 (\S n L}\ + \S n U3\). Lemma 7 (Lemma 2.1 in [25]): After a one-time preprocessing of time 0(k), the data structure D(S) can be implemented in time 0(bits(S) + \S\) for Construct (S), time 0(bits(B) + \B\) for Remove(S, D(S), B), and constant running time for Bad(D(S)). By abuse of notation we denote by G the current graph maintained by the algorithm where some edges and vertices might have been deleted and use input graph to denote the unmodified, strongly connected graph for which a good component is searched. Our algorithm for good component detection is given in Algorithm 4. It maintains in a list Q a partition of the vertices in G into sets such that every sec of G is contained in the subgraph induced by one of the vertex sets. The list is initialized with the set of all vertices in the strongly connected input graph. We will show that if a good component exists, its vertices must be fully contained in one of the vertex sets in the partition. The algorithm repeatedly removes a set S from Q and identifies and deletes bad vertices from G[S]. If no edge is contained in G[S], the set S is removed as it can only induce trivial components. Otherwise the subgraph G[S] is either determined to be strongly connected and output as a good component or a "small" maximal see in G[S] is identified. To find a small maximal sec the algorithm searches alternatingly in G[S] and in RevG[S] for a bottom sec and stops as soon as one of the searches stops. (A bottom sec in RevG[S] is a top sec in G[S].) We use OutdegH(v) to denote the out-degree of a vertex v in H 6 {G, RevG}. We only describe the search in G[S] here, the search in RevG[S] is analogous. The algorithm uses the hierarchical graph decomposition of G[S]. The subgraph Gi[S] for any i contains only the outedges of vertices with an outdegree of at most 2\ The search for a bottom see is started at i = 1, then i is increased one Input strongly connected graph G = (V, E), Streett pairs (L]:Uj) for j = 1, Output a good component in G if one exists add Construct(V) to Q while Q ± 0 do pull D(S) from Q while Bad(D(S)) ^ 0 do D(S) 2J Z <-S \ Reach(Bk, Hi[S}) t> Z cannot reach Bli if Z 0 then X <- SmallestBSCC(Hi[Z]) if X = S then t> good component return G[S] if \X\ < \S\/2 then add Remove(S,D(S),X) to Q add Construct(X) to Q go to Line 2 return no good component exists Fig. 4. Detection of good components for the winning set computation in graphs with fc-pair Streett objectives by one if necessary, up to at most |~log(|S|)]. If for some i we can identify a bottom sec that does not contain any blue vertex (i.e., a vertex for which some edges are missing in Gi), then the found sec in Gi[S] must also be a bottom sec in G[S]. If multiple bottom sees (without blue vertices) are found in Gi[S], we only consider the smallest one. The Procedure SmallestBSCC (Hr) returns the set of vertices that induces the smallest bottom sec in the graph H'. We then put the newly detected see and the "rest" of S back into Q. The idea of the running time analysis is as follows. We can show that a bottom sec of G[S] identified in iteration i of the outer for-loop must contain f2(2J) vertices. In time 0(n2x) a standard sec algorithm can compute all sees of Gi[S] and thus also the smallest bottom sec. The time needed for the search in all graphs Gi> [S] for 1 < i' < i can be bounded with an additional factor of two. Thus the work for the search is 0(n) per vertex in the identified sec. Given that the subgraph G[S] was split into at least one top and one bottom see, the smallest top or bottom sec contains at most half of the vertices of the subgraph. By searching for a smallest bottom sec (without blue vertices) in Gi[S] and RevGi[S], we find one top or bottom sec with at most half of the vertices of the subgraph. We charge the work for finding such an sec to the vertices in this see. We will show that this yields a total running time of 0(n2) for computing sees. We additionally have to take the time for the maintenance 277 of the data structures into account. Here we use the properties of the data structure D(S) described in Lemma 7 to obtain a running time of 0((n + b) logra) for the maintenance of the data structures and the identification of bad vertices over the whole algorithm. Combined these ideas lead to a total running time of O (n2 + b log n). Lemma 8: Let H 6 {G, RevG} be the graph and let i* be the iteration for which in Algorithm 4 the outer for-loop stops. Let Z be the non-empty set S\Reach(Bli», H{» [S]) and let X be the set of vertices that induces the smallest bottom see H[X] in Ht,[Z] returned by SmallestBSCC{Ht,[Z]). Assume we have \X\ < \S\/2. Then H[X] contains at least 2« -i vertices. Proof: As Bl^-i is the set of vertices in Hi»_i[S] with outdegree larger than 2J _1, any bottom see H[Y] that contains a vertex of Bl^-i, has \Y\ > 2l _1. Hence it suffices to show that X n ^ 0. Assume by contradiction that X n = 0. Since H[X] is a bot- tom sec, no vertex in X can reach any vertex in Bl^-i, i.e., X C S \ Reach(Bli*-i, Hi*[S\). As all edges in Hi»_i[S] are contained in Hi*[S], this implies X C S \ Reach{Bli,-1:Hi,-1[S]). Since SmallestBSCC finds the smallest bottom see in graph Hi for each i, the outer for-loop would thus have terminated in an iteration i < i* — 1. Contradiction. ■ Lemma 9 (Runtime): Algorithm 4 can be implemented in time 0(n2 + blogn). Proof: The preprocessing and initialization of the data structure and the removal of bad vertices in the whole algorithm take time 0(m + k + b) using Lemma 7. Additionally we maintain at each vertex a list of its incoming and a list of its outgoing edges including pointers to the lists of its neighbors, which we use to update the lists of its neighbors. Since each vertex is deleted at most once, this data structure can be constructed and maintained in total time 0(m). Consider the while loop where a set S is removed from Q. The search in G[S] and RevG[S] only increases the running time by a factor of two, thus we restrict the analysis of the running time to G[S]. Let n' < n be the number of vertices in S. The construction of Gi[S], Z, and G[X] can all be done in time 0(n' ■ 2X) for each i, i.e., in total time 0(n' • 2J ) up to level i*. If X = S, then the algorithm terminates and the time for processing S can be bounded by O(ra'-2logn ) = 0(ra'2).lf the processing of S ends when some bottom sec G[X] C G[S] induced by some set of vertices X is found, let i* be the value of i when G[X] is detected and inserted into Q, and let c be some constant such that the time spent in this search for X is bounded by c • n' ■ 2X _1. By Lemma 8 the set X contains at least 2J _1 vertices. Let \X\ = n\. The algorithm ensures ni < n'/2. We claim that the total running time for processing all sets S, except for the work in Remove and Construct, can be bounded by f(n) = 2c,n2. Whenever the algorithm does not terminate, we have by induction, and in particular for n' = n, f(n') < f(ni) + f(n' ~ ni) + crinx , < 2c.nl + 2c