Alladi Ramakrishnan Hall

Formal Methods in Network Games

Shibashis Guha

Université Libre De Bruxelles, Belgium

Network games (NGs) are played on directed graphs and are extensively used in network design and analysis. In the classical model, each player selects a path connecting her source and target vertices. The cost of traversing an edge depends on the load; namely, number of players that traverse it. NGs abstract the fact that different users may use a resource at different times and for different durations; time plays an important role in determining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, actual sharing and congestion of resources crucially depends on time. In the first part of the talk, we will discuss timed network games (TNGs), which add a time component to network games. The time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We will also mention how different reductions to a formal model called timed automata help in reasoning about TNGs.

In the second part of the talk, we consider search problems for NGs that include finding special strategy profiles such as a Nash equilibrium and a globally optimal solution. The networks modeled by NGs may be huge. In formal verification, abstraction has proven to be an extremely effective technique for reasoning about systems with big and even infinite state space. We describe an abstraction-refinement methodology for reasoning about NGs.

Based on joint works with Guy Avni and Orna Kupferman.