Tractable Representations for Boolean functional synthesis
Abstract:
It is often easy to write down the specification of a system as a relation between inputs and outputs. But implementing the system is a functional problem: to provide functions that produce outputs from inputs. The question we ask is if we can automatically synthesize such a function from the given relation? This question has generated a lot of interest in recent years, especially in the Boolean setting, where despite theoretical hardness results, many techniques and tools have been developed that now scale surprisingly well.
In this talk, we shine a light on this problem from a Knowledge Representation perspective. We identify structural properties and develop normal forms for the specification that guarantee provably efficient synthesis. Further, we move towards a characterization of what makes Boolean functional synthesis easy and examine techniques to compile into such forms.
Bio:
S. Akshay is a faculty member in the Department of Computer Science and Engineering at IIT Bombay. His research interests span formal methods and AI with a focus on automata theory, quantitative (timed/probabilistic) verification and automated synthesis. He has given multiple recent tutorials on automated functional synthesis in venues including Highlights 2022, AAAI 2022 and IJCAI 2022.