Distributional Transformers, Objectives and Invariants for Markov Decision Processes
Talk by S. Akshay
Abstract: Markov decision processes (MDP) can be viewed as transformers of probability distributions, giving rise to a sequence of distributions over MDP states. This view is useful in many applications, e.g., modeling robot swarms or chemical reaction networks, where the behavior is naturally interpreted as probability distributions over states. Somewhat surprisingly, in this setting basic safety problems turn out to be computationally intractable. The issue is further complicated by the role of memory: even for simple examples, policies for safety objectives over distributions can require infinite memory and randomization.
In this talk, we examine the implications of this distributional viewpoint and explore ways to address the resulting difficulties in both theory and practice. After presenting some theoretical insights, we adopt an over-approximation approach inspired by invariant synthesis in program verification. We develop a framework for inductive, template-based synthesis of certificates and policies for safety and reach-avoidance objectives in MDPs. If time permits, we will also discuss recent work showing how this framework extends naturally to richer objectives, including fairness and entropy constraints in MDPs. Finally, we show the practical effectiveness of our approach as well as explore limitations and future perspectives.
Bio: S. Akshay is Professor in the Department of Computer Science and Engineering at IIT Bombay, where he also holds the Shridhar Shukla Chair Professorship in Digital Trust. His research interests lie broadly in formal methods, with a focus on the verification of timed, recursive and distributed systems, automated functional synthesis, formal modelling and analysis of probabilistic and dynamical systems, and trust and certification issues in AI models. His work is motivated by applications in areas such as systems biology, cyber-physical systems and artificial intelligence.
He received a joint PhD from École Normale Supérieure de Cachan and Chennai Mathematical Institute in 2010, followed by postdoctoral appointments at the National University of Singapore and IRISA/ENS Cachan Bretagne in Rennes, France. He is also affiliated with the IIT Bombay Trust Lab, the Ashank Desai Centre for Policy Studies, and the Centre for Formal Design and Verification of Software Systems.
