An Abstraction-Refinement Methodologyfor Reasoning about Network Games†
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, ab...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2018-06-01
|
| Series: | Games |
| Subjects: | |
| Online Access: | http://www.mdpi.com/2073-4336/9/3/39 |
| _version_ | 1811228907493392384 |
|---|---|
| author | Guy Avni Shibashis Guha Orna Kupferman |
| author_facet | Guy Avni Shibashis Guha Orna Kupferman |
| author_sort | Guy Avni |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-12T10:04:32Z |
| format | Article |
| id | doaj.art-ad201db95f7e4bf6936f13303f4ef4ba |
| institution | Directory Open Access Journal |
| issn | 2073-4336 |
| language | English |
| last_indexed | 2024-04-12T10:04:32Z |
| publishDate | 2018-06-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Games |
| spelling | doaj.art-ad201db95f7e4bf6936f13303f4ef4ba2022-12-22T03:37:28ZengMDPI AGGames2073-43362018-06-01933910.3390/g9030039g9030039An Abstraction-Refinement Methodologyfor Reasoning about Network Games†Guy Avni0Shibashis Guha1Orna Kupferman2The Institute of Science and Technology Austria (IST Austria), Am Campus 1, 3400 Klosterneuburg, AustriaUniversité Libre de Bruxelles, Avenue Franklin Roosevelt 50, 1050 Bruxelles, BelgiumSchool of Computer Science and Engineering, Hebrew University, Jerusalem 91904, IsraelNetwork 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.http://www.mdpi.com/2073-4336/9/3/39network formation gamesabstraction-refinementNash equilibriumsocial optimum |
| spellingShingle | Guy Avni Shibashis Guha Orna Kupferman An Abstraction-Refinement Methodologyfor Reasoning about Network Games† Games network formation games abstraction-refinement Nash equilibrium social optimum |
| title | An Abstraction-Refinement Methodologyfor Reasoning about Network Games† |
| title_full | An Abstraction-Refinement Methodologyfor Reasoning about Network Games† |
| title_fullStr | An Abstraction-Refinement Methodologyfor Reasoning about Network Games† |
| title_full_unstemmed | An Abstraction-Refinement Methodologyfor Reasoning about Network Games† |
| title_short | An Abstraction-Refinement Methodologyfor Reasoning about Network Games† |
| title_sort | abstraction refinement methodologyfor reasoning about network games† |
| topic | network formation games abstraction-refinement Nash equilibrium social optimum |
| url | http://www.mdpi.com/2073-4336/9/3/39 |
| work_keys_str_mv | AT guyavni anabstractionrefinementmethodologyforreasoningaboutnetworkgames AT shibashisguha anabstractionrefinementmethodologyforreasoningaboutnetworkgames AT ornakupferman anabstractionrefinementmethodologyforreasoningaboutnetworkgames AT guyavni abstractionrefinementmethodologyforreasoningaboutnetworkgames AT shibashisguha abstractionrefinementmethodologyforreasoningaboutnetworkgames AT ornakupferman abstractionrefinementmethodologyforreasoningaboutnetworkgames |