Symmetrische und effiziente Synthese

Since the formulation of the synthesis problem for reactive systems by Church in the 60s, research on synthesis has lead to both theoretical insights and practical approaches for automatically constructing systems from their specifications. While the first solution of the problem was given by Büchi as early as 1969, only very recently, focus has shifted towards identifying ways to exploit the structure in reactive system specifications in order to lift the scalability of synthesis to industrial-sized designs. The recent progress in synthesis not only lead to a renewed interest in the subject, but also shed light onto the downsides of current synthesis approaches. In the original formulation of the problem, the structure of the produced solutions was not a concern. Experiments with current synthesis approaches has however shown that the computed implementations are usually very hard to understand and have little of the structure that manually constructed implementations have. Furthermore, the scalability of current synthesis approaches is still deemed to be insufficient for many industrial application scenarios, which prevents the introduction of reactive synthesis technology into industrial design flows. In this thesis, we tackle both of these problems for reactive synthesis. To counter the insufficient structure in the solutions, we analyse the problem of symmetric synthesis. In this alternative synthesis problem, the aim is to compute a solution that consists of multiple copies of the same process such that the overall system satisfies the specification. Such systems have no centralised control units, and are considered to be more robust and easier to maintain. We characterise undecidable and decidable cases of the problem, and provide a synthesis algorithm for rotation-symmetric architectures, which capture many cases of practical relevance. To improve the scalability in synthesis, we start with a simple but scalable approach to reactive synthesis that has shown its principal applicability in the field, and extend its main idea both in terms of scope and usability. We enhance its expressivity in a way that allows to synthesise robust systems, and remove its limitation to specifications of a very special form. Both improvements yield theoretical insights into the synthesis problem: we characterise which specification classes can be supported in synthesis approaches that use parity games with a fixed number of colours as the underlying computation model, and examine the properties of universal very-weak automata, on which we base a synthesis workflow that combines ease of specification with a low complexity of the underlying game solving step. As a side-result, we also obtain the first procedure to translate a formula in linear-time temporal logic (LTL) to a computation tree logic (CTL) formula with only universal path quantifiers, whenever possible. The new results on symmetric and efficient reactive synthesis are complemented by an easily accessible introductory chapter to the field of reactive synthesis that can also be read in isolation.paddle apparatus with membrane holder were identified.Trotz der Vorzüge der Synthese reaktiver Systeme gegenüber der manuellen Konstruktion solcher Systeme ist Synthese noch nicht als Teil industrieller Vorgehensmodelle etabliert. Als Hauptgrund für diese Diskrepanz gilt allgemein, dass sowohl die Qualität der synthetisierten Systeme bei Anwendung bisheriger Methoden unzureichend ist, als auch die Skalierbarkeit aktueller Syntheseverfahren der Verbesserung bedarf. Diese Dissertation behandelt beide diese Probleme der Synthese reaktiver Systeme auf breiter Front. Zur Verbesserung der Qualität synthetisierter Systeme wird die Synthese von strukturierten Systemen betrachtet. Experimente mit aktuellen Syntheseverfahren haben gezeigt, dass die erzeugten Implementierungen oft schwer zu verstehen sind und anders als handgeschriebene Implementierungen kaum Struktur haben. Abhilfe verschafft die Beschränkung auf die Erzeugung symmetrischer Systeme, die aus mehreren Kopien des selben Prozesses bestehen, so dass das Gesamtsystem die Spezifikation erfüllt. Solche Systeme haben keine zentrale Koordinationskomponente und werden allgemein als robuster und einfacher zu warten eingestuft. In dieser Dissertation werden entscheidbare und unentscheidbare Fälle des symmetrischen Syntheseproblems identifiziert und ein Synthesealgorithmus für rotationssymmetrische Systeme beschrieben. Diese Systemklasse deckt viele praktisch relevante Architekturen ab. Um das Problem der mangelnden Skalierbarkeit anzugehen, wird die Hauptidee des Generalised Reactivity(1) Syntheseansatzes, welcher seine praktische Anwendbarkeit bereits unter Beweis gestellt hat, aufgegriffen und sowohl bezüglich der Expressivität als auch der Benutzbarkeit vervollständigt. Die Erweiterung der Expressivität ermöglicht es, den resultierenden Ansatz für die Synthese robuster Systeme zu nutzen, während die Benutzbarkeit für industrielle Anwendungen durch die Aufhebung der Beschränkung, dass die Spezifikation eine sehr spezielle Form haben muss, erreicht wird. Beide Erweiterungen geben Einsicht in die Theorie der Synthese: Zum einen wird die Klasse der Spezifikationen, die in Syntheseansätzen verwendet werden können, die auf dem Lösen von Paritätsspielen mit einer vordefinierten Anzahl von Farben basieren, charakterisiert. Zum anderen wird Einsicht in die Eigenschaften universeller sehr schwacher Automaten gegeben. Ein Nebenprodukt der neuen Syntheseverfahren ist die erste Prozedur, um einen Ausdruck in linear-time temporal logic (LTL) in computation tree logic mit universellen Pfadquantoren (ACTL) zu übersetzen, wann immer dies möglich ist. Die Resultate zur symmetrischen und effizienten reaktiven Synthese werden von einer didaktisch aufbereiteten Einführung in das Gebiet der reaktiven Synthese begleitet, welche auch unabhängig von den übrigen Teilen der Dissertation gelesen werden kann