PRALINE : Repellor ALgorIthm for Nash Equilibria

Description

This tool computes pure Nash equilibria in concurrent games, with Büchi, reachability or safety objectives. It uses the repellor technique to compute possible equilibria paths in Büchi games, and solves reachability and safety objectives by performing a product of the game with a deterministic automaton describing these objectives.

Download

Users manual

manual.pdf

Sources

praline-1.2.tar.gz

Examples

Simple Games

To model small games graphically you can consider using an editor for the GML language (see GML on wikipedia).

Simple examples

Generating Games

In order to generate games with a big arena we provide an Ocaml functor that helps with this task. To use it, a basic knowledge of Ocaml is helpfull. The functor is in the module Generator of the PRALINE distribution. The input of the functor is a module that describes the transition table and the payoffs of the players. From it the functor Make provides a function that given an initial state, generates the arena that contains all the accessible state, and the game file.

Generated examples

Author

Romain Brenguier