Reactive Synthesis

          @misc{ scivideos_17244,
            doi = {},
            url = {https://simons.berkeley.edu/talks/tbd-266},
            author = {},
            keywords = {},
            language = {en},
            title = {Reactive Synthesis},
            publisher = {The Simons Institute for the Theory of Computing},
            year = {2021},
            month = {feb},
            note = {17244 see, \url{https://scivideos.org/index.php/Simons-Institute/17244}}
          }
          

Abstract

Reactive synthesis is the problem of translating a logical specification into a reactive system that is guaranteed to satisfy the specification for all possible behaviors of its environment. More than 60 years after its introduction by Alonzo Church, the synthesis problem is still one of the most intriguing challenges in the theory of reactive systems. Recent years have brought advances both in reasoning methods that can be used as tools in the synthesis process and in the synthesis approaches themselves. As a result, the complexity of the synthesized systems has risen steadily. However, the logical and algorithmic foundations of the synthesis problem are still far from complete. In this tutorial, I will give an overview of both the classic constructions and more recent ideas such as bounded synthesis and the synthesis of distributed systems. In the latter, we try to find a combination of process implementations that jointly guarantee that a given specification is satisfied. A reduction from multi-player games shows that the problem is in general undecidable. Despite this negative result, there is a long history of discoveries where the decidability of the synthesis problem was established for distributed systems with specific architectures, although usually with high computational cost. Compositional approaches and new specification languages like HyperLTL, which offer a more comprehensive logical representation of the distributed synthesis problem, are potential ways forward.