--- res: bibo_abstract: - Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. Search problems for NGs include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state spaces. We describe an abstraction-refinement methodology for reasoning about NGs. Our methodology is based on an abstraction function that maps the state space of an NG to a much smaller state space. We search for a global optimum and a Nash equilibrium by reasoning on an under- and an overapproximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. Our experimental results demonstrate the efficiency of the methodology.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Guy foaf_name: Avni, Guy foaf_surname: Avni foaf_workInfoHomepage: http://www.librecat.org/personId=463C8BC2-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0001-5588-8287 - foaf_Person: foaf_givenName: Shibashis foaf_name: Guha, Shibashis foaf_surname: Guha - foaf_Person: foaf_givenName: Orna foaf_name: Kupferman, Orna foaf_surname: Kupferman bibo_doi: 10.24963/ijcai.2017/11 dct_date: 2017^xs_gYear dct_identifier: - UT:000764137500011 dct_isPartOf: - http://id.crossref.org/issn/10450823 dct_language: eng dct_publisher: AAAI Press@ dct_title: An abstraction-refinement methodology for reasoning about network games@ ...