SYNT Camp 2019

BoSy is a reactive synthesis tool based on the bounded synthesis approach. Bounded synthesis ensures the minimality of the synthesized implementation by incrementally increasing a bound on the size of the solutions it considers. For each bound, the existence of a solution is encoded as a logical constraint solving problem that is solved by an appropriate solver. BoSy constructs bounded synthesis encodings into SAT, QBF, DQBF, EPR, and SMT.

In this tutorial, we explain, step by step, the transformation of a specification given in linear-time temporal logic (LTL) to a constraint system that represents the synthesis problem. We give an overview of implemented optimizations, possible enhancements and parts that can be re-used to create a new synthesis tool.

Link to Publication: https://link.springer.com/chapter/10.1007/978-3-319-63390-9_17

Leander Tentrup

Saarland University

BoSy is a reactive synthesis tool based on the bounded synthesis approach. Bounded synthesis ensures the minimality of the synthesized implementation by incrementally increasing a bound on the size of the solutions it considers. For each bound, the existence of a solution is encoded as a logical constraint solving problem that is solved by an appropriate solver. BoSy constructs bounded synthesis encodings into SAT, QBF, DQBF, EPR, and SMT.

In this tutorial, we explain, step by step, the transformation of a specification given in linear-time temporal logic (LTL) to a constraint system that represents the synthesis problem. We give an overview of implemented optimizations, possible enhancements and parts that can be re-used to create a new synthesis tool.

Leander Tentrup

Saarland University

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.

Guillermo A. Perez

University of Antwerp

Belgium

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.