Heinz Schwärtzel-Dissertationspreis für Grundlagen der Informatik 2020

Sickert-Zehnter, Salomon

Dr. Salomon Sickert-Zehnter

Im Rahmen der Abschlussfeier für Absolventinnen und Absolventen am 9. Dezember wurden in diesem Jahr zwei gleichwertige Heinz Schwärtzel-Dissertationspreise vergeben. Stifter Prof. Heinz Schwärtzel konnte aufgrund der Covid-19-Pandemie erstmals nicht persönlich anwesend sein. Vertreten wurde er durch Laudatorin Prof. Susanne Albers (Lehrstuhl für Algorithmen und Komplexität). Der Heinz Schwärtzel-Preis für Grundlagen der Informatik wird seit 2006 jährlich vergeben. Er richtet sich an hervorragende Promovierte der drei Münchner Universitäten TUM, LMU und Universität der Bundeswehr. Dem Stifter und Ehrenmitglied der Gesellschaft für Informatik e. V. ist es ein besonderes Anliegen, die grundlagenorientierte Informatik-Forschung mit diesem Preis zu fördern.
Nachdem im letzten Jahr die italienische Wissenschaftlerin Dr. Elisa Canzani von der Universität der Bundeswehr den Preis entgegennehmen durfte, teilen ihn sich heuer zwei Promovierte der TUM und erhalten je 750 Euro als Anerkennung ihrer Leistung.

Dr. Salomon Sickert-Zehnter befasst sich in seiner Dissertation am Lehrstuhl für Theoretische Informatik (Prof. Javier Esparza) mit dem Thema "A Unified Translation of Linear Temporal Logic to ω-Automata".

Laudatio:
"Unter der Synthese reaktiver Systeme versteht man die automatische Konstruktion von Steuereinheiten für diskrete Systeme. Der Entwickler spezifiziert hierbei nur das gewünschte Verhalten der Steuereinheit und erhält dann automatisch eine entsprechende Implementierung. Dieser Ansatz hat bereits wichtige Meilensteine erreicht. Die gebräuchlichen Synthese-Algorithmen verwenden lineare temporale Logik als Spezifikationssprache und übersetzen sie in einen äquivalenten deterministischen ω-Automaten. Der schwierigste Schritt hierbei ist die Übersetzung von nicht-deterministischen zu deterministischen ω-Automaten. Nach einer langen Suche hatte Muli Safra dieses Problem Ende der 80er Jahre gelöst.
Salomon Sickert-Zehnters Dissertation präsentiert einen fundamental neuen Ansatz für die Übersetzung von linearer temporaler Logik zu deterministischen Automaten. Anders als bei Safras Algorithmus wird die Determinisierung von Automaten übersprungen. Die Formel wird in Teile zerlegt, die mithilfe sehr einfacher Techniken getrennt voneinander zu deterministischen Automaten übersetzt und im letzten Schritt in einem Gesamtautomaten kombiniert werden. Das führt, verglichen mit Safras Konstruktion, zu signifikant kleineren Automaten. Die Ergebnisse der Dissertation wurden im renommierten Journal of the ACM veröffentlicht.
Salomon Sickert-Zehnter hat seine Algorithmen implementiert und in das LTL-Synthese-Tool Strix integriert. Bei dem jährlichen SYNTCOMP Wettbewerb hat Strix seit dem Debut 2018 alle LTL-Synthese-Kategorien jedes Jahr (2018, 2019 und 2020) gewonnen."