article published yes Guy Avni author 463C8BC2-F248-11E8-B48F-1D18A9856A870000-0001-5588-8287 Shibashis Guha author Orna Kupferman author ToHe department Formal Methods meets Algorithmic Game Theory project Rigorous Systems Engineering project Formal methods for the design and analysis of complex systems project 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 over-approximation defined on top of this smaller state space. When the approximations are too coarse to find such profiles, we refine the abstraction function. We extend the abstraction-refinement methodology to labeled networks, where the objectives of the players are regular languages. Our experimental results demonstrate the effectiveness of the methodology. https://research-explorer.ista.ac.at/download/6006/6008/2018_MDPI_Avni.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ MDPI2018 eng 2073-433610.3390/g9030039 93 https://research-explorer.ista.ac.at/record/1003 G. Avni, S. Guha, O. Kupferman, Games 9 (2018). Avni G, Guha S, Kupferman O. 2018. An abstraction-refinement methodology for reasoning about network games. Games. 9(3), 39. G. Avni, S. Guha, and O. Kupferman, “An abstraction-refinement methodology for reasoning about network games,” <i>Games</i>, vol. 9, no. 3. MDPI, 2018. Avni, Guy, et al. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” <i>Games</i>, vol. 9, no. 3, 39, MDPI, 2018, doi:<a href="https://doi.org/10.3390/g9030039">10.3390/g9030039</a>. Avni, G., Guha, S., &#38; Kupferman, O. (2018). An abstraction-refinement methodology for reasoning about network games. <i>Games</i>. MDPI. <a href="https://doi.org/10.3390/g9030039">https://doi.org/10.3390/g9030039</a> Avni, Guy, Shibashis Guha, and Orna Kupferman. “An Abstraction-Refinement Methodology for Reasoning about Network Games.” <i>Games</i>. MDPI, 2018. <a href="https://doi.org/10.3390/g9030039">https://doi.org/10.3390/g9030039</a>. Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. <i>Games</i>. 2018;9(3). doi:<a href="https://doi.org/10.3390/g9030039">10.3390/g9030039</a> 60062019-02-14T14:17:54Z2025-07-10T11:49:38Z