[FM-India]IARCS Verification Seminar Series -- Talk by Suman Sadhukhan on March 19 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Suman Sadhukhan, a postdoctoral researcher at University of Haifa. The talk is scheduled on Tuesday, March 19, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=M2xsZmdnaGYydGE1czZhamZscXFuaTcydnYgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas. All are welcome to join. Best regards, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Bidding Games on Graphs - In theory and in practice. Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: In a two-player zero-sum graph game, the players move a token throughout the game, producing an infinite play, which determines the winner of the game. Bidding games are graph games in which in each turn, a bidding (auction) determines which player moves the token: the players have budgets, and in each turn, both players simultaneously submit the bids that do not exceed the available budgets. The higher bidder moves the token, and pays the bid to the lower bidder (called Richman bidding). The standard solution concept of interest in bidding games are threshold budgets: the necessary and sufficient budget for winning the game. In this survey talk, on the theoretical side, we will explore discrete bidding games, where the keyword discrete stands for the bids having a fixed granularity. We obtain membership in NP ∩ coNP for solving parity bidding games with exponentially succinct representation. This will be followed by our newly proposed application of bidding games to a decentralized synthesis problem for multi-objective decision making. Here, synthesized policies express their scheduling urgency via bids and a bounded budget guarantees long-run fairness. Moreover, our proposed solution framework is modular, in the sense that if one objective changes, we may still combine the policy for the other objective without having the need to recompute it from scratch. These works have been in collaboration with Guy Avni and Kaushik Mallik. Bio: Suman Sadhukhan is currently a postdoctoral researcher at the University of Haifa, primarily working with Guy Avni on Bidding Games on Graphs. He obtained his PhD in 2022 from Inria Rennes where he was advised by Nathalie Bertrand, Nicolas Markey and Ocan Sankur, and worked on dynamic network congestion games from a verification perspective. He is interested in, but not restricted to, Games on Graphs, studying different game theoretic models from formal verification and reactive synthesis viewpoint. Prior to his PhD training, he was a student at Chennai Mathematical Institute where he studied Theoretical Computer Science and Mathematics.