TY  - CONF
AU  - Mari, Federico
AU  - Melatti, Igor
AU  - Salvo, Ivano
AU  - Tronci, Enrico
AU  - Alvisi, Lorenzo
AU  - Clement, Allen
AU  - Li, Harry
ED  - Cimatti, A.
ED  - Jones, R.
PY  - 2008
DA  - 2008//
TI  - Model Checking Nash Equilibria in MAD Distributed Systems
BT  - FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design
SP  - 1
EP  - 8
PB  - IEEE Press
CY  - Piscataway, NJ, USA
KW  - Model Checking
KW  - MAD Distributed System
KW  - 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.
SN  - 978-1-4244-2735-2
L1  - http://mclab.di.uniroma1.it/publications/papers/mari/2008/93_Mari_etal2008.pdf
UR  - https://doi.org/10.1109/FMCAD.2008.ECP.16
DO  - 10.1109/FMCAD.2008.ECP.16
N1  - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=93), last updated on Sat, 24 Nov 2012 13:46:12 +0100
ID  - Mari_etal2008
ER  -