Seminars

View all Seminars  |  Download ICal for this event

Controller Synthesis Techniques for Infinite-State Reactive Synthesis

Series: Ph.D. Thesis Defense

Speaker: Stanly Samuel

Date/Time: Jun 26 11:00:00

Location: CSA Auditorium, (Room No. 104, Ground Floor)

Faculty Advisor: Deepak D'Souza and K. V. Raghavan

Abstract:
Reactive systems are ubiquitous; some examples include controllers for cyber-physical systems and programs that run on multipurpose computers. This thesis addresses the challenging problem of automatically synthesizing correct-by-construction controllers for infinite-state reactive systems with a Linear Temporal Logic (LTL) specification. The contributions are twofold: (a) We propose an efficient framework for modelling and synthesizing such controllers, and (b) we show how to synthesize resilient controllers for infinite-state reactive systems (i.e., controllers resilient to a bounded number of environmental disturbances).

The key novelties of our contributions are: (a) a framework that uses symbolic fixpoint algorithms for logically-specified two-player zero-sum games (i.e., logical LTL games) that compactly represent infinite state spaces, resulting in impressive empirical performance, and (b) providing the first approach to synthesizing resilient controllers for infinite-state reactive systems. The latter approach adopts an abstraction-based synthesis strategy that first abstracts the infinite-state reactive synthesis problem into a finite-state two-player zero-sum game, synthesizes a controller for the finite-state game, and lifts this controller for the infinite-state system. The approaches enhance the qualitative and quantitative properties of controllers while ensuring scalability compared to previous approaches. We empirically evaluate these claims over controller synthesis, program repair, synchronization synthesis, and robot motion planning examples using our tools GenSys-LTL and RESCOT, respectively. Notably, the GenSys-LTL tool demonstrates a significant 206x/13x speed-up (arithmetic/geometric mean) over the state-of-the-art, scales well for non-trivial temporal specifications, and synthesizes controllers for previously unsolved benchmarks. RESCOT empirically validates the synthesis of controllers more resilient than other tools in this space

Speaker Bio:
Stanly Samuel is a PhD student in the Department of Computer Science and Automation at IISc, where his research focused on designing algorithms and building scalable tools in the domain of infinite-state reactive synthesis by leveraging techniques from program verification, theory of infinite games, symbolic constraint solving, logic, and automata. During his doctoral studies, he also explored intersections (of formal methods) with distributed systems and blockchain security, working in the industry to enhance the reliability of software in decentralized environments. His broader vision centers on advancing the theory and practice of formal methods to ensure safety and/or scalability in real-world systems, using symbolic or neuro-symbolic techniques. Stanly was an awardee of the Cisco PhD Fellowship.