2009 | OriginalPaper | Buchkapitel
Model Checking Coalition Nash Equilibria in MAD Distributed Systems
verfasst von : Federico Mari, Igor Melatti, Ivano Salvo, Enrico Tronci, Lorenzo Alvisi, Allen Clement, Harry Li
Erschienen in: Stabilization, Safety, and Security of Distributed Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We present two OBDD based model checking algorithms for the verification of Nash equilibria in finite state mechanisms modeling
Multiple Administrative Domains
(MAD) distributed systems with possibly colluding agents (
coalitions
) and with possibly faulty or malicious nodes (Byzantine agents). Given a finite state mechanism, a
proposed protocol
for each agent and the
maximum sizes
f
for Byzantine agents and
q
for agents collusions, our model checkers return
Pass
if the proposed protocol is an
ε
-
f
-
q
-Nash equilibrium, i.e. no coalition of size up to
q
may have an interest greater than
ε
in deviating from the proposed protocol when up to
f
Byzantine agents are present,
Fail
otherwise. We implemented our model checking algorithms within the NuSMV model checker: the first one
explicitly
checks equilibria for each coalition, while the second represents
symbolically
all coalitions. We present experimental results showing their effectiveness for moderate size mechanisms. For example, we can verify coalition Nash equilibria for mechanisms which corresponding normal form games would have more than 5 ×10
21
entries. Moreover, we compare the two approaches, and the explicit algorithm turns out to outperform the symbolic one. To the best of our knowledge, no model checking algorithm for verification of Nash equilibria of mechanisms with coalitions has been previously published.