Login
- Originaltitel:
- Verification of Reachability Properties and Termination for Probabilistic Systems
- Übersetzter Titel:
- Verifikation von Erreichbarkeitseigenschaften und Terminierung von Probabilistischen Systemen
- Autor:
- Gaiser, Andreas
- Jahr:
- 2013
- Dokumenttyp:
- Dissertation
- Fakultät/School:
- 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 entwick... »
- WWW:
- https://mediatum.ub.tum.de/?id=1115880
- Eingereicht am:
- 10.10.2012
- Mündliche Prüfung:
- 10.04.2013
- Dateigröße:
- 1600918 bytes
- Seiten:
- 232
- Urn (Zitierfähige URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130410-1115880-0-4
- Letzte Änderung:
- 07.06.2013
BibTeX