PT Unknown
AU Mari, F
   Melatti, I
   Salvo, I
   Tronci, E
   Alvisi, L
   Clement, A
   Li, H
TI Model Checking Nash Equilibria in MAD Distributed Systems
SE FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design
PY 2008
BP 1
EP 8
DI 10.1109/FMCAD.2008.ECP.16
DE Model Checking; MAD Distributed System; Nash Equilibrium
AB 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.
PI Piscataway, NJ, USA
ER