Die Dozenten der Informatik-Institute der Technischen Universität Braunschweig laden im Rahmen des Informatik-Kolloquiums zu folgendem Vortrag ein.
Prof. Dr. Bernd Finkbeiner, Universität des Saarlandes: Logics and Algorithms for the Synthesis of Distributed Systems
Beginn: 18.02.2015, 08:30 Uhr Ort: TU Braunschweig, Informatikzentrum, Mühlenpfordtstraße 23, 1. OG, Hörsaal M 161 Webseite: http://www.ibr.cs.tu-bs.de/cal/kolloq/2015-02-18-finkbeiner.html Kontakt: Prof. Dr.-Ing. Ina Schaefer
More than fifty years after its introduction by Alonzo Church, the synthesis problem is still one of the most intriguing challenges in the theory of discrete systems. On the one hand, synthesis algorithms have found game-changing applications in many areas of computer science and systems engineering, from the automatic construction of control strategies for robots and manufacturing plants to the computer-aided design of coordination protocols and human-computer interfaces. On the other hand, the logical and algorithmic foundations of the synthesis problem are far from complete.
Synthesis is particularly challenging in the setting of distributed systems, where 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, such as pipelines and rings, or other restrictions on the problem, such as local specifications. Encouraged by these findings, new specification languages like Coordination Logic aim for a comprehensive logical representation and a uniform algorithmic treatment of the decidable synthesis problems.
In this talk, I will trace the progress from isolated decidability results towards universal synthesis logics and algorithms. I will demonstrate how the logical representation of the synthesis problem simplifies the identification of decidable cases and give an overview on the state of the art in decision procedures and strategy construction algorithms for the synthesis of distributed systems.