| |
Record |
Links |
|
Author  |
Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Alvisi, Lorenzo; Clement, Allen; Li, Harry |
|
| |
Title |
Model Checking Nash Equilibria in MAD Distributed Systems |
Type |
Conference Article |
| |
Year |
2008 |
Publication |
FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design |
Abbreviated Journal |
|
|
| |
Volume |
|
Issue |
|
Pages |
1-8 |
|
| |
Keywords |
Model Checking, MAD Distributed System, Nash Equilibrium |
|
| |
Abstract |
We present a symbolic model checking algorithm for verification of Nash equilibria in finite state mechanisms modeling Multiple Administrative Domains (MAD) distributed systems. Given a finite state mechanism, a proposed protocol for each agent and an indifference threshold for rewards, our model checker returns PASS if the proposed protocol is a Nash equilibrium (up to the given indifference threshold) for the given mechanism, FAIL otherwise. We implemented our model checking algorithm inside the NuSMV model checker and present experimental results showing its effectiveness for moderate size mechanisms. For example, we can handle mechanisms which corresponding normal form games would have more than $10^20$ entries. To the best of our knowledge, no model checking algorithm for verification of mechanism Nash equilibria has been previously published. |
|
| |
Address |
|
|
| |
Corporate Author |
|
Thesis |
|
|
| |
Publisher |
IEEE Press |
Place of Publication |
Piscataway, NJ, USA |
Editor |
Cimatti, A.; Jones, R. |
|
| |
Language |
|
Summary Language |
|
Original Title |
|
|
| |
Series Editor |
|
Series Title |
|
Abbreviated Series Title |
|
|
| |
Series Volume |
|
Series Issue |
|
Edition |
|
|
| |
ISSN |
978-1-4244-2735-2 |
ISBN |
|
Medium |
|
|
| |
Area |
|
Expedition |
|
Conference |
|
|
| |
Notes |
|
Approved |
yes |
|
| |
Call Number |
Sapienza @ mari @ MarMelSalTroAlvCle08 |
Serial |
93 |
|
| Permanent link to this record |
