PRALINE : Repellor ALgorIthm for Nash Equilibria

Description

This tool computes pure Nash equilibria in concurrent games. The preferences of the players are given by payoff functions that map states to integers, the goal for a player is then to maximize the limit superior of her payoff; this can be seen as a generalization of Büchi objectives.

Download

praline-1.3.tar.gz

Installation

You need to have ocaml and ocamlgraph installed: on Debian-like systems this can be done by typing sudo apt-get install ocaml libocamlgraph-ocaml-dev. Then, extract the archive, open a command line in the extracted directory and type make. This should have created an executable file called praline.

Examples

Medium Access Control

Several users share access to a wireless channel. During each slot, they can choose to either transmit or wait for the next slot. If too many users are emitting in the same slot, then they fail to send data. Furthermore each attempt at transmitting costs energy to the players. They have to maximize the number of successful attempts using the energy available to them.

Here is the file medium_access_21.game that is available in the examples directory:

int trans1 = 0;
int energy1 = 1;
int trans2 = 0;
int energy2 = 1;

player p1 {trans1};
player p2 {trans2};

move {
  legal p1 0;
  legal p2 0;
  if (energy1 > 0) legal p1 1;
  if (energy2 > 0) legal p2 1;
}

update {
  if (action p1 == 1)  
    energy1 = energy1 - 1;
  if (action p2 == 1)
    energy2 = energy2 - 1;

  if (action p1 == 1 && action p2 == 0)
    trans1 = trans1 + 1;
  if (action p1 == 0 && action p2 == 1)
    trans2 = trans2 + 1;
}

To run PRALINE on this example just type ./praline examples/medium_access_21.game . Here is an example scenario:

number of players : 2
number of states : 5
number of edges : 10
payoff of solution 1 : p1 : 1 p2 : 1 
(0) exit;
(1) display the shape of the solution;
(2) output the shape in a file;
(3) output the strategy in a file;
(4) play against the strategy;
There is one Nash equilibrium and it has payoff 1 for each player. To see how this equilibrium behaves we will play against the strategy (4th choice).
 > 4
The current state is :
energy1 = 1 ; energy2 = 1 ; trans1 = 0 ; trans2 = 0 ; 
All the players are suspect.
p1 : 0 ; p2 : 0
Eve plays : 1,0
The natural outcome of this move is :
energy1 = 0 ; energy2 = 1 ; trans1 = 1 ; trans2 = 0 ; 
To obey Eve's move, we just press Enter.
 > 
The current state is :
energy1 = 0 ; energy2 = 1 ; trans1 = 1 ; trans2 = 0 ; 
All the players are suspect.
p1 : 1 ; p2 : 0
Eve plays : 0,1
The natural outcome of this move is :
energy1 = 0 ; energy2 = 0 ; trans1 = 1 ; trans2 = 1 ; 
 > 
The current state is :
energy1 = 0 ; energy2 = 0 ; trans1 = 1 ; trans2 = 1 ; 
All the players are suspect.
p1 : 1 ; p2 : 1
Eve plays : 0,0
The natural outcome of this move is :
energy1 = 0 ; energy2 = 0 ; trans1 = 1 ; trans2 = 1 ; 
 > 
The current state is :
energy1 = 0 ; energy2 = 0 ; trans1 = 1 ; trans2 = 1 ; 
All the players are suspect.
p1 : 1 ; p2 : 1
Eve plays : 0,0
The natural outcome of this move is :
energy1 = 0 ; energy2 = 0 ; trans1 = 1 ; trans2 = 1 ; 
We entered a loop so we can now exit PRALINE.
 > exit

Power Control

This example is inspired by the problem of power control in cellular networks. We consider the situation where a number of cellular telephones are emitting over a cellular network. Each agent can choose the emitting power of his phone. From the point of view of an agent, using a stronger power results in a better transmission, but it is costly since it uses energy, and it lowers the quality of the transmission for the others, because of interferences.

Here is the file describing this game and a sample scenario:

int pow1 = 0;
int pow2 = 0;

player p1
{ 
  1000 * (1 - exp
    ( -0.5 * pow1 / (pow2 + 1)))
    / (pow1 + 1)
};

player p2
{ 
  1000 * (1 - exp
    ( -0.5 * pow2 / (pow1 + 1)))
    / (pow2 + 1)
};

move{
  int levelMax = 2;

  legal p1 0;
  legal p2 0;
  
  if (pow1 < levelMax) legal p1 1 ;
  if (pow2 < levelMax) legal p2 1 ;
}

update{
  if ( action p1 == 1 ) pow1 = pow1 + 1;
  if ( action p2 == 1 ) pow2 = pow2 + 1;
}
$ ./praline examples/power_control_22.game
number of players : 2
number of states : 9
number of edges : 25
payoff of solution 1 : p1 : 94 p2 : 94 
payoff of solution 2 : p1 : 110 p2 : 110 
select a solution in [1-2] or 0 to quit
 > 2
(0) exit;
(1) display the shape of the solution;
(2) output the shape in a file;
(3) output the strategy in a file;
(4) play against the strategy;
 > 4
The current state is :
pow1 = 0 ; pow2 = 0 ; 
All the players are suspect.
p1 : 0 ; p2 : 0
Eve plays : 1,1
The natural outcome of this move is :
pow1 = 1 ; pow2 = 1 ; 
 > 
The current state is :
pow1 = 1 ; pow2 = 1 ; 
All the players are suspect.
p1 : 110 ; p2 : 110
Eve plays : 0,0
The natural outcome of this move is :
pow1 = 1 ; pow2 = 1 ; 
At this point we want to modify the outcome, so that the next state is different. This is done by entering an instruction, following the syntax of PRALINE game files:
 > pow1 = 2;
 > 
The current state is :
pow1 = 2 ; pow2 = 1 ; 
The suspect is p1 and her current payoff is 131
Eve plays : 0,1
The natural outcome of this move is :
pow1 = 2 ; pow2 = 2 ; 
 > 
The current state is :
pow1 = 2 ; pow2 = 2 ; 
The suspect is p1 and her current payoff is 94
Eve plays : 0,0
The natural outcome of this move is :
pow1 = 2 ; pow2 = 2 ; 
 > exit

Related Articles

[BBMU12]
P. Bouyer, R. Brenguier, N. Markey and M. UmmelsConcurrent games with ordered objectivesIn FoSSaCS'12, LNCS 7213, pages 301-315. Springer, 2012. ( PDF | PDF (long version) | BibTeX + Abstract )
[BBMU11]
P. Bouyer, R. Brenguier, N. Markey and M. UmmelsNash Equilibria in Concurrent Games with Büchi ObjectivesIn FSTTCS'11, Leibniz International Proceedings in Informatics 13, pages 375-386. Leibniz-Zentrum für Informatik, 2011. ( PDF | BibTeX + Abstract )

Author

Romain Brenguier

About LSV