%0 Conference Proceedings
%T Model Checking Nash Equilibria in MAD Distributed Systems
%A Mari, Federico
%A Melatti, Igor
%A Salvo, Ivano
%A Tronci, Enrico
%A Alvisi, Lorenzo
%A Clement, Allen
%A Li, Harry
%Y Cimatti, A.
%Y Jones, R.
%S FMCAD '08: Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design
%D 2008
%I IEEE Press
%C Piscataway, NJ, USA
%@ 978-1-4244-2735-2
%F Mari_etal2008
%O exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=93), last updated on Sat, 24 Nov 2012 13:46:12 +0100
%X 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.
%K Model Checking
%K MAD Distributed System
%K Nash Equilibrium
%R 10.1109/FMCAD.2008.ECP.16
%U http://mclab.di.uniroma1.it/publications/papers/mari/2008/93_Mari_etal2008.pdf
%U https://doi.org/10.1109/FMCAD.2008.ECP.16
%P 1-8