[FM-India]IARCS Verification Seminar Series -- Talk by Shibashis Guha on Nov. 1 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Shibashis Guha, a faculty member at the School of Technology and Computer Science at Tata Institute of Fundamental Research, Mumbai. The talk is scheduled on Tuesday, November 1, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MGsxMHR2dTUya2MzYTAxOHRhZmttbHFmZTUgdnNzLmlhcmNzQG0&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: A Game of Pawns Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: We introduce and study pawn games; a class of two-player turn-based zero-sum games in which the control of vertices changes dynamically throughout the game. Pawn games naturally model ongoing decision-making setting in which resources are transferable. Each vertex of a pawn game is owned by a pawn. In each round of the game, the pawns are partitioned between the two players. The player who moves the token from a vertex is the player who controls the pawn that owns the vertex. A pawn game is equipped with a mechanism, which the players apply after each round in order to update the set of pawns that they control. We define several grabbing-based mechanisms in which control of at most one pawn transfers at the end of each round. We study the complexity of solving reachability pawn games, where we parameterize the problem by the mechanism that is being used and by restrictions on pawn ownership of vertices. For the positive news, even though pawn games are exponentially-succinct turn-based games, we identify some natural classes that can be solved in PTIME. For the negative news, we identify some classes for which the problem is EXPTIME-complete. Our EXPTIME-hardness results are based on a class of games which we introduce and call Lock-and-Key games, and which may be of independent interest. This is a joint work with Guy Avni and Pranav Ghorpade. Bio: Shibashis Guha is a faculty member at the School of Technology and Computer Science at Tata Institute of Fundamental Research, Mumbai. Before this, he was a postdoc at the Verification Group in Université libre de Bruxelles and at The Hebrew University in the group of Prof. Orna Kupferman. He did his PhD from the Department of Computer Science and Engineering at IIT Delhi, under the supervision of Prof. S. Arun-Kumar. His research interests include reactive synthesis, probabilistic systems, timed automata, behavioural equivalences, formal methods and its intersection with algorithmic game theory.