Formal Methods in Network Games

Abstract: 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 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.

Bio: Shibashis is a postdoc in the Verification Group at Université libre De Bruxelles. Prior to this he was a postdoc at The Hebrew University of Jerusalem. He did his PhD from the Department of Computer Science and Engineering at IIT Delhi. His research interests are in timed and probabilistic systems, behavioural equivalences, formal methods and its intersection with algorithmic game theory.