Login
- Original title:
- Verification of Reachability Properties and Termination for Probabilistic Systems
- Translated title:
- Verifikation von Erreichbarkeitseigenschaften und Terminierung von Probabilistischen Systemen
- Author:
- Gaiser, Andreas
- Year:
- 2013
- Document type:
- Dissertation
- Faculty/School:
- Fakultät für Informatik
- Advisor:
- Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.)
- Referee:
- Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.); Kučera, Antonín (Prof., Ph.D.)
- Language:
- en
- Subject group:
- DAT Datenverarbeitung, Informatik
- Controlled terms:
- Zustandsgraph; Markov-Kette; Programmverifikation; Terminierung Informatik
- TUM classification:
- DAT 325d; MAT 607d; DAT 530d
- Abstract:
- 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.
- Translated abstract:
- 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
- Date of submission:
- 10.10.2012
- Oral examination:
- 10.04.2013
- File size:
- 1600918 bytes
- Pages:
- 232
- Urn (citeable URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130410-1115880-0-4
- Last change:
- 07.06.2013
BibTeX