The Border Gateway Protocol (BGP) is the single inter-domain routing protocol that enables network operators within each autonomous system (AS) to influence routing deci- sions by independently setting local policies on route filtering and selection. This independence leads to fragile networking and makes analysis of policy configurations very complex. To aid the systematic and efficient study of the policy configuration space, this paper presents network reduction, a scalability technique for policy-based routing systems. In network reduction, we provide two types of reduction rules that transform policy configurations by merging duplicate and complementary router configurations to simplify analysis. We show that the reductions are sound, dual of each other and are locally complete. The reductions are also computationally attractive, requiring only local configuration information and modification. We have developed a prototype of network reduction and demonstrated that it is applicable on various BGP systems and enables significant savings in analysis time. In addition to making possible safety analysis on large networks that would otherwise not complete within reasonable time, network reduction is also a useful tool for discovering possible redundancies in BGP systems. I. INTRODUCTION The Internet today runs on a complex routing protocol called the Border Gateway Protocol (BGP). It enables autonomous systems (ASes) worldwide to achieve global connectivity, subject to each system's local policy (which paths are allowed, and the route preference used to select best paths). The convergence behavior of the global Internet depends on how each AS configures its policy. Prior work has shown that policy misconfigurations can lead to rapid oscillation between routing states, slowing or even preventing convergence (11). This happens when the conflicting local policies cannot be reconciled: there is no solution to the routing problem. Other configurations support a unique stable solution, which normal protocol execution is bound to reach. We refer to such configurations as 'safe'. While abstract formal models of BGP (8), (5), (7) allow researchers to explore how local policies affect BGP stability, the membership problem for this safe subset is NP-hard, and real network configurations are very large, drastically limiting the feasibility of the safety test. In this paper, we present a novel network reduction tech- nique that enables networking researchers to study and analyze large BGP systems in a sound and automatic fashion. Central to network reduction is two forms of rewriting rules that transform policy configurations into smaller and simpler forms while preserving safety property. These rewriting rules are directed at known patterns in real networks, which exhibit considerable structural redundancy. Once a configuration is reduced, safety analysis can be performed directly to check for possible misconfigurations. To evaluate the effectiveness of the reduction technique for scaling up safety analysis, we use an automated analyzer (20) based on the Maude rewriting logic engine (12). In the Maude- based analyzer, a BGP system is encoded as a transition system driven by concurrent rewriting rules. Safety analysis is then performed by simulating execution runs on the transition system, as well as exhaustively exploring all execution runs for possible divergence. Our experimental results show that network reduction enables us to perform safety analysis effi- ciently, often completing the analysis on large networks that would otherwise not be possible to study within reasonable time. Prior work (19) demonstrates that a limited form of rewrit- ing rule based on merging identical router-level configurations can significantly improve convergence analysis time of BGP instances. This paper introduced a new form of rewriting rule, based on a new unified model (EPD). Using EPD model, we proved that the two forms of rules are dual. Moreover, we proved that they form a complete set of reduction rules that require only local rewrites; this and other properties of the reduction rules, have provided a deeper understanding of the redundancies presented in BGP systems, and established net- work reduction a sound and effective tool for scaling up formal analysis. Specifically, we make the following contributions: Formal model for reduction. We propose an abstract model for modeling Internet topology and policies. This abstract model, which we call the Extended Path Digraph (EPD), extends prior models (7), (16), and provides a basis for re- ducing instances prior to analysis. EPD enables the unification of configuration specification and analysis within a common model, resulting in simpler reductions. We further provide a tool developed using Maude for automatically extracting EPD from existing network topologies and policies. Network reduction. We present two reduction rules that trans- form EPD policy configurations to simplify analysis. These two reduction rules merge duplicate or complementary router- level configurations into one. We show that these reductions are sound and mutually dual, and establish a confluence result