Dagstuhl Seminar 23391
The Futures of Reactive Synthesis
( Sep 24 – Sep 29, 2023 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/23391
Organizers
- Nathanaël Fijalkow (CNRS - Talence, FR)
- Bernd Finkbeiner (CISPA - Saarbrücken, DE)
- Guillermo A. Pérez (University of Antwerp, BE)
- Elizabeth Polgreen (University of Edinburgh, GB)
Contact
- Marsha Kleinbauer (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Schedule
This report documents the program and the outcomes of Dagstuhl Seminar 23391 "The Futures of Reactive Synthesis".
The seminar was meant to gather neighbouring communities on a joint goal: Reactive Synthesis. We identified five trends: neural-symbolic computation, template-based solving for constraint programming, symbolic algorithms, syntax-guided synthesis, and model learning. They were represented by different participants, and in particular by four invited speakers. We had three female invited speakers and one male invited speaker; all delivered very insightful and forward-thinking talks:
- Anne-Kathrin Schmuck
- Armando Solar-Lezama
- Ruzica Piskac
- Dana Fisman
We introduced a number of mechanisms to encourage discussions and the exchange of ideas: an open problem session, long Q&A sessions after each invited talk, and most importantly working sessions. The working sessions were proposed by participants (who volunteered in advance, after a call by email to all participants). The proposer would have a few minutes to introduce the topic they would like to discuss. Each session included 3 or 4 different topics, discussed in parallel in smaller groups. In each case, we had (by some miracle!) a fair division of all participants into the 3 or 4 topics, and we had very good feedback that many working sessions resulted in very fruitful and insightful discussions. We had "progress report sessions" where the leaders of the working sessions gave a 5 or 10-min summary of the discussions.
We also had 9 contributed talks from participants, responding to an open call. They were 20 minutes each, and greatly contributed to getting all participants involved and for representing all trends and recent advances in the field.
We as organizers had very good feedback about the organization of the week: the rather light schedule gave enough time for people to discuss, and the different talks and organized sessions gave enough ways to get to know new people and topics. The seminar included a number of junior participants, who got to meet experts in the field. The mix of tools and theory topics covered during the seminar gives us hope that it will yield results both in the short and long term.
Creative Commons BY 4.0
Nathanaël Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, and Elizabeth Polgreen
Reactive systems are computer systems that maintain a continuous interaction with their environment. These include, for example, hardware circuits, communication protocols, or embedded controllers. Reactive synthesis is the task of constructing such systems automatically from logical specifications. Because synthesis eliminates the need for a manual implementation, it has the potential to revolutionize the development process for reactive systems. And indeed, synthesis has, over the past few years, found applications in several areas of systems engineering, notably in the construction of circuits and device drivers and in the synthesis of controllers for robots and manufacturing plants.
Rooted in automata theory and logic, reactive synthesis has been actively investigated since its inception by Alonzo Church more than fifty years ago. In the past decade the successful SYNTCOMP academic competition has been driving theoretical and practical progress. This has led to very efficient implementations of the existing techniques.
We believe that the next steps for reactive synthesis will require new insights, data structures, and approaches that may lead to considerable improvements. In this endeavor we will discuss the potential of neural-symbolic computation and more generally machine learning techniques, template-based solving in the context of constraint programming, symbolic algorithms, and connections to program synthesis and in particular Syntax Guided Synthesis
Nathanael Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, and Elizabeth Polgreen
- Shaull Almagor (Technion - Haifa, IL) [dblp]
- Guy Avni (University of Haifa, IL) [dblp]
- Mrudula Balachander (Free University of Brussels, BE)
- Véronique Bruyère (University of Mons, BE) [dblp]
- Michaël Cadilhac (DePaul University - Chicago, US) [dblp]
- Antonio Casares (University of Bordeaux, FR) [dblp]
- Rayna Dimitrova (CISPA - Saarbrücken, DE) [dblp]
- Alexandre Duret-Lutz (EPITA - Le Kremlin Bicêtre, FR) [dblp]
- Rüdiger Ehlers (TU Clausthal, DE) [dblp]
- Nathanaël Fijalkow (CNRS - Talence, FR) [dblp]
- Emmanuel Filiot (UL - Brussels, BE) [dblp]
- Bernd Finkbeiner (CISPA - Saarbrücken, DE) [dblp]
- Dana Fisman (Ben Gurion University - Beer Sheva, IL) [dblp]
- Hadar Frenkel (CISPA - Saarbrücken, DE)
- Swen Jacobs (CISPA - Saarbrücken, DE) [dblp]
- Ayrat Khalimov (TU Clausthal, DE) [dblp]
- Bakh Khoussainov (Univ. of Electronic Science &Technology - Chengdu, CN) [dblp]
- Rupak Majumdar (MPI-SWS - Kaiserslautern, DE) [dblp]
- Théo Matricon (University of Bordeaux, FR) [dblp]
- Niklas Metzger (CISPA - Saarbrücken, DE) [dblp]
- Rémi Morvan (University of Bordeaux, FR) [dblp]
- Anca Muscholl (University of Bordeaux, FR) [dblp]
- Pierre Ohlmann (University of Warsaw, PL) [dblp]
- Guillermo A. Pérez (University of Antwerp, BE) [dblp]
- Ruzica Piskac (Yale University - New Haven, US) [dblp]
- Elizabeth Polgreen (University of Edinburgh, GB) [dblp]
- Mickael Randour (F.R.S.-FNRS & UMONS - Université de Mons, BE) [dblp]
- César Sánchez (IMDEA Software Institute - Madrid, ES) [dblp]
- Mark Santolucito (Barnard College, Columbia University - New York, US) [dblp]
- Andre Schidler (TU Wien, AT) [dblp]
- Frederik Schmitt (CISPA - Saarbrücken, DE)
- Anne-Kathrin Schmuck (MPI-SWS - Kaiserslautern, DE) [dblp]
- Martina Seidl (Johannes Kepler Universität Linz, AT) [dblp]
- Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
- Hazem Torfah (Chalmers University of Technology - Göteborg, SE) [dblp]
- Tom van Dijk (University of Twente - Enschede, NL) [dblp]
- Shufang Zhu (University of Oxford, GB)
- Martin Zimmermann (Aalborg University, DK) [dblp]
Classification
- Artificial Intelligence
- Formal Languages and Automata Theory
- Programming Languages
Keywords
- Reactive synthesis
- program synthesis
- Temporal synthesis
- Program verification
