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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Reactive Synthesis Background & SYNTCOMPSYNT Camp at SW2 (SYNT Camp)
Chair(s): Guillermo A. Perez University of Antwerp, Leander Tentrup Saarland University
09:00
60m
Tutorial
Reactive Synthesis Background and the Synthesis Competition
SYNT Camp
Guillermo A. Perez University of Antwerp
10:00
30m
Tutorial
Hand-on Synthesis Experience with BoSy
SYNT Camp
Leander Tentrup Saarland University
Link to publication DOI Pre-print