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 epsilon-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than epsilon 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 x 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.

Model Checking Coalition Nash Equilibria in MAD Distributed Systems / Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Lorenzo, Alvisi; Allen, Clement; Harry, Li. - STAMPA. - 5873:(2009), pp. 531-546. (Intervento presentato al convegno 11th International Symposium on Stabilization, Safety and Security of Distributed Systems tenutosi a Lyon, FRANCE nel NOV 03-06, 2009) [10.1007/978-3-642-05118-0_37].

Model Checking Coalition Nash Equilibria in MAD Distributed Systems

MARI, FEDERICO;MELATTI, IGOR;SALVO, Ivano;TRONCI, Enrico;
2009

Abstract

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 epsilon-f-q-Nash equilibrium, i.e. no coalition of size up to q may have an interest greater than epsilon 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 x 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.
2009
11th International Symposium on Stabilization, Safety and Security of Distributed Systems
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
Model Checking Coalition Nash Equilibria in MAD Distributed Systems / Mari, Federico; Melatti, Igor; Salvo, Ivano; Tronci, Enrico; Lorenzo, Alvisi; Allen, Clement; Harry, Li. - STAMPA. - 5873:(2009), pp. 531-546. (Intervento presentato al convegno 11th International Symposium on Stabilization, Safety and Security of Distributed Systems tenutosi a Lyon, FRANCE nel NOV 03-06, 2009) [10.1007/978-3-642-05118-0_37].
File allegati a questo prodotto
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/379118
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 2
social impact