Benutzer: Gast  Login
Originaltitel:
Verification of Reachability Properties and Termination for Probabilistic Systems 
Übersetzter Titel:
Verifikation von Erreichbarkeitseigenschaften und Terminierung von Probabilistischen Systemen 
Jahr:
2013 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Gutachter:
Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.); Kučera, Antonín (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Schlagworte (SWD):
Zustandsgraph; Markov-Kette; Programmverifikation; Terminierung Informatik 
TU-Systematik:
DAT 325d; MAT 607d; DAT 530d 
Kurzfassung:
This thesis deals with reachability problems of probabilistic systems with large state spaces. To compute reachability probabilities of probabilistic programs we extend abstraction approaches such that they can use arbitrary abstract domains. We present a method for proving termination with probability one of probabilistic programs which uses termination provers for non-probabilistic programs. We also develop methods for the analysis of branching processes. 
Übersetzte Kurzfassung:
Diese Arbeit beschäftigt sich mit Erreichbarkeitsproblemen für probabilistische Systeme mit großen Zustandsräumen. Um Erreichbarkeitswahrscheinlichkeiten von probabilistischen Programmen zu bestimmen, erweitern wir Abstraktionsansätze, so dass beliebige abstrakte Domänen benutzt werden können. Wir präsentieren eine Methode, um Terminierung von probabilistischen Programmen mit Wahrscheinlichkeit 1 zu beweisen, die Terminierungsbeweiser für nichtprobabilistische Programme nutzt. Außerdem entwic...    »
 
Mündliche Prüfung:
10.04.2013 
Dateigröße:
1600918 bytes 
Seiten:
232 
Letzte Änderung:
07.06.2013