Model Checking MAD Distributed Systems

Details
Category: Research
Last Updated on Monday, 26 November 2012 16:01

Cooperative services are distributed systems in which nodes (agents) belong to Multiple Administrative Domains (MAD). Thus in a MAD distributed system each node owns its resources and there is no central authority owning all system nodes. Examples of MAD distributed systems include Internet routing, wireless mesh routing, file distribution, archival storage, cooperative backup, formation of autonomous vehicles. Proving correctness of a protocol for a MAD distributed system must take into account that each agent may modify its hardware or software if that is to its advantage. Thus, beyond showing the usual safety and liveness properties, we must also show that the protocol is a Nash equilibrium, that is, no agent participating in the protocol may have an interest in deviating from the behaviour prescribed by the protocol. In [SSS 2009, FMCAD 2008] we present a model checker for automatic verification of Nash equilibria in MAD distributed systems.