Analysis of two-player games played on graphs is central to  reactive synthesis and it has been carried out in much detail. In this talk, we will explore some natural extensions of these games which are played between a distributed team of processes and an adversarial environment. Many real-life distributed applications can be modelled using them. Our games are played on a network of asynchronous processes modelled as finite-state devices which synchronize on shared actions and support true concurrency. Processes are allowed to exchange the entire casual past on shared actions to respond to the environment.

Given a distributed game structure and a winning objective, the key algorithmic problem is: whether a distributed winning strategy meeting that objective exists or not. We will discuss some special classes of these games with natural winning objectives such as global safety, local parity etc and develop algorithms to solve this key decision problem efficiently. Another important concern is: for the affirmative instance of the above problem, existence of a finite-state distributed winning strategy and its construction. For the above mentioned cases, we will see an explicit construction of a finite-state distributed winning strategy.

This is ongoing work with PhD student Nehul Jain.

Short Bio:
Bharat Adsul is currently a Professor in the Department of Computer Science and Engineering at IIT Bombay. He received his Ph.D. from IIT Bombay in 2003 and worked at Chennai Mathematical Institute from 2003 to 2007. His research interests are in formal methods with special focus on concurrency (automata theory, logics, games, algebraic aspects), geometric complexity theory and mathematical programming in general.