Automated Run-Time Analysis of Probabilistic Programs

Kontakt

Marcel Hark

Telefon

work
+49 241 80 21214

E-Mail

E-Mail
  Entscheidungsbaum Urheberrecht: Joost-Pieter Katoen

Die Analyse der Korrektheit eines Systems ist in den letzten Jahren ein wichtiger Bestandteil der Entwicklung geworden. Einer der wichtigsten Aspekte ist hierbei die Terminierung des Programms auf allen möglichen Eingabeparametern. Wichtiger als der Beweis der universellen Terminierung des Programms sind in praktischen Anwendungen jedoch verlässliche Information über die schlimmst mögliche Laufzeit, die so genannte asymptotische Komplexität. Da diese Analyse per Hand sehr langwierig und bei großen Systemen kaum möglich ist, stand im Zentrum der Forschung der letzten Jahre die Entwicklung von leicht zu automatisierenden Techniken, woraus Systeme wie AproVE, KoAT und CoFloCo hervorgegangen sind.

In vielen Anwendungen ist jedoch nichtdeterministisches Verhalten zu finden, welches bisher nur sehr eingeschränkt analysiert werden kann. Probabilistische Programme erlauben eine bessere Approximation von Nichtdeterminismus. Der Übergang zu zufallsbasierten Systemen führt dazu, dass ein neuer Begriff von Laufzeit entsteht. Diese ist eine Zufallsvariable, die durch ihren Erwartungswert angenähert wird. Dadurch entstehen neue Begriffe der Terminierung, die neue pathologische Beispiele zulassen.

Ziel der Dissertation ist, neue Techniken aus bestehenden Konzepten für deterministische Programme zu entwickeln, um die erwartete Laufzeit eines probabilistischen Programms automatisch anzunähern.