TY - CONF AU - Mari, Federico AU - Melatti, Igor AU - Salvo, Ivano AU - Tronci, Enrico AU - Alvisi, Lorenzo AU - Clement, Allen AU - Li, Harry ED - Guerraoui, R. ED - Petit, F. PY - 2009 DA - 2009// TI - Model Checking Coalition Nash Equilibria in MAD Distributed Systems BT - Stabilization, Safety, and Security of Distributed Systems, 11th International Symposium, SSS 2009, Lyon, France, November 3-6, 2009. Proceedings T3 - Lecture Notes in Computer Science SP - 531 EP - 546 VL - 5873 PB - Springer AB - 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 \times 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. L1 - http://mclab.di.uniroma1.it/publications/papers/mari/2009/19_Mari_etal2009.pdf UR - https://doi.org/10.1007/978-3-642-05118-0_37 DO - 10.1007/978-3-642-05118-0_37 N1 - exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=19), last updated on Sat, 24 Nov 2012 13:41:37 +0100 ID - Mari_etal2009 ER -