During this short (~1 hour) presentation on the reactive synthesis problem and the synthesis competition (SYNTCOMP), I will start by arguing why automatic synthesis of reactive controllers is needed. I will also give a brief history of the problem, touching on the seminal works of Rabin, Buchi, and Church. Then, we will see the circuit-based physical instantiation of the synthesis problem that inspired the format of the first SYNTCOMP and the game-based theoretical tools that allow to solve it in an elegant way. We will then move to the logic-specification version of the problem (i.e. the basis for the LTL synthesis tracks of SYNTCOMP). I will explain the general ideas of how the logic specification is translated into an automaton and then once more into a game. Finally, I will mention recent applications synthesis tools have found in Reinforcement Learning, a sub-field of artificial intelligence, and conclude with open questions and necessary future work to bring synthesis tools closer to industrial applications.

I am an engineer turned academic (wannabe). I am into Embedded Systems, Formal Verification, Logic and Automata, and Artificial Intelligence. More specifically: weighted automata, (partial-observation) quantitative games, regret minimization, reactive synthesis, learning with guarantees, etc.