ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

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.

Sun 7 Apr

syntcompcamp-2019-tutorial
09:00 - 10:30: SYNT Camp - Reactive Synthesis Background & SYNTCOMP at SW2 (SYNT Camp)
Chair(s): Guillermo A. PerezUniversity of Antwerp, Leander TentrupSaarland University
syntcompcamp-2019-tutorial09:00 - 10:00
Tutorial
Guillermo A. PerezUniversity of Antwerp
syntcompcamp-2019-tutorial10:00 - 10:30
Tutorial
Leander TentrupSaarland University
Link to publication DOI Pre-print