A Gentle Introduction to Reactive Synthesis

The research field of reactive synthesis is fascinating. Starting from a specification of a reactive system, i.e., a computational system that operates in steps and in each steps reads some input and produces some output, a synthesis algorithm computes a reactive system that implements the specification and is correct-by-construction.

Unfortunately, learning the basics of reactive synthesis is a bit difficult. While nowadays an introductory article can be found in the Handbook of Model Checking, this article is best suited for reader already familiar with the basics of formal methods.

The following video provides a mostly self-contained introduction that is meant to also be suitable for (beginning) researchers from other fields of research, such as control theory or robotics, and for students of computer science who want to get to know the main ideas of reactive synthesis without having to take a complete formal methods course. In contrast to the an introductory video to the field of reactive synthesis by Bernd Finkbeiner, it is much slower paced and skips some advanced topics such as distributed synthesis completely. Also, it covers the question of how to model a specification for reactive synthesis in more detail.

Topics discussed in the video

• The basic idea of reactive synthesis (including a demo)

• Linear Temporal Logic as a specification logic

• How can a specification be unrealizable?

• What are games and what is their connection to reactive synthesis?

• What does it mean to solve a game?

• What are parity automata and parity games?

• Generalized Reactivity(1) Synthesis as a particularly efficient synthesis approach (including a demo)

• How does Generalized Reactivity(1) Synthesis work under the hood?

License

The video is currently in a “beta status” and as such not yet available under a creative commons license. However, permission is hereby granted to link to it, download it, and store it for personal use in research and teaching. The video may later be updated in order to improve some details and/or to correct potential errors.