Output-Sensitive Algorithms for Reactive Synthesis (OSARES)
The project is funded by the European Research Council for five years, from 2016 to 2021, as an ERC Consolidator Grant.
Distributed embedded systems have started to transform the role of computing technology in all sectors of our society. Applications include transport systems, building technology, energy management, health care, infrastructure, and environmental protection. These applications constitute a disruptive technology with the potential of vast savings in terms of energy, environmental pollution, and implementation costs. The flipside of these benefits is the potential for significant economical and possibly even life-threatening damage that could be caused if a distributed system fails to function as intended. Designing distributed systems that are safe, stable, and robust is difficult, because local design decisions may have global consequences, and many objectives can only be realized when multiple components cooperate.
Reactive synthesis has the potential to revolutionize the development of distributed embedded systems. From a given logical specification, the synthesis algorithm automatically constructs an implementation that is correct-by-design. This allows the developer to focus on “what” the system should do instead of “how” it should be done. Because synthesis analyzes objectives, not implementations, it can be applied at an early design stage, long before the system has been implemented. The goal of OSARES is to develop output-sensitive synthesis algorithms. In addition to optimal performance in the size of the specification, such algorithms also perform optimally in the size and structural complexity of the implementation. We aim for the principled analysis of the dependencies of different metrics on the complexity of the problem, as well as for improving the state of the art in practical synthesis. This entails work on both the theoretical level and on symbolic search algorithms, such as constraint solvers. We develop output-sensitive synthesis algorithms for the general classes of (control-dominated) discrete, real-time, and distributed reactive systems. Benchmarks for our new algorithms come from classic application areas like hardware synthesis, and from new and much more challenging application areas like distributed control and coordination, which are far beyond the reach of the currently available synthesis algorithms.
OSARES in the News
Currently there are several open PhD student positions and one open postdoc position. If you are interested, contact Bernd Finkbeiner. Candidates for PhD student positions should additionally submit an application to the Saarbrücken Graduate School of Computer Science (mention your interest in OSARES).
- Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, Leander Tentrup. Encodings of Bounded Synthesis. TACAS 2017.
- Bernd Finkbeiner. Synthesis of Reactive Systems. Verification and Synthesis of Correct and Secure Systems. Dependable Software Systems Engineering, 2016.
- Bernd Finkbeiner and Felix Klein. Bounded Cycle Synthesis. CAV 2016.
- Bernd Finkbeiner and Hazem Torfah. Synthesizing Skeletons for Reactive Systems. ATVA 2016.
- Bernd Finkbeiner. Bounded Synthesis for Petri Games. Correct System Design 2015.
- Bernd Finkbeiner, Manuel Gieseking and Ernst-Rüdiger Olderog. ADAM: Causality-Based Synthesis of Distributed Systems. 27th International Conference on Computer Aided Verification (CAV 2015).
- Bernd Finkbeiner and Sven Schewe. Bounded Synthesis. Software Tools for Technology Transfer (STTT 2013).
- Bernd Finkbeiner and Hans-Jörg Peter. Template-based Controller Synthesis for Timed Systems. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012).
- Rayna Dimitrova and Bernd Finkbeiner. Counterexample-guided Synthesis of Observation Predicates. 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2012).
- Bernd Finkbeiner and Swen Jacobs. Lazy Synthesis. 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012).
- Bernd Finkbeiner and Sven Schewe. Uniform Distributed Synthesis. Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005).