Forschungsbericht 2017 - Max-Planck-Institut für Softwaresysteme, Standort Saarbrücken

Von Newton und Turing zu cyber-physischen Systemen: Erforschung grundlegender Probleme der theoretischen Informatik

Autoren
Ouaknine, Joël
Abteilungen
Max-Planck-Institut für Softwaresysteme, Standort Saarbrücken, Saarbrücken
Zusammenfassung
Eine der großen Herausforderungen der Informatik ist es Ingenieuren und Programmierern zu ermöglichen, die Korrektheit der von ihnen entworfenen Computersysteme automatisch zu überprüfen. Die Gruppe Foundations of Algorithmic Verification konzentriert sich auf eine Reihe von fundamentalen algorithmischen Problemen für dynamische Systeme, mit dem Ziel, eine systematische exakte rechnerische Behandlung verschiedener wichtiger Klassen solcher Systeme und anderer fundamentaler Modelle, die in der Mathematik, Informatik und der quantitativen Wissenschaften verwendet werden, anzubieten.

Ein Denken im Sinne von Programmen statt von Gleichungen eröffnet eine neue Art der Wissenschaft.

Stephen Wolfram, 2002

Das tiefste und elementarste und deshalb noch ungelöste Problem in der heutigen Mathematik hat nichts mit Geometrie oder ganzen Zahlen zu tun: Es geht um die Berechnung.

Christos H. Papadimitriou, 2007

1937 veröffentlichte ein junger Engländer namens Alan Turing einen Artikel mit dem obskuren Titel „On computable numbers, with an application to the Entscheidungsproblem” in den Proceedings of the London Mathematical Society. Damit hat er wohl die mathematischen Grundlagen der modernen Informatik geschaffen. Bahnbrechend war Turings Nachweis, dass das berühmte Entscheidungsproblem, das der große deutsche Mathematiker David Hilbert einige Jahre zuvor formuliert hatte, nicht gelöst werden kann. Oder genauer: Turing wies nach (um im heutigen Jargon zu sprechen), dass sich die Frage, ob ein bestimmtes Computerprogramm anhält, nicht algorithmisch beantworten lässt – mit anderen Worten: Das berühmte Halteproblem ist unentscheidbar.

Während das Halteproblem (und damit zusammenhängende Fragen) damals als eher esoterisches Anliegen erschien, hat es in der heutigen Zeit enorm an Bedeutung und Relevanz gewonnen. Zeitsprung ins 21. Jahrhundert: Heute besteht weitgehend Einigkeit darüber, dass es zu den großen Herausforderungen der Informatik zählt, Ingenieure, Programmierer und Forscher in die Lage zu versetzen, die Korrektheit der von ihnen entwickelten Computersysteme automatisch zu verifizieren und zu zertifizieren. In immer mehr Anwendungsbereichen ist es absolut entscheidend, dass die Software, die inzwischen unzählige Aspekte unseres Alltags steuert (beispielsweise in Flugzeugsteuerungen), sich exakt wie beabsichtigt verhält, und damit katastrophale Folgen ausgeschlossen werden können.

Das moderne Gebiet der computergestützten formalen Verifikation beschäftigt sich, vereinfacht gesagt, damit, sicherzustellen, dass Computersysteme so funktionieren, wie sie gedacht waren. Zunächst hauptsächlich auf Hardware bezogen, hat die formale Verifikation in den letzten Jahren einen Paradigmenwechsel erlebt: Angesichts der Anforderungen, die in immer vielfältigeren und komplexeren Anwendungen an die Software-Verifikation gestellt werden, bestehen zentrale und drängende Herausforderungen durch Systemeigenschaften, die parametrisch, unbegrenzt, quantitativ, kontinuierlich oder in anderer Weise mit einer unendlichen Anzahl von Zuständen modelliert werden (anders als Hardware, für die typischerweise eine endlichen Zahl Zustände ausreicht).

Einer der ersten Erfolge der formalen Softwareverifikation war das TERMINATOR-Tool von Microsoft Research sowie dessen Nachfolger T2 zur Erkennung von Lebendigkeits-Fehlern (beispielsweise die Nichtbeendigung von Schleifen, bei denen ein Rechner sich aufhängt, umgangssprachlich als „Blue Screen of Death“ bezeichnet) in Dutzenden von Windows Gerätetreibern. Faktisch versuchten Microsoft Forscher das Halteproblem zu lösen, dessen Unlösbarkeit Turing Jahrzehnte zuvor nachgewiesen hatte! In der Praxis ist es den Forschern durch die Verwendung zahlloser heuristischer Ansätze, tiefer Mathematik und ausgeklügelter Algorithmen tatsächlich gelungen, einen erheblichen Teil der von ihnen in Angriff genommenen ‚unlösbaren‘ Problemfälle effektiv zu bewältigen, was zu einer spürbaren Verbesserung der Softwarequalität geführt hat (tatsächlich kommen Windows Abstürze oder Hänger lange nicht mehr so oft vor wie früher!).

Zurückkommend auf die Grundlagen, stellt sich allerdings die Frage, welche Klassen von Programmen sich, zumindest grundsätzlich, algorithmisch vollständig handhaben und analysieren lassen. Diese Herausforderung wird am MPI für Softwaresysteme in Angriff genommen, indem Computerprogramme dort abstrakt als dynamische Systeme betrachtet werden. Dabei wird versucht, exakte Algorithmen zu entwickeln, die die Forscher in die Lage versetzen, das Verhalten solcher Systeme vollständig zu analysieren. Konkret beschäftigen sich Wissenschaftler der Forschungsgruppe Foundations of Algorithmic Verification derzeit mit einer Reihe von zentralen algorithmischen Problemen in der Verifikation, Synthese, Performanz und Kontrolle von dynamischen Systemen, unter Verwendung von Methoden aus der Zahlentheorie sowie diophantischer und algebraischer Geometrie. Dabei wird das übergeordnete Ziel verfolgt, eine systematische exakte rechnerische Behandlung verschiedener bedeutender Klassen von dynamischen Systemen und anderer grundlegender Modelle anzubieten, die in Mathematik, Informatik und quantitativen Wissenschaften verwendet werden. Zu den bisher erzielten Resultaten zählen verschiedene Entscheidbarkeits- und Komplexitäts-Resultate  für linear rekurrente Folgen, die sich für die Modellierung einfacher Schleifen in Computerprogrammen verwenden lassen und die eine Reihe von seit langem offenen Fragen in der Mathematik und Informatik beantworten. Dazu wird auch auf die entsprechende Untersuchung verwiesen [Ouaknine und Worrell 2015]. Dennoch ist anzumerken, dass selbst für die sehr elementare Klasse der sogenannten „einfachen linearen Schleifen“ die Frage, ob das Halteproblem entscheidbar ist oder nicht, offen bleibt – eine Tatsache, die vor einigen Jahren von dem Mathematiker Terence Tao als „ein wenig ungeheuerlich“ bezeichnet wurde.

In ihrer neueren Arbeit haben Wissenschaftler des Instituts das sogenannte Zero-Problem für lineare Differentialgleichungen, also die Frage der algorithmischen Bestimmung, ob die eindeutige Lösung einer bestimmten linearen Differentialgleichung eine Null hat oder nicht, in Angriff genommen. Solche Gleichungen, die bis auf Isaac Newton zurückgehen, sind in der Mathematik, der Physik und der Technik allgegenwärtig. Sie sind zudem besonders nützlich in der Modellierung von cyber-physischen Systemen, d. h. digitalen Systemen, die sich in einer kontinuierlichen Umgebung bewegen und mit dieser interagieren. Mit Erstaunen haben die MPI-Forscher festgestellt, dass das Zero-Problem weder als entscheidbar (d. h. algorithmisch lösbar) noch als unentscheidbar galt! Mit anderen Worten war – und ist! – es noch immer eine offene Frage, ob sich algorithmisch bestimmen lässt, ob eine bestimmte lineare Differentialgleichung eine Null hat oder nicht (obwohl man natürlich in der Praxis oft mit Hilfe von Approximationstechniken aus der numerischen Analyse eine Antwort ableiten kann).

Im vergangenen Jahr hat die MPI-Gruppe zwei Artikel veröffentlicht [Chonev et al. 2016a; 2016b], in denen mehrere bedeutende Teilergebnisse vorgestellt wurden: Wenn es um die Existenz einer Null über ein begrenztes Zeitintervall geht, lässt sich dies algorithmisch bestimmen, sofern man von der Richtigkeit einer bestimmten Hypothese aus dem mathematischen Gebiet der Zahlentheorie ausgeht, die als Vermutung von Schanuel bekannt ist. (Die Vermutung von Schanuel ist eine weitreichende Hypothese, die unter anderem die Irrationalität und Transzendenz von Zahlen wie (e + ) impliziert – es handelt sich also um tiefe, ungelöste Fragestellungen in der Mathematik). Auch konnten die Forscher eine partielle Erklärung dafür liefern, dass das Zero-Problem im weitesten Sinne bis zum jetzigen Zeitpunkt offen blieb: Wenn man in der Lage wäre, es in der Dimension 9 (oder höher) zu lösen, würde das auch die Lösung verschiedener seit langem bestehender offener Probleme auf einem Gebiet der Mathematik ermöglichen, das als diophantische Approximation bezeichnet wird. Dabei zeigten sich – zumindest für die MPI-Forscher! – überraschende und unerwartete Verbindungen zwischen der Modellierung und Analyse cyber-physischer Systeme und anscheinend völlig unverbundenen tiefen mathematischen Theorien, die sich mit Problemen ganzer Zahlen beschäftigen.

Zusammenfassend lässt sich sagen, dass die moderne theoretische Informatik neue Herausforderungen und innovative Perspektiven auf alte und tiefe Probleme in der Mathematik bringt. Diese Synergie liefert neue und faszinierende wissenschaftliche Erkenntnisse und Fortschritte. Die Forscher des MPI freuen sich, an diesen Entwicklungen beteiligt zu sein.

Literaturhinweise

Ventsislav Chonev, Joël Ouaknine, and James Worrell. 2016a.
On Recurrent Reachability for Continuous Linear Dynamical Systems.
In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 515–524. ACM, 2016

Ventsislav Chonev, Joël Ouaknine, and James Worrell. 2016b.

On the Skolem Problem for Continuous Linear Dynamical Systems.
In Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming (ICALP), pages 100:1–100:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016.
Joël Ouaknine and James Worrell. 2015.
On Linear Recurrence Sequences and Loop Termination
SIGLOG News 2(2):4–13, 2015
Tao, Terence
Structure and randomness: pages from year one of a mathematical blog.
American Mathematical Society, 2008
Zur Redakteursansicht