Synthesis via Input/Output Separation
When: Thursday, July 8, 2021, 2:30pm (CEST).
Where: Zoom online, check the address in the Google Calendar Event.
Topic: Synthesis via Input/Output Separation.
Speaker: Dror Fried, Senior Lecturer at the Open University of Israel.
Abstract
Decomposition is a commonly used technique in various algorithms in formal methods. When we observe systems that describe a relation between inputs and outputs, a decomposition, or separation, of the system to input and output components seems only natural. Specifically in synthesis, where the challenge is to construct a strategy or a function that is essentially from inputs to outputs. But what sense does it really make? After all, the specification given by the user, is intended to describe an involved relation between the input and output parts. As such, the algorithms obtained so far are designed to exploit this tight correspondence between inputs and outputs towards strategy generation. In this talk I show how we use input/output separation for synthesis in both areas of Boolean functional synthesis and reactive synthesis. For Boolean functional synthesis I describe how to separate every Boolean formula to input and output components. In reactive synthesis I describe applications in which it is natural for the designer to write specifications that separate inputs and outputs. For both areas, I show how to exploit this separation towards more efficient synthesis algorithms. This talk is based on joint works with Gal Amram, Suguman Bansal, Supratick Chackraborty, Lucas Tabajara, Moshe Vardi, and Gera Weiss.
Short Bio
Dror Fried is a senior lecturer (assistant professor) in the Open University of Israel. He did his PhD in Ben-Gurion University in artificial intelligence, and his postdoc in Rice University in formal methods with Moshe Vardi’s CAVR group. His interests include formal methods, logic in computer science and automated reasoning.