Verifying Qualitative Properties of Probabilistic Programs
| Title | Verifying Qualitative Properties of Probabilistic Programs |
| Publication Type | Book Chapter |
| Year of Publication | 2004 |
| Authors | Benedikt Bollig, Leucker, M |
| Book Title | Validation of Stochastic Systems |
| Series Title | Lecture Notes in Computer Science |
| Volume | 2925 |
| Pagination | 124–146 |
| Publisher | Springer |
| Abstract | We present procedures for checking linear temporal logic and automata specifications of sequential and concurrent probabilistic programs. We follow two different approaches: For LTL and sequential probabilistic programs, our method proceeds in a tableau style fashion, while the remaining procedures are based on automata theory. |
| URL | http://link.springer.de/link/service/series/0558/papers/ |
Bibtex:
@inbook {BolligL03,
title = {Verifying Qualitative Properties of Probabilistic Programs},
booktitle = {Validation of Stochastic Systems},
series = {Lecture Notes in Computer Science},
volume = {2925},
year = {2004},
pages = {124{\textendash}146},
publisher = {Springer},
organization = {Springer},
abstract = {We present procedures for checking linear temporal logic and automata specifications of sequential and concurrent probabilistic programs. We follow two different approaches: For LTL and sequential probabilistic programs, our method proceeds in a tableau style fashion, while the remaining procedures are based on automata theory.},
url = {http://link.springer.de/link/service/series/0558/papers/},
author = {Benedikt Bollig and Martin Leucker}
}PDF:
Postscript:
