No label defined (Q4260002)

In dieser Arbeit wird ein neuer Synthesealgorithmus entwickelt, der aus einer temporal logischen Formel einen Büchi Automaten erzeugt, so daß dieser die durch die Formel definierte (\(\omega\)-reguläre Sprache erkennt. Im Gegensatz zu dem tableau-basierten Synthesealgorithmus arbeitet die hier entwickelte Methode induktiv über der Formelstruktur. Für eine anwendungsorientierte, praxisrelevante Teilklasse temporal logischer Formeln wird in dieser Arbeit bewiesen, daß die Komplexität der Synthese im wesentlichen linear in der Größe der Eingabeformel ist. Gemäß dem Titel der Arbeit werden mehrere Anwendungen aus den Bereichen System -- Level Synthese und formale Verifikation so aufgebaut, daß sie die günstigen Komplexitätseigenschaften des Synthesealgorithmus optimal nutzen. Der Synthesealgorithmus und die Anwendungen wurden im Prototyp ICOS (Interface COntroller Synthesis and Verifikation System) implementiert, so daß mit dessen Hilfe die praktische Relevanz des Synthesealgorithmus und der Anwendungen demonstriert werden konnten. Anhand einer kontrollbasierten, typischen Anwendung, die im industriellen Kontext angesiedelt ist, stellt diese Arbeit den Einsatz der hier entwickelten Anwendungen und Algorithmen exemplarisch dar.