A formal model based on game theory for the analysis of cooperation in distributed service discovery